Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

clingo: Add support for propagator undo mode. #87

Merged
merged 2 commits into from
Mar 7, 2023
Merged

clingo: Add support for propagator undo mode. #87

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a8965ce
clingo: Add support for propagator undo mode.
Feb 18, 2023
69bed28
clingo: Add "enableClingoPropagatorUndo" function.
Mar 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 22 additions & 0 deletions clasp/clingo.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,14 @@ struct ClingoPropagatorCheck_t {
};
};

//! Supported undo modes for clingo propagators.
struct ClingoPropagatorUndo_t {
enum Type {
Default = 0u, //!< Call AbstractPropagator::undo() only on levels with non-empty changelist.
Always = 1u //!< Call AbstractPropagator::undo() on all levels that have been propagated or checked.
};
};

//! Initialization adaptor for a Potassco::AbstractPropagator.
/*!
* The class provides a function for registering watches for the propagator.
Expand All @@ -70,6 +78,7 @@ struct ClingoPropagatorCheck_t {
class ClingoPropagatorInit : public ClaspConfig::Configurator {
public:
typedef ClingoPropagatorCheck_t::Type CheckType;
typedef ClingoPropagatorUndo_t::Type UndoType;
//! Creates a new adaptor.
/*!
* \param cb The (theory) propagator that should be added to solvers.
Expand All @@ -92,6 +101,17 @@ class ClingoPropagatorInit : public ClaspConfig::Configurator {
*/
void enableClingoPropagatorCheck(CheckType checkMode);

//! Sets the undo mode to use when checks are enabled.
/*!
* \param undoMode The undo mode to use.
*
* \note By default, AbstractPropagator::undo() is only called for levels on which
* at least one watched literal has been assigned. However, if undoMode is set
* to "Always", AbstractPropagator::undo() is also called for levels L with an
* empty change list if AbstractPropagator::check() has been called on L.
*/
void enableClingoPropagatorUndo(UndoType undoMode);

void enableHistory(bool b);

//! Adds a watch for lit to all solvers and returns encodeLit(lit).
Expand All @@ -112,6 +132,7 @@ class ClingoPropagatorInit : public ClaspConfig::Configurator {
Potassco::AbstractPropagator* propagator() const { return prop_; }
ClingoPropagatorLock* lock() const { return lock_; }
CheckType checkMode() const { return check_; }
UndoType undoMode() const { return undo_; }

uint32 init(uint32 lastStep, Potassco::AbstractSolver& s);
private:
Expand All @@ -137,6 +158,7 @@ class ClingoPropagatorInit : public ClaspConfig::Configurator {
ChangeList changes_;
uint32 step_;
CheckType check_;
UndoType undo_;
};

//! Adaptor for a Potassco::AbstractPropagator.
Expand Down
13 changes: 12 additions & 1 deletion src/clingo.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,13 @@ void ClingoPropagator::undoLevel(Solver& s) {
POTASSCO_REQUIRE(s.decisionLevel() == level_, "Invalid undo");
uint32 beg = undo_.back();
undo_.pop_back();

if (test_bit(beg, CHECK_BIT) && call_->undoMode() == ClingoPropagatorUndo_t::Always) {
assert(beg >= prop_);
Potassco::LitSpan change = Potassco::toSpan<Potassco::Lit_t>();
ScopedLock(call_->lock(), call_->propagator(), Inc(epoch_))->undo(Control(*this, s), change);
}

if (prop_ > beg) {
Potassco::LitSpan change = Potassco::toSpan(&trail_[0] + beg, prop_ - beg);
ScopedLock(call_->lock(), call_->propagator(), Inc(epoch_))->undo(Control(*this, s), change);
Expand Down Expand Up @@ -417,7 +424,7 @@ struct ClingoPropagatorInit::History : POTASSCO_EXT_NS::unordered_map<Potassco::
};

ClingoPropagatorInit::ClingoPropagatorInit(Potassco::AbstractPropagator& cb, ClingoPropagatorLock* lock, CheckType m)
: prop_(&cb), lock_(lock), history_(0), step_(1), check_(m) {
: prop_(&cb), lock_(lock), history_(0), step_(1), check_(m), undo_(ClingoPropagatorUndo_t::Default) {
}
ClingoPropagatorInit::~ClingoPropagatorInit() { delete history_; }
bool ClingoPropagatorInit::applyConfig(Solver& s) { return s.addPost(new ClingoPropagator(this)); }
Expand Down Expand Up @@ -504,6 +511,10 @@ void ClingoPropagatorInit::enableClingoPropagatorCheck(CheckType checkMode) {
check_ = checkMode;
}

void ClingoPropagatorInit::enableClingoPropagatorUndo(UndoType undoMode) {
undo_ = undoMode;
}

void ClingoPropagatorInit::enableHistory(bool b) {
if (!b) { delete history_; history_ = 0; }
else if (!history_) { history_ = new History(); }
Expand Down
24 changes: 22 additions & 2 deletions tests/facade_test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2161,7 +2161,7 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") {
ClaspFacade libclasp;
class Prop : public Potassco::AbstractPropagator {
public:
Prop() : last(0), checks(0), props(0), totals(0), fire(false) {}
Prop() : last(0), checks(0), props(0), totals(0), undos(0), fire(false) {}
virtual void propagate(Potassco::AbstractSolver& s, const ChangeList& c) {
const Potassco::AbstractAssignment& a = s.assignment();
++props;
Expand All @@ -2174,7 +2174,7 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") {
}
}
}
virtual void undo(const Potassco::AbstractSolver&, const ChangeList&) {}
virtual void undo(const Potassco::AbstractSolver&, const ChangeList&) { ++undos; }
virtual void check(Potassco::AbstractSolver& s) {
const Potassco::AbstractAssignment& a = s.assignment();
++checks;
Expand All @@ -2194,6 +2194,7 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") {
int checks;
int props;
int totals;
int undos;
bool fire;
} prop;
MyInit pp(prop);
Expand All @@ -2213,7 +2214,15 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") {
REQUIRE(libclasp.ctx.master()->numFreeVars() == 0);
}
SECTION("test check is called only once per fixpoint") {
int expectedUndos = 0;
pp.enableClingoPropagatorCheck(ClingoPropagatorCheck_t::Fixpoint);
SECTION("fixpoint default undo") {
expectedUndos = 0;
}
SECTION("fixpoint always undo") {
pp.enableClingoPropagatorUndo(ClingoPropagatorUndo_t::Always);
expectedUndos = 1;
}
libclasp.prepare();
REQUIRE(prop.checks == 1u);
libclasp.ctx.master()->propagate();
Expand All @@ -2225,15 +2234,26 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") {
libclasp.ctx.master()->propagate();
REQUIRE(prop.checks == 3u);
libclasp.ctx.master()->restart();
REQUIRE(prop.undos == expectedUndos);
libclasp.ctx.master()->propagate();
INFO("Restart introduces new fix point");
REQUIRE(prop.checks == 4u);
}
SECTION("with mode total check is called once on total") {
int expectedUndos = 0;
pp.enableClingoPropagatorCheck(ClingoPropagatorCheck_t::Total);
SECTION("total default undo") {
expectedUndos = 0;
}
SECTION("total always undo") {
pp.enableClingoPropagatorUndo(ClingoPropagatorUndo_t::Always);
expectedUndos = 1;
}
libclasp.solve();
libclasp.ctx.master()->undoUntil(0);
REQUIRE(prop.checks == 1u);
REQUIRE(prop.totals == 1u);
REQUIRE(prop.undos == expectedUndos);
}
SECTION("with mode fixpoint check is called once on total") {
pp.enableClingoPropagatorCheck(ClingoPropagatorCheck_t::Fixpoint);
Expand Down