Add option for stopping optimization at given bound.

* Add option '--opt-stop' for stopping optimization once a model M with
  cost(M) less or equal to the given bound is found.

clasp/cli/clasp_cli_options.inl

@@ -601,6 +601,9 @@ OPTION(opt_mode   , "", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(MinimizeMode_t
        "      <bound> : Set initial bound for objective function(s)", \
        FUN(arg) { MinimizeMode_t::Mode m = MinimizeMode_t::optimize; SumVec B; return (arg >> m >> opt(B)) && SET(SELF.optMode, m) && (SELF.optBound.swap(B), true); }, \
        GET_FUN(str) { str << SELF.optMode; if (!SELF.optBound.empty()) str << SELF.optBound; })
+OPTION(opt_stop, "", ARG(arg("<bound>...")), "Stop optimization on model with cost <= <bound> \n",
+       FUN(arg)     { SumVec B; return ITE(arg.peek() != '0' && arg.off(), true, arg >> B) && (SELF.optStop = B, true); },
+       GET_FUN(str) { ITE(SELF.optStop.empty(), str << off, str << SELF.optStop); })
 GROUP_END(SELF)
 #undef CLASP_SOLVE_OPTIONS
 #undef SELF

clasp/enumerator.h

@@ -92,6 +92,7 @@ struct EnumOptions {
 	ProjMode proMode;   /*!< Projection mode to use.      */
 	uint32   project;   /*!< Options for projection.      */
 	SumVec   optBound;  /*!< Initial bound for optimize statements. */
+	SumVec   optStop;   /*!< Optional stop bound for optimization. */
 };
 const char* modelType(const Model& m);
 

clasp/solve_algorithms.h

@@ -150,6 +150,7 @@ class SolveAlgorithm {
 	void setEnumerator(Enumerator& e);
 	void setEnumLimit(uint64 m)          { enumLimit_= m;  }
 	void setLimits(const SolveLimits& x) { limits_   = x;  }
+	void setOptLimit(const SumVec& bound);
 	//! If set to false, SharedContext::report() is not called for models.
 	/*!
 	 * \note The default is true, i.e. models are reported via SharedContext::report().
@@ -240,13 +241,16 @@ class SolveAlgorithm {
 	enum { value_stop = value_false|value_true };
 	bool attach(SharedContext& ctx, ModelHandler* onModel);
 	void detach();
+	bool hasLimit(const Model& m) const;
+	bool reportModel(Solver& s, bool sym) const;
 	SolveLimits    limits_;
 	SharedContext* ctx_;
 	EnumPtr        enum_;
 	ModelHandler*  onModel_;
 	PathPtr        path_;
 	CorePtr        core_;
 	uint64         enumLimit_;
+	SumVec         optLimit_;
 	double         time_;
 	int            last_;
 	bool           reportM_;

src/clasp_facade.cpp

@@ -470,7 +470,7 @@ struct ClaspFacade::SolveData {
 	~SolveData() { reset(); }
 	void init(SolveAlgorithm* algo, Enumerator* en);
 	void reset();
-	void prepareEnum(SharedContext& ctx, int64 numM, EnumOptions::OptMode opt, EnumMode mode, ProjectMode prj);
+	void prepareEnum(SharedContext& ctx, EnumMode mode, const EnumOptions& options);
 	bool interrupt(int sig) {
 		if (solving()) { return active->interrupt(sig); }
 		if (!qSig && sig != SolveStrategy::SIGCANCEL) { qSig = sig; }
@@ -522,18 +522,20 @@ void ClaspFacade::SolveData::reset() {
 	if (en.get())   { en->reset(); }
 	prepared = solved = false;
 }
-void ClaspFacade::SolveData::prepareEnum(SharedContext& ctx, int64 numM, EnumOptions::OptMode opt, EnumMode mode, ProjectMode proj) {
+void ClaspFacade::SolveData::prepareEnum(SharedContext& ctx, EnumMode mode, const EnumOptions& options) {
 	POTASSCO_REQUIRE(!active, "Solve operation still active");
 	if (ctx.ok() && !ctx.frozen() && !prepared) {
 		if (mode == enum_volatile && ctx.solveMode() == SharedContext::solve_multi) {
 			ctx.requestStepVar();
 		}
-		ctx.output.setProjectMode(proj);
-		int lim = en->init(ctx, opt, (int)Range<int64>(-1, INT_MAX).clamp(numM));
-		if (lim == 0 || numM < 0) {
+		ctx.output.setProjectMode(options.proMode);
+		int64 numM = options.numModels;
+		int lim = en->init(ctx, options.optMode, (int)Range<int64>(-1, INT_MAX).clamp(numM));
+		if (lim == 0 || options.numModels < 0) {
 			numM = lim;
 		}
 		algo->setEnumLimit(numM ? static_cast<uint64>(numM) : UINT64_MAX);
+		algo->setOptLimit(options.optStop);
 		prepared = true;
 	}
 }
@@ -979,7 +981,7 @@ void ClaspFacade::prepare(EnumMode enumMode) {
 	EnumOptions& en = config_->solve;
 	if (solved()) {
 		doUpdate(0, false, SIG_DFL);
-		solve_->prepareEnum(ctx, en.numModels, en.optMode, enumMode, en.proMode);
+		solve_->prepareEnum(ctx, enumMode, en);
 		ctx.endInit();
 	}
 	if (prepared()) { return; }
@@ -1003,7 +1005,7 @@ void ClaspFacade::prepare(EnumMode enumMode) {
 		ctx.setPreserveHeuristic(true);
 	}
 	POTASSCO_REQUIRE(!ctx.ok() || !ctx.frozen());
-	solve_->prepareEnum(ctx, en.numModels, en.optMode, enumMode, en.proMode);
+	solve_->prepareEnum(ctx, enumMode, en);
 	if      (!solve_->keepPrg) { builder_ = 0; }
 	else if (isAsp())          { static_cast<Asp::LogicProgram*>(builder_.get())->dispose(false); }
 	if (!builder_.get() && !ctx.heuristic.empty()) {

src/solve_algorithms.cpp

@@ -254,6 +254,23 @@ void SolveAlgorithm::setEnumerator(Enumerator& e) {
 	enum_.reset(&e);
 	enum_.release();
 }
+void SolveAlgorithm::setOptLimit(const SumVec& bound) {
+	optLimit_ = bound;
+}
+bool SolveAlgorithm::hasLimit(const Model& m) const {
+	if (!enum_->tentative() && m.num >= enumLimit_) return true;
+	if (enum_->optimize() && m.costs && !optLimit_.empty()) {
+		for (std::size_t i = 0, end = std::min(optLimit_.size(), m.costs->size()); i != end; ++i) {
+			if (optLimit_[i] != (*m.costs)[i]) {
+				return (*m.costs)[i] < optLimit_[i];
+			}
+		}
+		return true;
+	}
+	return false;
+}
+
+
 const Model& SolveAlgorithm::model() const {
 	return enum_->lastModel();
 }
@@ -347,10 +364,7 @@ bool SolveAlgorithm::next() {
 		last_ = doNext(last_);
 	}
 	if (last_ == value_true) {
-		Solver& s = *ctx_->solver(model().sId);
-		if (onModel_ && !onModel_->onModel(s, model()))       { last_ = value_stop; }
-		if (reportM_ && !ctx_->report(s, model()))            { last_ = value_stop; }
-		if (!enum_->tentative() && model().num >= enumLimit_) { last_ = value_stop; }
+		if (!reportModel(*ctx_->solver(model().sId), false)) { last_ = value_stop; }
 		return true;
 	}
 	else {
@@ -367,14 +381,18 @@ void SolveAlgorithm::stop() {
 		detach();
 	}
 }
-bool SolveAlgorithm::reportModel(Solver& s) const {
-	for (const Model& m = enum_->lastModel();;) {
+bool SolveAlgorithm::reportModel(Solver& s, bool sym) const {
+	for (const Model& m = model();;) {
 		bool r1 = !onModel_ || onModel_->onModel(s, m);
 		bool r2 = !reportM_ || s.sharedContext()->report(s, m);
-		bool res= r1 && r2 && (enumLimit_ > m.num || enum_->tentative());
-		if (!res || (res = !interrupted()) == false || !enum_->commitSymmetric(s)) { return res; }
+		if (!r1 || !r2 || hasLimit(m) || interrupted()) { return false; }
+		if (!sym || !enum_->commitSymmetric(s))         { return true;  }
 	}
 }
+
+bool SolveAlgorithm::reportModel(Solver& s) const {
+	return reportModel(s, true);
+}
 bool SolveAlgorithm::reportUnsat(Solver& s) const {
 	const Model&  m = enum_->lastModel();
 	EventHandler* h = s.sharedContext()->eventHandler();

tests/cli_test.cpp

@@ -614,6 +614,32 @@ TEST_CASE("Cli options", "[cli]") {
 		REQUIRE(b.avg == uint32(MovingAvg::Type::avg_sma));
 	}
 
+	SECTION("test opt-stop option")	{
+		SumVec exp;
+		REQUIRE(config.getValue("solve.opt_stop") == "no");
+		REQUIRE(config.solve.optStop.empty());
+
+		REQUIRE(config.setValue("solve.opt_stop", "10,17"));
+		REQUIRE(config.getValue("solve.opt_stop") == "10,17");
+		exp.push_back(10);
+		exp.push_back(17);
+		REQUIRE(config.solve.optStop == exp);
+
+		REQUIRE(config.setValue("solve.opt_stop", "-4"));
+		REQUIRE(config.getValue("solve.opt_stop") == "-4");
+		exp.assign(1, -4);
+		REQUIRE(config.solve.optStop == exp);
+
+		REQUIRE(config.setValue("solve.opt_stop", "off"));
+		REQUIRE(config.getValue("solve.opt_stop") == "no");
+		REQUIRE(config.solve.optStop.empty());
+
+		REQUIRE(config.setValue("solve.opt_stop", "0"));
+		REQUIRE(config.getValue("solve.opt_stop") == "0");
+		exp.assign(1, 0);
+		REQUIRE(config.solve.optStop == exp);
+	}
+
 	SECTION("test get values") {
 		std::string out;
 		REQUIRE(config.getValue(config.getKey(ClaspCliConfig::KEY_TESTER, "configuration"), out) == -1);