From 47bbc52eeb0026f01d0047ec35bdf12abad2892d Mon Sep 17 00:00:00 2001 From: SimonRohou Date: Sat, 2 Dec 2023 13:32:18 +0100 Subject: [PATCH] ContractorNetworks in Codac2 version --- .../core/2/cn/codac2_py_ContractorNetwork.cpp | 3 +- src/core/2/cn/codac2_Contractor.h | 15 ++++ src/core/2/cn/codac2_ContractorNetwork.cpp | 39 +++++++--- src/core/2/cn/codac2_ContractorNetwork.h | 21 +++++- src/core/2/cn/codac2_ContractorNode.cpp | 10 --- src/core/2/cn/codac2_ContractorNode.h | 17 ++--- src/core/2/cn/codac2_DomainNode.h | 18 ++++- src/core/2/cn/codac2_Var.h | 21 ++++++ src/core/2/contractors/codac2_CtcCN.h | 49 +++++++++++++ src/core/2/contractors/codac2_CtcInter.h | 47 ++++++++++++ src/core/2/contractors/codac2_CtcPaver.h | 71 +++++++++++++++++++ .../domains/interval/codac2_IntervalMatrix.h | 2 +- src/core/2/domains/paving/codac2_Paving.h | 30 +++++++- src/core/2/variables/codac2_Matrix.h | 8 +-- src/core/CMakeLists.txt | 3 + 15 files changed, 313 insertions(+), 41 deletions(-) create mode 100644 src/core/2/contractors/codac2_CtcCN.h create mode 100644 src/core/2/contractors/codac2_CtcInter.h create mode 100644 src/core/2/contractors/codac2_CtcPaver.h diff --git a/python/src/core/2/cn/codac2_py_ContractorNetwork.cpp b/python/src/core/2/cn/codac2_py_ContractorNetwork.cpp index 9f0c3ec1e..5add4022d 100644 --- a/python/src/core/2/cn/codac2_py_ContractorNetwork.cpp +++ b/python/src/core/2/cn/codac2_py_ContractorNetwork.cpp @@ -39,6 +39,7 @@ void export_ContractorNetwork_codac2(py::module& m) "n"_a) .def("contract", &ContractorNetwork::contract, - "todo") + "todo", + "verbose"_a=true) ; } \ No newline at end of file diff --git a/src/core/2/cn/codac2_Contractor.h b/src/core/2/cn/codac2_Contractor.h index 50ef62c89..549e1a078 100644 --- a/src/core/2/cn/codac2_Contractor.h +++ b/src/core/2/cn/codac2_Contractor.h @@ -15,6 +15,13 @@ namespace codac2 return std::make_shared::type,T...>>(*this, a...); \ } \ + #define make_available_in_cn__templated(template_args) \ + template \ + std::shared_ptr operator()(T&... a) \ + { \ + return std::make_shared>(*this, a...); \ + } \ + class Contractor { public: @@ -22,6 +29,14 @@ namespace codac2 virtual ~Contractor() = default; }; + template + class ContractorOnBox : public Contractor + { + public: + + virtual void contract(IntervalVector_& x) = 0; + }; + class Contractor1 : public Contractor { public: diff --git a/src/core/2/cn/codac2_ContractorNetwork.cpp b/src/core/2/cn/codac2_ContractorNetwork.cpp index 97e53d5ae..052b17081 100644 --- a/src/core/2/cn/codac2_ContractorNetwork.cpp +++ b/src/core/2/cn/codac2_ContractorNetwork.cpp @@ -1,4 +1,5 @@ #include +#include #include "codac2_ContractorNetwork.h" using namespace std; @@ -19,9 +20,8 @@ namespace codac2 void ContractorNetwork::add_ctc_to_stack(const shared_ptr& ctc) { - assert(!ctc->to_be_called()); - _stack.push_back(ctc); - ctc->set_call_flag(true); + if(find(_stack.begin(),_stack.end(),ctc) == _stack.end()) + _stack.push_back(ctc); } void ContractorNetwork::disable_auto_fixpoint(bool disable) @@ -29,9 +29,18 @@ namespace codac2 _auto_fixpoint = !disable; } - void ContractorNetwork::contract() + void ContractorNetwork::contract(bool verbose) { - do + if(verbose) + { + std::cout << "Contractor network (" << _v_ctc.size() + << " contractors, " << _v_domains.size() << " domains)" << std::endl; + std::cout << "Computing, " << _stack.size() << " contractors currently in stack" << std::endl; + } + + clock_t t_start = clock(); + + while(!_stack.empty()) { shared_ptr current_ctc = _stack.front(); _stack.pop_front(); @@ -43,10 +52,24 @@ namespace codac2 { auto p_c = ci.lock(); if(!_auto_fixpoint && current_ctc.get() == p_c.get()) continue; - if(!p_c->to_be_called()) - add_ctc_to_stack(p_c); + add_ctc_to_stack(p_c); } + } + + if(verbose) + std::cout << " Constraint propagation time: " << (double)(clock() - t_start)/CLOCKS_PER_SEC << "s" << std::endl; + } + + void ContractorNetwork::reset_all_vars() + { + for(auto& d : _v_domains) + if(d->is_var()) + d->reset(); + } - } while(!_stack.empty()); + void ContractorNetwork::trigger_all_contractors() + { + for(auto& c : _v_ctc) + add_ctc_to_stack(c); } } \ No newline at end of file diff --git a/src/core/2/cn/codac2_ContractorNetwork.h b/src/core/2/cn/codac2_ContractorNetwork.h index e836f6535..2c4256213 100644 --- a/src/core/2/cn/codac2_ContractorNetwork.h +++ b/src/core/2/cn/codac2_ContractorNetwork.h @@ -6,10 +6,10 @@ #include #include "codac2_DomainNode.h" #include "codac2_ContractorNode.h" +#include "codac2_Var.h" namespace codac2 { - class ContractorNetwork { public: @@ -18,7 +18,24 @@ namespace codac2 void add(const std::shared_ptr& ctc); void add_ctc_to_stack(const std::shared_ptr& ctc); void disable_auto_fixpoint(bool disable = true); - void contract(); + void contract(bool verbose = true); + + void reset_all_vars(); + + template + void reset_var(const Var *ref, const T& x) + { + for(auto& d : _v_domains) + if(d->raw_ptr() == ref) + { + static_cast&>(*d).get() = x; + return; + } + + assert(false && "unable to find variable"); + } + + void trigger_all_contractors(); //protected: diff --git a/src/core/2/cn/codac2_ContractorNode.cpp b/src/core/2/cn/codac2_ContractorNode.cpp index d4ca1d22c..98a0f4928 100644 --- a/src/core/2/cn/codac2_ContractorNode.cpp +++ b/src/core/2/cn/codac2_ContractorNode.cpp @@ -5,16 +5,6 @@ using namespace std; namespace codac2 { - void ContractorNodeBase::set_call_flag(bool flag) - { - _to_be_called = flag; - } - - bool ContractorNodeBase::to_be_called() const - { - return _to_be_called; - } - ostream& operator<<(ostream& os, const ContractorNodeBase& d) { os << "Contractor: " << d.contractor_class_name() << ", dom=" << d.nb_args() << endl; diff --git a/src/core/2/cn/codac2_ContractorNode.h b/src/core/2/cn/codac2_ContractorNode.h index d4f921b09..9e0ede9cd 100644 --- a/src/core/2/cn/codac2_ContractorNode.h +++ b/src/core/2/cn/codac2_ContractorNode.h @@ -17,20 +17,13 @@ namespace codac2 public: virtual ~ContractorNodeBase() = default; - virtual constexpr size_t nb_args() const = 0; + virtual size_t nb_args() const = 0; virtual std::list> call_contract() = 0; virtual Contractor* raw_ptr() const = 0; virtual void associate_domains(std::vector>& cn_domains) = 0; virtual std::string contractor_class_name() const = 0; - void set_call_flag(bool flag = true); - bool to_be_called() const; friend std::ostream& operator<<(std::ostream& os, const ContractorNodeBase& d); - - protected: - - bool _to_be_called = false; // this is redundant with the presence of the node - // in the CN stack, but avoids to search the node in the stack }; template @@ -51,7 +44,7 @@ namespace codac2 } - constexpr size_t nb_args() const + size_t nb_args() const { return std::tuple_size::value; } @@ -61,7 +54,7 @@ namespace codac2 return &(_ctc.get()); } - void add_domain_if_contracted(const std::shared_ptr& d, std::list>& l) + void process_domain_after_ctc(const std::shared_ptr& d, std::list>& l) { if(d->has_been_contrated()) l.push_back(d); @@ -69,7 +62,6 @@ namespace codac2 std::list> call_contract() { - _to_be_called = false; std::list> contracted_doms; std::apply( @@ -81,7 +73,7 @@ namespace codac2 std::apply( [this,&contracted_doms](auto &&... args) { - (add_domain_if_contracted(args,contracted_doms),...); + (process_domain_after_ctc(args,contracted_doms),...); }, _x); return contracted_doms; @@ -96,7 +88,6 @@ namespace codac2 d = std::dynamic_pointer_cast(cn_xi); return; } - cn_domains.push_back(d); } diff --git a/src/core/2/cn/codac2_DomainNode.h b/src/core/2/cn/codac2_DomainNode.h index c836e1500..2673166ba 100644 --- a/src/core/2/cn/codac2_DomainNode.h +++ b/src/core/2/cn/codac2_DomainNode.h @@ -6,6 +6,7 @@ #include #include #include "codac2_Domain.h" +#include "codac2_Var.h" namespace codac2 { @@ -23,6 +24,8 @@ namespace codac2 virtual const std::vector>& contractors() const = 0; virtual void add_ctc(const std::shared_ptr& ctc) = 0; virtual std::string domain_class_name() const = 0; + virtual void reset() = 0; + virtual bool is_var() const = 0; friend std::ostream& operator<<(std::ostream& os, const DomainNodeBase& d); }; @@ -34,6 +37,8 @@ namespace codac2 public: + constexpr static bool _is_var = std::is_base_of::value; + std::reference_wrapper make_ref(T_& x) { if constexpr (std::is_const::value) @@ -45,7 +50,7 @@ namespace codac2 return std::ref(x); } - DomainNode(T_& x) + explicit DomainNode(T_& x) : _x(make_ref(x)), _volume(x.dom_volume()) { if constexpr (std::is_const::value) @@ -92,6 +97,17 @@ namespace codac2 return typeid(T).name(); } + void reset() + { + if constexpr(_is_var) + _x.get().reset(); + } + + constexpr bool is_var() const + { + return _is_var; + } + protected: std::shared_ptr _local_dom = nullptr; diff --git a/src/core/2/cn/codac2_Var.h b/src/core/2/cn/codac2_Var.h index ce3198bf4..ec608906d 100644 --- a/src/core/2/cn/codac2_Var.h +++ b/src/core/2/cn/codac2_Var.h @@ -14,6 +14,7 @@ namespace codac2 public: virtual ~VarBase() = default; + VarBase& operator=(const VarBase& x) = delete; }; template @@ -25,6 +26,26 @@ namespace codac2 { } + + Var(const T& initial_value) + : _initial_value(initial_value) + { + + } + + void reset() + { + this->T::operator=(_initial_value); + } + + void reset(const T& x) + { + this->T::operator=(x); + } + + protected: + + T _initial_value; }; } diff --git a/src/core/2/contractors/codac2_CtcCN.h b/src/core/2/contractors/codac2_CtcCN.h new file mode 100644 index 000000000..d1f1947a0 --- /dev/null +++ b/src/core/2/contractors/codac2_CtcCN.h @@ -0,0 +1,49 @@ +/** + * \file + * + * ---------------------------------------------------------------------------- + * \date 2023 + * \author Simon Rohou + * \copyright Copyright 2023 Codac Team + * \license This program is distributed under the terms of + * the GNU Lesser General Public License (LGPL). + */ + +#ifndef __CODAC2_CTCCN_H__ +#define __CODAC2_CTCCN_H__ + +#include "codac2_Contractor.h" +#include "codac2_ContractorNetwork.h" + +namespace codac2 +{ + template + class CtcCN : public ContractorOnBox + { + public: + + CtcCN(ContractorNetwork& cn, Var>& var) + : _cn(cn), _ref_var(&var) + { + + } + + void contract(IntervalVector_& x) + { + _cn.reset_all_vars(); + _cn.reset_var(_ref_var,x); + _cn.trigger_all_contractors(); + _cn.contract(false); + x = *_ref_var; + } + + make_available_in_cn__templated(CtcCN) + + protected: + + ContractorNetwork& _cn; + const Var>* _ref_var; + }; +} + +#endif \ No newline at end of file diff --git a/src/core/2/contractors/codac2_CtcInter.h b/src/core/2/contractors/codac2_CtcInter.h new file mode 100644 index 000000000..667cd7a6f --- /dev/null +++ b/src/core/2/contractors/codac2_CtcInter.h @@ -0,0 +1,47 @@ +/** + * \file + * + * ---------------------------------------------------------------------------- + * \date 2023 + * \author Simon Rohou + * \copyright Copyright 2023 Codac Team + * \license This program is distributed under the terms of + * the GNU Lesser General Public License (LGPL). + */ + +#ifndef __CODAC2_CTCINTER_H__ +#define __CODAC2_CTCINTER_H__ + +#include "codac2_Contractor.h" + +namespace codac2 +{ + template + class CtcInter : public Contractor + { + public: + + CtcInter() + { + + } + + void contract(Paving& x, IntervalVector_& y) + { + IntervalVector_ y_ = IntervalVector_::empty_set(); + for(auto& li : x.leaves_list()) + { + y_ |= li->_x & y; + //li->_x &= y; + } + y = y_; + } + + make_available_in_cn__templated(CtcInter) + + protected: + + }; +} + +#endif \ No newline at end of file diff --git a/src/core/2/contractors/codac2_CtcPaver.h b/src/core/2/contractors/codac2_CtcPaver.h new file mode 100644 index 000000000..59d0beb96 --- /dev/null +++ b/src/core/2/contractors/codac2_CtcPaver.h @@ -0,0 +1,71 @@ +/** + * \file + * + * ---------------------------------------------------------------------------- + * \date 2023 + * \author Simon Rohou + * \copyright Copyright 2023 Codac Team + * \license This program is distributed under the terms of + * the GNU Lesser General Public License (LGPL). + */ + +#ifndef __CODAC2_CTCONPAVER_H__ +#define __CODAC2_CTCONPAVER_H__ + +#include "codac2_Contractor.h" + +namespace codac2 +{ + template + class CtcPaver : public Contractor + { + public: + + static bool compare_paving(Paving* first, Paving* second) + { + return first->box().volume() > second->box().volume(); + } + + CtcPaver(ContractorOnBox& ctc, size_t max_leaves) + : _ctc(ctc), _max_leaves(max_leaves) + { + + } + + void contract(Paving& x) + { + list*> l_subpav = x.leaves_list(); + size_t nb_leaves = l_subpav.size(); + + while(!l_subpav.empty()) + { + l_subpav.sort(compare_paving); + + Paving* q = l_subpav.front(); + l_subpav.pop_front(); + + _ctc.contract(q->_x); + + if(q->_x.is_empty()) + nb_leaves--; + + else if(nb_leaves < _max_leaves) + { + q->bisect(); + nb_leaves++; + l_subpav.push_back(q->_left.get()); + l_subpav.push_back(q->_right.get()); + } + } + } + + make_available_in_cn__templated(CtcPaver) + + protected: + + ContractorOnBox& _ctc; + size_t _max_leaves; + }; +} + +#endif \ No newline at end of file diff --git a/src/core/2/domains/interval/codac2_IntervalMatrix.h b/src/core/2/domains/interval/codac2_IntervalMatrix.h index 27cae35cd..255ab66ad 100644 --- a/src/core/2/domains/interval/codac2_IntervalMatrix.h +++ b/src/core/2/domains/interval/codac2_IntervalMatrix.h @@ -29,7 +29,7 @@ namespace codac2 using Eigen::Dynamic; template - class IntervalMatrix_ : public Eigen::Matrix, public Domain + class IntervalMatrix_ : public Eigen::Matrix, virtual public Domain { public: diff --git a/src/core/2/domains/paving/codac2_Paving.h b/src/core/2/domains/paving/codac2_Paving.h index 18dd777ab..ef2d873bf 100644 --- a/src/core/2/domains/paving/codac2_Paving.h +++ b/src/core/2/domains/paving/codac2_Paving.h @@ -22,7 +22,7 @@ namespace codac2 { template - class PavingBase + class PavingBase : virtual public Domain { public: @@ -115,6 +115,16 @@ namespace codac2 return (_left ? _left->nb_leaves() : 0) + (_right ? _right->nb_leaves() : 0); } + + DomainVolume dom_volume() const + { + DomainVolume vol; + dom_volume_push(vol); + return vol; + } + + template + friend std::ostream& operator<<(std::ostream& os, const PavingBase& p); protected: @@ -140,12 +150,30 @@ namespace codac2 } } + void dom_volume_push(DomainVolume& vol) const + { + if(is_leaf()) + vol.push_back(_x.volume()); + else + { + if(_left) _left->dom_volume_push(vol); + if(_right) _right->dom_volume_push(vol); + } + } + public: // todo IntervalVector_ _x; std::shared_ptr

_left = nullptr, _right = nullptr; }; + template + inline std::ostream& operator<<(std::ostream& os, const PavingBase& p) + { + os << "Paving"; + return os; + } + template class Paving : public PavingBase,N> { diff --git a/src/core/2/variables/codac2_Matrix.h b/src/core/2/variables/codac2_Matrix.h index b3e8fa032..af73684c8 100644 --- a/src/core/2/variables/codac2_Matrix.h +++ b/src/core/2/variables/codac2_Matrix.h @@ -68,7 +68,7 @@ namespace codac2 assert((R == Dynamic || (int)l.size() == R) && "ill-formed matrix"); int cols = -1; for(const auto& ri : l) { - assert(cols == -1 || cols == (int)ri.size() && "ill-formed matrix"); + assert((cols == -1 || cols == (int)ri.size()) && "ill-formed matrix"); cols = (int)ri.size(); } this->resize(l.size(),cols); @@ -98,7 +98,7 @@ namespace codac2 void init(double x) { - for(size_t i = 0 ; i < this->size() ; i++) + for(auto i = 0 ; i < this->size() ; i++) *(this->data()+i) = x; } @@ -190,8 +190,8 @@ namespace codac2 ibex::Matrix to_codac1(const Matrix_& x) { ibex::Matrix x_(x.rows(), x.cols()); - for(size_t i = 0 ; i < x.rows() ; i++) - for(size_t j = 0 ; j < x.cols() ; j++) + for(size_t i = 0 ; i < (size_t)x.rows() ; i++) + for(size_t j = 0 ; j < (size_t)x.cols() ; j++) x_[i][j] = x(i,j); return x_; } diff --git a/src/core/CMakeLists.txt b/src/core/CMakeLists.txt index 186d49a7f..0cd48e0f8 100644 --- a/src/core/CMakeLists.txt +++ b/src/core/CMakeLists.txt @@ -215,6 +215,9 @@ ${CMAKE_CURRENT_SOURCE_DIR}/2/contractors/codac2_CtcDiffInclusion.h ${CMAKE_CURRENT_SOURCE_DIR}/2/contractors/codac2_CtcLinobs.cpp ${CMAKE_CURRENT_SOURCE_DIR}/2/contractors/codac2_CtcLinobs.h + ${CMAKE_CURRENT_SOURCE_DIR}/2/contractors/codac2_CtcPaver.h + ${CMAKE_CURRENT_SOURCE_DIR}/2/contractors/codac2_CtcInter.h + ${CMAKE_CURRENT_SOURCE_DIR}/2/contractors/codac2_CtcCN.h ${CMAKE_CURRENT_SOURCE_DIR}/2/integration/codac2_AbstractDomain.cpp ${CMAKE_CURRENT_SOURCE_DIR}/2/integration/codac2_AbstractDomain.h ${CMAKE_CURRENT_SOURCE_DIR}/2/variables/codac2_Matrix.h