Skip to content

Commit

Permalink
Refactor flaw and resolver classes to add API listeners
Browse files Browse the repository at this point in the history
  • Loading branch information
riccardodebenedictis committed Oct 10, 2024
1 parent d7346cc commit 511423d
Show file tree
Hide file tree
Showing 5 changed files with 56 additions and 6 deletions.
14 changes: 12 additions & 2 deletions include/flaw.hpp
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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;

Expand Down Expand Up @@ -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.
*
Expand Down
11 changes: 9 additions & 2 deletions include/resolver.hpp
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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;
Expand Down Expand Up @@ -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.
*
Expand Down
4 changes: 4 additions & 0 deletions include/solver.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
19 changes: 18 additions & 1 deletion src/flaw.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
{
Expand Down Expand Up @@ -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
14 changes: 13 additions & 1 deletion src/resolver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
{
Expand All @@ -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

0 comments on commit 511423d

Please sign in to comment.