diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-30 14:06:27 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-30 14:06:34 -0500 |
| commit | 2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df (patch) | |
| tree | 6c72c3145cef49e76b1f8e5577947d441e14f938 /src/smt | |
| parent | f7c6707fa38a850d6798c747b3c45ef10769fa7c (diff) | |
Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 98ed9c4fd..784d82228 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -552,6 +552,11 @@ class SmtEnginePrivate : public NodeManagerListener { */ unsigned d_simplifyAssertionsDepth; + /** whether certain preprocess steps are necessary */ + bool d_needsExpandDefs; + bool d_needsRewriteBoolTerms; + bool d_needsConstrainSubTypes; + public: /** * Map from skolem variables to index in d_assertions containing @@ -679,6 +684,9 @@ public: d_abstractValueMap(&d_fakeContext), d_abstractValues(), d_simplifyAssertionsDepth(0), + d_needsExpandDefs(true), + d_needsRewriteBoolTerms(true), + d_needsConstrainSubTypes(true), //TODO d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_pbsProcessor(smt.d_userContext), @@ -3860,6 +3868,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + dumpAssertions("pre-constrain-subtypes", d_assertions); { // Any variables of subtype types need to be constrained properly. @@ -4194,6 +4203,7 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; dumpAssertions("post-everything", d_assertions); + //set instantiation level of everything to zero if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ |