diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2017-03-06 00:25:26 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.stanford.edu> | 2017-03-06 00:25:26 -0800 |
commit | 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 (patch) | |
tree | f7897714f42c89eac1547039de37fa25a730537a /src/smt/smt_engine.cpp | |
parent | f81c51ca8af1c38126336f0c31a33fba72614dc1 (diff) |
Adding support for bool-to-bv
Squashed commit of the following:
commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Mar 6 00:16:16 2017 -0800
Remove IFF case
commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date: Mon Feb 20 12:37:06 2017 -0800
proof support for bvcomp
commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 21:09:04 2017 -0800
Added missing cases to operator<< for bv rewrite rules.
commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 11:43:51 2017 -0800
Added rewrite rules for new bitvector kinds.
commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Feb 13 14:41:49 2017 -0800
First draft of bool-to-bv pass.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b94e08fad..2aaf43569 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -602,6 +602,9 @@ private: // Lift bit-vectors of size 1 to booleans void bvToBool(); + // Convert booleans to bit-vectors of size 1 + void boolToBv(); + // Abstract common structure over small domains to UF // return true if changes were made. void bvAbstraction(); @@ -1371,10 +1374,18 @@ void SmtEngine::setDefaults() { if(options::bitvectorToBool.wasSetByUser()) { throw OptionException("bv-to-bool not supported with unsat cores"); } - Notice() << "SmtEngine: turning off bitvector-to-bool support unsat-cores" << endl; + Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat-cores" << endl; options::bitvectorToBool.set(false); } + if(options::boolToBitvector()) { + if(options::boolToBitvector.wasSetByUser()) { + throw OptionException("bool-to-bv not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat-cores" << endl; + options::boolToBitvector.set(false); + } + if(options::bvIntroducePow2()) { if(options::bvIntroducePow2.wasSetByUser()) { throw OptionException("bv-intro-pow2 not supported with unsat cores"); @@ -3016,6 +3027,16 @@ void SmtEnginePrivate::bvToBool() { } } +void SmtEnginePrivate::boolToBv() { + Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << endl; + spendResource(options::preprocessStep()); + std::vector<Node> new_assertions; + d_smt.d_theoryEngine->ppBoolToBv(d_assertions.ref(), new_assertions); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, Rewriter::rewrite(new_assertions[i])); + } +} + bool SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); @@ -3927,6 +3948,14 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } + // Convert non-top-level Booleans to bit-vectors of size 1 + if(options::boolToBitvector()) { + dumpAssertions("pre-bool-to-bv", d_assertions); + Chat() << "...doing boolToBv..." << endl; + boolToBv(); + dumpAssertions("post-bool-to-bv", d_assertions); + Trace("smt") << "POST boolToBv" << endl; + } if(options::sepPreSkolemEmp()) { for (unsigned i = 0; i < d_assertions.size(); ++ i) { Node prev = d_assertions[i]; @@ -3938,6 +3967,7 @@ void SmtEnginePrivate::processAssertions() { } } } + if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; |