/*! \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
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
return d_funcToSignature.size() != 0;
}
-
bool AbstractionModule::isConjunctionOfAtoms(TNode node) {
TNodeSet seen;
return isConjunctionOfAtomsRec(node, 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;
}
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];
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
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) {
}
}
-
-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
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;
/*! \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
}
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 "
}
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);
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);
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);
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";
}
}
/*! \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
}
}
-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) {
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";
}
}
/*! \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
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) {
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());
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;
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;
}
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());
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;
}
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;
}
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;
}
}
void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) {
+ NodeManager* nm = NodeManager::currentNM();
bool changed = true;
while(changed) {
// d_bv->spendResource();
}
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);
/*! \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
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);
}
// 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;
}
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;
}
/*! \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
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;
// }
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;
// }
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;
}
}
}
}
-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;
/*! \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
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;
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:
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;
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) {
/*! \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
* @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;
}
? 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) {
/*! \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
* @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) {
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);
}
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);
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();
}
}
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;
/*! \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
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);
}
}
-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);
}
}
d_out->conflict(assertions[0]);
return;
}
- Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions);
+ Node conflict = utils::mkAnd(assertions);
d_out->conflict(conflict);
return;
}
}
}
-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;
}
}
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;
}
}
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);
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);
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;
}
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);
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
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;
}
}
}
-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;
/*! \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
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);
}
/**
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
*
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);
}
/**
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
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);
}
}
}
}
-
-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)
{
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);
}
}
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 ||
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
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
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 ||
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];
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;
}
}
- // 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 ||
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
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;
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
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
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);
}
}
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
}
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
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;
}
/*! \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
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;
}
}
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 <>
}
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 <>
}
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 <>
}
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);
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;
}
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;
}
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)))
// (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);
/*! \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
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
*
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
*
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);
}
/**
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);
* 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
*
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])));
}
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
*
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]);
}
/**
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);
}
/**
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);
}
/**
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;
}
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);
// 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";
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;
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;
}
{
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;
}
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
*
* @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);
}
/**
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);
}
/**
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;
}
/* ------------------------------------------------------------------------- */
-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
/* 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. */
projects / cvc5.git / commitdiff