From 511423d7d3e05e81f927a3375dfef11b2d8bdc6c Mon Sep 17 00:00:00 2001
From: Riccardo De Benedictis <riccardo.debenedictis@cnr.it>
Date: Thu, 10 Oct 2024 12:39:34 +0200
Subject: [PATCH] Refactor flaw and resolver classes to add API listeners

---
 include/flaw.hpp     | 14 ++++++++++++--
 include/resolver.hpp | 11 +++++++++--
 include/solver.hpp   |  4 ++++
 src/flaw.cpp         | 19 ++++++++++++++++++-
 src/resolver.cpp     | 14 +++++++++++++-
 5 files changed, 56 insertions(+), 6 deletions(-)

diff --git a/include/flaw.hpp b/include/flaw.hpp
index d0839f1..63547ca 100644
--- a/include/flaw.hpp
+++ b/include/flaw.hpp
@@ -1,13 +1,15 @@
 #pragma once
 
+#include "lit.hpp"
+#include "rational.hpp"
 #include <functional>
 #include <memory>
 #include <vector>
 #include <cstdint>
-#include "lit.hpp"
-#include "rational.hpp"
 
 #ifdef ENABLE_API
+#include "sat_value_listener.hpp"
+#include "idl_value_listener.hpp"
 #include "json.hpp"
 #endif
 
@@ -23,7 +25,11 @@ namespace ratio
    *
    * The `flaw` class represents a flaw in a solver. A flaw is a problem or inconsistency that needs to be resolved by applying resolvers. It keeps track of the resolvers that caused the flaw, the resolvers that support the flaw, the estimated cost of the flaw, and other relevant information.
    */
+#ifdef ENABLE_API
+  class flaw : public semitone::sat_value_listener, public semitone::idl_value_listener
+#else
   class flaw
+#endif
   {
     friend class graph;
 
@@ -124,6 +130,10 @@ namespace ratio
     virtual void compute_resolvers() = 0;
 
 #ifdef ENABLE_API
+    void on_sat_value_changed(VARIABLE_TYPE v) override;
+
+    void on_idl_value_changed(VARIABLE_TYPE v) override;
+
     /**
      * @brief Get a JSON representation of the data of the flaw.
      *
diff --git a/include/resolver.hpp b/include/resolver.hpp
index 5999a39..adceeb3 100644
--- a/include/resolver.hpp
+++ b/include/resolver.hpp
@@ -1,11 +1,12 @@
 #pragma once
 
-#include <cstdint>
-#include <vector>
 #include "rational.hpp"
 #include "lit.hpp"
+#include <cstdint>
+#include <vector>
 
 #ifdef ENABLE_API
+#include "sat_value_listener.hpp"
 #include "json.hpp"
 #endif
 
@@ -23,7 +24,11 @@ namespace ratio
    * It contains information about the flaw it solves, the rho variable, the intrinsic cost, and the preconditions.
    * Derived classes must implement the `apply()` function to apply the resolver.
    */
+#ifdef ENABLE_API
+  class resolver : public semitone::sat_value_listener
+#else
   class resolver
+#endif
   {
     friend class graph;
     friend class flaw;
@@ -72,6 +77,8 @@ namespace ratio
     virtual void apply() = 0;
 
 #ifdef ENABLE_API
+    void on_sat_value_changed(VARIABLE_TYPE v) override;
+
     /**
      * @brief Get a JSON representation of the data of the resolver.
      *
diff --git a/include/solver.hpp b/include/solver.hpp
index ca4e626..594bc90 100644
--- a/include/solver.hpp
+++ b/include/solver.hpp
@@ -42,6 +42,10 @@ namespace ratio
   class solver : public riddle::core
   {
     friend class graph;
+#ifdef ENABLE_API
+    friend class flaw;
+    friend class resolver;
+#endif
 
   public:
     solver(std::string_view name = "oRatio") noexcept;
diff --git a/src/flaw.cpp b/src/flaw.cpp
index 8b4502a..0369f3a 100644
--- a/src/flaw.cpp
+++ b/src/flaw.cpp
@@ -6,7 +6,15 @@
 
 namespace ratio
 {
-    flaw::flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, bool exclusive) noexcept : s(s), causes(causes), exclusive(exclusive), position(s.get_idl_theory().new_var()) {}
+    flaw::flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, bool exclusive) noexcept : s(s), causes(causes), exclusive(exclusive), position(s.get_idl_theory().new_var())
+    {
+#ifdef ENABLE_API
+        s.get_sat().add_listener(*this);
+        s.get_idl_theory().add_listener(*this);
+
+        listen_idl(position);
+#endif
+    }
 
     resolver &flaw::get_cheapest_resolver() const noexcept
     {
@@ -38,5 +46,14 @@ namespace ratio
 
         // we initialize the phi variable of this flaw as the conjunction of the flaw's causes' rho variables..
         phi = s.get_sat().new_conj(std::move(cs));
+#ifdef ENABLE_API
+        listen_sat(variable(phi));
+#endif
     }
+
+#ifdef ENABLE_API
+    void flaw::on_sat_value_changed(VARIABLE_TYPE v) { s.flaw_state_changed(*this); }
+
+    void flaw::on_idl_value_changed(VARIABLE_TYPE v) { s.flaw_position_changed(*this); }
+#endif
 } // namespace ratio
diff --git a/src/resolver.cpp b/src/resolver.cpp
index 980e2d0..b7a3a22 100644
--- a/src/resolver.cpp
+++ b/src/resolver.cpp
@@ -12,7 +12,15 @@
 namespace ratio
 {
     resolver::resolver(flaw &f, const utils::rational &intrinsic_cost) : resolver(f, utils::lit(f.get_solver().get_sat().new_var()), intrinsic_cost) {}
-    resolver::resolver(flaw &f, const utils::lit &rho, const utils::rational &intrinsic_cost) : f(f), rho(rho), intrinsic_cost(intrinsic_cost) { assert(f.get_solver().get_sat().value(rho) != utils::False); }
+    resolver::resolver(flaw &f, const utils::lit &rho, const utils::rational &intrinsic_cost) : f(f), rho(rho), intrinsic_cost(intrinsic_cost)
+    {
+        assert(f.get_solver().get_sat().value(rho) != utils::False);
+#ifdef ENABLE_API
+        f.get_solver().get_sat().add_listener(*this);
+
+        listen_sat(variable(rho));
+#endif
+    }
 
     utils::rational resolver::get_estimated_cost() const noexcept
     {
@@ -32,4 +40,8 @@ namespace ratio
                                     .get_estimated_cost();
 #endif
     }
+
+#ifdef ENABLE_API
+    void resolver::on_sat_value_changed(VARIABLE_TYPE v) { f.get_solver().resolver_state_changed(*this); }
+#endif
 } // namespace ratio