From 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 8 Nov 2016 10:09:53 -0600 Subject: Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint. --- src/smt/smt_engine.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/smt/smt_engine.cpp') 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; -- cgit v1.2.3