Update subproject references and change on_sat_value_changed paramete…

…r type from std::size_t to utils::var in resolver and flaw classes
ratioSolver · Nov 11, 2024 · 3d3df76 · 3d3df76
1 parent 3e0e7f0
commit 3d3df76
Show file tree

Hide file tree

Showing 12 changed files with 39 additions and 39 deletions.
diff --git a/extern/riddle b/extern/riddle
diff --git a/extern/semitone b/extern/semitone
diff --git a/include/flaw.hpp b/include/flaw.hpp
@@ -75,9 +75,9 @@ namespace ratio
     /**
      * @brief Get the position variable associated to this flaw.
      *
-     * @return std::size_t the position variable associated to this flaw.
+     * @return utils::var the position variable associated to this flaw.
      */
-    std::size_t get_position() const noexcept { return position; }
+    utils::var get_position() const noexcept { return position; }
 
     /**
      * @brief Check whether this flaw has been expanded.
@@ -130,9 +130,9 @@ namespace ratio
     virtual void compute_resolvers() = 0;
 
 #ifdef ENABLE_API
-    void on_sat_value_changed(std::size_t v) override;
+    void on_sat_value_changed(utils::var v) override;
 
-    void on_idl_value_changed(std::size_t v) override;
+    void on_idl_value_changed(utils::var v) override;
 
     /**
      * @brief Get a JSON representation of the data of the flaw.
@@ -151,7 +151,7 @@ namespace ratio
     const bool enqueue;                                            // whether this flaw must be enqueued or can be expanded..
     utils::lit phi;                                                // the literal indicating whether the flaw is active or not (this literal is initialized by the `init` procedure)..
     utils::rational est_cost = utils::rational::positive_infinite; // the current estimated cost of the flaw..
-    std::size_t position;                                          // the position variable (i.e., an integer time-point) associated to this flaw..
+    utils::var position;                                           // the position variable (i.e., an integer time-point) associated to this flaw..
     bool expanded = false;                                         // whether this flaw has been expanded or not..
     std::vector<std::reference_wrapper<resolver>> resolvers;       // the resolvers for this flaw..
     std::vector<std::reference_wrapper<resolver>> supports;        // the resolvers supported by this flaw (used for propagating cost estimates)..

diff --git a/include/graph.hpp b/include/graph.hpp
@@ -276,18 +276,18 @@ namespace ratio
     void pop() noexcept override;
 
   private:
-    solver &slv;                                                                  // the solver this graph belongs to..
-    std::unordered_map<std::size_t, std::vector<std::unique_ptr<flaw>>> phis;     // the phi variables (propositional variable to flaws) of the flaws..
-    std::vector<std::unique_ptr<flaw>> pending_flaws;                             // pending flaws, waiting for root-level to be initialized..
-    std::unordered_map<std::size_t, std::vector<std::unique_ptr<resolver>>> rhos; // the rho variables (propositional variable to resolver) of the resolvers..
-    std::optional<std::reference_wrapper<flaw>> c_flaw;                           // the current flaw..
-    std::optional<std::reference_wrapper<resolver>> c_res;                        // the current resolver..
-    utils::lit tmp_ni;                                                            // the temporary controlling literal, used for restoring the controlling literal..
-    utils::lit ni{utils::TRUE_lit};                                               // the current controlling literal..
-    std::deque<std::reference_wrapper<flaw>> flaw_q;                              // the flaw queue (for the graph building procedure)..
-    std::unordered_set<flaw *> visited;                                           // the visited flaws, for graph cost propagation (and deferrable flaws check)..
-    std::unordered_set<flaw *> active_flaws;                                      // the currently active flaws..
-    std::size_t gamma;                                                            // the variable representing the validity of this graph..
+    solver &slv;                                                                 // the solver this graph belongs to..
+    std::unordered_map<utils::var, std::vector<std::unique_ptr<flaw>>> phis;     // the phi variables (propositional variable to flaws) of the flaws..
+    std::vector<std::unique_ptr<flaw>> pending_flaws;                            // pending flaws, waiting for root-level to be initialized..
+    std::unordered_map<utils::var, std::vector<std::unique_ptr<resolver>>> rhos; // the rho variables (propositional variable to resolver) of the resolvers..
+    std::optional<std::reference_wrapper<flaw>> c_flaw;                          // the current flaw..
+    std::optional<std::reference_wrapper<resolver>> c_res;                       // the current resolver..
+    utils::lit tmp_ni;                                                           // the temporary controlling literal, used for restoring the controlling literal..
+    utils::lit ni{utils::TRUE_lit};                                              // the current controlling literal..
+    std::deque<std::reference_wrapper<flaw>> flaw_q;                             // the flaw queue (for the graph building procedure)..
+    std::unordered_set<flaw *> visited;                                          // the visited flaws, for graph cost propagation (and deferrable flaws check)..
+    std::unordered_set<flaw *> active_flaws;                                     // the currently active flaws..
+    utils::var gamma;                                                            // the variable representing the validity of this graph..
 
     /**
      * @brief Represents a layer in the solver.

diff --git a/include/resolver.hpp b/include/resolver.hpp
@@ -77,7 +77,7 @@ namespace ratio
     virtual void apply() = 0;
 
 #ifdef ENABLE_API
-    void on_sat_value_changed(std::size_t v) override;
+    void on_sat_value_changed(utils::var v) override;
 
     /**
      * @brief Get a JSON representation of the data of the resolver.

diff --git a/include/types/consumable_resource.hpp b/include/types/consumable_resource.hpp
@@ -36,10 +36,10 @@ namespace ratio
 
       void something_changed();
 
-      void on_sat_value_changed(std::size_t) override { something_changed(); }
-      void on_rdl_value_changed(std::size_t) override { something_changed(); }
-      void on_lra_value_changed(std::size_t) override { something_changed(); }
-      void on_ov_value_changed(std::size_t) override { something_changed(); }
+      void on_sat_value_changed(utils::var) override { something_changed(); }
+      void on_rdl_value_changed(utils::var) override { something_changed(); }
+      void on_lra_value_changed(utils::var) override { something_changed(); }
+      void on_ov_value_changed(utils::var) override { something_changed(); }
 
       consumable_resource &cr;
     };

diff --git a/include/types/reusable_resource.hpp b/include/types/reusable_resource.hpp
@@ -136,10 +136,10 @@ namespace ratio
 
       void something_changed();
 
-      void on_sat_value_changed(std::size_t) override { something_changed(); }
-      void on_rdl_value_changed(std::size_t) override { something_changed(); }
-      void on_lra_value_changed(std::size_t) override { something_changed(); }
-      void on_ov_value_changed(std::size_t) override { something_changed(); }
+      void on_sat_value_changed(utils::var) override { something_changed(); }
+      void on_rdl_value_changed(utils::var) override { something_changed(); }
+      void on_lra_value_changed(utils::var) override { something_changed(); }
+      void on_ov_value_changed(utils::var) override { something_changed(); }
 
       reusable_resource &rr;
     };

diff --git a/include/types/state_variable.hpp b/include/types/state_variable.hpp
@@ -135,10 +135,10 @@ namespace ratio
 
       void something_changed();
 
-      void on_sat_value_changed(std::size_t) override { something_changed(); }
-      void on_rdl_value_changed(std::size_t) override { something_changed(); }
-      void on_lra_value_changed(std::size_t) override { something_changed(); }
-      void on_ov_value_changed(std::size_t) override { something_changed(); }
+      void on_sat_value_changed(utils::var) override { something_changed(); }
+      void on_rdl_value_changed(utils::var) override { something_changed(); }
+      void on_lra_value_changed(utils::var) override { something_changed(); }
+      void on_ov_value_changed(utils::var) override { something_changed(); }
 
       state_variable &sv;
     };

diff --git a/src/flaw.cpp b/src/flaw.cpp
@@ -52,8 +52,8 @@ namespace ratio
     }
 
 #ifdef ENABLE_API
-    void flaw::on_sat_value_changed(std::size_t v) { s.flaw_state_changed(*this); }
+    void flaw::on_sat_value_changed(utils::var v) { s.flaw_state_changed(*this); }
 
-    void flaw::on_idl_value_changed(std::size_t v) { s.flaw_position_changed(*this); }
+    void flaw::on_idl_value_changed(utils::var v) { s.flaw_position_changed(*this); }
 #endif
 } // namespace ratio
diff --git a/src/resolver.cpp b/src/resolver.cpp
@@ -42,6 +42,6 @@ namespace ratio
     }
 
 #ifdef ENABLE_API
-    void resolver::on_sat_value_changed(std::size_t v) { f.get_solver().resolver_state_changed(*this); }
+    void resolver::on_sat_value_changed(utils::var v) { f.get_solver().resolver_state_changed(*this); }
 #endif
 } // namespace ratio
diff --git a/src/types/reusable_resource.cpp b/src/types/reusable_resource.cpp
@@ -133,7 +133,7 @@ namespace ratio
 
                             // we compute the possible resolvers..
                             std::vector<std::pair<utils::lit, double>> choices;
-                            std::unordered_set<std::size_t> vars;
+                            std::unordered_set<utils::var> vars;
                             // we consider all the pairs of atoms in the Minimal Conflict Sets (MCSs)..
                             for (const auto &as : utils::combinations(std::vector<atom *>(overlapping_atoms.cbegin(), overlapping_atoms.cend()), 2))
                             {
@@ -333,7 +333,7 @@ namespace ratio
     reusable_resource::rr_flaw::rr_flaw(reusable_resource &rr_tp, const riddle::component &rr, const std::set<atom *> &mcs) : flaw(rr_tp.get_solver(), smart_type::get_resolvers(mcs), true, false), rr_tp(rr_tp), rr(rr), mcs(mcs) {}
     void reusable_resource::rr_flaw::compute_resolvers()
     {
-        std::unordered_set<std::size_t> vars;
+        std::unordered_set<utils::var> vars;
         for (const auto &as : utils::combinations(std::vector<atom *>(mcs.cbegin(), mcs.cend()), 2))
         {
             if (const auto a0_it = rr_tp.leqs.find(as[0]); a0_it != rr_tp.leqs.cend())

diff --git a/src/types/state_variable.cpp b/src/types/state_variable.cpp
@@ -71,7 +71,7 @@ namespace ratio
                     has_conflict = true;
                     // we compute the possible resolvers..
                     std::vector<std::pair<utils::lit, double>> choices;
-                    std::unordered_set<std::size_t> vars;
+                    std::unordered_set<utils::var> vars;
                     // we consider all the pairs of atoms in the Minimal Conflict Sets (MCSs)..
                     for (const auto &as : utils::combinations(std::vector<atom *>(overlapping_atoms.cbegin(), overlapping_atoms.cend()), 2))
                     {
@@ -259,7 +259,7 @@ namespace ratio
     state_variable::sv_flaw::sv_flaw(state_variable &sv_tp, const riddle::component &sv, const std::set<atom *> &mcs) : flaw(sv_tp.get_solver(), smart_type::get_resolvers(mcs), true, false), sv_tp(sv_tp), sv(sv), mcs(mcs) {}
     void state_variable::sv_flaw::compute_resolvers()
     {
-        std::unordered_set<std::size_t> vars;
+        std::unordered_set<utils::var> vars;
         for (const auto &as : utils::combinations(std::vector<atom *>(mcs.cbegin(), mcs.cend()), 2))
         {
             if (const auto a0_it = sv_tp.leqs.find(as[0]); a0_it != sv_tp.leqs.cend())
+1 −1		extern/utils
+4 −4		include/item.hpp
+1 −1		src/item.cpp
+1 −1		extern/json
+2 −2		include/constr.hpp
+5 −5		include/dl/dl_distance_constraint.hpp
+25 −25		include/dl/idl_theory.hpp
+3 −3		include/dl/idl_value_listener.hpp
+23 −23		include/dl/rdl_theory.hpp
+3 −3		include/dl/rdl_value_listener.hpp
+31 −31		include/lra/lra_theory.hpp
+3 −3		include/lra/lra_value_listener.hpp
+12 −12		include/ov/ov_theory.hpp
+5 −5		include/ov/ov_value_listener.hpp
+7 −7		include/sat_core.hpp
+3 −3		include/sat_value_listener.hpp
+1 −1		include/theory.hpp
+2 −2		src/constr.cpp
+16 −16		src/dl/idl_theory.cpp
+16 −16		src/dl/rdl_theory.cpp
+16 −16		src/lra/lra_theory.cpp
+8 −8		src/ov/ov_theory.cpp
+3 −3		src/sat_core.cpp
+1 −1		src/theory.cpp
+8 −8		tests/test_dl.cpp
+17 −17		tests/test_sat.cpp