diff options
Diffstat (limited to 'src/theory/bv/abstraction.cpp')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 265 |
1 files changed, 166 insertions, 99 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 4ef484594..a36ec2e16 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -2,9 +2,9 @@ /*! \file abstraction.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Guy Katz, Tim King + ** Liana Hadarean, Aina Niemetz, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -29,57 +29,74 @@ using namespace CVC4::context; using namespace std; using namespace CVC4::theory::bv::utils; -bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { +bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, + std::vector<Node>& new_assertions) +{ Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n"; TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime); - for (unsigned i = 0; i < assertions.size(); ++i) { - if (assertions[i].getKind() == kind::OR) { - for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { - if (!isConjunctionOfAtoms(assertions[i][j])) { + for (unsigned i = 0; i < assertions.size(); ++i) + { + if (assertions[i].getKind() == kind::OR) + { + for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) + { + if (!isConjunctionOfAtoms(assertions[i][j])) + { continue; } Node signature = computeSignature(assertions[i][j]); storeSignature(signature, assertions[i][j]); - Debug("bv-abstraction") << " assertion: " << assertions[i][j] <<"\n"; - Debug("bv-abstraction") << " signature: " << signature <<"\n"; + Debug("bv-abstraction") << " assertion: " << assertions[i][j] << "\n"; + Debug("bv-abstraction") << " signature: " << signature << "\n"; } } } finalizeSignatures(); - for (unsigned i = 0; i < assertions.size(); ++i) { - if (assertions[i].getKind() == kind::OR && - assertions[i][0].getKind() == kind::AND) { + for (unsigned i = 0; i < assertions.size(); ++i) + { + if (assertions[i].getKind() == kind::OR + && assertions[i][0].getKind() == kind::AND) + { std::vector<Node> new_children; - for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { - if (hasSignature(assertions[i][j])) { + for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) + { + if (hasSignature(assertions[i][j])) + { new_children.push_back(abstractSignatures(assertions[i][j])); - } else { + } + else + { new_children.push_back(assertions[i][j]); } } - new_assertions.push_back(utils::mkNode(kind::OR, new_children)); - } else { + new_assertions.push_back(utils::mkOr(new_children)); + } + else + { // assertions that are not changed new_assertions.push_back(assertions[i]); } } - if (options::skolemizeArguments()) { + if (options::skolemizeArguments()) + { skolemizeArguments(new_assertions); } - // if we are using the eager solver reverse the abstraction - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - if (d_funcToSignature.size() == 0) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + { + if (d_funcToSignature.size() == 0) + { // we did not change anything return false; } NodeNodeMap seen; - for (unsigned i = 0; i < new_assertions.size(); ++i) { + for (unsigned i = 0; i < new_assertions.size(); ++i) + { new_assertions[i] = reverseAbstraction(new_assertions[i], seen); } // we undo the abstraction functions so the logic is QF_BV still @@ -90,7 +107,6 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st return d_funcToSignature.size() != 0; } - bool AbstractionModule::isConjunctionOfAtoms(TNode node) { TNodeSet seen; return isConjunctionOfAtomsRec(node, seen); @@ -146,83 +162,98 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) { return res; } -void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) { - for (unsigned i = 0; i < assertions.size(); ++i) { +void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) +{ + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < assertions.size(); ++i) + { TNode assertion = assertions[i]; - if (assertion.getKind() != kind::OR) - continue; + if (assertion.getKind() != kind::OR) continue; bool is_skolemizable = true; - for (unsigned k = 0; k < assertion.getNumChildren(); ++k) { - if (assertion[k].getKind() != kind::EQUAL || - assertion[k][0].getKind() != kind::APPLY_UF || - assertion[k][1].getKind() != kind::CONST_BITVECTOR || - assertion[k][1].getConst<BitVector>() != BitVector(1, 1u)) { + for (unsigned k = 0; k < assertion.getNumChildren(); ++k) + { + if (assertion[k].getKind() != kind::EQUAL + || assertion[k][0].getKind() != kind::APPLY_UF + || assertion[k][1].getKind() != kind::CONST_BITVECTOR + || assertion[k][1].getConst<BitVector>() != BitVector(1, 1u)) + { is_skolemizable = false; break; } } - if (!is_skolemizable) - continue; + if (!is_skolemizable) continue; ArgsTable assertion_table; // collect function symbols and their arguments - for (unsigned j = 0; j < assertion.getNumChildren(); ++j) { + for (unsigned j = 0; j < assertion.getNumChildren(); ++j) + { TNode current = assertion[j]; - Assert (current.getKind() == kind::EQUAL && - current[0].getKind() == kind::APPLY_UF); + Assert(current.getKind() == kind::EQUAL + && current[0].getKind() == kind::APPLY_UF); TNode func = current[0]; ArgsVec args; - for (unsigned k = 0; k < func.getNumChildren(); ++k) { + for (unsigned k = 0; k < func.getNumChildren(); ++k) + { args.push_back(func[k]); } assertion_table.addEntry(func.getOperator(), args); } - NodeBuilder<> assertion_builder (kind::OR); + NodeBuilder<> assertion_builder(kind::OR); // construct skolemized assertion - for (ArgsTable::iterator it = assertion_table.begin(); it != assertion_table.end(); ++it) { + for (ArgsTable::iterator it = assertion_table.begin(); + it != assertion_table.end(); + ++it) + { // for each function symbol ++(d_statistics.d_numArgsSkolemized); TNode func = it->first; ArgsTableEntry& args = it->second; - NodeBuilder<> skolem_func (kind::APPLY_UF); + NodeBuilder<> skolem_func(kind::APPLY_UF); skolem_func << func; std::vector<Node> skolem_args; - for (unsigned j = 0; j < args.getArity(); ++j) { + for (unsigned j = 0; j < args.getArity(); ++j) + { bool all_same = true; - for (unsigned k = 1; k < args.getNumEntries(); ++k) { - if ( args.getEntry(k)[j] != args.getEntry(0)[j]) - all_same = false; + for (unsigned k = 1; k < args.getNumEntries(); ++k) + { + if (args.getEntry(k)[j] != args.getEntry(0)[j]) all_same = false; } - Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); + Node new_arg = all_same + ? (Node)args.getEntry(0)[j] + : utils::mkVar(utils::getSize(args.getEntry(0)[j])); skolem_args.push_back(new_arg); skolem_func << new_arg; } - - Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); + Node skolem_func_eq1 = + nm->mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); // enumerate arguments assignments std::vector<Node> or_assignments; - for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) { + for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) + { NodeBuilder<> arg_assignment(kind::AND); - ArgsVec& args = *it; - for (unsigned k = 0; k < args.size(); ++k) { - Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]); + ArgsVec& args = *it; + for (unsigned k = 0; k < args.size(); ++k) + { + Node eq = nm->mkNode(kind::EQUAL, args[k], skolem_args[k]); arg_assignment << eq; } or_assignments.push_back(arg_assignment); } - Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments)); + Node new_func_def = + utils::mkAnd(skolem_func_eq1, utils::mkOr(or_assignments)); assertion_builder << new_func_def; } Node new_assertion = assertion_builder; - Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n"; + Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " + << assertions[i] << " => \n"; Debug("bv-abstraction-dbg") << " " << new_assertion; assertions[i] = new_assertion; } @@ -243,22 +274,27 @@ Node AbstractionModule::computeSignature(TNode node) { return sig; } -Node AbstractionModule::getSignatureSkolem(TNode node) { - Assert (node.getKind() == kind::VARIABLE); +Node AbstractionModule::getSignatureSkolem(TNode node) +{ + Assert(node.getKind() == kind::VARIABLE); + NodeManager* nm = NodeManager::currentNM(); unsigned bitwidth = utils::getSize(node); - if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) { + if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) + { d_signatureSkolems[bitwidth] = vector<Node>(); } vector<Node>& skolems = d_signatureSkolems[bitwidth]; // get the index of bv variables of this size unsigned index = getBitwidthIndex(bitwidth); - Assert (skolems.size() + 1 >= index ); - if (skolems.size() == index) { + Assert(skolems.size() + 1 >= index); + if (skolems.size() == index) + { ostringstream os; - os << "sig_" <<bitwidth <<"_" << index; - NodeManager* nm = NodeManager::currentNM(); - skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures")); + os << "sig_" << bitwidth << "_" << index; + skolems.push_back(nm->mkSkolem(os.str(), + nm->mkBitVectorType(bitwidth), + "skolem for computing signatures")); } ++(d_signatureIndices[bitwidth]); return skolems[index]; @@ -392,70 +428,95 @@ void AbstractionModule::storeGeneralization(TNode s, TNode t) { d_sigToGeneralization[s] = t; } -void AbstractionModule::finalizeSignatures() { +void AbstractionModule::finalizeSignatures() +{ NodeManager* nm = NodeManager::currentNM(); - Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures num signatures = " << d_signatures.size() <<"\n"; + Debug("bv-abstraction") + << "AbstractionModule::finalizeSignatures num signatures = " + << d_signatures.size() << "\n"; TNodeSet new_signatures; // "unify" signatures - for (SignatureMap::const_iterator ss = d_signatures.begin(); ss != d_signatures.end(); ++ss) { - for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) { + for (SignatureMap::const_iterator ss = d_signatures.begin(); + ss != d_signatures.end(); + ++ss) + { + for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) + { TNode t = getGeneralization(tt->first); TNode s = getGeneralization(ss->first); - if (t != s) { + if (t != s) + { int status = comparePatterns(s, t); - Assert (status); - if (status < 0) - continue; - if (status == 1) { + Assert(status); + if (status < 0) continue; + if (status == 1) + { storeGeneralization(t, s); - } else { + } + else + { storeGeneralization(s, t); } } } } // keep only most general signatures - for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { + for (SignatureMap::iterator it = d_signatures.begin(); + it != d_signatures.end();) + { TNode sig = it->first; TNode gen = getGeneralization(sig); - if (sig != gen) { - Assert (d_signatures.find(gen) != d_signatures.end()); + if (sig != gen) + { + Assert(d_signatures.find(gen) != d_signatures.end()); // update the count - d_signatures[gen]+= d_signatures[sig]; + d_signatures[gen] += d_signatures[sig]; d_signatures.erase(it++); - } else { + } + else + { ++it; } } - // remove signatures that are not frequent enough - for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { - if (it->second <= 7) { + for (SignatureMap::iterator it = d_signatures.begin(); + it != d_signatures.end();) + { + if (it->second <= 7) + { d_signatures.erase(it++); - } else { + } + else + { ++it; } } - for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) { + for (SignatureMap::const_iterator it = d_signatures.begin(); + it != d_signatures.end(); + ++it) + { TNode signature = it->first; // we already processed this signature - Assert (d_signatureToFunc.find(signature) == d_signatureToFunc.end()); + Assert(d_signatureToFunc.find(signature) == d_signatureToFunc.end()); - Debug("bv-abstraction") << "Processing signature " << signature << " count " << it->second << "\n"; + Debug("bv-abstraction") << "Processing signature " << signature << " count " + << it->second << "\n"; std::vector<TypeNode> arg_types; TNodeSet seen; collectArgumentTypes(signature, arg_types, seen); - Assert (signature.getType().isBoolean()); + Assert(signature.getType().isBoolean()); // make function return a bitvector of size 1 - //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); - TypeNode range = NodeManager::currentNM()->mkBitVectorType(1); + // Node bv_function = nm->mkNode(kind::ITE, signature, utils::mkConst(1, + // 1u), utils::mkConst(1, 0u)); + TypeNode range = nm->mkBitVectorType(1); TypeNode abs_type = nm->mkFunctionType(arg_types, range); - Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); + Node abs_func = + nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; // NOTE: signature expression type is BOOLEAN @@ -465,7 +526,8 @@ void AbstractionModule::finalizeSignatures() { d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size()); - Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n"; + Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " + << d_signatureToFunc.size() << " signatures. \n"; } void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) { @@ -510,15 +572,18 @@ void AbstractionModule::collectArguments(TNode node, TNode signature, std::vecto } } - -Node AbstractionModule::abstractSignatures(TNode assertion) { - Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; +Node AbstractionModule::abstractSignatures(TNode assertion) +{ + Debug("bv-abstraction") << "AbstractionModule::abstractSignatures " + << assertion << "\n"; + NodeManager* nm = NodeManager::currentNM(); // assume the assertion has been fully abstracted Node signature = getGeneralizedSignature(assertion); - Debug("bv-abstraction") << " with sig "<< signature <<"\n"; + Debug("bv-abstraction") << " with sig " << signature << "\n"; NodeNodeMap::iterator it = d_signatureToFunc.find(signature); - if (it!= d_signatureToFunc.end()) { + if (it != d_signatureToFunc.end()) + { std::vector<Node> args; TNode func = it->second; // pushing the function symbol @@ -526,14 +591,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) { TNodeSet seen; collectArguments(assertion, signature, args, seen); std::vector<TNode> real_args; - for (unsigned i = 1; i < args.size(); ++i) { + for (unsigned i = 1; i < args.size(); ++i) + { real_args.push_back(args[i]); } d_argsTable.addEntry(func, real_args); - Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), - utils::mkConst(1, 1u)); - Debug("bv-abstraction") << "=> "<< result << "\n"; - Assert (result.getType() == assertion.getType()); + Node result = nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::APPLY_UF, args), utils::mkConst(1, 1u)); + Debug("bv-abstraction") << "=> " << result << "\n"; + Assert(result.getType() == assertion.getType()); return result; } return assertion; |