Update listener classes and member functions in smart_type.hpp and sm…

…art_type.cpp
ratioSolver · Apr 17, 2024 · 125cb0f · 125cb0f
1 parent 6630b99
commit 125cb0f
Show file tree

Hide file tree

Showing 8 changed files with 221 additions and 5 deletions.
diff --git a/extern/semitone b/extern/semitone
diff --git a/include/smart_type.hpp b/include/smart_type.hpp
@@ -87,7 +87,7 @@ namespace ratio
      */
     virtual ~atom_listener();
 
-  private:
+  protected:
     riddle::atom &atm; // The atom object to listen to
   };
 

diff --git a/include/types/consumable_resource.hpp b/include/types/consumable_resource.hpp
@@ -6,6 +6,9 @@ namespace ratio
 {
   class consumable_resource final : public smart_type, public timeline
   {
+    class cr_atom_listener;
+    friend class cr_atom_listener;
+
   public:
     consumable_resource(solver &slv);
 
@@ -18,7 +21,26 @@ namespace ratio
     json::json extract() const noexcept override;
 #endif
 
+    class cr_atom_listener final : private atom_listener
+    {
+    public:
+      cr_atom_listener(consumable_resource &cr, atom &a);
+
+      void something_changed();
+
+      void on_sat_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_rdl_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_lra_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_ov_value_changed(VARIABLE_TYPE) override { something_changed(); }
+
+      consumable_resource &cr;
+    };
+
   private:
-    std::vector<std::reference_wrapper<atom>> atoms;
+    std::set<const riddle::item *> to_check;                        // the consumable-resource instances whose atoms have changed..
+    std::vector<std::reference_wrapper<atom>> atoms;                // the atoms of the consumable-resource..
+    std::vector<std::unique_ptr<cr_atom_listener>> listeners;       // we store, for each atom, its atom listener..
+    std::map<atom *, std::map<atom *, utils::lit>> leqs;            // all the possible ordering constraints..
+    std::map<atom *, std::map<utils::enum_val *, utils::lit>> frbs; // all the possible forbidding constraints..
   };
 } // namespace ratio
diff --git a/include/types/reusable_resource.hpp b/include/types/reusable_resource.hpp
@@ -6,6 +6,9 @@ namespace ratio
 {
   class reusable_resource final : public smart_type, public timeline
   {
+    class rr_atom_listener;
+    friend class rr_atom_listener;
+
   public:
     reusable_resource(solver &slv);
 
@@ -18,7 +21,26 @@ namespace ratio
     json::json extract() const noexcept override;
 #endif
 
+    class rr_atom_listener final : private atom_listener
+    {
+    public:
+      rr_atom_listener(reusable_resource &rr, atom &a);
+
+      void something_changed();
+
+      void on_sat_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_rdl_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_lra_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_ov_value_changed(VARIABLE_TYPE) override { something_changed(); }
+
+      reusable_resource &rr;
+    };
+
   private:
-    std::vector<std::reference_wrapper<atom>> atoms;
+    std::set<const riddle::item *> to_check;                        // the reusable-resource instances whose atoms have changed..
+    std::vector<std::reference_wrapper<atom>> atoms;                // the atoms of the reusable-resource..
+    std::vector<std::unique_ptr<rr_atom_listener>> listeners;       // we store, for each atom, its atom listener..
+    std::map<atom *, std::map<atom *, utils::lit>> leqs;            // all the possible ordering constraints..
+    std::map<atom *, std::map<utils::enum_val *, utils::lit>> frbs; // all the possible forbidding constraints..
   };
 } // namespace ratio
diff --git a/include/types/state_variable.hpp b/include/types/state_variable.hpp
@@ -6,6 +6,9 @@ namespace ratio
 {
   class state_variable final : public smart_type, public timeline
   {
+    class sv_atom_listener;
+    friend class sv_atom_listener;
+
   public:
     state_variable(solver &slv);
 
@@ -18,7 +21,26 @@ namespace ratio
     json::json extract() const noexcept override;
 #endif
 
+    class sv_atom_listener final : private atom_listener
+    {
+    public:
+      sv_atom_listener(state_variable &sv, atom &a);
+
+      void something_changed();
+
+      void on_sat_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_rdl_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_lra_value_changed(VARIABLE_TYPE) override { something_changed(); }
+      void on_ov_value_changed(VARIABLE_TYPE) override { something_changed(); }
+
+      state_variable &sv;
+    };
+
   private:
-    std::vector<std::reference_wrapper<atom>> atoms;
+    std::set<const riddle::item *> to_check;                        // the state-variable instances whose atoms have changed..
+    std::vector<std::reference_wrapper<atom>> atoms;                // the atoms of the state-variable..
+    std::vector<std::unique_ptr<sv_atom_listener>> listeners;       // we store, for each atom, its atom listener..
+    std::map<atom *, std::map<atom *, utils::lit>> leqs;            // all the possible ordering constraints..
+    std::map<atom *, std::map<utils::enum_val *, utils::lit>> frbs; // all the possible forbidding constraints..
   };
 } // namespace ratio
diff --git a/src/types/consumable_resource.cpp b/src/types/consumable_resource.cpp
@@ -15,6 +15,56 @@ namespace ratio
             get_solver().get_predicate("Interval")->get().call(atm);
             restore_ni();
         }
+
+        // we store the variables for on-line flaw resolution..
+        // the ordering constraints between the atoms are stored in the leqs map..
+        const auto start = atm->get("start");
+        const auto end = atm->get("end");
+        for (const auto &c_atm : atoms)
+        {
+            const auto c_start = c_atm.get().get("start");
+            const auto c_end = c_atm.get().get("end");
+#ifdef DL_TN
+            auto before = get_solver().get_rdl_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(end)->get_value(), std::static_pointer_cast<riddle::arith_item>(c_start)->get_value());
+            auto after = get_solver().get_rdl_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(c_end)->get_value(), std::static_pointer_cast<riddle::arith_item>(start)->get_value());
+#elif defined(LRA_TN)
+            auto before = get_solver().get_lra_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(end)->get_value(), std::static_pointer_cast<riddle::arith_item>(c_start)->get_value());
+            auto after = get_solver().get_lra_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(c_end)->get_value(), std::static_pointer_cast<riddle::arith_item>(start)->get_value());
+            [[maybe_unused]] bool nc = get_solver().get_sat().new_clause({!before, !after}); // the ordering constraints are always disjunctive..
+            assert(nc);
+#endif
+            if (get_solver().get_sat().value(before) == utils::Undefined)
+                leqs[atm.get()][&c_atm.get()] = before;
+            if (get_solver().get_sat().value(after) == utils::Undefined)
+                leqs[&c_atm.get()][atm.get()] = after;
+        }
+
+        const auto tau = atm->get("tau");
+        if (is_enum(*tau))
+            for (const auto &cr : get_solver().domain(static_cast<const riddle::enum_item &>(*tau)))
+            {
+                auto var = get_solver().get_ov_theory().allows(static_cast<const riddle::enum_item &>(*tau).get_value(), cr.get());
+                if (get_solver().get_sat().value(var) == utils::Undefined)
+                    frbs[atm.get()][&cr.get()] = var;
+            }
+
         atoms.push_back(*atm);
+        auto listener = std::make_unique<cr_atom_listener>(*this, *atm);
+        listener->something_changed();
+        listeners.push_back(std::move(listener));
+    }
+
+    consumable_resource::cr_atom_listener::cr_atom_listener(consumable_resource &cr, atom &a) : atom_listener(a), cr(cr) {}
+    void consumable_resource::cr_atom_listener::something_changed()
+    {
+        if (cr.get_solver().get_sat().value(atm.get_sigma()) == utils::True)
+        { // the atom is active
+            const auto tau = atm.get("tau");
+            if (is_enum(*tau))
+                for (const auto &c_cr : cr.get_solver().domain(static_cast<const riddle::enum_item &>(*tau)))
+                    cr.to_check.insert(static_cast<const riddle::item *>(&c_cr.get()));
+            else
+                cr.to_check.insert(tau.get());
+        }
     }
 } // namespace ratio
diff --git a/src/types/reusable_resource.cpp b/src/types/reusable_resource.cpp
@@ -15,6 +15,56 @@ namespace ratio
             get_solver().get_predicate("Interval")->get().call(atm);
             restore_ni();
         }
+
+        // we store the variables for on-line flaw resolution..
+        // the ordering constraints between the atoms are stored in the leqs map..
+        const auto start = atm->get("start");
+        const auto end = atm->get("end");
+        for (const auto &c_atm : atoms)
+        {
+            const auto c_start = c_atm.get().get("start");
+            const auto c_end = c_atm.get().get("end");
+#ifdef DL_TN
+            auto before = get_solver().get_rdl_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(end)->get_value(), std::static_pointer_cast<riddle::arith_item>(c_start)->get_value());
+            auto after = get_solver().get_rdl_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(c_end)->get_value(), std::static_pointer_cast<riddle::arith_item>(start)->get_value());
+#elif defined(LRA_TN)
+            auto before = get_solver().get_lra_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(end)->get_value(), std::static_pointer_cast<riddle::arith_item>(c_start)->get_value());
+            auto after = get_solver().get_lra_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(c_end)->get_value(), std::static_pointer_cast<riddle::arith_item>(start)->get_value());
+            [[maybe_unused]] bool nc = get_solver().get_sat().new_clause({!before, !after}); // the ordering constraints are always disjunctive..
+            assert(nc);
+#endif
+            if (get_solver().get_sat().value(before) == utils::Undefined)
+                leqs[atm.get()][&c_atm.get()] = before;
+            if (get_solver().get_sat().value(after) == utils::Undefined)
+                leqs[&c_atm.get()][atm.get()] = after;
+        }
+
+        const auto tau = atm->get("tau");
+        if (is_enum(*tau))
+            for (const auto &rr : get_solver().domain(static_cast<const riddle::enum_item &>(*tau)))
+            {
+                auto var = get_solver().get_ov_theory().allows(static_cast<const riddle::enum_item &>(*tau).get_value(), rr.get());
+                if (get_solver().get_sat().value(var) == utils::Undefined)
+                    frbs[atm.get()][&rr.get()] = var;
+            }
+
         atoms.push_back(*atm);
+        auto listener = std::make_unique<rr_atom_listener>(*this, *atm);
+        listener->something_changed();
+        listeners.push_back(std::move(listener));
+    }
+
+    reusable_resource::rr_atom_listener::rr_atom_listener(reusable_resource &rr, atom &a) : atom_listener(a), rr(rr) {}
+    void reusable_resource::rr_atom_listener::something_changed()
+    {
+        if (rr.get_solver().get_sat().value(atm.get_sigma()) == utils::True)
+        { // the atom is active
+            const auto tau = atm.get("tau");
+            if (is_enum(*tau))
+                for (const auto &c_rr : rr.get_solver().domain(static_cast<const riddle::enum_item &>(*tau)))
+                    rr.to_check.insert(static_cast<const riddle::item *>(&c_rr.get()));
+            else
+                rr.to_check.insert(tau.get());
+        }
     }
 } // namespace ratio
diff --git a/src/types/state_variable.cpp b/src/types/state_variable.cpp
@@ -15,6 +15,56 @@ namespace ratio
             get_solver().get_predicate("Interval")->get().call(atm);
             restore_ni();
         }
+
+        // we store the variables for on-line flaw resolution..
+        // the ordering constraints between the atoms are stored in the leqs map..
+        const auto start = atm->get("start");
+        const auto end = atm->get("end");
+        for (const auto &c_atm : atoms)
+        {
+            const auto c_start = c_atm.get().get("start");
+            const auto c_end = c_atm.get().get("end");
+#ifdef DL_TN
+            auto before = get_solver().get_rdl_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(end)->get_value(), std::static_pointer_cast<riddle::arith_item>(c_start)->get_value());
+            auto after = get_solver().get_rdl_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(c_end)->get_value(), std::static_pointer_cast<riddle::arith_item>(start)->get_value());
+#elif defined(LRA_TN)
+            auto before = get_solver().get_lra_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(end)->get_value(), std::static_pointer_cast<riddle::arith_item>(c_start)->get_value());
+            auto after = get_solver().get_lra_theory().new_leq(std::static_pointer_cast<riddle::arith_item>(c_end)->get_value(), std::static_pointer_cast<riddle::arith_item>(start)->get_value());
+            [[maybe_unused]] bool nc = get_solver().get_sat().new_clause({!before, !after}); // the ordering constraints are always disjunctive..
+            assert(nc);
+#endif
+            if (get_solver().get_sat().value(before) == utils::Undefined)
+                leqs[atm.get()][&c_atm.get()] = before;
+            if (get_solver().get_sat().value(after) == utils::Undefined)
+                leqs[&c_atm.get()][atm.get()] = after;
+        }
+
+        const auto tau = atm->get("tau");
+        if (is_enum(*tau))
+            for (const auto &sv : get_solver().domain(static_cast<const riddle::enum_item &>(*tau)))
+            {
+                auto var = get_solver().get_ov_theory().allows(static_cast<const riddle::enum_item &>(*tau).get_value(), sv.get());
+                if (get_solver().get_sat().value(var) == utils::Undefined)
+                    frbs[atm.get()][&sv.get()] = var;
+            }
+
         atoms.push_back(*atm);
+        auto listener = std::make_unique<sv_atom_listener>(*this, *atm);
+        listener->something_changed();
+        listeners.push_back(std::move(listener));
+    }
+
+    state_variable::sv_atom_listener::sv_atom_listener(state_variable &sv, atom &a) : atom_listener(a), sv(sv) {}
+    void state_variable::sv_atom_listener::something_changed()
+    {
+        if (sv.get_solver().get_sat().value(atm.get_sigma()) == utils::True)
+        { // the atom is active
+            const auto tau = atm.get("tau");
+            if (is_enum(*tau))
+                for (const auto &c_sv : sv.get_solver().domain(static_cast<const riddle::enum_item &>(*tau)))
+                    sv.to_check.insert(static_cast<const riddle::item *>(&c_sv.get()));
+            else
+                sv.to_check.insert(tau.get());
+        }
     }
 } // namespace ratio