[codac2] templated paving with weak_ptrs

codac-team · Dec 4, 2023 · 58573fd · 58573fd
1 parent 47bbc52
commit 58573fd
Show file tree

Hide file tree

Showing 7 changed files with 151 additions and 114 deletions.
diff --git a/src/core/2/cn/codac2_ContractorNetwork.cpp b/src/core/2/cn/codac2_ContractorNetwork.cpp
@@ -29,7 +29,7 @@ namespace codac2
     _auto_fixpoint = !disable;
   }
 
-  void ContractorNetwork::contract(bool verbose)
+  double ContractorNetwork::contract(bool verbose)
   {
     if(verbose)
     {
@@ -45,7 +45,7 @@ namespace codac2
       shared_ptr<ContractorNodeBase> current_ctc = _stack.front();
       _stack.pop_front();
 
-      auto contracted_doms = current_ctc->call_contract();
+      auto contracted_doms = current_ctc->call_contract(false);
 
       for(auto& d : contracted_doms)
         for(auto& ci : d->contractors())
@@ -56,8 +56,10 @@ namespace codac2
         }
     }
 
+    double elapsed_time = (double)(clock()-t_start)/CLOCKS_PER_SEC;
     if(verbose)
-      std::cout << "  Constraint propagation time: " << (double)(clock() - t_start)/CLOCKS_PER_SEC << "s" << std::endl;
+      std::cout << "  Constraint propagation time: " << elapsed_time << "s" << std::endl;
+    return elapsed_time;
   }
 
   void ContractorNetwork::reset_all_vars()

diff --git a/src/core/2/cn/codac2_ContractorNetwork.h b/src/core/2/cn/codac2_ContractorNetwork.h
@@ -18,7 +18,7 @@ namespace codac2
       void add(const std::shared_ptr<ContractorNodeBase>& ctc);
       void add_ctc_to_stack(const std::shared_ptr<ContractorNodeBase>& ctc);
       void disable_auto_fixpoint(bool disable = true);
-      void contract(bool verbose = true);
+      double contract(bool verbose = true);
 
       void reset_all_vars();
 

diff --git a/src/core/2/cn/codac2_ContractorNode.h b/src/core/2/cn/codac2_ContractorNode.h
@@ -18,7 +18,7 @@ namespace codac2
 
       virtual ~ContractorNodeBase() = default;
       virtual size_t nb_args() const = 0;
-      virtual std::list<std::shared_ptr<DomainNodeBase>> call_contract() = 0;
+      virtual std::list<std::shared_ptr<DomainNodeBase>> call_contract(bool verbose = false) = 0;
       virtual Contractor* raw_ptr() const = 0;
       virtual void associate_domains(std::vector<std::shared_ptr<DomainNodeBase>>& cn_domains) = 0;
       virtual std::string contractor_class_name() const = 0;
@@ -60,8 +60,10 @@ namespace codac2
           l.push_back(d);
       }
 
-      std::list<std::shared_ptr<DomainNodeBase>> call_contract()
+      std::list<std::shared_ptr<DomainNodeBase>> call_contract(bool verbose = false)
       {
+        if(verbose)
+          std::cout << "Calling " << contractor_class_name() << std::endl;
         std::list<std::shared_ptr<DomainNodeBase>> contracted_doms;
 
         std::apply(

diff --git a/src/core/2/cn/codac2_DomainNode.h b/src/core/2/cn/codac2_DomainNode.h
@@ -103,6 +103,12 @@ namespace codac2
           _x.get().reset();
       }
 
+      void reset(const T& x)
+      {
+        if constexpr(_is_var)
+          _x.get().reset(x);
+      }
+
       constexpr bool is_var() const
       {
         return _is_var;

diff --git a/src/core/2/contractors/codac2_CtcInter.h b/src/core/2/contractors/codac2_CtcInter.h
@@ -28,13 +28,10 @@ namespace codac2
 
       void contract(Paving<N>& x, IntervalVector_<N>& y)
       {
-        IntervalVector_<N> y_ = IntervalVector_<N>::empty_set();
-        for(auto& li : x.leaves_list())
-        {
-          y_ |= li->_x & y;
-          //li->_x &= y;
-        }
-        y = y_;
+        auto y_ = y;
+        y.set_empty();
+        for(const auto& l : x.leaves())
+          y |= y_ & l.lock()->box();
       }
 
       make_available_in_cn__templated(CtcInter<N>)

diff --git a/src/core/2/contractors/codac2_CtcPaver.h b/src/core/2/contractors/codac2_CtcPaver.h
@@ -21,9 +21,9 @@ namespace codac2
   {
     public:
 
-      static bool compare_paving(Paving<N>* first, Paving<N>* second)
+      static bool compare_paving(const std::weak_ptr<PavingNode<N>>& first, const std::weak_ptr<PavingNode<N>>& second)
       {
-        return first->box().volume() > second->box().volume();
+        return first.lock()->_x.volume() > second.lock()->_x.volume();
       }
 
       CtcPaver(ContractorOnBox<N>& ctc, size_t max_leaves)
@@ -34,15 +34,16 @@ namespace codac2
 
       void contract(Paving<N>& x)
       {
-        list<Paving<N>*> l_subpav = x.leaves_list();
+        auto l_subpav = x.leaves();
         size_t nb_leaves = l_subpav.size();
 
         while(!l_subpav.empty())
         {
           l_subpav.sort(compare_paving);
 
-          Paving<N>* q = l_subpav.front();
+          std::shared_ptr<PavingNode<N>> q = l_subpav.front().lock();
           l_subpav.pop_front();
+          assert(q.use_count() > 1);
 
           _ctc.contract(q->_x);
 
@@ -53,8 +54,8 @@ namespace codac2
           {
             q->bisect();
             nb_leaves++;
-            l_subpav.push_back(q->_left.get());
-            l_subpav.push_back(q->_right.get());
+            l_subpav.push_back(q->left());
+            l_subpav.push_back(q->right());
           }
         }
       }