diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-09 18:38:12 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-02-09 18:38:12 -0800 |
| commit | a70490bc79933a55041f35d5896f79004e578f05 (patch) | |
| tree | 3b89ea09cf7c653b293b86dd7431132de4676fe5 /src/theory | |
| parent | 13af27ec180e73eecc846c99bd563f85577683ee (diff) | |
Remove mkNode from bv::utils (#1587)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/bv/abstraction.cpp | 265 | ||||
| -rw-r--r-- | src/theory/bv/bitblast_strategies_template.h | 226 | ||||
| -rw-r--r-- | src/theory/bv/bv_inequality_graph.cpp | 35 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 35 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 83 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 47 | ||||
| -rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 222 | ||||
| -rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 20 | ||||
| -rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 118 | ||||
| -rw-r--r-- | src/theory/bv/slicer.cpp | 65 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 256 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 823 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 293 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 260 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 27 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_utils.h | 24 |
16 files changed, 1637 insertions, 1162 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 4ef484594..a36ec2e16 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -2,9 +2,9 @@ /*! \file abstraction.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Guy Katz, Tim King + ** Liana Hadarean, Aina Niemetz, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -29,57 +29,74 @@ using namespace CVC4::context; using namespace std; using namespace CVC4::theory::bv::utils; -bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { +bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, + std::vector<Node>& new_assertions) +{ Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n"; TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime); - for (unsigned i = 0; i < assertions.size(); ++i) { - if (assertions[i].getKind() == kind::OR) { - for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { - if (!isConjunctionOfAtoms(assertions[i][j])) { + for (unsigned i = 0; i < assertions.size(); ++i) + { + if (assertions[i].getKind() == kind::OR) + { + for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) + { + if (!isConjunctionOfAtoms(assertions[i][j])) + { continue; } Node signature = computeSignature(assertions[i][j]); storeSignature(signature, assertions[i][j]); - Debug("bv-abstraction") << " assertion: " << assertions[i][j] <<"\n"; - Debug("bv-abstraction") << " signature: " << signature <<"\n"; + Debug("bv-abstraction") << " assertion: " << assertions[i][j] << "\n"; + Debug("bv-abstraction") << " signature: " << signature << "\n"; } } } finalizeSignatures(); - for (unsigned i = 0; i < assertions.size(); ++i) { - if (assertions[i].getKind() == kind::OR && - assertions[i][0].getKind() == kind::AND) { + for (unsigned i = 0; i < assertions.size(); ++i) + { + if (assertions[i].getKind() == kind::OR + && assertions[i][0].getKind() == kind::AND) + { std::vector<Node> new_children; - for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { - if (hasSignature(assertions[i][j])) { + for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) + { + if (hasSignature(assertions[i][j])) + { new_children.push_back(abstractSignatures(assertions[i][j])); - } else { + } + else + { new_children.push_back(assertions[i][j]); } } - new_assertions.push_back(utils::mkNode(kind::OR, new_children)); - } else { + new_assertions.push_back(utils::mkOr(new_children)); + } + else + { // assertions that are not changed new_assertions.push_back(assertions[i]); } } - if (options::skolemizeArguments()) { + if (options::skolemizeArguments()) + { skolemizeArguments(new_assertions); } - // if we are using the eager solver reverse the abstraction - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - if (d_funcToSignature.size() == 0) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + { + if (d_funcToSignature.size() == 0) + { // we did not change anything return false; } NodeNodeMap seen; - for (unsigned i = 0; i < new_assertions.size(); ++i) { + for (unsigned i = 0; i < new_assertions.size(); ++i) + { new_assertions[i] = reverseAbstraction(new_assertions[i], seen); } // we undo the abstraction functions so the logic is QF_BV still @@ -90,7 +107,6 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st return d_funcToSignature.size() != 0; } - bool AbstractionModule::isConjunctionOfAtoms(TNode node) { TNodeSet seen; return isConjunctionOfAtomsRec(node, seen); @@ -146,83 +162,98 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) { return res; } -void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) { - for (unsigned i = 0; i < assertions.size(); ++i) { +void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) +{ + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < assertions.size(); ++i) + { TNode assertion = assertions[i]; - if (assertion.getKind() != kind::OR) - continue; + if (assertion.getKind() != kind::OR) continue; bool is_skolemizable = true; - for (unsigned k = 0; k < assertion.getNumChildren(); ++k) { - if (assertion[k].getKind() != kind::EQUAL || - assertion[k][0].getKind() != kind::APPLY_UF || - assertion[k][1].getKind() != kind::CONST_BITVECTOR || - assertion[k][1].getConst<BitVector>() != BitVector(1, 1u)) { + for (unsigned k = 0; k < assertion.getNumChildren(); ++k) + { + if (assertion[k].getKind() != kind::EQUAL + || assertion[k][0].getKind() != kind::APPLY_UF + || assertion[k][1].getKind() != kind::CONST_BITVECTOR + || assertion[k][1].getConst<BitVector>() != BitVector(1, 1u)) + { is_skolemizable = false; break; } } - if (!is_skolemizable) - continue; + if (!is_skolemizable) continue; ArgsTable assertion_table; // collect function symbols and their arguments - for (unsigned j = 0; j < assertion.getNumChildren(); ++j) { + for (unsigned j = 0; j < assertion.getNumChildren(); ++j) + { TNode current = assertion[j]; - Assert (current.getKind() == kind::EQUAL && - current[0].getKind() == kind::APPLY_UF); + Assert(current.getKind() == kind::EQUAL + && current[0].getKind() == kind::APPLY_UF); TNode func = current[0]; ArgsVec args; - for (unsigned k = 0; k < func.getNumChildren(); ++k) { + for (unsigned k = 0; k < func.getNumChildren(); ++k) + { args.push_back(func[k]); } assertion_table.addEntry(func.getOperator(), args); } - NodeBuilder<> assertion_builder (kind::OR); + NodeBuilder<> assertion_builder(kind::OR); // construct skolemized assertion - for (ArgsTable::iterator it = assertion_table.begin(); it != assertion_table.end(); ++it) { + for (ArgsTable::iterator it = assertion_table.begin(); + it != assertion_table.end(); + ++it) + { // for each function symbol ++(d_statistics.d_numArgsSkolemized); TNode func = it->first; ArgsTableEntry& args = it->second; - NodeBuilder<> skolem_func (kind::APPLY_UF); + NodeBuilder<> skolem_func(kind::APPLY_UF); skolem_func << func; std::vector<Node> skolem_args; - for (unsigned j = 0; j < args.getArity(); ++j) { + for (unsigned j = 0; j < args.getArity(); ++j) + { bool all_same = true; - for (unsigned k = 1; k < args.getNumEntries(); ++k) { - if ( args.getEntry(k)[j] != args.getEntry(0)[j]) - all_same = false; + for (unsigned k = 1; k < args.getNumEntries(); ++k) + { + if (args.getEntry(k)[j] != args.getEntry(0)[j]) all_same = false; } - Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); + Node new_arg = all_same + ? (Node)args.getEntry(0)[j] + : utils::mkVar(utils::getSize(args.getEntry(0)[j])); skolem_args.push_back(new_arg); skolem_func << new_arg; } - - Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); + Node skolem_func_eq1 = + nm->mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); // enumerate arguments assignments std::vector<Node> or_assignments; - for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) { + for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) + { NodeBuilder<> arg_assignment(kind::AND); - ArgsVec& args = *it; - for (unsigned k = 0; k < args.size(); ++k) { - Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]); + ArgsVec& args = *it; + for (unsigned k = 0; k < args.size(); ++k) + { + Node eq = nm->mkNode(kind::EQUAL, args[k], skolem_args[k]); arg_assignment << eq; } or_assignments.push_back(arg_assignment); } - Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments)); + Node new_func_def = + utils::mkAnd(skolem_func_eq1, utils::mkOr(or_assignments)); assertion_builder << new_func_def; } Node new_assertion = assertion_builder; - Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n"; + Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " + << assertions[i] << " => \n"; Debug("bv-abstraction-dbg") << " " << new_assertion; assertions[i] = new_assertion; } @@ -243,22 +274,27 @@ Node AbstractionModule::computeSignature(TNode node) { return sig; } -Node AbstractionModule::getSignatureSkolem(TNode node) { - Assert (node.getKind() == kind::VARIABLE); +Node AbstractionModule::getSignatureSkolem(TNode node) +{ + Assert(node.getKind() == kind::VARIABLE); + NodeManager* nm = NodeManager::currentNM(); unsigned bitwidth = utils::getSize(node); - if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) { + if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) + { d_signatureSkolems[bitwidth] = vector<Node>(); } vector<Node>& skolems = d_signatureSkolems[bitwidth]; // get the index of bv variables of this size unsigned index = getBitwidthIndex(bitwidth); - Assert (skolems.size() + 1 >= index ); - if (skolems.size() == index) { + Assert(skolems.size() + 1 >= index); + if (skolems.size() == index) + { ostringstream os; - os << "sig_" <<bitwidth <<"_" << index; - NodeManager* nm = NodeManager::currentNM(); - skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures")); + os << "sig_" << bitwidth << "_" << index; + skolems.push_back(nm->mkSkolem(os.str(), + nm->mkBitVectorType(bitwidth), + "skolem for computing signatures")); } ++(d_signatureIndices[bitwidth]); return skolems[index]; @@ -392,70 +428,95 @@ void AbstractionModule::storeGeneralization(TNode s, TNode t) { d_sigToGeneralization[s] = t; } -void AbstractionModule::finalizeSignatures() { +void AbstractionModule::finalizeSignatures() +{ NodeManager* nm = NodeManager::currentNM(); - Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures num signatures = " << d_signatures.size() <<"\n"; + Debug("bv-abstraction") + << "AbstractionModule::finalizeSignatures num signatures = " + << d_signatures.size() << "\n"; TNodeSet new_signatures; // "unify" signatures - for (SignatureMap::const_iterator ss = d_signatures.begin(); ss != d_signatures.end(); ++ss) { - for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) { + for (SignatureMap::const_iterator ss = d_signatures.begin(); + ss != d_signatures.end(); + ++ss) + { + for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) + { TNode t = getGeneralization(tt->first); TNode s = getGeneralization(ss->first); - if (t != s) { + if (t != s) + { int status = comparePatterns(s, t); - Assert (status); - if (status < 0) - continue; - if (status == 1) { + Assert(status); + if (status < 0) continue; + if (status == 1) + { storeGeneralization(t, s); - } else { + } + else + { storeGeneralization(s, t); } } } } // keep only most general signatures - for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { + for (SignatureMap::iterator it = d_signatures.begin(); + it != d_signatures.end();) + { TNode sig = it->first; TNode gen = getGeneralization(sig); - if (sig != gen) { - Assert (d_signatures.find(gen) != d_signatures.end()); + if (sig != gen) + { + Assert(d_signatures.find(gen) != d_signatures.end()); // update the count - d_signatures[gen]+= d_signatures[sig]; + d_signatures[gen] += d_signatures[sig]; d_signatures.erase(it++); - } else { + } + else + { ++it; } } - // remove signatures that are not frequent enough - for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { - if (it->second <= 7) { + for (SignatureMap::iterator it = d_signatures.begin(); + it != d_signatures.end();) + { + if (it->second <= 7) + { d_signatures.erase(it++); - } else { + } + else + { ++it; } } - for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) { + for (SignatureMap::const_iterator it = d_signatures.begin(); + it != d_signatures.end(); + ++it) + { TNode signature = it->first; // we already processed this signature - Assert (d_signatureToFunc.find(signature) == d_signatureToFunc.end()); + Assert(d_signatureToFunc.find(signature) == d_signatureToFunc.end()); - Debug("bv-abstraction") << "Processing signature " << signature << " count " << it->second << "\n"; + Debug("bv-abstraction") << "Processing signature " << signature << " count " + << it->second << "\n"; std::vector<TypeNode> arg_types; TNodeSet seen; collectArgumentTypes(signature, arg_types, seen); - Assert (signature.getType().isBoolean()); + Assert(signature.getType().isBoolean()); // make function return a bitvector of size 1 - //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); - TypeNode range = NodeManager::currentNM()->mkBitVectorType(1); + // Node bv_function = nm->mkNode(kind::ITE, signature, utils::mkConst(1, + // 1u), utils::mkConst(1, 0u)); + TypeNode range = nm->mkBitVectorType(1); TypeNode abs_type = nm->mkFunctionType(arg_types, range); - Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); + Node abs_func = + nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; // NOTE: signature expression type is BOOLEAN @@ -465,7 +526,8 @@ void AbstractionModule::finalizeSignatures() { d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size()); - Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n"; + Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " + << d_signatureToFunc.size() << " signatures. \n"; } void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) { @@ -510,15 +572,18 @@ void AbstractionModule::collectArguments(TNode node, TNode signature, std::vecto } } - -Node AbstractionModule::abstractSignatures(TNode assertion) { - Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; +Node AbstractionModule::abstractSignatures(TNode assertion) +{ + Debug("bv-abstraction") << "AbstractionModule::abstractSignatures " + << assertion << "\n"; + NodeManager* nm = NodeManager::currentNM(); // assume the assertion has been fully abstracted Node signature = getGeneralizedSignature(assertion); - Debug("bv-abstraction") << " with sig "<< signature <<"\n"; + Debug("bv-abstraction") << " with sig " << signature << "\n"; NodeNodeMap::iterator it = d_signatureToFunc.find(signature); - if (it!= d_signatureToFunc.end()) { + if (it != d_signatureToFunc.end()) + { std::vector<Node> args; TNode func = it->second; // pushing the function symbol @@ -526,14 +591,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) { TNodeSet seen; collectArguments(assertion, signature, args, seen); std::vector<TNode> real_args; - for (unsigned i = 1; i < args.size(); ++i) { + for (unsigned i = 1; i < args.size(); ++i) + { real_args.push_back(args[i]); } d_argsTable.addEntry(func, real_args); - Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), - utils::mkConst(1, 1u)); - Debug("bv-abstraction") << "=> "<< result << "\n"; - Assert (result.getType() == assertion.getType()); + Node result = nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::APPLY_UF, args), utils::mkConst(1, 1u)); + Debug("bv-abstraction") << "=> " << result << "\n"; + Assert(result.getType() == assertion.getType()); return result; } return assertion; diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h index 7bfc1c5c5..60e7fc051 100644 --- a/src/theory/bv/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast_strategies_template.h @@ -2,9 +2,9 @@ /*! \file bitblast_strategies_template.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Clark Barrett + ** Liana Hadarean, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -518,64 +518,71 @@ void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T> } template <class T> -void DefaultUdivBB (TNode node, std::vector<T>& q, TBitblaster<T>* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); +void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); std::vector<T> r; - uDivModRec(a, b, q, r, utils::getSize(node)); + uDivModRec(a, b, q, r, utils::getSize(node)); // adding a special case for division by 0 - std::vector<T> iszero; - for (unsigned i = 0; i < b.size(); ++i) { - iszero.push_back(mkIff(b[i], mkFalse<T>())); + std::vector<T> iszero; + for (unsigned i = 0; i < b.size(); ++i) + { + iszero.push_back(mkIff(b[i], mkFalse<T>())); } - T b_is_0 = mkAnd(iszero); - - for (unsigned i = 0; i < q.size(); ++i) { - q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 - r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a + T b_is_0 = mkAnd(iszero); + + for (unsigned i = 0; i < q.size(); ++i) + { + q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 + r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a } // cache the remainder in case we need it later - Node remainder = Rewriter::rewrite( - utils::mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); + Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); bb->storeBBTerm(remainder, r); } template <class T> -void DefaultUremBB (TNode node, std::vector<T>& rem, TBitblaster<T>* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); +void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); std::vector<T> q; - uDivModRec(a, b, q, rem, utils::getSize(node)); + uDivModRec(a, b, q, rem, utils::getSize(node)); // adding a special case for division by 0 - std::vector<T> iszero; - for (unsigned i = 0; i < b.size(); ++i) { - iszero.push_back(mkIff(b[i], mkFalse<T>())); + std::vector<T> iszero; + for (unsigned i = 0; i < b.size(); ++i) + { + iszero.push_back(mkIff(b[i], mkFalse<T>())); } - T b_is_0 = mkAnd(iszero); - - for (unsigned i = 0; i < q.size(); ++i) { - q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 - rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a + T b_is_0 = mkAnd(iszero); + + for (unsigned i = 0; i < q.size(); ++i) + { + q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 + rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a } // cache the quotient in case we need it later - Node quotient = Rewriter::rewrite( - utils::mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); + Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); bb->storeBBTerm(quotient, q); } - template <class T> void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { Debug("bitvector") << "theory::bv:: Unimplemented kind " @@ -596,10 +603,11 @@ void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { } template <class T> -void DefaultShlBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n"; - Assert (node.getKind() == kind::BITVECTOR_SHL && - res.size() == 0); +void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); @@ -608,47 +616,56 @@ void DefaultShlBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { unsigned size = utils::getSize(node); unsigned log2_size = std::ceil(log2((double)size)); Node a_size = utils::mkConst(size, size); - Node b_ult_a_size_node = - Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size)); + Node b_ult_a_size_node = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); // ensure that the inequality is bit-blasted - bb->bbAtom(b_ult_a_size_node); + bb->bbAtom(b_ult_a_size_node); T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); std::vector<T> prev_res; - res = a; + res = a; // we only need to look at the bits bellow log2_a_size - for(unsigned s = 0; s < log2_size; ++s) { + for (unsigned s = 0; s < log2_size; ++s) + { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched - prev_res = res; - unsigned threshold = pow(2, s); - for(unsigned i = 0; i < a.size(); ++i) { - if (i < threshold) { + prev_res = res; + unsigned threshold = pow(2, s); + for (unsigned i = 0; i < a.size(); ++i) + { + if (i < threshold) + { // if b[s] is true then we must have shifted by at least 2^b bits so - // all bits bellow 2^s will be 0, otherwise just use previous shift value + // all bits bellow 2^s will be 0, otherwise just use previous shift + // value res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); - } else { + } + else + { // if b[s]= 0, use previous value, otherwise shift by threshold bits - Assert(i >= threshold); - res[i] = mkIte(b[s], prev_res[i-threshold], prev_res[i]); + Assert(i >= threshold); + res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]); } } } prev_res = res; - for (unsigned i = 0; i < b.size(); ++i) { + for (unsigned i = 0; i < b.size(); ++i) + { // this is fine because b_ult_a_size has been bit-blasted - res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); + res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); } - - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + + if (Debug.isOn("bitvector-bb")) + { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } template <class T> -void DefaultLshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n"; - Assert (node.getKind() == kind::BITVECTOR_LSHR && - res.size() == 0); +void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); @@ -657,49 +674,56 @@ void DefaultLshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { unsigned size = utils::getSize(node); unsigned log2_size = std::ceil(log2((double)size)); Node a_size = utils::mkConst(size, size); - Node b_ult_a_size_node = - Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size)); + Node b_ult_a_size_node = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); // ensure that the inequality is bit-blasted - bb->bbAtom(b_ult_a_size_node); - T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); + bb->bbAtom(b_ult_a_size_node); + T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); res = a; std::vector<T> prev_res; - - for(unsigned s = 0; s < log2_size; ++s) { + + for (unsigned s = 0; s < log2_size; ++s) + { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched - prev_res = res; - int threshold = pow(2, s); - for(unsigned i = 0; i < a.size(); ++i) { - if (i + threshold >= a.size()) { + prev_res = res; + int threshold = pow(2, s); + for (unsigned i = 0; i < a.size(); ++i) + { + if (i + threshold >= a.size()) + { // if b[s] is true then we must have shifted by at least 2^b bits so // all bits above 2^s will be 0, otherwise just use previous shift value res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); - } else { + } + else + { // if b[s]= 0, use previous value, otherwise shift by threshold bits - Assert (i+ threshold < a.size()); - res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i+threshold]); + Assert(i + threshold < a.size()); + res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); } } } - + prev_res = res; - for (unsigned i = 0; i < b.size(); ++i) { + for (unsigned i = 0; i < b.size(); ++i) + { // this is fine because b_ult_a_size has been bit-blasted - res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); + res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); } - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + if (Debug.isOn("bitvector-bb")) + { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } template <class T> -void DefaultAshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { - - Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n"; - Assert (node.getKind() == kind::BITVECTOR_ASHR && - res.size() == 0); +void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); @@ -708,42 +732,50 @@ void DefaultAshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { unsigned size = utils::getSize(node); unsigned log2_size = std::ceil(log2((double)size)); Node a_size = utils::mkConst(size, size); - Node b_ult_a_size_node = - Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size)); + Node b_ult_a_size_node = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); // ensure that the inequality is bit-blasted - bb->bbAtom(b_ult_a_size_node); + bb->bbAtom(b_ult_a_size_node); T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); - + res = a; T sign_bit = a.back(); std::vector<T> prev_res; - for(unsigned s = 0; s < log2_size; ++s) { + for (unsigned s = 0; s < log2_size; ++s) + { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched - prev_res = res; - int threshold = pow(2, s); - for(unsigned i = 0; i < a.size(); ++i) { - if (i + threshold >= a.size()) { + prev_res = res; + int threshold = pow(2, s); + for (unsigned i = 0; i < a.size(); ++i) + { + if (i + threshold >= a.size()) + { // if b[s] is true then we must have shifted by at least 2^b bits so - // all bits above 2^s will be the sign bit, otherwise just use previous shift value + // all bits above 2^s will be the sign bit, otherwise just use previous + // shift value res[i] = mkIte(b[s], sign_bit, prev_res[i]); - } else { + } + else + { // if b[s]= 0, use previous value, otherwise shift by threshold bits - Assert (i+ threshold < a.size()); - res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i+threshold]); + Assert(i + threshold < a.size()); + res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); } } } prev_res = res; - for (unsigned i = 0; i < b.size(); ++i) { + for (unsigned i = 0; i < b.size(); ++i) + { // this is fine because b_ult_a_size has been bit-blasted - res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit); + res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit); } - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + if (Debug.isOn("bitvector-bb")) + { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index d0b299d3b..12d415cad 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -2,9 +2,9 @@ /*! \file bv_inequality_graph.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Morgan Deters + ** Liana Hadarean, Aina Niemetz, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -415,15 +415,17 @@ void InequalityGraph::backtrack() { } } -Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) { - Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); +Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) +{ + Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); + NodeManager* nm = NodeManager::currentNM(); TNode a = diseq[0][0]; TNode b = diseq[0][1]; - Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b); - Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); - Node eq = diseq[0]; - Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq); - return lemma; + Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b); + Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a); + Node eq = diseq[0]; + Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq); + return lemma; } void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) { @@ -460,14 +462,19 @@ BitVector InequalityGraph::getValueInModel(TNode node) const { return getValue(id); } -void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) { - for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { +void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) +{ + NodeManager* nm = NodeManager::currentNM(); + for (ModelValues::const_iterator it = d_modelValues.begin(); + it != d_modelValues.end(); + ++it) + { TermId id = (*it).first; BitVector value = (*it).second.value; TNode var = getTermNode(id); Node constant = utils::mkConst(value); - Node assignment = utils::mkNode(kind::EQUAL, var, constant); - assignments.push_back(assignment); - Debug("bitvector-model") << " " << var <<" => " << constant << "\n"; + Node assignment = nm->mkNode(kind::EQUAL, var, constant); + assignments.push_back(assignment); + Debug("bitvector-model") << " " << var << " => " << constant << "\n"; } } diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index a6e3153cb..ef5844e1f 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -2,9 +2,9 @@ /*! \file bv_subtheory_algebraic.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Morgan Deters + ** Liana Hadarean, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -244,6 +244,7 @@ bool AlgebraicSolver::check(Theory::Effort e) { uint64_t original_bb_cost = 0; + NodeManager* nm = NodeManager::currentNM(); NodeSet seen_assertions; // Processing assertions from scratch for (AssertionQueue::const_iterator it = assertionsBegin(); it != assertionsEnd(); ++it) { @@ -296,7 +297,7 @@ bool AlgebraicSolver::check(Theory::Effort e) { if (Dump.isOn("bv-algebraic")) { Node expl = d_explanations[id]; - Node query = utils::mkNot(utils::mkNode(kind::IMPLIES, expl, fact)); + Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact)); Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(query.toExpr()); @@ -457,10 +458,10 @@ void AlgebraicSolver::setConflict(TNode conflict) { bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { if (fact.getKind() != kind::EQUAL) return false; + NodeManager* nm = NodeManager::currentNM(); TNode left = fact[0]; TNode right = fact[1]; - if (left.isVar() && !right.hasSubterm(left)) { bool changed = subst.addSubstitution(left, right, reason); return changed; @@ -485,15 +486,13 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { right_children.push_back(right[i]); } Assert (right_children.size()); - Node new_right = right_children.size() > 1 ? utils::mkNode(kind::BITVECTOR_XOR, right_children) - : right_children[0]; + Node new_right = utils::mkNaryNode(kind::BITVECTOR_XOR, right_children); std::vector<Node> left_children; for (unsigned i = 1; i < left.getNumChildren(); ++i) { left_children.push_back(left[i]); } - 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); + Node new_left = utils::mkNaryNode(kind::BITVECTOR_XOR, left_children); + Node new_fact = nm->mkNode(kind::EQUAL, new_left, new_right); bool changed = subst.addSubstitution(fact, new_fact, reason); return changed; } @@ -503,11 +502,12 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { nb << left[i]; } Node inverse = left.getNumChildren() == 2? (Node)left[1] : (Node)nb; - Node new_right = utils::mkNode(kind::BITVECTOR_XOR, right, inverse); + Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse); bool changed = subst.addSubstitution(var, new_right, reason); if (Dump.isOn("bv-algebraic")) { - Node query = utils::mkNot(utils::mkNode(kind::EQUAL, fact, utils::mkNode(kind::EQUAL, var, new_right))); + Node query = utils::mkNot(nm->mkNode( + kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right))); Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(query.toExpr()); @@ -524,9 +524,9 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { right.getMetaKind() == kind::metakind::VARIABLE && left.hasSubterm(right)) { TNode var = right; - Node new_left = utils::mkNode(kind::BITVECTOR_XOR, var, left); + Node new_left = nm->mkNode(kind::BITVECTOR_XOR, var, left); Node zero = utils::mkConst(utils::getSize(var), 0u); - Node new_fact = utils::mkNode(kind::EQUAL, zero, new_left); + Node new_fact = nm->mkNode(kind::EQUAL, zero, new_left); bool changed = subst.addSubstitution(fact, new_fact, reason); return changed; } @@ -535,9 +535,9 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { left.getMetaKind() == kind::metakind::VARIABLE && right.hasSubterm(left)) { TNode var = left; - Node new_right = utils::mkNode(kind::BITVECTOR_XOR, var, right); + Node new_right = nm->mkNode(kind::BITVECTOR_XOR, var, right); Node zero = utils::mkConst(utils::getSize(var), 0u); - Node new_fact = utils::mkNode(kind::EQUAL, zero, new_right); + Node new_fact = nm->mkNode(kind::EQUAL, zero, new_right); bool changed = subst.addSubstitution(fact, new_fact, reason); return changed; } @@ -547,7 +547,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { left.getNumChildren() == 2 && right.getKind() == kind::CONST_BITVECTOR && right.getConst<BitVector>() == BitVector(utils::getSize(left), 0u)) { - Node new_fact = utils::mkNode(kind::EQUAL, left[0], left[1]); + Node new_fact = nm->mkNode(kind::EQUAL, left[0], left[1]); bool changed = subst.addSubstitution(fact, new_fact, reason); return changed; } @@ -564,6 +564,7 @@ bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) { } void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) { + NodeManager* nm = NodeManager::currentNM(); bool changed = true; while(changed) { // d_bv->spendResource(); @@ -613,7 +614,7 @@ void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, } for (unsigned j = 0; j < left.getNumChildren(); ++j) { - Node eq_j = utils::mkNode(kind::EQUAL, left[j], right[j]); + Node eq_j = nm->mkNode(kind::EQUAL, left[j], right[j]); unsigned id = d_explanations.size(); TNode expl = d_explanations[current_id]; storeExplanation(expl); diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 8ef2b471f..1c59ae2d4 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -2,9 +2,9 @@ /*! \file bv_subtheory_core.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Tim King + ** Liana Hadarean, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -211,19 +211,24 @@ bool CoreSolver::check(Theory::Effort e) { return true; } -void CoreSolver::buildModel() { +void CoreSolver::buildModel() +{ Debug("bv-core") << "CoreSolver::buildModel() \n"; + NodeManager* nm = NodeManager::currentNM(); d_modelValues.clear(); TNodeSet constants; TNodeSet constants_in_eq_engine; // collect constants in equality engine eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); - while (!eqcs_i.isFinished()) { + while (!eqcs_i.isFinished()) + { TNode repr = *eqcs_i; - if (repr.getKind() == kind::CONST_BITVECTOR) { + if (repr.getKind() == kind::CONST_BITVECTOR) + { // must check if it's just the constant eq::EqClassIterator it(repr, &d_equalityEngine); - if (!(++it).isFinished() || true) { + if (!(++it).isFinished() || true) + { constants.insert(repr); constants_in_eq_engine.insert(repr); } @@ -234,63 +239,79 @@ void CoreSolver::buildModel() { // build repr to value map eqcs_i = eq::EqClassesIterator(&d_equalityEngine); - while (!eqcs_i.isFinished()) { + while (!eqcs_i.isFinished()) + { TNode repr = *eqcs_i; ++eqcs_i; - if (!repr.isVar() && - repr.getKind() != kind::CONST_BITVECTOR && - !d_bv->isSharedTerm(repr)) { + if (!repr.isVar() && repr.getKind() != kind::CONST_BITVECTOR + && !d_bv->isSharedTerm(repr)) + { continue; } TypeNode type = repr.getType(); - if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) { - Debug("bv-core-model") << " processing " << repr <<"\n"; + if (type.isBitVector() && repr.getKind() != kind::CONST_BITVECTOR) + { + Debug("bv-core-model") << " processing " << repr << "\n"; // we need to assign a value for it TypeEnumerator te(type); Node val; - do { + do + { val = *te; ++te; // Debug("bv-core-model") << " trying value " << val << "\n"; - // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n"; - // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n"; + // Debug("bv-core-model") << " is in set? " << constants.count(val) << + // "\n"; Debug("bv-core-model") << " enumerator done? " << + // te.isFinished() << "\n"; } while (constants.count(val) != 0 && !(te.isFinished())); - if (te.isFinished() && constants.count(val) != 0) { - // if we cannot enumerate anymore values we just return the lemma stating that - // at least two of the representatives are equal. + if (te.isFinished() && constants.count(val) != 0) + { + // if we cannot enumerate anymore values we just return the lemma + // stating that at least two of the representatives are equal. std::vector<TNode> representatives; representatives.push_back(repr); for (TNodeSet::const_iterator it = constants_in_eq_engine.begin(); - it != constants_in_eq_engine.end(); ++it) { + it != constants_in_eq_engine.end(); + ++it) + { TNode constant = *it; - if (utils::getSize(constant) == utils::getSize(repr)) { + if (utils::getSize(constant) == utils::getSize(repr)) + { representatives.push_back(constant); } } - for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + for (ModelValue::const_iterator it = d_modelValues.begin(); + it != d_modelValues.end(); + ++it) + { representatives.push_back(it->first); } std::vector<Node> equalities; - for (unsigned i = 0; i < representatives.size(); ++i) { - for (unsigned j = i + 1; j < representatives.size(); ++j) { + for (unsigned i = 0; i < representatives.size(); ++i) + { + for (unsigned j = i + 1; j < representatives.size(); ++j) + { TNode a = representatives[i]; TNode b = representatives[j]; - if (a.getKind() == kind::CONST_BITVECTOR && - b.getKind() == kind::CONST_BITVECTOR) { - Assert (a != b); + if (a.getKind() == kind::CONST_BITVECTOR + && b.getKind() == kind::CONST_BITVECTOR) + { + Assert(a != b); continue; } - if (utils::getSize(a) == utils::getSize(b)) { - equalities.push_back(utils::mkNode(kind::EQUAL, a, b)); + if (utils::getSize(a) == utils::getSize(b)) + { + equalities.push_back(nm->mkNode(kind::EQUAL, a, b)); } } } // better off letting the SAT solver split on values - if (equalities.size() > d_lemmaThreshold) { + if (equalities.size() > d_lemmaThreshold) + { d_isComplete = false; return; } @@ -300,8 +321,8 @@ void CoreSolver::buildModel() { Debug("bv-core") << " lemma: " << lemma << "\n"; return; } - - Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ; + + Debug("bv-core-model") << " " << repr << " => " << val << "\n"; constants.insert(val); d_modelValues[repr] = val; } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index d828cc892..970b0331b 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -2,9 +2,9 @@ /*! \file bv_subtheory_inequality.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Morgan Deters + ** Liana Hadarean, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -58,8 +58,9 @@ bool InequalitySolver::check(Theory::Effort e) { TNode b = fact[0][0]; ok = addInequality(a, b, true, fact); // propagate + // NodeManager *nm = NodeManager::currentNM(); // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) { - // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); + // Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b)); // d_bv->storePropagation(neq, SUB_INEQUALITY); // d_explanations[neq] = fact; // } @@ -73,7 +74,7 @@ bool InequalitySolver::check(Theory::Effort e) { ok = addInequality(a, b, true, fact); // propagate // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) { - // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); + // Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b)); // d_bv->storePropagation(neq, SUB_INEQUALITY); // d_explanations[neq] = fact; // } @@ -106,32 +107,39 @@ bool InequalitySolver::check(Theory::Effort e) { return true; } -EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) { - if (!isComplete()) - return EQUALITY_UNKNOWN; +EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) +{ + if (!isComplete()) return EQUALITY_UNKNOWN; - Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b); - Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + NodeManager* nm = NodeManager::currentNM(); + Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b); + Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a); // if an inequality containing the terms has been asserted then we know // the equality is false - if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) { + if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) + { return EQUALITY_FALSE; } - if (!d_inequalityGraph.hasValueInModel(a) || - !d_inequalityGraph.hasValueInModel(b)) { + if (!d_inequalityGraph.hasValueInModel(a) + || !d_inequalityGraph.hasValueInModel(b)) + { return EQUALITY_UNKNOWN; } - // TODO: check if this disequality is entailed by inequalities via transitivity + // TODO: check if this disequality is entailed by inequalities via + // transitivity BitVector a_val = d_inequalityGraph.getValueInModel(a); BitVector b_val = d_inequalityGraph.getValueInModel(b); - if (a_val == b_val) { + if (a_val == b_val) + { return EQUALITY_TRUE_IN_MODEL; - } else { + } + else + { return EQUALITY_FALSE_IN_MODEL; } } @@ -222,13 +230,16 @@ void InequalitySolver::preRegister(TNode node) { } } -bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) { +bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) +{ bool ok = d_inequalityGraph.addInequality(a, b, strict, fact); if (!ok || !strict) return ok; Node one = utils::mkConst(utils::getSize(a), 1); - Node a_plus_one = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_PLUS, a, one)); - if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end()) { + Node a_plus_one = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, a, one)); + if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end()) + { ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact); } return ok; diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index bb45b771d..bed922830 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -2,9 +2,9 @@ /*! \file bv_to_bool.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Clark Barrett, Tim King + ** Liana Hadarean, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -94,107 +94,113 @@ bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) { return false; } -Node BvToBoolPreprocessor::convertBvAtom(TNode node) { - Assert (node.getType().isBoolean() && - node.getKind() == kind::EQUAL); - Assert (utils::getSize(node[0]) == 1); - Assert (utils::getSize(node[1]) == 1); +Node BvToBoolPreprocessor::convertBvAtom(TNode node) +{ + Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL); + Assert(utils::getSize(node[0]) == 1); + Assert(utils::getSize(node[1]) == 1); Node a = convertBvTerm(node[0]); Node b = convertBvTerm(node[1]); - Node result = utils::mkNode(kind::EQUAL, a, b); - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvAtom " << node <<" => " << result << "\n"; + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvAtom " << node + << " => " << result << "\n"; ++(d_statistics.d_numAtomsLifted); return result; } -Node BvToBoolPreprocessor::convertBvTerm(TNode node) { - Assert (node.getType().isBitVector() && - node.getType().getBitVectorSize() == 1); +Node BvToBoolPreprocessor::convertBvTerm(TNode node) +{ + Assert(node.getType().isBitVector() + && node.getType().getBitVectorSize() == 1); - if (hasBoolCache(node)) - return getBoolCache(node); - - if (!isConvertibleBvTerm(node)) { + if (hasBoolCache(node)) return getBoolCache(node); + + NodeManager* nm = NodeManager::currentNM(); + + if (!isConvertibleBvTerm(node)) + { ++(d_statistics.d_numTermsForcedLifted); - Node result = utils::mkNode(kind::EQUAL, node, d_one); + Node result = nm->mkNode(kind::EQUAL, node, d_one); addToBoolCache(node, result); - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node + << " => " << result << "\n"; return result; } - if (node.getNumChildren() == 0) { - Assert (node.getKind() == kind::CONST_BITVECTOR); + if (node.getNumChildren() == 0) + { + Assert(node.getKind() == kind::CONST_BITVECTOR); Node result = node == d_one ? utils::mkTrue() : utils::mkFalse(); // addToCache(node, result); - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; - return result; + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node + << " => " << result << "\n"; + return result; } ++(d_statistics.d_numTermsLifted); - + Kind kind = node.getKind(); - if (kind == kind::ITE) { + if (kind == kind::ITE) + { Node cond = liftNode(node[0]); Node true_branch = convertBvTerm(node[1]); Node false_branch = convertBvTerm(node[2]); - Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch); + Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch); addToBoolCache(node, result); - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; - return result; + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node + << " => " << result << "\n"; + return result; } Kind new_kind; // special case for XOR as it has to be binary // while BITVECTOR_XOR can be n-ary - if (kind == kind::BITVECTOR_XOR) { + if (kind == kind::BITVECTOR_XOR) + { new_kind = kind::XOR; Node result = convertBvTerm(node[0]); - for (unsigned i = 1; i < node.getNumChildren(); ++i) { + for (unsigned i = 1; i < node.getNumChildren(); ++i) + { Node converted = convertBvTerm(node[i]); - result = utils::mkNode(kind::XOR, result, converted); + result = nm->mkNode(kind::XOR, result, converted); } - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; - return result; + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node + << " => " << result << "\n"; + return result; } - if (kind == kind::BITVECTOR_COMP) { - Node result = utils::mkNode(kind::EQUAL, node[0], node[1]); + if (kind == kind::BITVECTOR_COMP) + { + Node result = nm->mkNode(kind::EQUAL, node[0], node[1]); addToBoolCache(node, result); - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; - return result; + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node + << " => " << result << "\n"; + return result; } - switch(kind) { - case kind::BITVECTOR_OR: - new_kind = kind::OR; - break; - case kind::BITVECTOR_AND: - new_kind = kind::AND; - break; - case kind::BITVECTOR_XOR: - new_kind = kind::XOR; - break; - case kind::BITVECTOR_NOT: - new_kind = kind::NOT; - break; - default: - Unhandled(); + switch (kind) + { + case kind::BITVECTOR_OR: new_kind = kind::OR; break; + case kind::BITVECTOR_AND: new_kind = kind::AND; break; + case kind::BITVECTOR_XOR: new_kind = kind::XOR; break; + case kind::BITVECTOR_NOT: new_kind = kind::NOT; break; + default: Unhandled(); } NodeBuilder<> builder(new_kind); - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - builder << convertBvTerm(node[i]); + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + builder << convertBvTerm(node[i]); } - + Node result = builder; addToBoolCache(node, result); - Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; - return result; + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node + << " => " << result << "\n"; + return result; } - - Node BvToBoolPreprocessor::liftNode(TNode current) { Node result; @@ -274,47 +280,46 @@ bool BvToBoolPreprocessor::hasLowerCache(TNode term) const { return d_lowerCache.find(term) != d_lowerCache.end(); } -Node BvToBoolPreprocessor::lowerNode(TNode current, bool topLevel) { +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) { + NodeManager* nm = NodeManager::currentNM(); + 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 { + } + else + { result = current; } - } else { + } + 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; + 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()) { + 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_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: @@ -323,18 +328,20 @@ Node BvToBoolPreprocessor::lowerNode(TNode current, bool topLevel) { case kind::BITVECTOR_SGE: // Should have been removed by rewriting. Unreachable(); - default: - break; + default: break; } NodeBuilder<> builder(new_kind); - if (kind != new_kind) { + if (kind != new_kind) + { ++(d_statistics.d_numTermsLowered); } - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) + { builder << current.getOperator(); } Node converted; - if (new_kind == kind::ITE) { + if (new_kind == kind::ITE) + { // Special-case ITE because need condition to be Boolean. converted = lowerNode(current[0], true); builder << converted; @@ -342,26 +349,33 @@ Node BvToBoolPreprocessor::lowerNode(TNode current, bool topLevel) { builder << converted; converted = lowerNode(current[2]); builder << converted; - } else { - for (unsigned i = 0; i < current.getNumChildren(); ++i) { + } + else + { + for (unsigned i = 0; i < current.getNumChildren(); ++i) + { converted = lowerNode(current[i]); - builder << converted; + builder << converted; } } result = builder; } - if (result.getType().isBoolean()) { + if (result.getType().isBoolean()) + { ++(d_statistics.d_numTermsForcedLowered); - result = utils::mkNode(kind::ITE, result, d_one, d_zero); + result = nm->mkNode(kind::ITE, result, d_one, d_zero); } addToLowerCache(current, result); } - if (topLevel) { - result = utils::mkNode(kind::EQUAL, result, d_one); + if (topLevel) + { + result = nm->mkNode(kind::EQUAL, result, d_one); } - Assert (result != Node()); - Debug("bool-to-bv") << "BvToBoolPreprocessor::lowerNode " << current << " => \n" << result << "\n"; - return result; + 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) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 710e25345..f8317cf15 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -2,9 +2,9 @@ /*! \file eager_bitblaster.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Guy Katz + ** Liana Hadarean, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -88,10 +88,12 @@ void EagerBitblaster::bbFormula(TNode node) { * @param node the atom to be bitblasted * */ -void EagerBitblaster::bbAtom(TNode node) { +void EagerBitblaster::bbAtom(TNode node) +{ node = node.getKind() == kind::NOT ? node[0] : node; if (node.getKind() == kind::BITVECTOR_BITOF) return; - if (hasBBAtom(node)) { + if (hasBBAtom(node)) + { return; } @@ -104,17 +106,19 @@ void EagerBitblaster::bbAtom(TNode node) { ? d_atomBBStrategies[normalized.getKind()](normalized, this) : normalized; - if (!options::proof()) { + if (!options::proof()) + { atom_bb = Rewriter::rewrite(atom_bb); } // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); + Node atom_definition = + NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb); AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, - TNode::null()); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); } void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 33342dc2e..cc4f52d8d 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -2,9 +2,9 @@ /*! \file lazy_bitblaster.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Morgan Deters + ** Liana Hadarean, Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -89,62 +89,76 @@ TLazyBitblaster::~TLazyBitblaster() * @param node the atom to be bitblasted * */ -void TLazyBitblaster::bbAtom(TNode node) { - node = node.getKind() == kind::NOT? node[0] : node; +void TLazyBitblaster::bbAtom(TNode node) +{ + NodeManager* nm = NodeManager::currentNM(); + node = node.getKind() == kind::NOT ? node[0] : node; - if (hasBBAtom(node)) { + if (hasBBAtom(node)) + { return; } - + // make sure it is marked as an atom addAtom(node); - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; ++d_statistics.d_numAtoms; - - /// if we are using bit-vector abstraction bit-blast the original interpretation - if (options::bvAbstraction() && - d_abstraction != NULL && - d_abstraction->isAbstraction(node)) { + /// if we are using bit-vector abstraction bit-blast the original + /// interpretation + if (options::bvAbstraction() && d_abstraction != NULL + && d_abstraction->isAbstraction(node)) + { // node must be of the form P(args) = bv1 Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node)); Node atom_bb; - if (expansion.getKind() == kind::CONST_BOOLEAN) { + if (expansion.getKind() == kind::CONST_BOOLEAN) + { atom_bb = expansion; - } else { - Assert (expansion.getKind() == kind::AND); + } + else + { + Assert(expansion.getKind() == kind::AND); std::vector<Node> atoms; - for (unsigned i = 0; i < expansion.getNumChildren(); ++i) { + for (unsigned i = 0; i < expansion.getNumChildren(); ++i) + { Node normalized_i = Rewriter::rewrite(expansion[i]); - Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ? - Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](normalized_i, this)) : - normalized_i; + Node atom_i = + normalized_i.getKind() != kind::CONST_BOOLEAN + ? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()]( + normalized_i, this)) + : normalized_i; atoms.push_back(atom_i); } atom_bb = utils::mkAnd(atoms); } - Assert (!atom_bb.isNull()); - Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); + Assert(!atom_bb.isNull()); + Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); return; } // the bitblasted definition of the atom Node normalized = Rewriter::rewrite(node); - Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? - d_atomBBStrategies[normalized.getKind()](normalized, this) : normalized; + Node atom_bb = + normalized.getKind() != kind::CONST_BOOLEAN + ? d_atomBBStrategies[normalized.getKind()](normalized, this) + : normalized; - if (!options::proof()) { + if (!options::proof()) + { atom_bb = Rewriter::rewrite(atom_bb); } // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); + Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); } void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { @@ -307,19 +321,24 @@ prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) { return d_satSolver->solve(budget); } - -void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) { +void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) +{ + NodeManager* nm = NodeManager::currentNM(); prop::SatClause conflictClause; d_satSolver->getUnsatCore(conflictClause); - for (unsigned i = 0; i < conflictClause.size(); i++) { + for (unsigned i = 0; i < conflictClause.size(); i++) + { prop::SatLiteral lit = conflictClause[i]; TNode atom = d_cnfStream->getNode(lit); - Node not_atom; - if (atom.getKind() == kind::NOT) { + Node not_atom; + if (atom.getKind() == kind::NOT) + { not_atom = atom[0]; - } else { - not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); + } + else + { + not_atom = nm->mkNode(kind::NOT, atom); } conflict.push_back(not_atom); } @@ -394,24 +413,30 @@ void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) d_bv->d_out->safePoint(amount); } - -EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { +EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) +{ int numAssertions = d_bv->numAssertions(); - Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n"; - Debug("bv-equality-status")<< "BVSatSolver has full model? " << (d_fullModelAssertionLevel.get() == numAssertions) <<"\n"; + Debug("bv-equality-status") + << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n"; + Debug("bv-equality-status") + << "BVSatSolver has full model? " + << (d_fullModelAssertionLevel.get() == numAssertions) << "\n"; // First check if it trivially rewrites to false/true - Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b)); + Node a_eq_b = + Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b)); if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - if (d_fullModelAssertionLevel.get() != numAssertions) { + if (d_fullModelAssertionLevel.get() != numAssertions) + { return theory::EQUALITY_UNKNOWN; } // Check if cache is valid (invalidated in check and pops) - if (d_bv->d_invalidateModelCache.get()) { + if (d_bv->d_invalidateModelCache.get()) + { invalidateModelCache(); } d_bv->d_invalidateModelCache.set(false); @@ -419,18 +444,17 @@ EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { Node a_value = getTermModel(a, true); Node b_value = getTermModel(b, true); - Assert (a_value.isConst() && - b_value.isConst()); + Assert(a_value.isConst() && b_value.isConst()); - if (a_value == b_value) { - Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n"; + if (a_value == b_value) + { + Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n"; return theory::EQUALITY_TRUE_IN_MODEL; } - Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n"; + Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n"; return theory::EQUALITY_FALSE_IN_MODEL; } - bool TLazyBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index f70eed096..851db1526 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -540,53 +540,64 @@ bool Slicer::isCoreTerm(TNode node) { } return d_coreTermCache[node]; } -unsigned Slicer::d_numAddedEqualities = 0; +unsigned Slicer::d_numAddedEqualities = 0; -void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) { - Assert (node.getKind() == kind::EQUAL); +void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) +{ + Assert(node.getKind() == kind::EQUAL); + NodeManager* nm = NodeManager::currentNM(); TNode t1 = node[0]; TNode t2 = node[1]; - uint32_t width = utils::getSize(t1); - - Base base1(width); - if (t1.getKind() == kind::BITVECTOR_CONCAT) { + uint32_t width = utils::getSize(t1); + + Base base1(width); + if (t1.getKind() == kind::BITVECTOR_CONCAT) + { int size = 0; - // no need to count the last child since the end cut point is implicit - for (int i = t1.getNumChildren() - 1; i >= 1 ; --i) { + // no need to count the last child since the end cut point is implicit + for (int i = t1.getNumChildren() - 1; i >= 1; --i) + { size = size + utils::getSize(t1[i]); - base1.sliceAt(size); + base1.sliceAt(size); } } - Base base2(width); - if (t2.getKind() == kind::BITVECTOR_CONCAT) { - unsigned size = 0; - for (int i = t2.getNumChildren() - 1; i >= 1; --i) { + Base base2(width); + if (t2.getKind() == kind::BITVECTOR_CONCAT) + { + unsigned size = 0; + for (int i = t2.getNumChildren() - 1; i >= 1; --i) + { size = size + utils::getSize(t2[i]); - base2.sliceAt(size); + base2.sliceAt(size); } } - base1.sliceWith(base2); - if (!base1.isEmpty()) { + base1.sliceWith(base2); + if (!base1.isEmpty()) + { // we split the equalities according to the base - int last = 0; - for (unsigned i = 1; i <= utils::getSize(t1); ++i) { - if (base1.isCutPoint(i)) { - Node extract1 = utils::mkExtract(t1, i-1, last); - Node extract2 = utils::mkExtract(t2, i-1, last); + int last = 0; + for (unsigned i = 1; i <= utils::getSize(t1); ++i) + { + if (base1.isCutPoint(i)) + { + Node extract1 = utils::mkExtract(t1, i - 1, last); + Node extract2 = utils::mkExtract(t2, i - 1, last); last = i; - Assert (utils::getSize(extract1) == utils::getSize(extract2)); - equalities.push_back(utils::mkNode(kind::EQUAL, extract1, extract2)); + Assert(utils::getSize(extract1) == utils::getSize(extract2)); + equalities.push_back(nm->mkNode(kind::EQUAL, extract1, extract2)); } } - } else { + } + else + { // just return same equality equalities.push_back(node); } - d_numAddedEqualities += equalities.size() - 1; -} + d_numAddedEqualities += equalities.size() - 1; +} std::string UnionFind::debugPrint(TermId id) { ostringstream os; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c6f2ec74b..fd9ad0c6a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -2,9 +2,9 @@ /*! \file theory_bv.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Clark Barrett + ** Liana Hadarean, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -252,7 +252,7 @@ void TheoryBV::mkAckermanizationAssertions(std::vector<Node>& assertions) { for (unsigned i = 0; i < args1.getNumChildren(); ++i) { eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); } - args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs); + args_eq = utils::mkAnd(eqs); } else { AlwaysAssert (args1.getKind() == kind::SELECT && args1[0] == func); @@ -363,28 +363,33 @@ void TheoryBV::sendConflict() { } } -void TheoryBV::checkForLemma(TNode fact) { - if (fact.getKind() == kind::EQUAL) { - if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) { +void TheoryBV::checkForLemma(TNode fact) +{ + if (fact.getKind() == kind::EQUAL) + { + NodeManager* nm = NodeManager::currentNM(); + if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) + { TNode urem = fact[0]; TNode result = fact[1]; TNode divisor = urem[1]; - Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); - Node divisor_eq_0 = mkNode( - kind::EQUAL, divisor, mkZero(getSize(divisor))); - Node split = utils::mkNode( - kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = + nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); + Node split = nm->mkNode( + kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); lemma(split); } - if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { + if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) + { TNode urem = fact[1]; TNode result = fact[0]; TNode divisor = urem[1]; - Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); - Node divisor_eq_0 = mkNode( - kind::EQUAL, divisor, mkZero(getSize(divisor))); - Node split = utils::mkNode( - kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = + nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); + Node split = nm->mkNode( + kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); lemma(split); } } @@ -431,7 +436,7 @@ void TheoryBV::check(Effort e) d_out->conflict(assertions[0]); return; } - Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions); + Node conflict = utils::mkAnd(assertions); d_out->conflict(conflict); return; } @@ -505,59 +510,76 @@ void TheoryBV::check(Effort e) } } -bool TheoryBV::doExtfInferences( std::vector< Node >& terms ) { +bool TheoryBV::doExtfInferences(std::vector<Node>& terms) +{ + NodeManager* nm = NodeManager::currentNM(); bool sentLemma = false; - eq::EqualityEngine * ee = getEqualityEngine(); - std::map< Node, Node > op_map; - for( unsigned j=0; j<terms.size(); j++ ){ + eq::EqualityEngine* ee = getEqualityEngine(); + std::map<Node, Node> op_map; + for (unsigned j = 0; j < terms.size(); j++) + { TNode n = terms[j]; - Assert (n.getKind() == kind::BITVECTOR_TO_NAT - || n.getKind() == kind::INT_TO_BITVECTOR ); - if( n.getKind()==kind::BITVECTOR_TO_NAT ){ - //range lemmas - if( d_extf_range_infer.find( n )==d_extf_range_infer.end() ){ - d_extf_range_infer.insert( n ); + Assert(n.getKind() == kind::BITVECTOR_TO_NAT + || n.getKind() == kind::INT_TO_BITVECTOR); + if (n.getKind() == kind::BITVECTOR_TO_NAT) + { + // range lemmas + if (d_extf_range_infer.find(n) == d_extf_range_infer.end()) + { + d_extf_range_infer.insert(n); unsigned bvs = n[0].getType().getBitVectorSize(); - Node min = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - Node max = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) ); - Node lem = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, n, min ), NodeManager::currentNM()->mkNode( kind::LT, n, max ) ); - Trace("bv-extf-lemma") << "BV extf lemma (range) : " << lem << std::endl; - d_out->lemma( lem ); + Node min = nm->mkConst(Rational(0)); + Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); + Node lem = nm->mkNode(kind::AND, + nm->mkNode(kind::GEQ, n, min), + nm->mkNode(kind::LT, n, max)); + Trace("bv-extf-lemma") + << "BV extf lemma (range) : " << lem << std::endl; + d_out->lemma(lem); sentLemma = true; } } - Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n[0] ) : n[0]; + Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0]; op_map[r] = n; } - for( unsigned j=0; j<terms.size(); j++ ){ + for (unsigned j = 0; j < terms.size(); j++) + { TNode n = terms[j]; - Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n ) : n; - std::map< Node, Node >::iterator it = op_map.find( r ); - if( it!=op_map.end() ){ + Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n; + std::map<Node, Node>::iterator it = op_map.find(r); + if (it != op_map.end()) + { Node parent = it->second; - //Node cterm = parent[0]==n ? parent : NodeManager::currentNM()->mkNode( parent.getOperator(), n ); - Node cterm = parent[0].eqNode( n ); - Trace("bv-extf-lemma-debug") << "BV extf collapse based on : " << cterm << std::endl; - if( d_extf_collapse_infer.find( cterm )==d_extf_collapse_infer.end() ){ - d_extf_collapse_infer.insert( cterm ); - + // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(), + // n ); + Node cterm = parent[0].eqNode(n); + Trace("bv-extf-lemma-debug") + << "BV extf collapse based on : " << cterm << std::endl; + if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end()) + { + d_extf_collapse_infer.insert(cterm); + Node t = n[0]; - if( n.getKind()==kind::INT_TO_BITVECTOR ){ - Assert( t.getType().isInteger() ); - //congruent modulo 2^( bv width ) + if (n.getKind() == kind::INT_TO_BITVECTOR) + { + Assert(t.getType().isInteger()); + // congruent modulo 2^( bv width ) unsigned bvs = n.getType().getBitVectorSize(); - Node coeff = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) ); - Node k = NodeManager::currentNM()->mkSkolem( "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence" ); - t = NodeManager::currentNM()->mkNode( kind::PLUS, t, NodeManager::currentNM()->mkNode( kind::MULT, coeff, k ) ); + Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); + Node k = nm->mkSkolem( + "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence"); + t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k)); } - Node lem = parent.eqNode( t ); - - if( parent[0]!=n ){ - Assert( ee->areEqual( parent[0], n ) ); - lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, parent[0].eqNode( n ), lem ); + Node lem = parent.eqNode(t); + + if (parent[0] != n) + { + Assert(ee->areEqual(parent[0], n)); + lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem); } - Trace("bv-extf-lemma") << "BV extf lemma (collapse) : " << lem << std::endl; - d_out->lemma( lem ); + Trace("bv-extf-lemma") + << "BV extf lemma (collapse) : " << lem << std::endl; + d_out->lemma(lem); sentLemma = true; } } @@ -667,33 +689,44 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st return false; } -int TheoryBV::getReduction( int effort, Node n, Node& nr ) { +int TheoryBV::getReduction(int effort, Node n, Node& nr) +{ Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl; - if( n.getKind()==kind::BITVECTOR_TO_NAT ){ - //taken from rewrite code + NodeManager* const nm = NodeManager::currentNM(); + if (n.getKind() == kind::BITVECTOR_TO_NAT) + { + // taken from rewrite code const unsigned size = utils::getSize(n[0]); - NodeManager* const nm = NodeManager::currentNM(); const Node z = nm->mkConst(Rational(0)); const Node bvone = utils::mkOne(1); NodeBuilder<> result(kind::PLUS); Integer i = 1; - for(unsigned bit = 0; bit < size; ++bit, i *= 2) { - Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]), bvone); + for (unsigned bit = 0; bit < size; ++bit, i *= 2) + { + Node cond = + nm->mkNode(kind::EQUAL, + nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]), + bvone); result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z); } nr = Node(result); return -1; - }else if( n.getKind()==kind::INT_TO_BITVECTOR ){ - //taken from rewrite code + } + else if (n.getKind() == kind::INT_TO_BITVECTOR) + { + // taken from rewrite code const unsigned size = n.getOperator().getConst<IntToBitVector>().size; - NodeManager* const nm = NodeManager::currentNM(); const Node bvzero = utils::mkZero(1); const Node bvone = utils::mkOne(1); std::vector<Node> v; Integer i = 2; - while(v.size() < size) { - Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2))); - cond = Rewriter::rewrite( cond ); + while (v.size() < size) + { + Node cond = nm->mkNode( + kind::GEQ, + nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))), + nm->mkConst(Rational(i, 2))); + cond = Rewriter::rewrite(cond); v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); i *= 2; } @@ -704,26 +737,34 @@ int TheoryBV::getReduction( int effort, Node n, Node& nr ) { } return 0; } - -Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - switch(in.getKind()) { - case kind::EQUAL: + +Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, + SubstitutionMap& outSubstitutions) +{ + switch (in.getKind()) + { + case kind::EQUAL: { - if (in[0].isVar() && !in[1].hasSubterm(in[0])) { + if (in[0].isVar() && !in[1].hasSubterm(in[0])) + { ++(d_statistics.d_solveSubstitutions); outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].isVar() && !in[0].hasSubterm(in[1])) { + if (in[1].isVar() && !in[0].hasSubterm(in[1])) + { ++(d_statistics.d_solveSubstitutions); outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } Node node = Rewriter::rewrite(in); - if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) || - (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) { + if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) + || (node[1].getKind() == kind::BITVECTOR_EXTRACT + && node[0].isConst())) + { Node extract = node[0].isConst() ? node[1] : node[0]; - if (extract[0].getKind() == kind::VARIABLE) { + if (extract[0].getKind() == kind::VARIABLE) + { Node c = node[0].isConst() ? node[0] : node[1]; unsigned high = utils::getExtractHigh(extract); @@ -731,18 +772,23 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu unsigned var_bitwidth = utils::getSize(extract[0]); std::vector<Node> children; - if (low == 0) { - Assert (high != var_bitwidth - 1); + if (low == 0) + { + Assert(high != var_bitwidth - 1); unsigned skolem_size = var_bitwidth - high - 1; Node skolem = utils::mkVar(skolem_size); children.push_back(skolem); children.push_back(c); - } else if (high == var_bitwidth - 1) { + } + else if (high == var_bitwidth - 1) + { unsigned skolem_size = low; Node skolem = utils::mkVar(skolem_size); children.push_back(c); children.push_back(skolem); - } else { + } + else + { unsigned skolem1_size = low; unsigned skolem2_size = var_bitwidth - high - 1; Node skolem1 = utils::mkVar(skolem1_size); @@ -751,22 +797,22 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu children.push_back(c); children.push_back(skolem1); } - Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children); - Assert (utils::getSize(concat) == utils::getSize(extract[0])); + Node concat = utils::mkConcat(children); + Assert(utils::getSize(concat) == utils::getSize(extract[0])); outSubstitutions.addSubstitution(extract[0], concat); return PP_ASSERT_STATUS_SOLVED; } } } break; - case kind::BITVECTOR_ULT: - case kind::BITVECTOR_SLT: - case kind::BITVECTOR_ULE: - case kind::BITVECTOR_SLE: + case kind::BITVECTOR_ULT: + case kind::BITVECTOR_SLT: + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_SLE: - default: - // TODO other predicates - break; + default: + // TODO other predicates + break; } return PP_ASSERT_STATUS_UNSOLVED; } @@ -795,7 +841,7 @@ Node TheoryBV::ppRewrite(TNode t) RewriteRule<ConcatToMult>::run<true>(res[1]); Node factor = mult[0]; Node sum = RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0]; - Node new_eq =utils::mkNode(kind::EQUAL, sum, mult); + Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq); if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){ res = Rewriter::rewrite(rewr_eq); @@ -808,17 +854,20 @@ Node TheoryBV::ppRewrite(TNode t) res = RewriteRule<ZeroExtendEqConst>::run<false>(t); } - // if(t.getKind() == kind::EQUAL && - // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) || - // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == kind::BITVECTOR_PLUS))) { + // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == + // kind::BITVECTOR_PLUS) || + // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == + // kind::BITVECTOR_PLUS))) { // // if we have an equality between a multiplication and addition // // try to express multiplication in terms of addition // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1]; // if (RewriteRule<MultSlice>::applies(mult)) { // Node new_mult = RewriteRule<MultSlice>::run<false>(mult); - // Node new_eq = Rewriter::rewrite(utils::mkNode(kind::EQUAL, new_mult, add)); + // Node new_eq = + // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, + // new_mult, add)); // // the simplification can cause the formula to blow up // // only apply if formula reduced @@ -985,7 +1034,8 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { Node c_eq_0 = c.eqNode(zero); Node b_eq_c = b.eqNode(c); - Node dis = utils::mkNode(kind::OR, b_eq_0, c_eq_0, b_eq_c); + Node dis = NodeManager::currentNM()->mkNode( + kind::OR, b_eq_0, c_eq_0, b_eq_c); Node imp = in.impNode(dis); learned << imp; } @@ -1021,15 +1071,19 @@ void TheoryBV::setProofLog( BitVectorProof * bvp ) { } } -void TheoryBV::setConflict(Node conflict) { - if (options::bvAbstraction()) { +void TheoryBV::setConflict(Node conflict) +{ + if (options::bvAbstraction()) + { + NodeManager* const nm = NodeManager::currentNM(); Node new_conflict = d_abstractionModule->simplifyConflict(conflict); std::vector<Node> lemmas; lemmas.push_back(new_conflict); d_abstractionModule->generalizeConflict(new_conflict, lemmas); - for (unsigned i = 0; i < lemmas.size(); ++i) { - lemma(utils::mkNode(kind::NOT, lemmas[i])); + for (unsigned i = 0; i < lemmas.size(); ++i) + { + lemma(nm->mkNode(kind::NOT, lemmas[i])); } } d_conflict = true; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index ad5b37a2d..6a36b61a4 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -2,9 +2,9 @@ /*! \file theory_bv_rewrite_rules_normalization.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Clark Barrett, Tim King + ** Liana Hadarean, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -67,13 +67,14 @@ bool RewriteRule<ExtractNot>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_NOT); } -template<> inline -Node RewriteRule<ExtractNot>::apply(TNode node) { +template <> +inline Node RewriteRule<ExtractNot>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl; unsigned low = utils::getExtractLow(node); unsigned high = utils::getExtractHigh(node); Node a = utils::mkExtract(node[0][0], high, low); - return utils::mkNode(kind::BITVECTOR_NOT, a); + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, a); } /** @@ -93,41 +94,48 @@ bool RewriteRule<ExtractSignExtend>::applies(TNode node) { return false; } -template<> inline -Node RewriteRule<ExtractSignExtend>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << node << ")" << std::endl; - TNode extendee = node[0][0]; +template <> +inline Node RewriteRule<ExtractSignExtend>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << node << ")" + << std::endl; + TNode extendee = node[0][0]; unsigned extendee_size = utils::getSize(extendee); unsigned high = utils::getExtractHigh(node); - unsigned low = utils::getExtractLow(node); + unsigned low = utils::getExtractLow(node); - Node resultNode; + Node resultNode; // extract falls on extendee - if (high < extendee_size) { - resultNode = utils::mkExtract(extendee, high, low); - } else if (low < extendee_size && high >= extendee_size) { + if (high < extendee_size) + { + resultNode = utils::mkExtract(extendee, high, low); + } + else if (low < extendee_size && high >= extendee_size) + { // if extract overlaps sign extend and extendee Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low); unsigned new_amount = high - extendee_size + 1; resultNode = utils::mkSignExtend(low_extract, new_amount); - } else { + } + else + { // extract only over sign extend - Assert (low >= extendee_size); - unsigned top = utils::getSize(extendee) - 1; + Assert(low >= extendee_size); + unsigned top = utils::getSize(extendee) - 1; Node most_significant_bit = utils::mkExtract(extendee, top, top); std::vector<Node> bits; - for (unsigned i = 0; i < high - low + 1; ++i) { - bits.push_back(most_significant_bit); + for (unsigned i = 0; i < high - low + 1; ++i) + { + bits.push_back(most_significant_bit); } - resultNode = utils::mkNode(kind::BITVECTOR_CONCAT, bits); + resultNode = utils::mkConcat(bits); } - Debug("bv-rewrite") << " =>" << resultNode << std::endl; - return resultNode; + Debug("bv-rewrite") << " =>" << resultNode + << std::endl; + return resultNode; } - - /** * ExtractArith * @@ -142,19 +150,21 @@ bool RewriteRule<ExtractArith>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_MULT)); } -template<> inline -Node RewriteRule<ExtractArith>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<ExtractArith>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" + << std::endl; unsigned low = utils::getExtractLow(node); - Assert (low == 0); + Assert(low == 0); unsigned high = utils::getExtractHigh(node); std::vector<Node> children; - for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { - children.push_back(utils::mkExtract(node[0][i], high, low)); + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) + { + children.push_back(utils::mkExtract(node[0][i], high, low)); } - Kind kind = node[0].getKind(); - return utils::mkNode(kind, children); - + Kind kind = node[0].getKind(); + return utils::mkNaryNode(kind, children); } /** @@ -171,19 +181,22 @@ bool RewriteRule<ExtractArith2>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_MULT)); } -template<> inline -Node RewriteRule<ExtractArith2>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<ExtractArith2>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" + << std::endl; unsigned low = utils::getExtractLow(node); unsigned high = utils::getExtractHigh(node); std::vector<Node> children; - for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { - children.push_back(utils::mkExtract(node[0][i], high, 0)); + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) + { + children.push_back(utils::mkExtract(node[0][i], high, 0)); } - Kind kind = node[0].getKind(); - Node op_children = utils::mkNode(kind, children); - - return utils::mkExtract(op_children, high, low); + Kind kind = node[0].getKind(); + Node op_children = utils::mkNaryNode(kind, children); + + return utils::mkExtract(op_children, high, low); } template<> inline @@ -204,33 +217,41 @@ bool RewriteRule<FlattenAssocCommut>::applies(TNode node) { return false; } - -template<> inline -Node RewriteRule<FlattenAssocCommut>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<FlattenAssocCommut>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" + << std::endl; std::vector<Node> processingStack; processingStack.push_back(node); std::vector<Node> children; - Kind kind = node.getKind(); - - while (! processingStack.empty()) { + Kind kind = node.getKind(); + + while (!processingStack.empty()) + { TNode current = processingStack.back(); processingStack.pop_back(); // flatten expression - if (current.getKind() == kind) { - for (unsigned i = 0; i < current.getNumChildren(); ++i) { + if (current.getKind() == kind) + { + for (unsigned i = 0; i < current.getNumChildren(); ++i) + { processingStack.push_back(current[i]); } - } else { - children.push_back(current); + } + else + { + children.push_back(current); } } - if (node.getKind() == kind::BITVECTOR_PLUS || - node.getKind() == kind::BITVECTOR_MULT) { - return utils::mkNode(kind, children); + if (node.getKind() == kind::BITVECTOR_PLUS + || node.getKind() == kind::BITVECTOR_MULT) + { + return utils::mkNaryNode(kind, children); } - else { + else + { return utils::mkSortedNode(kind, children); } } @@ -310,89 +331,103 @@ static inline void updateCoefMap(TNode current, unsigned size, } } - -static inline void addToChildren(TNode term, unsigned size, BitVector coeff, std::vector<Node>& children) { - if (coeff == BitVector(size, (unsigned)0)) { +static inline void addToChildren(TNode term, + unsigned size, + BitVector coeff, + std::vector<Node> &children) +{ + NodeManager *nm = NodeManager::currentNM(); + if (coeff == BitVector(size, (unsigned)0)) + { return; } - else if (coeff == BitVector(size, (unsigned)1)) { - children.push_back(term); + else if (coeff == BitVector(size, (unsigned)1)) + { + children.push_back(term); } - else if (coeff == -BitVector(size, (unsigned)1)) { + else if (coeff == -BitVector(size, (unsigned)1)) + { // avoid introducing an extra multiplication - children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term)); + children.push_back(nm->mkNode(kind::BITVECTOR_NEG, term)); } - else if (term.getKind() == kind::BITVECTOR_MULT) { + else if (term.getKind() == kind::BITVECTOR_MULT) + { NodeBuilder<> nb(kind::BITVECTOR_MULT); TNode::iterator child_it = term.begin(); - for(; child_it != term.end(); ++child_it) { + for (; child_it != term.end(); ++child_it) + { nb << *child_it; } nb << utils::mkConst(coeff); children.push_back(Node(nb)); } - else { + else + { Node coeffNode = utils::mkConst(coeff); - Node product = utils::mkNode(kind::BITVECTOR_MULT, term, coeffNode); - children.push_back(product); + Node product = nm->mkNode(kind::BITVECTOR_MULT, term, coeffNode); + children.push_back(product); } } - template<> inline bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_PLUS); } - -template<> inline -Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl; - unsigned size = utils::getSize(node); - BitVector constSum(size, (unsigned)0); +template <> +inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" + << std::endl; + unsigned size = utils::getSize(node); + BitVector constSum(size, (unsigned)0); std::map<Node, BitVector> factorToCoefficient; // combine like-terms - for(unsigned i= 0; i < node.getNumChildren(); ++i) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { TNode current = node[i]; updateCoefMap(current, size, factorToCoefficient, constSum); } - - std::vector<Node> children; - // construct result + std::vector<Node> children; + + // construct result std::map<Node, BitVector>::const_iterator it = factorToCoefficient.begin(); - - for (; it != factorToCoefficient.end(); ++it) { - addToChildren(it->first, size, it->second, children); - } - if (constSum != BitVector(size, (unsigned)0)) { - children.push_back(utils::mkConst(constSum)); + for (; it != factorToCoefficient.end(); ++it) + { + addToChildren(it->first, size, it->second, children); } - if(children.size() == 0) { - return utils::mkConst(size, (unsigned)0); + if (constSum != BitVector(size, (unsigned)0)) + { + children.push_back(utils::mkConst(constSum)); } - return utils::mkNode(kind::BITVECTOR_PLUS, children); + unsigned csize = children.size(); + return csize == 0 + ? utils::mkZero(size) + : utils::mkNaryNode(kind::BITVECTOR_PLUS, children); } - template<> inline bool RewriteRule<MultSimplify>::applies(TNode node) { return node.getKind() == kind::BITVECTOR_MULT; } -template<> inline -Node RewriteRule<MultSimplify>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl; - unsigned size = utils::getSize(node); +template <> +inline Node RewriteRule<MultSimplify>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); + unsigned size = utils::getSize(node); BitVector constant(size, Integer(1)); bool isNeg = false; std::vector<Node> children; - for (const TNode& current : node) + for (const TNode ¤t : node) { Node c = current; if (c.getKind() == kind::BITVECTOR_NEG) @@ -405,10 +440,13 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { { BitVector value = c.getConst<BitVector>(); constant = constant * value; - if(constant == BitVector(size, (unsigned) 0)) { - return utils::mkConst(size, 0); + if (constant == BitVector(size, (unsigned)0)) + { + return utils::mkConst(size, 0); } - } else { + } + else + { children.push_back(c); } } @@ -436,17 +474,16 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - Node ret = utils::mkNode(kind::BITVECTOR_MULT, children); + Node ret = utils::mkNaryNode(kind::BITVECTOR_MULT, children); // if negative, negate entire node if (isNeg && size > 1) { - ret = utils::mkNode(kind::BITVECTOR_NEG, ret); + ret = nm->mkNode(kind::BITVECTOR_NEG, ret); } return ret; } - template<> inline bool RewriteRule<MultDistribConst>::applies(TNode node) { if (node.getKind() != kind::BITVECTOR_MULT || @@ -463,28 +500,32 @@ bool RewriteRule<MultDistribConst>::applies(TNode node) { factor.getKind() == kind::BITVECTOR_NEG); } -template<> inline -Node RewriteRule<MultDistribConst>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<MultDistribConst>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode constant = node[1]; TNode factor = node[0]; Assert(constant.getKind() == kind::CONST_BITVECTOR); - if (factor.getKind() == kind::BITVECTOR_NEG) { + if (factor.getKind() == kind::BITVECTOR_NEG) + { // push negation on the constant part BitVector const_bv = constant.getConst<BitVector>(); - return utils::mkNode(kind::BITVECTOR_MULT, - factor[0], - utils::mkConst(-const_bv)); + return nm->mkNode( + kind::BITVECTOR_MULT, factor[0], utils::mkConst(-const_bv)); } std::vector<Node> children; - for(unsigned i = 0; i < factor.getNumChildren(); ++i) { - children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], constant)); + for (unsigned i = 0; i < factor.getNumChildren(); ++i) + { + children.push_back(nm->mkNode(kind::BITVECTOR_MULT, factor[i], constant)); } - - return utils::mkNode(factor.getKind(), children); + + return utils::mkNaryNode(factor.getKind(), children); } template<> inline @@ -502,25 +543,29 @@ bool RewriteRule<MultDistrib>::applies(TNode node) { node[1].getKind() == kind::BITVECTOR_SUB; } -template<> inline -Node RewriteRule<MultDistrib>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<MultDistrib>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" + << std::endl; - bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS || - node[0].getKind() == kind::BITVECTOR_SUB; + NodeManager *nm = NodeManager::currentNM(); + bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS + || node[0].getKind() == kind::BITVECTOR_SUB; TNode factor = !is_rhs_factor ? node[0] : node[1]; TNode sum = is_rhs_factor ? node[0] : node[1]; - Assert (factor.getKind() != kind::BITVECTOR_PLUS && - factor.getKind() != kind::BITVECTOR_SUB && - (sum.getKind() == kind::BITVECTOR_PLUS || - sum.getKind() == kind::BITVECTOR_SUB)); + Assert(factor.getKind() != kind::BITVECTOR_PLUS + && factor.getKind() != kind::BITVECTOR_SUB + && (sum.getKind() == kind::BITVECTOR_PLUS + || sum.getKind() == kind::BITVECTOR_SUB)); std::vector<Node> children; - for(unsigned i = 0; i < sum.getNumChildren(); ++i) { - children.push_back(utils::mkNode(kind::BITVECTOR_MULT, sum[i], factor)); + for (unsigned i = 0; i < sum.getNumChildren(); ++i) + { + children.push_back(nm->mkNode(kind::BITVECTOR_MULT, sum[i], factor)); } - - return utils::mkNode(sum.getKind(), children); + + return utils::mkNaryNode(sum.getKind(), children); } template<> inline @@ -543,19 +588,19 @@ bool RewriteRule<ConcatToMult>::applies(TNode node) { return true; } -template<> inline -Node RewriteRule<ConcatToMult>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<ConcatToMult>(" << node << ")" << std::endl; - unsigned size = utils::getSize(node); +template <> +inline Node RewriteRule<ConcatToMult>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<ConcatToMult>(" << node << ")" + << std::endl; + unsigned size = utils::getSize(node); Node factor = node[0][0]; Assert(utils::getSize(factor) == utils::getSize(node)); BitVector amount = BitVector(size, utils::getSize(node[1])); Node coef = utils::mkConst(BitVector(size, 1u).leftShift(amount)); - return utils::mkNode(kind::BITVECTOR_MULT, factor, coef); + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, factor, coef); } - - template<> inline bool RewriteRule<SolveEq>::applies(TNode node) { if (node.getKind() != kind::EQUAL || @@ -566,10 +611,11 @@ bool RewriteRule<SolveEq>::applies(TNode node) { return true; } - -// Doesn't do full solving (yet), instead, if a term appears both on lhs and rhs, it subtracts from both sides so that one side's coeff is zero -template<> inline -Node RewriteRule<SolveEq>::apply(TNode node) { +// Doesn't do full solving (yet), instead, if a term appears both on lhs and +// rhs, it subtracts from both sides so that one side's coeff is zero +template <> +inline Node RewriteRule<SolveEq>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl; TNode left = node[0]; @@ -582,83 +628,105 @@ Node RewriteRule<SolveEq>::apply(TNode node) { std::map<Node, BitVector> leftMap, rightMap; // Collect terms and coefficients plus constant for left - if (left.getKind() == kind::BITVECTOR_PLUS) { - for(unsigned i= 0; i < left.getNumChildren(); ++i) { + if (left.getKind() == kind::BITVECTOR_PLUS) + { + for (unsigned i = 0; i < left.getNumChildren(); ++i) + { updateCoefMap(left[i], size, leftMap, leftConst); } } - else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right) { + else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right) + { return utils::mkFalse(); } - else { + else + { updateCoefMap(left, size, leftMap, leftConst); } // Collect terms and coefficients plus constant for right - if (right.getKind() == kind::BITVECTOR_PLUS) { - for(unsigned i= 0; i < right.getNumChildren(); ++i) { + if (right.getKind() == kind::BITVECTOR_PLUS) + { + for (unsigned i = 0; i < right.getNumChildren(); ++i) + { updateCoefMap(right[i], size, rightMap, rightConst); } } - else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left) { + else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left) + { return utils::mkFalse(); } - else { + else + { updateCoefMap(right, size, rightMap, rightConst); } std::vector<Node> childrenLeft, childrenRight; - std::map<Node, BitVector>::const_iterator iLeft = leftMap.begin(), iLeftEnd = leftMap.end(); - std::map<Node, BitVector>::const_iterator iRight = rightMap.begin(), iRightEnd = rightMap.end(); + std::map<Node, BitVector>::const_iterator iLeft = leftMap.begin(), + iLeftEnd = leftMap.end(); + std::map<Node, BitVector>::const_iterator iRight = rightMap.begin(), + iRightEnd = rightMap.end(); BitVector coeffLeft; TNode termLeft; - if (iLeft != iLeftEnd) { + if (iLeft != iLeftEnd) + { coeffLeft = iLeft->second; termLeft = iLeft->first; } BitVector coeffRight; TNode termRight; - if (iRight != iRightEnd) { + if (iRight != iRightEnd) + { coeffRight = iRight->second; termRight = iRight->first; } bool incLeft, incRight; - while (iLeft != iLeftEnd || iRight != iRightEnd) { + while (iLeft != iLeftEnd || iRight != iRightEnd) + { incLeft = incRight = false; - if (iLeft != iLeftEnd && (iRight == iRightEnd || termLeft < termRight)) { + if (iLeft != iLeftEnd && (iRight == iRightEnd || termLeft < termRight)) + { addToChildren(termLeft, size, coeffLeft, childrenLeft); incLeft = true; - } - else if (iLeft == iLeftEnd || termRight < termLeft) { + } + else if (iLeft == iLeftEnd || termRight < termLeft) + { Assert(iRight != iRightEnd); addToChildren(termRight, size, coeffRight, childrenRight); incRight = true; } - else { - if (coeffLeft > coeffRight) { + else + { + if (coeffLeft > coeffRight) + { addToChildren(termLeft, size, coeffLeft - coeffRight, childrenLeft); } - else if (coeffRight > coeffLeft) { + else if (coeffRight > coeffLeft) + { addToChildren(termRight, size, coeffRight - coeffLeft, childrenRight); } incLeft = incRight = true; } - if (incLeft) { + if (incLeft) + { ++iLeft; - if (iLeft != iLeftEnd) { + if (iLeft != iLeftEnd) + { Assert(termLeft < iLeft->first); coeffLeft = iLeft->second; termLeft = iLeft->first; } } - if (incRight) { + if (incRight) + { ++iRight; - if (iRight != iRightEnd) { + if (iRight != iRightEnd) + { Assert(termRight < iRight->first); coeffRight = iRight->second; termRight = iRight->first; @@ -666,87 +734,99 @@ Node RewriteRule<SolveEq>::apply(TNode node) { } } - // construct result + // construct result - // If both constants are nonzero, combine on right, otherwise leave them where they are - if (rightConst != zero) { + // If both constants are nonzero, combine on right, otherwise leave them where + // they are + if (rightConst != zero) + { rightConst = rightConst - leftConst; leftConst = zero; - if (rightConst != zero) { + if (rightConst != zero) + { childrenRight.push_back(utils::mkConst(rightConst)); } } - else if (leftConst != zero) { + else if (leftConst != zero) + { childrenLeft.push_back(utils::mkConst(leftConst)); } Node newLeft, newRight; - if(childrenRight.size() == 0 && leftConst != zero) { - Assert(childrenLeft.back().isConst() && childrenLeft.back().getConst<BitVector>() == leftConst); - if (childrenLeft.size() == 1) { + if (childrenRight.size() == 0 && leftConst != zero) + { + Assert(childrenLeft.back().isConst() + && childrenLeft.back().getConst<BitVector>() == leftConst); + if (childrenLeft.size() == 1) + { // c = 0 ==> false return utils::mkFalse(); } - // special case - if right is empty and left has a constant, move the constant + // special case - if right is empty and left has a constant, move the + // constant childrenRight.push_back(utils::mkConst(-leftConst)); childrenLeft.pop_back(); } - if(childrenLeft.size() == 0) { - if (rightConst != zero) { - Assert(childrenRight.back().isConst() && childrenRight.back().getConst<BitVector>() == rightConst); - if (childrenRight.size() == 1) { + if (childrenLeft.size() == 0) + { + if (rightConst != zero) + { + Assert(childrenRight.back().isConst() + && childrenRight.back().getConst<BitVector>() == rightConst); + if (childrenRight.size() == 1) + { // 0 = c ==> false return utils::mkFalse(); } - // special case - if left is empty and right has a constant, move the constant + // special case - if left is empty and right has a constant, move the + // constant newLeft = utils::mkConst(-rightConst); childrenRight.pop_back(); } - else { - newLeft = utils::mkConst(size, (unsigned)0); + else + { + newLeft = utils::mkConst(size, (unsigned)0); } } - else if (childrenLeft.size() == 1) { - newLeft = childrenLeft[0]; - } - else { - newLeft = utils::mkNode(kind::BITVECTOR_PLUS, childrenLeft); + else + { + newLeft = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenLeft); } - if (childrenRight.size() == 0) { + if (childrenRight.size() == 0) + { newRight = utils::mkConst(size, (unsigned)0); } - else if (childrenRight.size() == 1) { - newRight = childrenRight[0]; - } - else { - newRight = utils::mkNode(kind::BITVECTOR_PLUS, childrenRight); + else + { + newRight = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenRight); } // Assert(newLeft == Rewriter::rewrite(newLeft)); // Assert(newRight == Rewriter::rewrite(newRight)); - if (newLeft == newRight) { - Assert (newLeft == utils::mkConst(size, (unsigned)0)); + if (newLeft == newRight) + { + Assert(newLeft == utils::mkConst(size, (unsigned)0)); return utils::mkTrue(); } - if (newLeft < newRight) { - Assert((newRight == left && newLeft == right) || - Rewriter::rewrite(newRight) != left || - Rewriter::rewrite(newLeft) != right); + if (newLeft < newRight) + { + Assert((newRight == left && newLeft == right) + || Rewriter::rewrite(newRight) != left + || Rewriter::rewrite(newLeft) != right); return newRight.eqNode(newLeft); } - - Assert((newLeft == left && newRight == right) || - Rewriter::rewrite(newLeft) != left || - Rewriter::rewrite(newRight) != right); + + Assert((newLeft == left && newRight == right) + || Rewriter::rewrite(newLeft) != left + || Rewriter::rewrite(newRight) != right); return newLeft.eqNode(newRight); } - template<> inline bool RewriteRule<BitwiseEq>::applies(TNode node) { if (node.getKind() != kind::EQUAL || @@ -901,10 +981,12 @@ bool RewriteRule<NegSub>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_SUB); } -template<> inline -Node RewriteRule<NegSub>::apply(TNode node) { +template <> +inline Node RewriteRule<NegSub>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl; - return utils::mkNode(kind::BITVECTOR_SUB, node[0][1], node[0][0]); + return NodeManager::currentNM()->mkNode( + kind::BITVECTOR_SUB, node[0][1], node[0][0]); } template<> inline @@ -913,19 +995,19 @@ bool RewriteRule<NegPlus>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_PLUS); } -template<> inline -Node RewriteRule<NegPlus>::apply(TNode node) { +template <> +inline Node RewriteRule<NegPlus>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl; + NodeManager *nm = NodeManager::currentNM(); std::vector<Node> children; - for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { - children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i])); + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) + { + children.push_back(nm->mkNode(kind::BITVECTOR_NEG, node[0][i])); } - return utils::mkNode(kind::BITVECTOR_PLUS, children); + return utils::mkNaryNode(kind::BITVECTOR_PLUS, children); } - - - struct Count { unsigned pos; unsigned neg; @@ -954,62 +1036,83 @@ bool RewriteRule<AndSimplify>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_AND); } -template<> inline -Node RewriteRule<AndSimplify>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<AndSimplify>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); // this will remove duplicates std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); - BitVector constant = utils::mkBitVectorOnes(size); - - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + BitVector constant = utils::mkBitVectorOnes(size); + + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { TNode current = node[i]; // simplify constants - if (current.getKind() == kind::CONST_BITVECTOR) { + if (current.getKind() == kind::CONST_BITVECTOR) + { BitVector bv = current.getConst<BitVector>(); constant = constant & bv; - } else { - if (current.getKind() == kind::BITVECTOR_NOT) { + } + else + { + if (current.getKind() == kind::BITVECTOR_NOT) + { insert(subterms, current[0], true); - } else { + } + else + { insert(subterms, current, false); } } } std::vector<Node> children; - - if (constant == BitVector(size, (unsigned)0)) { - return utils::mkZero(size); + + if (constant == BitVector(size, (unsigned)0)) + { + return utils::mkZero(size); } - if (constant != utils::mkBitVectorOnes(size)) { - children.push_back(utils::mkConst(constant)); + if (constant != utils::mkBitVectorOnes(size)) + { + children.push_back(utils::mkConst(constant)); } - - std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); - for (; it != subterms.end(); ++it) { - if (it->second.pos > 0 && it->second.neg > 0) { - // if we have a and ~a - return utils::mkZero(size); - } else { - // idempotence - if (it->second.neg > 0) { + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = + subterms.begin(); + + for (; it != subterms.end(); ++it) + { + if (it->second.pos > 0 && it->second.neg > 0) + { + // if we have a and ~a + return utils::mkZero(size); + } + else + { + // idempotence + if (it->second.neg > 0) + { // if it only occured negated - children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); - } else { + children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first)); + } + else + { // if it only occured positive - children.push_back(it->first); + children.push_back(it->first); } } } - if (children.size() == 0) { - return utils::mkOnes(size); + if (children.size() == 0) + { + return utils::mkOnes(size); } - - return utils::mkSortedNode(kind::BITVECTOR_AND, children); + + return utils::mkSortedNode(kind::BITVECTOR_AND, children); } template<> inline @@ -1062,62 +1165,82 @@ bool RewriteRule<OrSimplify>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_OR); } -template<> inline -Node RewriteRule<OrSimplify>::apply(TNode node) { +template <> +inline Node RewriteRule<OrSimplify>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl; + NodeManager *nm = NodeManager::currentNM(); // this will remove duplicates std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); - BitVector constant(size, (unsigned)0); - - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + BitVector constant(size, (unsigned)0); + + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { TNode current = node[i]; // simplify constants - if (current.getKind() == kind::CONST_BITVECTOR) { + if (current.getKind() == kind::CONST_BITVECTOR) + { BitVector bv = current.getConst<BitVector>(); constant = constant | bv; - } else { - if (current.getKind() == kind::BITVECTOR_NOT) { + } + else + { + if (current.getKind() == kind::BITVECTOR_NOT) + { insert(subterms, current[0], true); - } else { + } + else + { insert(subterms, current, false); } } } std::vector<Node> children; - - if (constant == utils::mkBitVectorOnes(size)) { - return utils::mkOnes(size); + + if (constant == utils::mkBitVectorOnes(size)) + { + return utils::mkOnes(size); } - if (constant != BitVector(size, (unsigned)0)) { - children.push_back(utils::mkConst(constant)); + if (constant != BitVector(size, (unsigned)0)) + { + children.push_back(utils::mkConst(constant)); } - - std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); - for (; it != subterms.end(); ++it) { - if (it->second.pos > 0 && it->second.neg > 0) { - // if we have a or ~a - return utils::mkOnes(size); - } else { - // idempotence - if (it->second.neg > 0) { + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = + subterms.begin(); + + for (; it != subterms.end(); ++it) + { + if (it->second.pos > 0 && it->second.neg > 0) + { + // if we have a or ~a + return utils::mkOnes(size); + } + else + { + // idempotence + if (it->second.neg > 0) + { // if it only occured negated - children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); - } else { + children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first)); + } + else + { // if it only occured positive - children.push_back(it->first); + children.push_back(it->first); } } } - if (children.size() == 0) { - return utils::mkZero(size); + if (children.size() == 0) + { + return utils::mkZero(size); } - return utils::mkSortedNode(kind::BITVECTOR_OR, children); + return utils::mkSortedNode(kind::BITVECTOR_OR, children); } template<> inline @@ -1125,32 +1248,44 @@ bool RewriteRule<XorSimplify>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_XOR); } -template<> inline -Node RewriteRule<XorSimplify>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl; - +template <> +inline Node RewriteRule<XorSimplify>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); - BitVector constant; - bool const_set = false; + BitVector constant; + bool const_set = false; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { TNode current = node[i]; // simplify constants - if (current.getKind() == kind::CONST_BITVECTOR) { + if (current.getKind() == kind::CONST_BITVECTOR) + { BitVector bv = current.getConst<BitVector>(); - if (const_set) { + if (const_set) + { constant = constant ^ bv; - } else { - const_set = true; + } + else + { + const_set = true; constant = bv; } - } else { + } + else + { // collect number of occurances of each term and its negation - if (current.getKind() == kind::BITVECTOR_NOT) { + if (current.getKind() == kind::BITVECTOR_NOT) + { insert(subterms, current[0], true); - } else { + } + else + { insert(subterms, current, false); } } @@ -1158,27 +1293,34 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { std::vector<Node> children; - std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = + subterms.begin(); unsigned true_count = 0; - bool seen_false = false; - for (; it != subterms.end(); ++it) { - unsigned pos = it->second.pos; // number of positive occurances - unsigned neg = it->second.neg; // number of negated occurances + bool seen_false = false; + for (; it != subterms.end(); ++it) + { + unsigned pos = it->second.pos; // number of positive occurances + unsigned neg = it->second.neg; // number of negated occurances // remove duplicates using the following rules // a xor a ==> false // false xor false ==> false - seen_false = seen_false? seen_false : (pos > 1 || neg > 1); + seen_false = seen_false ? seen_false : (pos > 1 || neg > 1); // check what did not reduce - if (pos % 2 && neg % 2) { + if (pos % 2 && neg % 2) + { // we have a xor ~a ==> true ++true_count; - } else if (pos % 2) { + } + else if (pos % 2) + { // we had a positive occurence left - children.push_back(it->first); - } else if (neg % 2) { + children.push_back(it->first); + } + else if (neg % 2) + { // we had a negative occurence left - children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); + children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first)); } // otherwise both reduced to false } @@ -1186,32 +1328,36 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { std::vector<BitVector> xorConst; BitVector true_bv = utils::mkBitVectorOnes(size); BitVector false_bv(size, (unsigned)0); - - if (true_count) { + + if (true_count) + { // true xor ... xor true ==> true (odd) - // ==> false (even) - xorConst.push_back(true_count % 2? true_bv : false_bv); + // ==> false (even) + xorConst.push_back(true_count % 2 ? true_bv : false_bv); } - if (seen_false) { - xorConst.push_back(false_bv); + if (seen_false) + { + xorConst.push_back(false_bv); } - if(const_set) { - xorConst.push_back(constant); + if (const_set) + { + xorConst.push_back(constant); } - if (xorConst.size() > 0) { + if (xorConst.size() > 0) + { BitVector result = xorConst[0]; - for (unsigned i = 1; i < xorConst.size(); ++i) { - result = result ^ xorConst[i]; + for (unsigned i = 1; i < xorConst.size(); ++i) + { + result = result ^ xorConst[i]; } - children.push_back(utils::mkConst(result)); + children.push_back(utils::mkConst(result)); } Assert(children.size()); - - return utils::mkSortedNode(kind::BITVECTOR_XOR, children); -} + return utils::mkSortedNode(kind::BITVECTOR_XOR, children); +} /** * BitwiseSlicing @@ -1247,48 +1393,61 @@ bool RewriteRule<BitwiseSlicing>::applies(TNode node) { return false; } -template<> inline -Node RewriteRule<BitwiseSlicing>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<BitwiseSlicing>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); // get the constant - bool found_constant = false ; + bool found_constant = false; TNode constant; - std::vector<Node> other_children; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - if (node[i].getKind() == kind::CONST_BITVECTOR && !found_constant) { + std::vector<Node> other_children; + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + if (node[i].getKind() == kind::CONST_BITVECTOR && !found_constant) + { constant = node[i]; - found_constant = true; - } else { - other_children.push_back(node[i]); + found_constant = true; + } + else + { + other_children.push_back(node[i]); } } - Assert (found_constant && other_children.size() == node.getNumChildren() - 1); + Assert(found_constant && other_children.size() == node.getNumChildren() - 1); + + Node other = utils::mkNaryNode(node.getKind(), other_children); - Node other = utils::mkNode(node.getKind(), other_children); - BitVector bv_constant = constant.getConst<BitVector>(); - std::vector<Node> concat_children; + std::vector<Node> concat_children; int start = bv_constant.getSize() - 1; int end = start; - for (int i = end - 1; i >= 0; --i) { - if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i)) { + for (int i = end - 1; i >= 0; --i) + { + if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i)) + { Node other_extract = utils::mkExtract(other, end, start); Node const_extract = utils::mkExtract(constant, end, start); - Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + Node bitwise_op = + nm->mkNode(node.getKind(), const_extract, other_extract); concat_children.push_back(bitwise_op); - start = end = i; - } else { - start--; + start = end = i; } - if (i == 0) { + else + { + start--; + } + if (i == 0) + { Node other_extract = utils::mkExtract(other, end, 0); Node const_extract = utils::mkExtract(constant, end, 0); - Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + Node bitwise_op = + nm->mkNode(node.getKind(), const_extract, other_extract); concat_children.push_back(bitwise_op); } - } - Node result = utils::mkNode(kind::BITVECTOR_CONCAT, concat_children); + Node result = utils::mkConcat(concat_children); Debug("bv-rewrite") << " =>" << result << std::endl; return result; } diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 4877da1d1..575a40aff 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -2,9 +2,9 @@ /*! \file theory_bv_rewrite_rules_operator_elimination.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Clark Barrett, Morgan Deters + ** Liana Hadarean, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -31,57 +31,62 @@ bool RewriteRule<UgtEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_UGT); } -template<> -Node RewriteRule<UgtEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<UgtEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" + << std::endl; TNode a = node[0]; TNode b = node[1]; - Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a); + Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a); return result; } - template<> bool RewriteRule<UgeEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_UGE); } -template<> -Node RewriteRule<UgeEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<UgeEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" + << std::endl; TNode a = node[0]; TNode b = node[1]; - Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a); + Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a); return result; } - template<> bool RewriteRule<SgtEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SGT); } -template<> -Node RewriteRule<SgtEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<SgtEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" + << std::endl; TNode a = node[0]; TNode b = node[1]; - Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a); + Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_SLT, b, a); return result; } - template<> bool RewriteRule<SgeEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SGE); } -template<> -Node RewriteRule<SgeEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<SgeEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" + << std::endl; TNode a = node[0]; TNode b = node[1]; - Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a); + Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_SLE, b, a); return result; } @@ -91,17 +96,18 @@ bool RewriteRule<SltEliminate>::applies(TNode node) { } template <> -Node RewriteRule<SltEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl; - +Node RewriteRule<SltEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); unsigned size = utils::getSize(node[0]); Integer val = Integer(1).multiplyByPow2(size - 1); Node pow_two = utils::mkConst(size, val); - Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); - Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); - - return utils::mkNode(kind::BITVECTOR_ULT, a, b); - + Node a = nm->mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); + Node b = nm->mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); + + return nm->mkNode(kind::BITVECTOR_ULT, a, b); } template <> @@ -110,13 +116,15 @@ bool RewriteRule<SleEliminate>::applies(TNode node) { } template <> -Node RewriteRule<SleEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl; - +Node RewriteRule<SleEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; TNode b = node[1]; - Node b_slt_a = utils::mkNode(kind::BITVECTOR_SLT, b, a); - return utils::mkNode(kind::NOT, b_slt_a); + Node b_slt_a = nm->mkNode(kind::BITVECTOR_SLT, b, a); + return nm->mkNode(kind::NOT, b_slt_a); } template <> @@ -125,29 +133,33 @@ bool RewriteRule<UleEliminate>::applies(TNode node) { } template <> -Node RewriteRule<UleEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")" << std::endl; - +Node RewriteRule<UleEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; TNode b = node[1]; - Node b_ult_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); - return utils::mkNode(kind::NOT, b_ult_a); + Node b_ult_a = nm->mkNode(kind::BITVECTOR_ULT, b, a); + return nm->mkNode(kind::NOT, b_ult_a); } - template <> bool RewriteRule<CompEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_COMP); } template <> -Node RewriteRule<CompEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl; - Node comp = utils::mkNode(kind::EQUAL, node[0], node[1]); +Node RewriteRule<CompEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); + Node comp = nm->mkNode(kind::EQUAL, node[0], node[1]); Node one = utils::mkConst(1, 1); - Node zero = utils::mkConst(1, 0); + Node zero = utils::mkConst(1, 0); - return utils::mkNode(kind::ITE, comp, one, zero); + return nm->mkNode(kind::ITE, comp, one, zero); } template <> @@ -156,15 +168,17 @@ bool RewriteRule<SubEliminate>::applies(TNode node) { } template <> -Node RewriteRule<SubEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl; - Node negb = utils::mkNode(kind::BITVECTOR_NEG, node[1]); +Node RewriteRule<SubEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); + Node negb = nm->mkNode(kind::BITVECTOR_NEG, node[1]); Node a = node[0]; - return utils::mkNode(kind::BITVECTOR_PLUS, a, negb); + return nm->mkNode(kind::BITVECTOR_PLUS, a, negb); } - template<> bool RewriteRule<RepeatEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_REPEAT); @@ -296,29 +310,35 @@ bool RewriteRule<NandEliminate>::applies(TNode node) { node.getNumChildren() == 2); } -template<> -Node RewriteRule<NandEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<NandEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; - TNode b = node[1]; - Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b); - Node result = utils::mkNode(kind::BITVECTOR_NOT, andNode); + TNode b = node[1]; + Node andNode = nm->mkNode(kind::BITVECTOR_AND, a, b); + Node result = nm->mkNode(kind::BITVECTOR_NOT, andNode); return result; } -template<> -bool RewriteRule<NorEliminate>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_NOR && - node.getNumChildren() == 2); +template <> +bool RewriteRule<NorEliminate>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_NOR && node.getNumChildren() == 2); } -template<> -Node RewriteRule<NorEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<NorEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; - TNode b = node[1]; - Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b); - Node result = utils::mkNode(kind::BITVECTOR_NOT, orNode); + TNode b = node[1]; + Node orNode = nm->mkNode(kind::BITVECTOR_OR, a, b); + Node result = nm->mkNode(kind::BITVECTOR_NOT, orNode); return result; } @@ -328,68 +348,91 @@ bool RewriteRule<XnorEliminate>::applies(TNode node) { node.getNumChildren() == 2); } -template<> -Node RewriteRule<XnorEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<XnorEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; - TNode b = node[1]; - Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b); - Node result = utils::mkNode(kind::BITVECTOR_NOT, xorNode); + TNode b = node[1]; + Node xorNode = nm->mkNode(kind::BITVECTOR_XOR, a, b); + Node result = nm->mkNode(kind::BITVECTOR_NOT, xorNode); return result; } - template<> bool RewriteRule<SdivEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SDIV); } -template<> -Node RewriteRule<SdivEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<SdivEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; TNode b = node[1]; unsigned size = utils::getSize(a); - - Node one = utils::mkConst(1, 1); - Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one); - Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); - Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); - Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - - Node a_udiv_b = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b); - Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b); - - Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0); - Node result = utils::mkNode(kind::ITE, condition, neg_result, a_udiv_b); - + + Node one = utils::mkConst(1, 1); + Node a_lt_0 = + nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one); + Node b_lt_0 = + nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one); + Node abs_a = + nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = + nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); + + Node a_udiv_b = + nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL + : kind::BITVECTOR_UDIV, + abs_a, + abs_b); + Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); + + Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0); + Node result = nm->mkNode(kind::ITE, condition, neg_result, a_udiv_b); + return result; } - template<> bool RewriteRule<SremEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SREM); } -template<> -Node RewriteRule<SremEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<SremEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode a = node[0]; TNode b = node[1]; unsigned size = utils::getSize(a); - - Node one = utils::mkConst(1, 1); - Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one); - Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); - Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); - Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - - Node a_urem_b = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b); - Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b); - - Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); + + Node one = utils::mkConst(1, 1); + Node a_lt_0 = + nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one); + Node b_lt_0 = + nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one); + Node abs_a = + nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = + nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); + + Node a_urem_b = + nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL + : kind::BITVECTOR_UREM, + abs_a, + abs_b); + Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); + + Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); return result; } @@ -399,13 +442,16 @@ bool RewriteRule<SmodEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SMOD); } -template<> -Node RewriteRule<SmodEliminate>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl; +template <> +Node RewriteRule<SmodEliminate>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode s = node[0]; TNode t = node[1]; unsigned size = utils::getSize(s); - + // (bvsmod s t) abbreviates // (let ((?msb_s ((_ extract |m-1| |m-1|) s)) // (?msb_t ((_ extract |m-1| |m-1|) t))) @@ -422,33 +468,36 @@ Node RewriteRule<SmodEliminate>::apply(TNode node) { // (bvadd u t) // (bvneg u)))))))) - Node msb_s = utils::mkExtract(s, size-1, size-1); - Node msb_t = utils::mkExtract(t, size-1, size-1); + Node msb_s = utils::mkExtract(s, size - 1, size - 1); + Node msb_t = utils::mkExtract(t, size - 1, size - 1); - Node bit1 = utils::mkConst(1, 1); - Node bit0 = utils::mkConst(1, 0); + Node bit1 = utils::mkConst(1, 1); + Node bit0 = utils::mkConst(1, 0); - Node abs_s = msb_s.eqNode(bit0).iteNode(s, utils::mkNode(kind::BITVECTOR_NEG, s)); - Node abs_t = msb_t.eqNode(bit0).iteNode(t, utils::mkNode(kind::BITVECTOR_NEG, t)); + Node abs_s = + msb_s.eqNode(bit0).iteNode(s, nm->mkNode(kind::BITVECTOR_NEG, s)); + Node abs_t = + msb_t.eqNode(bit0).iteNode(t, nm->mkNode(kind::BITVECTOR_NEG, t)); - Node u = utils::mkNode(kind::BITVECTOR_UREM, abs_s, abs_t); - Node neg_u = utils::mkNode(kind::BITVECTOR_NEG, u); + Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t); + Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u); Node cond0 = u.eqNode(utils::mkConst(size, 0)); Node cond1 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit0)); Node cond2 = msb_s.eqNode(bit1).andNode(msb_t.eqNode(bit0)); Node cond3 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit1)); - Node result = cond0.iteNode(u, - cond1.iteNode(u, - cond2.iteNode(utils::mkNode(kind::BITVECTOR_PLUS, neg_u, t), - cond3.iteNode(utils::mkNode(kind::BITVECTOR_PLUS, u, t), neg_u)))); + Node result = cond0.iteNode( + u, + cond1.iteNode( + u, + cond2.iteNode( + nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t), + cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u)))); return result; - } - template<> bool RewriteRule<ZeroExtendEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index fb083c568..169b28e34 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -2,9 +2,9 @@ /*! \file theory_bv_rewrite_rules_simplification.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Clark Barrett, Tim King + ** Liana Hadarean, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -324,30 +324,36 @@ bool RewriteRule<XorOne>::applies(TNode node) { return false; } -template<> inline -Node RewriteRule<XorOne>::apply(TNode node) { +template <> +inline Node RewriteRule<XorOne>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl; - Node ones = utils::mkOnes(utils::getSize(node)); + NodeManager *nm = NodeManager::currentNM(); + Node ones = utils::mkOnes(utils::getSize(node)); std::vector<Node> children; bool found_ones = false; // XorSimplify should have been called before - for(unsigned i = 0; i < node.getNumChildren(); ++i) { - if (node[i] == ones) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + if (node[i] == ones) + { // make sure only ones occurs only once found_ones = !found_ones; - } else { - children.push_back(node[i]); + } + else + { + children.push_back(node[i]); } } - Node result = utils::mkNode(kind::BITVECTOR_XOR, children); - if (found_ones) { - result = utils::mkNode(kind::BITVECTOR_NOT, result); + Node result = utils::mkNaryNode(kind::BITVECTOR_XOR, children); + if (found_ones) + { + result = nm->mkNode(kind::BITVECTOR_NOT, result); } return result; } - /** * XorZero * @@ -368,23 +374,25 @@ bool RewriteRule<XorZero>::applies(TNode node) { return false; } -template<> inline -Node RewriteRule<XorZero>::apply(TNode node) { +template <> +inline Node RewriteRule<XorZero>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl; std::vector<Node> children; Node zero = utils::mkConst(utils::getSize(node), 0); - + // XorSimplify should have been called before - for(unsigned i = 0; i < node.getNumChildren(); ++i) { - if (node[i] != zero) { - children.push_back(node[i]); + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + if (node[i] != zero) + { + children.push_back(node[i]); } } - Node res = utils::mkNode(kind::BITVECTOR_XOR, children); + Node res = utils::mkNaryNode(kind::BITVECTOR_XOR, children); return res; } - /** * BitwiseNotAnd * @@ -441,13 +449,14 @@ bool RewriteRule<XorNot>::applies(TNode node) { Unreachable(); } -template<> inline -Node RewriteRule<XorNot>::apply(TNode node) { +template <> +inline Node RewriteRule<XorNot>::apply(TNode node) +{ Unreachable(); Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl; Node a = node[0][0]; - Node b = node[1][0]; - return utils::mkNode(kind::BITVECTOR_XOR, a, b); + Node b = node[1][0]; + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, a, b); } /** @@ -462,13 +471,16 @@ bool RewriteRule<NotXor>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_XOR); } -template<> inline -Node RewriteRule<NotXor>::apply(TNode node) { +template <> +inline Node RewriteRule<NotXor>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl; std::vector<Node> children; TNode::iterator child_it = node[0].begin(); - children.push_back(utils::mkNode(kind::BITVECTOR_NOT, *child_it)); - for(++child_it; child_it != node[0].end(); ++child_it) { + children.push_back( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *child_it)); + for (++child_it; child_it != node[0].end(); ++child_it) + { children.push_back(*child_it); } return utils::mkSortedNode(kind::BITVECTOR_XOR, children); @@ -538,19 +550,21 @@ Node RewriteRule<LteSelf>::apply(TNode node) { * 0 < a ==> a != 0 */ -template<> inline -bool RewriteRule<ZeroUlt>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_ULT && - node[0] == utils::mkZero(utils::getSize(node[0]))); +template <> +inline bool RewriteRule<ZeroUlt>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ULT + && node[0] == utils::mkZero(utils::getSize(node[0]))); } -template<> inline -Node RewriteRule<ZeroUlt>::apply(TNode node) { +template <> +inline Node RewriteRule<ZeroUlt>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl; - return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1])); + NodeManager *nm = NodeManager::currentNM(); + return nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, node[0], node[1])); } - /** * UltZero * @@ -579,10 +593,11 @@ bool RewriteRule<UltOne>::applies(TNode node) { node[1] == utils::mkOne(utils::getSize(node[0]))); } -template<> inline -Node RewriteRule<UltOne>::apply(TNode node) { +template <> +inline Node RewriteRule<UltOne>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl; - return utils::mkNode( + return NodeManager::currentNM()->mkNode( kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0]))); } @@ -595,15 +610,16 @@ bool RewriteRule<SltZero>::applies(TNode node) { node[1] == utils::mkZero(utils::getSize(node[0]))); } -template<> inline -Node RewriteRule<SltZero>::apply(TNode node) { +template <> +inline Node RewriteRule<SltZero>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl; - unsigned size = utils::getSize(node[0]); + unsigned size = utils::getSize(node[0]); Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1); - return utils::mkNode(kind::EQUAL, most_significant_bit, utils::mkOne(1)); + return NodeManager::currentNM()->mkNode( + kind::EQUAL, most_significant_bit, utils::mkOne(1)); } - /** * UltSelf * @@ -635,10 +651,11 @@ bool RewriteRule<UleZero>::applies(TNode node) { node[1] == utils::mkZero(utils::getSize(node[0]))); } -template<> inline -Node RewriteRule<UleZero>::apply(TNode node) { +template <> +inline Node RewriteRule<UleZero>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl; - return utils::mkNode(kind::EQUAL, node[0], node[1]); + return NodeManager::currentNM()->mkNode(kind::EQUAL, node[0], node[1]); } /** @@ -712,13 +729,14 @@ bool RewriteRule<NotUlt>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_ULT); } -template<> inline -Node RewriteRule<NotUlt>::apply(TNode node) { +template <> +inline Node RewriteRule<NotUlt>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl; Node ult = node[0]; Node a = ult[0]; - Node b = ult[1]; - return utils::mkNode(kind::BITVECTOR_ULE, b, a); + Node b = ult[1]; + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a); } /** @@ -733,13 +751,14 @@ bool RewriteRule<NotUle>::applies(TNode node) { node[0].getKind() == kind::BITVECTOR_ULE); } -template<> inline -Node RewriteRule<NotUle>::apply(TNode node) { +template <> +inline Node RewriteRule<NotUle>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl; Node ult = node[0]; Node a = ult[0]; - Node b = ult[1]; - return utils::mkNode(kind::BITVECTOR_ULT, b, a); + Node b = ult[1]; + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a); } /** @@ -769,7 +788,7 @@ template <> inline Node RewriteRule<MultPow2>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl; - + NodeManager *nm = NodeManager::currentNM(); unsigned size = utils::getSize(node); std::vector<Node> children; unsigned exponent = 0; @@ -797,12 +816,12 @@ inline Node RewriteRule<MultPow2>::apply(TNode node) } else { - a = utils::mkNode(kind::BITVECTOR_MULT, children); + a = utils::mkNaryNode(kind::BITVECTOR_MULT, children); } if (isNeg && size > 1) { - a = utils::mkNode(kind::BITVECTOR_NEG, a); + a = nm->mkNode(kind::BITVECTOR_NEG, a); } Node extract = utils::mkExtract(a, size - exponent - 1, 0); @@ -877,10 +896,10 @@ Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) { // Node extract2 = utils::mkExtract(node[1], k - 1, 0); // Node k_zeroes = utils::mkConst(n - k, 0u); - // Node new_mult = utils::mkNode(kind::BITVECTOR_MULT, extract1, extract2); - // Node result = utils::mkExtract(utils::mkNode(kind::BITVECTOR_CONCAT, k_zeroes, new_mult), - // high, low); - + // NodeManager *nm = NodeManager::currentNM(); + // Node new_mult = nm->mkNode(kind::BITVECTOR_MULT, extract1, extract2); + // Node result = utils::mkExtract(nm->mkNode(kind::BITVECTOR_CONCAT, k_zeroes, new_mult), high, low); + // since the extract is over multiplier bits that have to be 0, return 0 Node result = utils::mkConst(bitwidth, 0u); // std::cout << "MultLeadingBit " << node <<" => " << result <<"\n"; @@ -927,6 +946,7 @@ template <> inline Node RewriteRule<UdivPow2>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl; + NodeManager *nm = NodeManager::currentNM(); unsigned size = utils::getSize(node); Node a = node[0]; bool isNeg = false; @@ -941,11 +961,11 @@ inline Node RewriteRule<UdivPow2>::apply(TNode node) Node extract = utils::mkExtract(a, size - 1, power); Node zeros = utils::mkConst(power, 0); - ret = utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract); + ret = nm->mkNode(kind::BITVECTOR_CONCAT, zeros, extract); } if (isNeg && size > 1) { - ret = utils::mkNode(kind::BITVECTOR_NEG, ret); + ret = nm->mkNode(kind::BITVECTOR_NEG, ret); } return ret; } @@ -1020,7 +1040,8 @@ inline Node RewriteRule<UremPow2>::apply(TNode node) { Node extract = utils::mkExtract(a, power - 1, 0); Node zeros = utils::mkZero(utils::getSize(node) - power); - ret = utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract); + ret = NodeManager::currentNM()->mkNode( + kind::BITVECTOR_CONCAT, zeros, extract); } return ret; } @@ -1103,24 +1124,29 @@ bool RewriteRule<BBPlusNeg>::applies(TNode node) { return neg_count > 1; } -template<> inline -Node RewriteRule<BBPlusNeg>::apply(TNode node) { +template <> +inline Node RewriteRule<BBPlusNeg>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl; - + NodeManager *nm = NodeManager::currentNM(); std::vector<Node> children; - unsigned neg_count = 0; - for(unsigned i = 0; i < node.getNumChildren(); ++i) { - if (node[i].getKind() == kind::BITVECTOR_NEG) { - ++neg_count; - children.push_back(utils::mkNode(kind::BITVECTOR_NOT, node[i][0])); - } else { - children.push_back(node[i]); + unsigned neg_count = 0; + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + if (node[i].getKind() == kind::BITVECTOR_NEG) + { + ++neg_count; + children.push_back(nm->mkNode(kind::BITVECTOR_NOT, node[i][0])); + } + else + { + children.push_back(node[i]); } } - Assert(neg_count!= 0); - children.push_back(utils::mkConst(utils::getSize(node), neg_count)); + Assert(neg_count != 0); + children.push_back(utils::mkConst(utils::getSize(node), neg_count)); - return utils::mkNode(kind::BITVECTOR_PLUS, children); + return utils::mkNaryNode(kind::BITVECTOR_PLUS, children); } template<> inline @@ -1376,29 +1402,31 @@ bool RewriteRule<MultSlice>::applies(TNode node) { * * @return */ -template<> inline -Node RewriteRule<MultSlice>::apply(TNode node) { +template <> +inline Node RewriteRule<MultSlice>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<MultSlice>(" << node << ")" << std::endl; + NodeManager *nm = NodeManager::currentNM(); unsigned bitwidth = utils::getSize(node[0]); - Node zeros = utils::mkConst(bitwidth/2, 0); + Node zeros = utils::mkConst(bitwidth / 2, 0); TNode a = node[0]; - Node bottom_a = utils::mkExtract(a, bitwidth/2 - 1, 0); - Node top_a = utils::mkExtract(a, bitwidth -1, bitwidth/2); + Node bottom_a = utils::mkExtract(a, bitwidth / 2 - 1, 0); + Node top_a = utils::mkExtract(a, bitwidth - 1, bitwidth / 2); TNode b = node[1]; - Node bottom_b = utils::mkExtract(b, bitwidth/2 - 1, 0); - Node top_b = utils::mkExtract(b, bitwidth -1, bitwidth/2); + Node bottom_b = utils::mkExtract(b, bitwidth / 2 - 1, 0); + Node top_b = utils::mkExtract(b, bitwidth - 1, bitwidth / 2); - Node term1 = utils::mkNode(kind::BITVECTOR_MULT, - utils::mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_a), - utils::mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_b)); + Node term1 = nm->mkNode(kind::BITVECTOR_MULT, + nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_a), + nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_b)); - Node term2 = utils::mkNode(kind::BITVECTOR_CONCAT, - utils::mkNode(kind::BITVECTOR_MULT, top_b, bottom_a), - zeros); - Node term3 = utils::mkNode(kind::BITVECTOR_CONCAT, - utils::mkNode(kind::BITVECTOR_MULT, top_a, bottom_b), - zeros); - return utils::mkNode(kind::BITVECTOR_PLUS, term1, term2, term3); + Node term2 = nm->mkNode(kind::BITVECTOR_CONCAT, + nm->mkNode(kind::BITVECTOR_MULT, top_b, bottom_a), + zeros); + Node term3 = nm->mkNode(kind::BITVECTOR_CONCAT, + nm->mkNode(kind::BITVECTOR_MULT, top_a, bottom_b), + zeros); + return nm->mkNode(kind::BITVECTOR_PLUS, term1, term2, term3); } /** @@ -1430,16 +1458,20 @@ bool RewriteRule<UltPlusOne>::applies(TNode node) { return true; } -template<> inline -Node RewriteRule<UltPlusOne>::apply(TNode node) { +template <> +inline Node RewriteRule<UltPlusOne>::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl; + NodeManager *nm = NodeManager::currentNM(); TNode x = node[0]; TNode y1 = node[1]; TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1]; - unsigned size = utils::getSize(x); - Node not_y_eq_1 = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, y, utils::mkOnes(size))); - Node not_y_lt_x = utils::mkNode(kind::NOT, utils::mkNode(kind::BITVECTOR_ULT, y, x)); - return utils::mkNode(kind::AND, not_y_eq_1, not_y_lt_x); + unsigned size = utils::getSize(x); + Node not_y_eq_1 = + nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, y, utils::mkOnes(size))); + Node not_y_lt_x = + nm->mkNode(kind::NOT, nm->mkNode(kind::BITVECTOR_ULT, y, x)); + return nm->mkNode(kind::AND, not_y_eq_1, not_y_lt_x); } /** @@ -1467,24 +1499,28 @@ bool RewriteRule<IsPowerOfTwo>::applies(TNode node) { TNode b = t[1]; unsigned size = utils::getSize(t); if(size < 2) return false; - Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b)); + Node diff = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b)); return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size))); } -template<> inline -Node RewriteRule<IsPowerOfTwo>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")" << std::endl; - TNode term = utils::isZero(node[0])? node[1] : node[0]; +template <> +inline Node RewriteRule<IsPowerOfTwo>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")" + << std::endl; + NodeManager *nm = NodeManager::currentNM(); + TNode term = utils::isZero(node[0]) ? node[1] : node[0]; TNode a = term[0]; TNode b = term[1]; - unsigned size = utils::getSize(term); - Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b)); - Assert (diff.isConst()); + unsigned size = utils::getSize(term); + Node diff = Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b)); + Assert(diff.isConst()); TNode x = diff == utils::mkConst(size, 1u) ? a : b; Node one = utils::mkConst(size, 1u); Node sk = utils::mkVar(size); - Node sh = utils::mkNode(kind::BITVECTOR_SHL, one, sk); - Node x_eq_sh = utils::mkNode(kind::EQUAL, x, sh); + Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk); + Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh); return x_eq_sh; } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index affdd05bb..acd3beee3 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -282,33 +282,6 @@ Node mkVar(unsigned size) /* ------------------------------------------------------------------------- */ -Node mkNode(Kind kind, TNode child) -{ - return NodeManager::currentNM()->mkNode(kind, child); -} - -Node mkNode(Kind kind, TNode child1, TNode child2) -{ - return NodeManager::currentNM()->mkNode(kind, child1, child2); -} - -Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) -{ - return NodeManager::currentNM()->mkNode(kind, child1, child2, child3); -} - -Node mkNode(Kind kind, std::vector<Node>& children) -{ - Assert(children.size() > 0); - if (children.size() == 1) - { - return children[0]; - } - return NodeManager::currentNM()->mkNode(kind, children); -} - -/* ------------------------------------------------------------------------- */ - Node mkSortedNode(Kind kind, TNode child1, TNode child2) { Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 727f5040f..54b0cedab 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -96,17 +96,29 @@ Node mkConst(const BitVector& value); /* Create bit-vector variable. */ Node mkVar(unsigned size); -/* Create n-ary node of given kind. */ -Node mkNode(Kind kind, TNode child); -Node mkNode(Kind kind, TNode child1, TNode child2); -Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); -Node mkNode(Kind kind, std::vector<Node>& children); - /* Create n-ary bit-vector node of kind BITVECTOR_AND, BITVECTOR_OR or * BITVECTOR_XOR where its children are sorted */ Node mkSortedNode(Kind kind, TNode child1, TNode child2); Node mkSortedNode(Kind kind, std::vector<Node>& children); +/* Create n-ary node of associative/commutative kind. */ +template<bool ref_count> +Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes) +{ + Assert (k == kind::AND + || k == kind::OR + || k == kind::XOR + || k == kind::BITVECTOR_AND + || k == kind::BITVECTOR_OR + || k == kind::BITVECTOR_XOR + || k == kind::BITVECTOR_PLUS + || k == kind::BITVECTOR_SUB + || k == kind::BITVECTOR_MULT); + + if (nodes.size() == 1) { return nodes[0]; } + return NodeManager::currentNM()->mkNode(k, nodes); +} + /* Create node of kind NOT. */ Node mkNot(Node child); /* Create node of kind AND. */ |