Update submodule references in extern/riddle and extern/semitone

CMakeLists.txt

@@ -6,6 +6,7 @@ include(CTest)
 enable_testing()
 
 set(JSON_INCLUDE_UTILS OFF CACHE BOOL "Enable JSON Utils" FORCE)
+set(BUILD_LISTENERS ON CACHE BOOL "Builds the listeners" FORCE)
 
 add_subdirectory(extern/riddle)
 add_subdirectory(extern/semitone)
@@ -30,9 +31,9 @@ message(STATUS "Heuristic type: ${HEURISTIC_TYPE}")
 
 option(ENABLE_VISUALIZATION "Enable visualization features" OFF)
 
-add_library(oRatioLib src/solver.cpp src/graph.cpp src/flaw.cpp src/resolver.cpp src/smart_type.cpp src/flaws/atom_flaw.cpp src/flaws/bool_flaw.cpp src/flaws/disj_flaw.cpp src/flaws/disjunction_flaw.cpp src/flaws/enum_flaw.cpp)
+add_library(oRatioLib src/solver.cpp src/graph.cpp src/flaw.cpp src/resolver.cpp src/smart_type.cpp src/flaws/atom_flaw.cpp src/flaws/bool_flaw.cpp src/flaws/disj_flaw.cpp src/flaws/disjunction_flaw.cpp src/flaws/enum_flaw.cpp src/types/agent.cpp)
 target_link_libraries(oRatioLib PUBLIC RiDDLe SeMiTONE)
-target_include_directories(oRatioLib PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include> $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include/flaws> $<BUILD_INTERFACE:${CMAKE_CURRENT_BINARY_DIR}>)
+target_include_directories(oRatioLib PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include> $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include/flaws> $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include/types> $<BUILD_INTERFACE:${CMAKE_CURRENT_BINARY_DIR}>)
 
 if(${TEMPORAL_NETWORK_TYPE} STREQUAL "LRA")
     set(INIT_STRING "predicate Impulse(real at) { at >= origin; at <= horizon; } predicate Interval(real start, real end) { start >= origin; start <= end; end <= horizon; } real origin, horizon; origin >= 0.0; origin <= horizon;" CACHE STRING "Initialization string")

include/graph.hpp

@@ -10,8 +10,11 @@
 
 namespace ratio
 {
+  class smart_type;
   class graph : public semitone::theory
   {
+    friend class smart_type;
+
   public:
     graph(solver &slv) noexcept;
 
@@ -64,9 +67,9 @@ namespace ratio
      *
      * If there is a current resolver, the controlling literal is the rho variable of the resolver. Otherwise, it is TRUE.
      *
-     * @return utils::lit The current controlling literal.
+     * @return const utils::lit& The current controlling literal.
      */
-    utils::lit get_ni() const noexcept { return res.has_value() ? res->get().get_rho() : utils::TRUE_lit; }
+    const utils::lit &get_ni() const noexcept { return ni; }
 
   protected:
     /**
@@ -83,6 +86,14 @@ namespace ratio
      */
     void expand_flaw(flaw &f);
 
+    void set_ni(const utils::lit &v) noexcept
+    {
+      tmp_ni = ni;
+      ni = v;
+    }
+
+    void restore_ni() noexcept { ni = tmp_ni; }
+
   private:
     bool propagate(const utils::lit &) noexcept override { return true; }
     bool check() noexcept override { return true; }
@@ -95,6 +106,8 @@ namespace ratio
     std::vector<std::unique_ptr<flaw>> pending_flaws;                               // pending flaws, waiting for root-level to be initialized..
     std::unordered_map<VARIABLE_TYPE, std::vector<std::unique_ptr<resolver>>> rhos; // the rho variables (propositional variable to resolver) of the resolvers..
     std::optional<std::reference_wrapper<resolver>> 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 *> active_flaws;                                        // the currently active flaws..
     VARIABLE_TYPE gamma;                                                            // the variable representing the validity of this graph..

include/smart_type.hpp

@@ -6,6 +6,10 @@
 #include "rdl_value_listener.hpp"
 #include "ov_value_listener.hpp"
 
+#ifdef ENABLE_VISUALIZATION
+#include "json.hpp"
+#endif
+
 namespace ratio
 {
   class solver;
@@ -21,12 +25,12 @@ namespace ratio
 
   public:
     /**
-     * @brief Constructs a smart_type object with the specified parent scope and name.
+     * @brief Constructs a smart_type object with the specified solver and name.
      *
-     * @param parent The parent scope of the smart_type.
+     * @param slv The solver object to associate with the smart_type.
      * @param name The name of the smart_type.
      */
-    smart_type(scope &parent, const std::string &name);
+    smart_type(solver &slv, const std::string &name);
 
     /**
      * @brief Default destructor for the smart_type class.
@@ -40,20 +44,24 @@ namespace ratio
      */
     solver &get_solver() const { return slv; }
 
+  protected:
+    void set_ni(const utils::lit &v) noexcept; // temporally sets the graph's `ni` literal..
+    void restore_ni() noexcept;                // restores the graph's `ni` literal..
+
   private:
     /**
      * @brief Returns all the decisions to take for solving the current inconsistencies with their choices' estimated costs.
      *
      * @return A vector of decisions, each represented by a vector of pairs containing the literals representing the choice and its estimated cost.
      */
-    virtual std::vector<std::vector<std::pair<utils::lit, double>>> get_current_incs() = 0;
+    virtual std::vector<std::vector<std::pair<utils::lit, double>>> get_current_incs() const noexcept = 0;
 
     /**
      * @brief Notifies the smart_type that a new atom has been created.
      *
      * @param atm The new atom that has been created.
      */
-    virtual void new_atom(atom &atm) = 0;
+    virtual void new_atom(std::shared_ptr<ratio::atom> &atm) noexcept = 0;
 
   private:
     solver &slv;
@@ -82,4 +90,32 @@ namespace ratio
   private:
     riddle::atom &atm; // The atom object to listen to
   };
+
+  /**
+   * @brief Represents a timeline.
+   *
+   * The timeline class provides an interface for working with timelines.
+   * It is an abstract base class that can be inherited to create specific timeline implementations.
+   */
+  class timeline
+  {
+  public:
+    /**
+     * @brief Destructor for the timeline class.
+     *
+     * The destructor is declared as virtual to ensure that derived classes can be properly destroyed.
+     */
+    virtual ~timeline() = default;
+
+#ifdef ENABLE_VISUALIZATION
+    /**
+     * @brief Extracts the timeline data as JSON.
+     *
+     * This function extracts the timeline data and returns it as a JSON object.
+     *
+     * @return The timeline data as a JSON object.
+     */
+    virtual json::json extract() const noexcept = 0;
+#endif
+  };
 } // namespace ratio

include/solver.hpp

@@ -119,6 +119,21 @@ namespace ratio
     graph &gr;                 // the causal graph
   };
 
+  /**
+   * Checks if the given atom is of type "Impulse".
+   *
+   * @param atm The atom to check.
+   * @return True if the atom is of type "Impulse", false otherwise.
+   */
+  inline bool is_impulse(const atom &atm) noexcept { return atm.get_core().get_predicate("Impulse")->get().is_assignable_from(atm.get_type()); }
+  /**
+   * Checks if the given atom is of type "Interval".
+   *
+   * @param atm The atom to check.
+   * @return True if the atom is of type "Interval", false otherwise.
+   */
+  inline bool is_interval(const atom &atm) noexcept { return atm.get_core().get_predicate("Interval")->get().is_assignable_from(atm.get_type()); }
+
 #ifdef ENABLE_VISUALIZATION
   json::json to_json(const solver &rhs) noexcept;
   json::json to_timelines(const solver &rhs) noexcept;

include/types/agent.hpp

@@ -0,0 +1,23 @@
+#pragma once
+
+#include "smart_type.hpp"
+
+namespace ratio
+{
+  class agent final : public smart_type, public timeline
+  {
+    agent(solver &slv);
+
+  private:
+    std::vector<std::vector<std::pair<utils::lit, double>>> get_current_incs() const noexcept override { return {}; }
+
+    void new_atom(std::shared_ptr<ratio::atom> &atm) noexcept override;
+
+#ifdef ENABLE_VISUALIZATION
+    json::json extract() const noexcept override;
+#endif
+
+  private:
+    std::vector<std::reference_wrapper<atom>> atoms;
+  };
+} // namespace ratio

src/flaws/bool_flaw.cpp

@@ -1,6 +1,5 @@
 #include <cassert>
 #include "bool_flaw.hpp"
-#include "solver.hpp"
 #include "graph.hpp"
 
 namespace ratio

src/flaws/disj_flaw.cpp

@@ -1,6 +1,5 @@
 #include <cassert>
 #include "disj_flaw.hpp"
-#include "solver.hpp"
 #include "graph.hpp"
 
 namespace ratio

src/flaws/disjunction_flaw.cpp

@@ -1,6 +1,5 @@
 #include <cassert>
 #include "disjunction_flaw.hpp"
-#include "solver.hpp"
 #include "graph.hpp"
 
 namespace ratio

src/flaws/enum_flaw.cpp

@@ -1,6 +1,5 @@
 #include <cassert>
 #include "enum_flaw.hpp"
-#include "solver.hpp"
 #include "graph.hpp"
 
 namespace ratio

src/graph.cpp

@@ -8,6 +8,7 @@ namespace ratio
 
     void graph::new_causal_link(flaw &f, resolver &r)
     {
+        LOG_TRACE("[" << slv.get_name() << "] Creating causal link between flaw " << f.get_phi() << " and resolver " << r.get_rho());
         r.preconditions.push_back(f);
         f.supports.push_back(r);
         // activating the resolver requires the activation of the flaw..
@@ -23,7 +24,7 @@ namespace ratio
         assert(!f.expanded);
         assert(get_sat().root_level());
 
-        LOG_TRACE("[" << slv.get_name() << "] Expanding flaw");
+        LOG_TRACE("[" << slv.get_name() << "] Expanding flaw " << f.get_phi());
         f.compute_resolvers(); // we compute the flaw's resolvers..
         f.expanded = true;     // we mark the flaw as expanded..
 
@@ -63,8 +64,10 @@ namespace ratio
         // we apply the flaw's resolvers..
         for (const auto &r : f.resolvers)
         {
-            LOG_TRACE("[" << slv.get_name() << "] Applying resolver");
-            res = r;
+            LOG_TRACE("[" << slv.get_name() << "] Applying resolver " << r.get_rho());
+            res = r;                   // we write down the resolver so that new flaws know their cause..
+            set_ni(r.get().get_rho()); // we temporally set the resolver's rho as the controlling literal..
+
             // activating the resolver results in the flaw being solved..
             if (!get_sat().new_clause({!r.get().get_rho(), f.get_phi()}))
                 throw riddle::unsolvable_exception();
@@ -77,7 +80,8 @@ namespace ratio
                 if (!get_sat().new_clause({!r.get().get_rho()}))
                     throw riddle::unsolvable_exception();
             }
-            res = std::nullopt;
+            restore_ni();       // we restore the controlling literal..
+            res = std::nullopt; // we reset the resolver..
         }
 
         // we bind the variables to the SMT theory..

src/smart_type.cpp

@@ -1,9 +1,12 @@
 #include "smart_type.hpp"
-#include "solver.hpp"
+#include "graph.hpp"
 
 namespace ratio
 {
-    smart_type::smart_type(scope &parent, const std::string &name) : riddle::component_type(parent, name), slv(dynamic_cast<solver &>(parent.get_core())) {}
+    smart_type::smart_type(solver &slv, const std::string &name) : riddle::component_type(slv, name), slv(slv) {}
+
+    void smart_type::set_ni(const utils::lit &v) noexcept { slv.get_graph().set_ni(v); }
+    void smart_type::restore_ni() noexcept { slv.get_graph().restore_ni(); }
 
     atom_listener::~atom_listener()
     {

src/solver.cpp

@@ -1,6 +1,5 @@
 #include <cassert>
 #include <algorithm>
-#include "solver.hpp"
 #include "graph.hpp"
 #include "init.hpp"
 #include "smart_type.hpp"
@@ -309,7 +308,7 @@ namespace ratio
             while (!q.empty())
             {
                 if (auto st = dynamic_cast<smart_type *>(q.front()))
-                    st->new_atom(*atm);
+                    st->new_atom(atm);
                 for (const auto &p : q.front()->get_parents())
                     q.push(&p.get());
                 q.pop();

src/types/agent.cpp

@@ -0,0 +1,18 @@
+#include "agent.hpp"
+#include "solver.hpp"
+
+namespace ratio
+{
+    agent::agent(solver &slv) : smart_type(slv, "agent") {}
+
+    void agent::new_atom(std::shared_ptr<ratio::atom> &atm) noexcept
+    {
+        if (atm->is_fact())
+        {
+            set_ni(atm->get_sigma());
+            if (is_impulse(*atm))
+                atm->get_core().get_predicate("Impulse")->get();
+        }
+        atoms.push_back(*atm);
+    }
+} // namespace ratio