Clingo heuristic (#40)

* Rename ClaspConfig::Configurator::addPost().

* Since there is actually no reason to limit a Configurator to adding
  post propagators, rename Configurator::addPost() to the more general
  Configurator::applyConfig().

* Add support for clingo heuristic.

* Fix non-matching size types.

* Add support for clingo lock to ClingoHeuristic.

clasp/clasp_facade.h

@@ -69,12 +69,12 @@ namespace Clasp {
 //! Configuration object for configuring solving via the ClaspFacade.
 class ClaspConfig : public BasicSatConfig {
 public:
-	//! Interface for injecting user-provided post propagators.
+	//! Interface for injecting user-provided configurations.
 	class Configurator {
 	public:
 		virtual ~Configurator();
 		virtual void prepare(SharedContext&);
-		virtual bool addPost(Solver& s) = 0;
+		virtual bool applyConfig(Solver& s) = 0;
 		virtual void unfreeze(SharedContext&);
 	};
 	typedef BasicSatConfig UserConfig;

clasp/clingo.h

@@ -29,6 +29,7 @@
  */
 #include <potassco/clingo.h>
 #include <clasp/clasp_facade.h>
+#include <clasp/solver.h>
 namespace Clasp {
 
 /*!
@@ -80,7 +81,7 @@ class ClingoPropagatorInit : public ClaspConfig::Configurator {
 	// base class
 	virtual void prepare(SharedContext&);
 	//! Adds a ClingoPropagator adapting the propagator() to s.
-	virtual bool addPost(Solver& s);
+	virtual bool applyConfig(Solver& s);
 	virtual void unfreeze(SharedContext&);
 
 	// for clingo
@@ -212,6 +213,43 @@ class ClingoAssignment : public Potassco::AbstractAssignment {
 	const Solver* solver_;
 };
 
+class ClingoHeuristic : public DecisionHeuristic {
+public:
+	class Factory : public BasicSatConfig::HeuristicCreator {
+	public:
+		/*!
+		 * \param clingoHeuristic The heuristic that should be added to solvers.
+		 * \param lock An optional lock that should be applied during calls to AbstractHeuristic::decide().
+		 */
+		explicit Factory(Potassco::AbstractHeuristic& clingoHeuristic, ClingoPropagatorLock* lock = 0);
+		DecisionHeuristic* create(Heuristic_t::Type t, const HeuParams& p);
+	private:
+		Potassco::AbstractHeuristic* clingo_;
+		ClingoPropagatorLock*        lock_;
+	};
+
+	explicit ClingoHeuristic(Potassco::AbstractHeuristic& clingoHeuristic, DecisionHeuristic* claspHeuristic, ClingoPropagatorLock* lock);
+	virtual void startInit(const Solver& s);
+	virtual void endInit(Solver& s);
+	virtual void detach(Solver& s);
+	virtual void setConfig(const HeuParams& p);
+	virtual void updateVar(const Solver& s, Var v, uint32 n);
+	virtual void simplify(const Solver& s, LitVec::size_type st);
+	virtual void undoUntil(const Solver& s, LitVec::size_type st);
+	virtual void newConstraint(const Solver& s, const Literal* first, LitVec::size_type size, ConstraintType t);
+	virtual void updateReason(const Solver& s, const LitVec& lits, Literal resolveLit);
+	virtual bool bump(const Solver& s, const WeightLitVec& lits, double adj);
+	virtual Literal doSelect(Solver& s);
+	virtual Literal selectRange(Solver& s, const Literal* first, const Literal* last);
+
+	DecisionHeuristic* fallback() const;
+private:
+	typedef SingleOwnerPtr<DecisionHeuristic> HeuPtr;
+	Potassco::AbstractHeuristic* clingo_;
+	HeuPtr                       clasp_;
+	ClingoPropagatorLock*        lock_;
+};
+
 ///@}
 }
 #endif

clasp/solver_strategies.h

@@ -528,7 +528,6 @@ class UserConfiguration : public Configuration {
 //! Simple factory for decision heuristics.
 struct Heuristic_t {
 	enum Type { Default = 0, Berkmin = 1, Vsids = 2, Vmtf = 3, Domain = 4, Unit = 5, None = 6, User = 7  };
-	typedef DecisionHeuristic* (*Creator)(Type t, const HeuParams& p);
 	static inline bool        isLookback(uint32 type) { return type >= (uint32)Berkmin && type < (uint32)Unit; }
 	//! Default callback for creating decision heuristics.
 	static DecisionHeuristic* create(Type t, const HeuParams& p);
@@ -542,7 +541,11 @@ typedef ProjectMode_t::Mode ProjectMode;
 //! Basic configuration for one or more SAT solvers.
 class BasicSatConfig : public UserConfiguration, public ContextParams {
 public:
-	typedef Heuristic_t::Creator HeuristicCreator;
+	struct HeuristicCreator {
+		virtual ~HeuristicCreator();
+		virtual DecisionHeuristic* create(Heuristic_t::Type t, const HeuParams& p) = 0;
+	};
+
 	BasicSatConfig();
 	void               prepare(SharedContext&);
 	const CtxOpts&     context()            const { return *this; }
@@ -556,14 +559,14 @@ class BasicSatConfig : public UserConfiguration, public ContextParams {
 
 	virtual void       reset();
 	virtual void       resize(uint32 numSolver, uint32 numSearch);
-	//! Sets callback function for creating heuristics.
-	void               setHeuristicCreator(HeuristicCreator hc);
+	void               setHeuristicCreator(HeuristicCreator* hc, Ownership_t::Type = Ownership_t::Acquire);
 private:
 	typedef PodVector<SolverOpts>::type SolverVec;
 	typedef PodVector<SearchOpts>::type SearchVec;
-	SolverVec solver_;
-	SearchVec search_;
-	HeuristicCreator heu_;
+	typedef SingleOwnerPtr<HeuristicCreator> HeuFactory;
+	SolverVec  solver_;
+	SearchVec  search_;
+	HeuFactory heu_;
 };
 
 //! Base class for solving related events.

src/clasp_facade.cpp

@@ -51,11 +51,11 @@ struct ClaspConfig::Impl {
 			if (own == Ownership_t::Acquire) { store_set_bit(cfg, AcquireBit); }
 			assert(ptr() == c);
 		}
-		bool addPost(Solver& s) {
+		bool applyConfig(Solver& s) {
 			POTASSCO_ASSERT(s.id() < 64, "invalid solver id!");
 			if (test_bit(set, s.id()))  { return true;  }
 			if (test_bit(cfg, OnceBit)) { store_set_bit(set, s.id()); }
-			return this->ptr()->addPost(s);
+			return this->ptr()->applyConfig(s);
 		}
 		void prepare(SharedContext& ctx) {
 			if (ctx.concurrency() < 64) {
@@ -125,7 +125,7 @@ bool ClaspConfig::Impl::addPost(Solver& s, const SolverParams& opts) {
 	}
 	for (PPVec::iterator it = pp.begin(), end = pp.end(); it != end; ++it) {
 		// protect call to user code
-		LOCKED() { if (!it->addPost(s)) { return false; } }
+		LOCKED() { if (!it->applyConfig(s)) { return false; } }
 	}
 	return true;
 #undef LOCKED

src/clingo.cpp

@@ -354,7 +354,7 @@ ClingoPropagatorInit::ClingoPropagatorInit(Potassco::AbstractPropagator& cb, Cli
 }
 ClingoPropagatorInit::~ClingoPropagatorInit()       { delete history_; }
 void ClingoPropagatorInit::prepare(SharedContext&)  {}
-bool ClingoPropagatorInit::addPost(Solver& s)       { return s.addPost(new ClingoPropagator(this)); }
+bool ClingoPropagatorInit::applyConfig(Solver& s)   { return s.addPost(new ClingoPropagator(this)); }
 void ClingoPropagatorInit::unfreeze(SharedContext&) {
 	if (history_) {
 		for (ChangeList::const_iterator it = changes_.begin(), end = changes_.end(); it != end; ++it) {
@@ -416,4 +416,50 @@ void ClingoPropagatorInit::enableHistory(bool b) {
 	else if (!history_) { history_ = new History(); }
 }
 
+/////////////////////////////////////////////////////////////////////////////////////////
+// ClingoHeuristic
+/////////////////////////////////////////////////////////////////////////////////////////
+ClingoHeuristic::ClingoHeuristic(Potassco::AbstractHeuristic& clingoHeuristic, DecisionHeuristic* claspHeuristic, ClingoPropagatorLock* lock)
+	: clingo_(&clingoHeuristic)
+	, clasp_(claspHeuristic)
+	, lock_(lock) {}
+
+Literal ClingoHeuristic::doSelect(Solver& s) {
+	typedef Scoped<Potassco::AbstractHeuristic, ClingoPropagatorLock, &ClingoPropagatorLock::lock, &ClingoPropagatorLock::unlock, Nop> ScopedLock;
+	Literal fallback = clasp_->doSelect(s);
+	if (s.hasConflict())
+		return fallback;
+
+	ClingoAssignment assignment(s);
+	Potassco::Lit_t lit = ScopedLock(lock_, clingo_)->decide(s.id(), assignment, encodeLit(fallback));
+	Literal decision = lit != 0 ? decodeLit(lit) : fallback;
+	return s.validVar(decision.var()) && !s.isFalse(decision) ? decision : fallback;
+}
+
+void ClingoHeuristic::startInit(const Solver& s)    { clasp_->startInit(s); }
+void ClingoHeuristic::endInit(Solver& s)            { clasp_->endInit(s); }
+void ClingoHeuristic::detach(Solver& s)             { if (clasp_.is_owner()) { clasp_->detach(s); } }
+void ClingoHeuristic::setConfig(const HeuParams& p) { clasp_->setConfig(p); }
+void ClingoHeuristic::newConstraint(const Solver& s, const Literal* p, LitVec::size_type sz, ConstraintType t) {
+	clasp_->newConstraint(s, p, sz, t);
+}
+
+void ClingoHeuristic::updateVar(const Solver& s, Var v, uint32 n)                   { clasp_->updateVar(s, v, n); }
+void ClingoHeuristic::simplify(const Solver& s, LitVec::size_type st)               { clasp_->simplify(s, st); }
+void ClingoHeuristic::undoUntil(const Solver& s, LitVec::size_type st)              { clasp_->undoUntil(s, st); }
+void ClingoHeuristic::updateReason(const Solver& s, const LitVec& x, Literal r)     { clasp_->updateReason(s, x, r); }
+bool ClingoHeuristic::bump(const Solver& s, const WeightLitVec& w, double d)        { return clasp_->bump(s, w, d); }
+Literal ClingoHeuristic::selectRange(Solver& s, const Literal* f, const Literal* l) { return clasp_->selectRange(s, f, l); }
+
+
+DecisionHeuristic* ClingoHeuristic::fallback() const { return clasp_.get();  }
+
+ClingoHeuristic::Factory::Factory(Potassco::AbstractHeuristic& clingoHeuristic, ClingoPropagatorLock* lock)
+	: clingo_(&clingoHeuristic)
+	, lock_(lock) {}
+
+DecisionHeuristic* ClingoHeuristic::Factory::create(Heuristic_t::Type t, const HeuParams& p) {
+	return new ClingoHeuristic(*clingo_, Heuristic_t::create(t, p), lock_);
+}
+
 }

src/lookahead.cpp

@@ -363,15 +363,11 @@ class Restricted : public UnitHeuristic {
 	typedef ConstraintType    con_t;
 	Restricted(DecisionHeuristic* other)
 		: UnitHeuristic()
-		, other_(other) {
+		, other_(other)
+		, disabled_(false) {
 	}
 	Literal doSelect(Solver& s) {
-		Lookahead* look = static_cast<Lookahead*>(s.getPost(Lookahead::priority_reserved_look));
-		if (look && !look->hasLimit()) { look = 0; }
-		Literal x = look ? look->heuristic(s) : lit_true();
-		if (x == lit_true()) { x = other_->doSelect(s); }
-		if (!look)          { s.setHeuristic(other_.release(), Ownership_t::Acquire); }
-		return x;
+		return !disabled_ ? heuristic(s) : other_->doSelect(s);
 	}
 	// heuristic interface - forward to other
 	void startInit(const Solver& s)           { other_->startInit(s); }
@@ -386,8 +382,27 @@ class Restricted : public UnitHeuristic {
 	void updateVar(const Solver& s, Var v, uint32 n)                          { other_->updateVar(s, v, n); }
 	Literal selectRange(Solver& s, const Literal* f, const Literal* l)        { return other_->selectRange(s, f, l); }
 private:
+	void disable(Solver& s) {
+		disabled_ = true;
+		if (s.heuristic() == this)
+			s.setHeuristic(other_.release(), Ownership_t::Acquire);
+	}
+	Literal heuristic(Solver& s) {
+		Literal choice;
+		Lookahead* look = static_cast<Lookahead*>(s.getPost(Lookahead::priority_reserved_look));
+		if (!look || !look->hasLimit()) {
+			choice = other_->doSelect(s);
+			disable(s);
+		}
+		else {
+			Literal p = look->heuristic(s);
+			choice = p != lit_true() ? p : other_->doSelect(s);
+		}
+		return choice;
+	}
 	typedef SingleOwnerPtr<DecisionHeuristic> HeuPtr;
 	HeuPtr other_;
+	bool   disabled_;
 };
 
 UnitHeuristic* UnitHeuristic::restricted(DecisionHeuristic* other) {

src/solver_strategies.cpp

@@ -245,10 +245,12 @@ bool UserConfiguration::addPost(Solver& s) const {
 	}
 	return ok;
 }
+
+BasicSatConfig::HeuristicCreator::~HeuristicCreator() {}
+
 BasicSatConfig::BasicSatConfig() {
 	solver_.push_back(SolverParams());
 	search_.push_back(SolveParams());
-	heu_ = 0;
 }
 void BasicSatConfig::prepare(SharedContext& ctx) {
 	uint32 warn = 0;
@@ -268,8 +270,8 @@ DecisionHeuristic* BasicSatConfig::heuristic(uint32 i)  const {
 	if (hId == Heuristic_t::Default && p.search == SolverStrategies::use_learning) hId = Heuristic_t::Berkmin;
 	POTASSCO_REQUIRE(p.search == SolverStrategies::use_learning || !Heuristic_t::isLookback(hId), "Selected heuristic requires lookback!");
 	DecisionHeuristic* h = 0;
-	if (heu_) { h = heu_(hId, p.heuristic); }
-	if (!h)   { h = Heuristic_t::create(hId, p.heuristic); }
+	if (heu_.get()) { h = heu_->create(hId, p.heuristic); }
+	if (!h) { h = Heuristic_t::create(hId, p.heuristic); }
 	if (Lookahead::isType(p.lookType) && p.lookOps > 0 && hId != Heuristic_t::Unit) {
 		h = UnitHeuristic::restricted(h);
 	}
@@ -296,8 +298,8 @@ void BasicSatConfig::resize(uint32 solver, uint32 search) {
 	solver_.resize(solver);
 	search_.resize(search);
 }
-void BasicSatConfig::setHeuristicCreator(HeuristicCreator hc) {
-	heu_ = hc;
+void BasicSatConfig::setHeuristicCreator(HeuristicCreator* hc, Ownership_t::Type owner) {
+	HeuFactory(hc, owner).swap(heu_);
 }
 /////////////////////////////////////////////////////////////////////////////////////////
 // Heuristics