summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h9
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bb38e5e4a..7405241b7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -39,11 +39,6 @@ namespace theory {
class QuantifiersEngine;
-namespace quantifiers {
- class TermDb;
- class TermDbSygus;
-}
-
class InstantiationNotify {
public:
InstantiationNotify(){}
@@ -53,6 +48,8 @@ public:
};
namespace quantifiers {
+ class TermDb;
+ class TermDbSygus;
class FirstOrderModel;
//modules
class InstantiationEngine;
@@ -343,6 +340,8 @@ public:
bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
/** is in conflict */
bool inConflict() { return d_conflict; }
+ /** set conflict */
+ void setConflict();
/** get number of waiting lemmas */
unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
/** get needs check */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback