Skip to content

Commit

Permalink
Issue #64: Add additional runtime checks.
Browse files Browse the repository at this point in the history
* Check for unsupported updates in ClaspFacade::update() and
  ClaspFacade::prepare(). The former requires real multi-shot mode,
  while the latter requires at least multi-solve mode. Throw
  std::logic_error if these requirements are not met.
  • Loading branch information
BenKaufmann committed Feb 21, 2021
1 parent 6d73ccd commit 2984c30
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/clasp_facade.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -972,6 +972,7 @@ bool ClaspFacade::read() {

void ClaspFacade::prepare(EnumMode enumMode) {
POTASSCO_REQUIRE(solve_.get() && !solving());
POTASSCO_REQUIRE(!solved() || ctx.solveMode() == SharedContext::solve_multi);
EnumOptions& en = config_->solve;
if (solved()) {
doUpdate(0, false, SIG_DFL);
Expand Down Expand Up @@ -1020,7 +1021,8 @@ ClaspFacade::Result ClaspFacade::solve(const LitVec& a, EventHandler* handler) {
}

ProgramBuilder& ClaspFacade::update(bool updateConfig, void (*sigAct)(int)) {
POTASSCO_REQUIRE(config_ && program() && !solving());
POTASSCO_REQUIRE(config_ && program() && !solving(), "Program updates not supported!");
POTASSCO_REQUIRE(!program()->frozen() || incremental(), "Program updates not supported!");
doUpdate(program(), updateConfig, sigAct);
return *program();
}
Expand Down
28 changes: 28 additions & 0 deletions tests/facade_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,34 @@ TEST_CASE("Facade", "[facade]") {
REQUIRE(!asp.frozen());
}

SECTION("testUpdateChecks") {
Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config);
lpAdd(asp, "a :- not b. b :- not a.");

SECTION("cannotSolveAgainInSingleSolveMode") {
REQUIRE(libclasp.solve().sat());
REQUIRE_THROWS_AS(libclasp.prepare(), std::logic_error);
REQUIRE_THROWS_AS(libclasp.solve(), std::logic_error);
}

SECTION("maySolveAgainInMultiSolveMode") {
libclasp.ctx.setSolveMode(Clasp::SharedContext::solve_multi);
REQUIRE(libclasp.solve().sat());
REQUIRE_NOTHROW(libclasp.prepare());
REQUIRE_FALSE(libclasp.solved());
REQUIRE(libclasp.solve().sat());
}

SECTION("cannotUpdateInSingleShotMode") {
Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config);
libclasp.keepProgram();
lpAdd(asp, "a :- not b. b :- not a.");
REQUIRE(libclasp.solve().sat());
REQUIRE_THROWS_AS(libclasp.update(), std::logic_error);
REQUIRE_THROWS_AS(libclasp.prepare(), std::logic_error);
}
}

SECTION("testPrepareTooStrongBound") {
config.solve.numModels = 0;
config.solve.optBound.assign(1, 0);
Expand Down

0 comments on commit 2984c30

Please sign in to comment.