diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 12:17:46 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 12:17:46 +0100 |
| commit | 52514cada7c0c7c4fff69c85e0bd735abfdc03fd (patch) | |
| tree | 401b5ab2efae7a0d3971d07d01ff61b0ab18fbcd /src/theory/quantifiers_engine.h | |
| parent | 0e761324a33a993ae9a268bc2d2ed46f7e86b42d (diff) | |
Remove two obsolete versions of MBQI.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f56cd0d19..199fe79b9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -256,7 +256,7 @@ public: /** do substitution */ Node getSubstitute( Node n, std::vector< Node >& terms ); /** exist instantiation ? */ - bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); + //bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true ); /** add require phase */ |