dflat/clasp-3.1.4-facade.patch at master · bbliem/dflat · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
--- libclasp/clasp/clasp_facade.h	2015-12-10 13:14:58.000000000 +0100
+++ libclasp/clasp/clasp_facade.h	2016-05-27 11:31:22.392488115 +0200
@@ -220,7 +220,7 @@
 	/*!
 	 * \pre solving() is false and program updates are enabled.
 	 */
-	ProgramBuilder&    update(bool updateConfig = false);
+	ProgramBuilder&    update(bool updateConfig = false, bool updateProgram = true);
 	//@}

 	//! Solves the current problem.
@@ -334,6 +334,7 @@
 	bool prepared()    const;
 	bool interrupted() const;
 	bool solved()      const;
+	const LitVec& assumptions() const { return assume_; }

 	ExpectedQuantity   getStat(const char* path)const;
 	const char*        getKeys(const char* path)const;
--- libclasp/src/clasp_facade.cpp	2015-12-10 13:14:58.000000000 +0100
+++ libclasp/src/clasp_facade.cpp	2016-05-27 11:31:22.419155456 +0200
@@ -375,7 +375,7 @@
 	return lpStats_.get() != 0; // currently only ASP supports program updates
 }

-ProgramBuilder& ClaspFacade::update(bool reloadConfig) {
+ProgramBuilder& ClaspFacade::update(bool reloadConfig, bool updateProgram) {
 	CLASP_ASSERT_CONTRACT(config_ && program() && !solving());
 	CLASP_ASSERT_CONTRACT_MSG(step_.result.signal != SIGINT, "Interrupt not handled!");
 	if (reloadConfig) {
@@ -384,7 +384,7 @@
 	if (solved()) {
 		startStep(step() + 1);
 	}
-	if (builder_->frozen()) {
+	if (builder_->frozen() && updateProgram) {
 		assume_.clear();
 		builder_->updateProgram();
 	}