diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-08 10:09:53 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-08 10:10:08 -0600 |
commit | 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa (patch) | |
tree | 960adfe7c475b1d5c54dbb4c43b035ee6c740151 /src/smt/smt_engine.cpp | |
parent | 1f9f7a3bd665575fd25f0fe93547ee0564cc18c9 (diff) |
Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 46469fb0d..d726b836f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -102,6 +102,7 @@ #include "util/hash.h" #include "util/proof.h" #include "util/resource_manager.h" +#include "options/sep_options.h" using namespace std; using namespace CVC4; @@ -3963,6 +3964,17 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } + if(options::sepPreSkolemEmp()) { + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Node prev = d_assertions[i]; + Node next = sep::TheorySepRewriter::preprocess( prev ); + if( next!=prev ){ + d_assertions.replace( i, Rewriter::rewrite( next ) ); + Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl; + Trace("sep-preprocess") << " ...got " << d_assertions[i] << endl; + } + } + } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; |