From: lianah Date: Sun, 15 Jun 2014 20:10:32 +0000 (-0400) Subject: fixed fuzzer assertion failures for bv X-Git-Tag: cvc5-1.0.0~6807 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a7cdebd56cc8c2ffe600e3f4fc85007c29de03e;p=cvc5.git fixed fuzzer assertion failures for bv --- diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 0b65ea0db..750e67a2d 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -40,16 +40,18 @@ SubstitutionEx::SubstitutionEx(theory::SubstitutionMap* modelMap) , d_modelMap(modelMap) {} -void SubstitutionEx::addSubstitution(TNode from, TNode to, TNode reason) { +bool SubstitutionEx::addSubstitution(TNode from, TNode to, TNode reason) { Debug("bv-substitution") << "SubstitutionEx::addSubstitution: "<< from <<" => "<< to <<"\n"; Debug("bv-substitution") << " reason "<addSubstitution(from, to); d_cacheInvalid = true; - Assert (from != to); - Assert (d_substitutions.find(from) == d_substitutions.end()); d_substitutions[from] = SubstitutionElement(to, reason); + return true; } Node SubstitutionEx::apply(TNode node) { @@ -446,12 +448,12 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { if (left.isVar() && !right.hasSubterm(left)) { - subst.addSubstitution(left, right, reason); - return true; + bool changed = subst.addSubstitution(left, right, reason); + return changed; } if (right.isVar() && !left.hasSubterm(right)) { - subst.addSubstitution(right, left, reason); - return true; + bool changed = subst.addSubstitution(right, left, reason); + return changed; } // xor simplification @@ -478,8 +480,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { Node new_left = left_children.size() > 1 ? utils::mkNode(kind::BITVECTOR_XOR, left_children) : left_children[0]; Node new_fact = utils::mkNode(kind::EQUAL, new_left, new_right); - subst.addSubstitution(fact, new_fact, reason); - return true; + bool changed = subst.addSubstitution(fact, new_fact, reason); + return changed; } NodeBuilder<> nb(kind::BITVECTOR_XOR); @@ -488,7 +490,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { } Node inverse = left.getNumChildren() == 2? (Node)left[1] : (Node)nb; Node new_right = utils::mkNode(kind::BITVECTOR_XOR, right, inverse); - subst.addSubstitution(var, new_right, reason); + bool changed = subst.addSubstitution(var, new_right, reason); if (Dump.isOn("bv-algebraic")) { Node query = utils::mkNot(utils::mkNode(kind::IFF, fact, utils::mkNode(kind::EQUAL, var, new_right))); @@ -500,7 +502,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { } - return true; + return changed; } // (a xor t = a) <=> (t = 0) @@ -511,8 +513,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { Node new_left = utils::mkNode(kind::BITVECTOR_XOR, var, left); Node zero = utils::mkConst(utils::getSize(var), 0u); Node new_fact = utils::mkNode(kind::EQUAL, zero, new_left); - subst.addSubstitution(fact, new_fact, reason); - return true; + bool changed = subst.addSubstitution(fact, new_fact, reason); + return changed; } if (right.getKind() == kind::BITVECTOR_XOR && @@ -522,8 +524,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { Node new_right = utils::mkNode(kind::BITVECTOR_XOR, var, right); Node zero = utils::mkConst(utils::getSize(var), 0u); Node new_fact = utils::mkNode(kind::EQUAL, zero, new_right); - subst.addSubstitution(fact, new_fact, reason); - return true; + bool changed = subst.addSubstitution(fact, new_fact, reason); + return changed; } // (a xor b = 0) <=> (a = b) @@ -532,8 +534,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { right.getKind() == kind::CONST_BITVECTOR && right.getConst() == BitVector(utils::getSize(left), 0u)) { Node new_fact = utils::mkNode(kind::EQUAL, left[0], left[1]); - subst.addSubstitution(fact, new_fact, reason); - return true; + bool changed = subst.addSubstitution(fact, new_fact, reason); + return changed; } diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 4acab29b3..a39631696 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -77,7 +77,16 @@ class SubstitutionEx { public: SubstitutionEx(theory::SubstitutionMap* modelMap); - void addSubstitution(TNode from, TNode to, TNode reason); + /** + * Returnst true if the substitution map did not contain from. + * + * @param from + * @param to + * @param reason + * + * @return + */ + bool addSubstitution(TNode from, TNode to, TNode reason); Node apply(TNode node); Node explain(TNode node) const; }; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 5cff67005..3e6e02952 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1166,7 +1166,8 @@ bool RewriteRule::applies(TNode node) { node.getKind() != kind::BITVECTOR_XOR) || utils::getSize(node) == 1) return false; - + // find the first constant and return true if it's not only 1..1 or only 0..0 + // (there could be more than one constant) for (unsigned i = 0; i < node.getNumChildren(); ++i) { if (node[i].getKind() == kind::CONST_BITVECTOR) { BitVector constant = node[i].getConst(); @@ -1178,6 +1179,7 @@ bool RewriteRule::applies(TNode node) { if (!constant.isBitSet(i)) return true; } + return false; } } return false; @@ -1187,13 +1189,12 @@ template<> inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; // get the constant - bool found_constant CVC4_UNUSED = false ; + bool found_constant = false ; TNode constant; std::vector other_children; for (unsigned i = 0; i < node.getNumChildren(); ++i) { - if (node[i].getKind() == kind::CONST_BITVECTOR) { + if (node[i].getKind() == kind::CONST_BITVECTOR && !found_constant) { constant = node[i]; - Assert (!found_constant); found_constant = true; } else { other_children.push_back(node[i]);