summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r--src/prop/theory_proxy.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index ceb328d90..f3fe634e2 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -85,7 +85,7 @@ public:
void enqueueTheoryLiteral(const SatLiteral& l);
- SatLiteral getNextDecisionRequest();
+ SatLiteral getNextDecisionRequest(bool& stopSearch);
bool theoryNeedCheck() const;
@@ -112,6 +112,8 @@ public:
void checkTime();
+ bool isDecisionEngineDone();
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback