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.h4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index eca108587..6afc4f925 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -265,8 +265,6 @@ public:
Node getInstantiatedConjunction(Node q);
/** get unsat core lemmas */
bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
- bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
- std::map<Node, Node>& weak_imp);
/** get explanation for instantiation lemmas */
void getExplanationForInstLemmas(const std::vector<Node>& lems,
std::map<Node, Node>& quant,
@@ -317,7 +315,7 @@ public:
~Statistics();
};/* class QuantifiersEngine::Statistics */
Statistics d_statistics;
-
+
private:
/** reference to theory engine object */
TheoryEngine* d_te;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback