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 | |
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')
-rw-r--r-- | src/options/bv_options | 3 | ||||
-rw-r--r-- | src/smt/dump.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 32 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies_template.h | 44 | ||||
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 123 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 11 | ||||
-rw-r--r-- | src/theory/bv/kinds | 12 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 73 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 35 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 26 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 1 |
15 files changed, 373 insertions, 12 deletions
diff --git a/src/options/bv_options b/src/options/bv_options index 4a7cbd139..035d6ae31 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -45,6 +45,9 @@ expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1 option bitvectorToBool --bv-to-bool bool :default false :read-write lift bit-vectors of size 1 to booleans when possible +option boolToBitvector --bool-to-bv bool :default false :read-write + convert booleans to bit-vectors of size 1 when possible + option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-write always return -1 on division by zero diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index b1222a51e..ce146da0e 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -59,6 +59,8 @@ void DumpC::setDumpFromString(const std::string& optarg) { } else if(!strcmp(p, "boolean-terms")) { } else if(!strcmp(p, "constrain-subtypes")) { } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "bv-to-bool")) { + } else if(!strcmp(p, "bool-to-bv")) { } else if(!strcmp(p, "strings-pp")) { } else if(!strcmp(p, "skolem-quant")) { } else if(!strcmp(p, "simplify")) { @@ -163,9 +165,9 @@ assertions\n\ + Output the assertions after preprocessing and before clausification.\n\ Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ - simplify static-learning ite-removal repeat-simplify\n\ - rewrite-apply-to-const theory-preprocessing.\n\ + boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\ + strings-pp skolem-quant simplify static-learning ite-removal\n\ + repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\ PASS can also be the special value \"everything\", in which case the\n\ assertions are printed before any preprocessing (with\n\ \"assertions:pre-everything\") or after all preprocessing completes\n\ 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; diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h index 48221aad4..3a9106984 100644 --- a/src/theory/bv/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast_strategies_template.h @@ -740,6 +740,50 @@ void DefaultAshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { } template <class T> +void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULTBV); + std::vector<T> a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // construct bitwise comparison + res.push_back(uLessThanBB(a, b, false)); +} + +template <class T> +void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SLTBV); + std::vector<T> a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // construct bitwise comparison + res.push_back(sLessThanBB(a, b, false)); +} + +template <class T> +void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ITE); + std::vector<T> cond, thenpart, elsepart; + bb->bbTerm(node[0], cond); + bb->bbTerm(node[1], thenpart); + bb->bbTerm(node[2], elsepart); + + Assert(cond.size() == 1); + Assert(thenpart.size() == elsepart.size()); + + for (unsigned i = 0; i < thenpart.size(); ++i) { + // (~cond OR thenpart) AND (cond OR elsepart) + res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i]))); + } +} + +template <class T> void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { Assert (node.getKind() == kind::BITVECTOR_EXTRACT); Assert(bits.size() == 0); diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 0a7d165a2..aa5ae9c16 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -404,6 +404,9 @@ template <class T> void TBitblaster<T>::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB<T>; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB<T>; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ULTBV ] = DefaultUltbvBB<T>; + d_termBBStrategies [ kind::BITVECTOR_SLTBV ] = DefaultSltbvBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ITE ] = DefaultIteBB<T>; d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB<T>; d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB<T>; d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB<T>; diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index b38352b77..5b7fe160c 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -226,7 +226,6 @@ Node BvToBoolPreprocessor::liftNode(TNode current) { return result; } - void BvToBoolPreprocessor::liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { for (unsigned i = 0; i < assertions.size(); ++i) { Node new_assertion = liftNode(assertions[i]); @@ -239,14 +238,136 @@ BvToBoolPreprocessor::Statistics::Statistics() : d_numTermsLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsLifted", 0) , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0) , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0) + , d_numTermsLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsLowered", 0) + , d_numAtomsLowered("theory::bv::BvToBoolPreprocess::NumberOfAtomsLowered", 0) + , d_numTermsForcedLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLowered", 0) { smtStatisticsRegistry()->registerStat(&d_numTermsLifted); smtStatisticsRegistry()->registerStat(&d_numAtomsLifted); smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted); + smtStatisticsRegistry()->registerStat(&d_numTermsLowered); + smtStatisticsRegistry()->registerStat(&d_numAtomsLowered); + smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); } BvToBoolPreprocessor::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted); smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted); smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted); + smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); + smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered); + smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); +} + +void BvToBoolPreprocessor::addToLowerCache(TNode term, Node new_term) { + Assert (new_term != Node()); + Assert (!hasLowerCache(term)); + d_lowerCache[term] = new_term; +} + +Node BvToBoolPreprocessor::getLowerCache(TNode term) const { + Assert(hasLowerCache(term)); + return d_lowerCache.find(term)->second; +} + +bool BvToBoolPreprocessor::hasLowerCache(TNode term) const { + return d_lowerCache.find(term) != d_lowerCache.end(); +} + +Node BvToBoolPreprocessor::lowerNode(TNode current, bool topLevel) { + Node result; + if (hasLowerCache(current)) { + result = getLowerCache(current); + } else { + if (current.getNumChildren() == 0) { + if (current.getKind() == kind::CONST_BOOLEAN) { + result = (current == utils::mkTrue()) ? d_one : d_zero; + } else { + result = current; + } + } else { + Kind kind = current.getKind(); + Kind new_kind = kind; + switch(kind) { + case kind::EQUAL: + new_kind = kind::BITVECTOR_COMP; + break; + case kind::AND: + new_kind = kind::BITVECTOR_AND; + break; + case kind::OR: + new_kind = kind::BITVECTOR_OR; + break; + case kind::NOT: + new_kind = kind::BITVECTOR_NOT; + break; + case kind::XOR: + new_kind = kind::BITVECTOR_XOR; + break; + case kind::ITE: + if (current.getType().isBitVector() || current.getType().isBoolean()) { + new_kind = kind::BITVECTOR_ITE; + } + break; + case kind::BITVECTOR_ULT: + new_kind = kind::BITVECTOR_ULTBV; + break; + case kind::BITVECTOR_SLT: + new_kind = kind::BITVECTOR_SLTBV; + break; + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_UGT: + case kind::BITVECTOR_UGE: + case kind::BITVECTOR_SLE: + case kind::BITVECTOR_SGT: + case kind::BITVECTOR_SGE: + // Should have been removed by rewriting. + Unreachable(); + default: + break; + } + NodeBuilder<> builder(new_kind); + if (kind != new_kind) { + ++(d_statistics.d_numTermsLowered); + } + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + Node converted; + if (new_kind == kind::ITE) { + // Special-case ITE because need condition to be Boolean. + converted = lowerNode(current[0], true); + builder << converted; + converted = lowerNode(current[1]); + builder << converted; + converted = lowerNode(current[2]); + builder << converted; + } else { + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + converted = lowerNode(current[i]); + builder << converted; + } + } + result = builder; + } + if (result.getType().isBoolean()) { + ++(d_statistics.d_numTermsForcedLowered); + result = utils::mkNode(kind::ITE, result, d_one, d_zero); + } + addToLowerCache(current, result); + } + if (topLevel) { + result = utils::mkNode(kind::EQUAL, result, d_one); + } + Assert (result != Node()); + Debug("bool-to-bv") << "BvToBoolPreprocessor::lowerNode " << current << " => \n" << result << "\n"; + return result; +} + +void BvToBoolPreprocessor::lowerBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { + for (unsigned i = 0; i < assertions.size(); ++i) { + Node new_assertion = lowerNode(assertions[i], true); + new_assertions.push_back(new_assertion); + Trace("bool-to-bv") << " " << assertions[i] <<" => " << new_assertions[i] <<"\n"; + } } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 25d67b98e..7e351c9c6 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -34,6 +34,9 @@ class BvToBoolPreprocessor { IntStat d_numTermsLifted; IntStat d_numAtomsLifted; IntStat d_numTermsForcedLifted; + IntStat d_numTermsLowered; + IntStat d_numAtomsLowered; + IntStat d_numTermsForcedLowered; Statistics(); ~Statistics(); }; @@ -57,9 +60,17 @@ class BvToBoolPreprocessor { Node convertBvTerm(TNode node); Node liftNode(TNode current); Statistics d_statistics; + + NodeNodeMap d_lowerCache; + void addToLowerCache(TNode term, Node new_term); + Node getLowerCache(TNode term) const; + bool hasLowerCache(TNode term) const; + Node lowerNode(TNode current, bool topLevel = false); + public: BvToBoolPreprocessor(); void liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + void lowerBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); }; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 0ab33379f..da2833ca0 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -61,6 +61,7 @@ operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)" operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)" operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)" + operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)" operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)" operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)" @@ -70,6 +71,10 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)" operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_ULTBV 2 "bit-vector unsigned less than but returns bv of size 1 instead of boolean" +operator BITVECTOR_SLTBV 2 "bit-vector signed less than but returns bv of size 1 instead of boolean" +operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean" + operator BITVECTOR_REDOR 1 "bit-vector redor" operator BITVECTOR_REDAND 1 "bit-vector redand" @@ -145,8 +150,6 @@ typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompTypeRule - typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -174,6 +177,11 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_ULTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_SLTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule + typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index aaa3c561d..5957c641d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -88,6 +88,7 @@ enum RewriteRuleId { EvalLshr, EvalAshr, EvalUlt, + EvalUltBv, EvalUle, EvalExtract, EvalSignExtend, @@ -95,7 +96,10 @@ enum RewriteRuleId { EvalRotateRight, EvalNeg, EvalSlt, + EvalSltBv, EvalSle, + EvalITEBv, + EvalComp, /// simplification rules /// all of these rules decrease formula size @@ -222,6 +226,9 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalUle : out << "EvalUle"; return out; case EvalSlt : out << "EvalSlt"; return out; case EvalSle : out << "EvalSle"; return out; + case EvalSltBv: out << "EvalSltBv"; return out; + case EvalITEBv: out << "EvalITEBv"; return out; + case EvalComp: out << "EvalComp"; return out; case EvalExtract : out << "EvalExtract"; return out; case EvalSignExtend : out << "EvalSignExtend"; return out; case EvalRotateLeft : out << "EvalRotateLeft"; return out; diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index a7e50974c..3605a6970 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -295,6 +295,24 @@ Node RewriteRule<EvalUlt>::apply(TNode node) { } template<> inline +bool RewriteRule<EvalUltBv>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULTBV && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule<EvalUltBv>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<EvalUltBv>(" << node << ")" << std::endl; + BitVector a = node[0].getConst<BitVector>(); + BitVector b = node[1].getConst<BitVector>(); + + if (a.unsignedLessThan(b)) { + return utils::mkConst(1,1); + } + return utils::mkConst(1, 0); +} + +template<> inline bool RewriteRule<EvalSlt>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT && utils::isBVGroundTerm(node)); @@ -314,6 +332,45 @@ Node RewriteRule<EvalSlt>::apply(TNode node) { } template<> inline +bool RewriteRule<EvalSltBv>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_SLTBV && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule<EvalSltBv>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<EvalSltBv>(" << node << ")" << std::endl; + BitVector a = node[0].getConst<BitVector>(); + BitVector b = node[1].getConst<BitVector>(); + + if (a.signedLessThan(b)) { + return utils::mkConst(1, 1); + } + return utils::mkConst(1, 0); + +} + +template<> inline +bool RewriteRule<EvalITEBv>::applies(TNode node) { + Debug("bv-rewrite") << "RewriteRule<EvalITEBv>::applies(" << node << ")" << std::endl; + return (node.getKind() == kind::BITVECTOR_ITE && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule<EvalITEBv>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<EvalITEBv>(" << node << ")" << std::endl; + BitVector cond = node[0].getConst<BitVector>(); + + if (node[0] == utils::mkConst(1, 1)) { + return node[1]; + } else { + Assert(node[0] == utils::mkConst(1, 0)); + return node[2]; + } +} + +template<> inline bool RewriteRule<EvalUle>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ULE && utils::isBVGroundTerm(node)); @@ -419,6 +476,22 @@ Node RewriteRule<EvalEquals>::apply(TNode node) { } +template<> inline +bool RewriteRule<EvalComp>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_COMP && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule<EvalComp>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl; + BitVector a = node[0].getConst<BitVector>(); + BitVector b = node[1].getConst<BitVector>(); + if (a == b) { + return utils::mkConst(1, 1); + } + return utils::mkConst(1, 0); +} } } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 4c6afa7b9..e40612ba6 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -77,6 +77,16 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) { return RewriteResponse(REWRITE_DONE, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteUltBv(TNode node, bool prerewrite) { + // reduce common subexpressions on both sides + Node resultNode = LinearRewriteStrategy + < RewriteRule<EvalUltBv> + >::apply(node); + + return RewriteResponse(REWRITE_DONE, resultNode); +} + + RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule < EvalSlt > @@ -92,6 +102,14 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteSltBv(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule < EvalSltBv > + >::apply(node); + + return RewriteResponse(REWRITE_DONE, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUle>, @@ -146,6 +164,14 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule < EvalITEBv > + >::apply(node); + + return RewriteResponse(REWRITE_DONE, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){ Node resultNode = node; @@ -303,10 +329,10 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy - < RewriteRule<CompEliminate> - >::apply(node); + < RewriteRule < EvalComp > + >::apply(node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { @@ -678,6 +704,9 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor; d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand; + d_rewriteTable [ kind::BITVECTOR_ULTBV ] = RewriteUltBv; + d_rewriteTable [ kind::BITVECTOR_SLTBV ] = RewriteSltBv; + d_rewriteTable [ kind::BITVECTOR_ITE ] = RewriteITEBv; d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 538754a4b..8c3a20661 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -41,13 +41,16 @@ class TheoryBVRewriter { static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false); static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSltBv(TNode node, bool prerewrite = false); static RewriteResponse RewriteUle(TNode node, bool prerewrite = false); static RewriteResponse RewriteSle(TNode node, bool prerewrite = false); static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false); static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false); static RewriteResponse RewriteUge(TNode node, bool prerewrite = false); static RewriteResponse RewriteSge(TNode node, bool prerewrite = false); + static RewriteResponse RewriteITEBv(TNode node, bool prerewrite = false); static RewriteResponse RewriteNot(TNode node, bool prerewrite = false); static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false); static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 3995aa74f..1c59ff8b1 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -58,7 +58,7 @@ class BitVectorBitOfTypeRule { } }; /* class BitVectorBitOfTypeRule */ -class BitVectorCompTypeRule { +class BitVectorBVPredTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -72,7 +72,29 @@ class BitVectorCompTypeRule { } return nodeManager->mkBitVectorType(1); } -}; /* class BitVectorCompTypeRule */ +}; /* class BitVectorBVPredTypeRule */ + +class BitVectorITETypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + Assert(n.getNumChildren() == 3); + TypeNode thenpart = n[1].getType(check); + if (check) { + TypeNode cond = n[0].getType(check); + if (cond != nodeManager->mkBitVectorType(1)) { + throw TypeCheckingExceptionPrivate( + n, "expecting condition to be bit-vector term size 1"); + } + TypeNode elsepart = n[2].getType(check); + if (thenpart != elsepart) { + throw TypeCheckingExceptionPrivate( + n, "expecting then and else parts to have same type"); + } + } + return thenpart; + } +}; /* class BitVectorITETypeRule */ class BitVectorFixedWidthTypeRule { public: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4054350aa..58f3e4f74 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1915,6 +1915,10 @@ void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<N d_bvToBoolPreprocessor.liftBvToBool(assertions, new_assertions); } +void TheoryEngine::ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { + d_bvToBoolPreprocessor.lowerBoolToBv(assertions, new_assertions); +} + bool TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; return bv_theory->applyAbstraction(assertions, new_assertions); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7ce8345f7..d8ddf7ffc 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -837,6 +837,7 @@ private: public: void staticInitializeBVOptions(const std::vector<Node>& assertions); void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + void ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); void mkAckermanizationAsssertions(std::vector<Node>& assertions); |