diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-21 00:26:55 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-21 00:26:55 +0200 |
| commit | 1603631331714b79d1be9d8d3305ca60786981cf (patch) | |
| tree | e081c64ddb284f51f2c318916d55660dc91187ca /src/theory/quantifiers_engine.h | |
| parent | f342e03da57a73c2261ed2ca06c651cc4153df8a (diff) | |
Fix --inst-max-level for strategies that use arbitrary representative terms.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5315a1de8..e914280c5 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -237,6 +237,8 @@ public: int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); + /** is term eligble for instantiation? */ + bool isTermEligibleForInstantiation( Node n, Node f, bool print = false ); public: /** get number of quantifiers */ int getNumQuantifiers() { return (int)d_quants.size(); } |