summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/signatures/th_bv_bitblast.plf23
-rw-r--r--src/options/bv_options3
-rw-r--r--src/smt/dump.cpp8
-rw-r--r--src/smt/smt_engine.cpp32
-rw-r--r--src/theory/bv/bitblast_strategies_template.h44
-rw-r--r--src/theory/bv/bitblaster_template.h3
-rw-r--r--src/theory/bv/bv_to_bool.cpp123
-rw-r--r--src/theory/bv/bv_to_bool.h11
-rw-r--r--src/theory/bv/kinds12
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h7
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h73
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp35
-rw-r--r--src/theory/bv/theory_bv_rewriter.h3
-rw-r--r--src/theory/bv/theory_bv_type_rules.h26
-rw-r--r--src/theory/theory_engine.cpp4
-rw-r--r--src/theory/theory_engine.h1
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<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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback