From 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 6 Mar 2017 00:25:26 -0800 Subject: [PATCH] Adding support for bool-to-bv Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass. --- proofs/signatures/th_bv_bitblast.plf | 23 ++++ src/options/bv_options | 3 + src/smt/dump.cpp | 8 +- src/smt/smt_engine.cpp | 32 ++++- src/theory/bv/bitblast_strategies_template.h | 44 +++++++ src/theory/bv/bitblaster_template.h | 3 + src/theory/bv/bv_to_bool.cpp | 123 +++++++++++++++++- src/theory/bv/bv_to_bool.h | 11 ++ src/theory/bv/kinds | 12 +- src/theory/bv/theory_bv_rewrite_rules.h | 7 + ...ory_bv_rewrite_rules_constant_evaluation.h | 73 +++++++++++ src/theory/bv/theory_bv_rewriter.cpp | 35 ++++- src/theory/bv/theory_bv_rewriter.h | 3 + src/theory/bv/theory_bv_type_rules.h | 26 +++- src/theory/theory_engine.cpp | 4 + src/theory/theory_engine.h | 1 + 16 files changed, 396 insertions(+), 12 deletions(-) diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 3cc1ec296..2b2fe0868 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -533,6 +533,29 @@ (! c (^ (bblast_bvslt bx by n) f) (th_holds (iff (bvslt n x y) f)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVCOMP +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvcomp ((x bblt) (y bblt) (n mpz)) bblt + (match x ((bbltc bx x') (match y ((bbltc by y') + (bbltc (bblast_eq_rec x' y' (iff bx by)) bbltn)) + (default (fail bblt)))) + (default (fail bblt)) + )) + +(declare bv_bbl_bvcomp (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvcomp xb yb n) rb) + (bblast_term 1 (bvcomp n x y) rb))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; BITBLASTING CONNECTORS 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 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 @@ -739,6 +739,50 @@ void DefaultAshrBB (TNode node, std::vector& res, TBitblaster* bb) { } } +template +void DefaultUltbvBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULTBV); + std::vector 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 +void DefaultSltbvBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SLTBV); + std::vector 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 +void DefaultIteBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ITE); + std::vector 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 void DefaultExtractBB (TNode node, std::vector& bits, TBitblaster* bb) { Assert (node.getKind() == kind::BITVECTOR_EXTRACT); 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 void TBitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; + d_termBBStrategies [ kind::BITVECTOR_ULTBV ] = DefaultUltbvBB; + d_termBBStrategies [ kind::BITVECTOR_SLTBV ] = DefaultSltbvBB; + d_termBBStrategies [ kind::BITVECTOR_ITE ] = DefaultIteBB; d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB; d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB; d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB; 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& assertions, std::vector& 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& assertions, std::vector& 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& assertions, std::vector& new_assertions); + void lowerBoolToBv(const std::vector& assertions, std::vector& 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 @@ -294,6 +294,24 @@ Node RewriteRule::apply(TNode node) { return utils::mkFalse(); } +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULTBV && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BitVector a = node[0].getConst(); + BitVector b = node[1].getConst(); + + if (a.unsignedLessThan(b)) { + return utils::mkConst(1,1); + } + return utils::mkConst(1, 0); +} + template<> inline bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT && @@ -313,6 +331,45 @@ Node RewriteRule::apply(TNode node) { } +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_SLTBV && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BitVector a = node[0].getConst(); + BitVector b = node[1].getConst(); + + if (a.signedLessThan(b)) { + return utils::mkConst(1, 1); + } + return utils::mkConst(1, 0); + +} + +template<> inline +bool RewriteRule::applies(TNode node) { + Debug("bv-rewrite") << "RewriteRule::applies(" << node << ")" << std::endl; + return (node.getKind() == kind::BITVECTOR_ITE && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BitVector cond = node[0].getConst(); + + 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::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ULE && @@ -419,6 +476,22 @@ Node RewriteRule::apply(TNode node) { } +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_COMP && + utils::isBVGroundTerm(node)); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BitVector a = node[0].getConst(); + BitVector b = node[1].getConst(); + 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 + >::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, @@ -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 - >::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& assertions, std::vector& assertions, std::vector& new_assertions) { + d_bvToBoolPreprocessor.lowerBoolToBv(assertions, new_assertions); +} + bool TheoryEngine::ppBvAbstraction(const std::vector& assertions, std::vector& 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& assertions); void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); + void ppBoolToBv(const std::vector& assertions, std::vector& new_assertions); bool ppBvAbstraction(const std::vector& assertions, std::vector& new_assertions); void mkAckermanizationAsssertions(std::vector& assertions); -- 2.30.2