clingo: Add support for propagator undo mode. (#87)

* clingo: Add support for propagator undo mode.

* Add support for new clingo propagator undo mode "Always". If set,
  AbstractPropagator::undo() is called for all decision levels L on
  which AbstractPropagator::check() was called even if no watched
  literal was assigned on L.

* NOTE: For now, undo mode "Always" does not distinguish "Total" from
  "Fixpoint" checks.

* clingo: Add "enableClingoPropagatorUndo" function.

* Replace default argument "undoMode" of enableClingoPropagatorCheck()
  with separate function.

clasp/clingo.h

@@ -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.
@@ -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.
@@ -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).
@@ -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:
@@ -137,6 +158,7 @@ class ClingoPropagatorInit : public ClaspConfig::Configurator {
 	ChangeList changes_;
 	uint32     step_;
 	CheckType  check_;
+	UndoType   undo_;
 };
 
 //! Adaptor for a Potassco::AbstractPropagator.

src/clingo.cpp

@@ -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);
@@ -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)); }
@@ -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(); }

tests/facade_test.cpp

@@ -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;
@@ -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;
@@ -2194,6 +2194,7 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") {
 			int checks;
 			int props;
 			int totals;
+			int undos;
 			bool fire;
 		} prop;
 		MyInit pp(prop);
@@ -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();
@@ -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);