From cbfd4e87765b716e8d21bd115f5917edef63f8a4 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 1 Feb 2016 11:22:12 -0800 Subject: [PATCH] Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file. --- src/theory/bv/bv_subtheory_algebraic.cpp | 264 ++++++++++++----------- 1 file changed, 141 insertions(+), 123 deletions(-) diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index fc9d67cb4..beca25a88 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -16,23 +16,28 @@ #include "theory/bv/bv_subtheory_algebraic.h" #include "options/bv_options.h" -#include "smt_util/boolean_simplification.h" #include "smt/smt_statistics_registry.h" +#include "smt_util/boolean_simplification.h" #include "theory/bv/bv_quick_check.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" -using namespace std; -using namespace CVC4; using namespace CVC4::context; using namespace CVC4::prop; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace bv { + bool hasExpensiveBVOperators(TNode fact); +Node mergeExplanations(const std::vector& expls); +Node mergeExplanations(TNode expl1, TNode expl2); + SubstitutionEx::SubstitutionEx(theory::SubstitutionMap* modelMap) : d_substitutions() @@ -42,17 +47,18 @@ SubstitutionEx::SubstitutionEx(theory::SubstitutionMap* modelMap) {} bool SubstitutionEx::addSubstitution(TNode from, TNode to, TNode reason) { - Debug("bv-substitution") << "SubstitutionEx::addSubstitution: "<< from <<" => "<< to <<"\n"; - Debug("bv-substitution") << " reason "< "<< to << "\n" << " reason "<addSubstitution(from, to); + if (d_substitutions.find(from) != d_substitutions.end()) { + return false; + } + + d_modelMap->addSubstitution(from, to); d_cacheInvalid = true; d_substitutions[from] = SubstitutionElement(to, reason); - return true; + return true; } Node SubstitutionEx::apply(TNode node) { @@ -85,7 +91,7 @@ Node SubstitutionEx::internalApply(TNode node) { while (!stack.empty()) { SubstitutionStackElement head = stack.back(); stack.pop_back(); - + TNode current = head.node; if (hasCache(current)) { @@ -112,12 +118,12 @@ Node SubstitutionEx::internalApply(TNode node) { storeCache(current, current, utils::mkTrue()); continue; } - - // children already processed + + // children already processed if (head.childrenAdded) { NodeBuilder<> nb(current.getKind()); std::vector reasons; - + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { TNode op = current.getOperator(); Assert (hasCache(op)); @@ -156,9 +162,10 @@ Node SubstitutionEx::internalApply(TNode node) { } Node SubstitutionEx::explain(TNode node) const { - if(!hasCache(node)) + if(!hasCache(node)) { return utils::mkTrue(); - + } + Debug("bv-substitution") << "SubstitutionEx::explain("<< node <<")\n"; Node res = getReason(node); Debug("bv-substitution") << " with "<< res <<"\n"; @@ -181,7 +188,7 @@ Node SubstitutionEx::getCache(TNode node) const { } void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) { - // Debug("bv-substitution") << "SubstitutionEx::storeCache(" << from <<", " << to <<", "<< reason<<")\n"; + // Debug("bv-substitution") << "SubstitutionEx::storeCache(" << from <<", " << to <<", "<< reason<<")\n"; Assert (!hasCache(from)); d_cache[from] = SubstitutionElement(to, reason); } @@ -204,6 +211,7 @@ AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv) {} AlgebraicSolver::~AlgebraicSolver() { + if(d_modelMap != NULL) { delete d_modelMap; } delete d_quickXplain; delete d_quickSolver; delete d_ctx; @@ -212,23 +220,25 @@ AlgebraicSolver::~AlgebraicSolver() { bool AlgebraicSolver::check(Theory::Effort e) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); - if (!Theory::fullEffort(e)) + if (!Theory::fullEffort(e)) { return true; + } - if (!useHeuristic()) + if (!useHeuristic()) { return true; - + } + ++(d_numCalls); - + TimerStat::CodeTimer algebraicTimer(d_statistics.d_solveTime); Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check (" << e << ")\n"; ++(d_statistics.d_numCallstoCheck); d_explanations.clear(); - d_ids.clear(); - d_inputAssertions.clear(); + d_ids.clear(); + d_inputAssertions.clear(); std::vector worklist; @@ -240,39 +250,39 @@ bool AlgebraicSolver::check(Theory::Effort e) { Debug("bv-subtheory-algebraic") << " " << *it << "\n"; TNode assertion = *it; unsigned id = worklist.size(); - d_ids[assertion] = id; + d_ids[assertion] = id; worklist.push_back(WorklistElement(assertion, id)); - d_inputAssertions.insert(assertion); + d_inputAssertions.insert(assertion); storeExplanation(assertion); uint64_t assertion_size = d_quickSolver->computeAtomWeight(assertion, seen_assertions); Assert (original_bb_cost <= original_bb_cost + assertion_size); - original_bb_cost+= assertion_size; + original_bb_cost+= assertion_size; } for (unsigned i = 0; i < worklist.size(); ++i) { d_ids[worklist[i].node] = worklist[i].id; } - + Debug("bv-subtheory-algebraic") << "Assertions " << worklist.size() <<" : \n"; - Assert (d_explanations.size() == worklist.size()); + Assert (d_explanations.size() == worklist.size()); delete d_modelMap; d_modelMap = new SubstitutionMap(d_context); SubstitutionEx subst(d_modelMap); // first round of substitutions - processAssertions(worklist, subst); + processAssertions(worklist, subst); if (!d_isDifficult.get()) { // skolemize all possible extracts ExtractSkolemizer skolemizer(d_modelMap); skolemizer.skolemize(worklist); // second round of substitutions - processAssertions(worklist, subst); + processAssertions(worklist, subst); } - + NodeSet subst_seen; uint64_t subst_bb_cost = 0; @@ -283,15 +293,15 @@ bool AlgebraicSolver::check(Theory::Effort e) { TNode fact = worklist[r].node; unsigned id = worklist[r].id; - + if (Dump.isOn("bv-algebraic")) { Node expl = d_explanations[id]; Node query = utils::mkNot(utils::mkNode(kind::IMPLIES, expl, fact)); - Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); - Dump("bv-algebraic") << PushCommand(); + Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); + Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(query.toExpr()); Dump("bv-algebraic") << CheckSatCommand(); - Dump("bv-algebraic") << PopCommand(); + Dump("bv-algebraic") << PopCommand(); } if (fact.isConst() && @@ -306,16 +316,16 @@ bool AlgebraicSolver::check(Theory::Effort e) { d_bv->setConflict(conflict); d_isComplete.set(true); Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n"; - + if (Dump.isOn("bv-algebraic")) { - Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict"); - Dump("bv-algebraic") << PushCommand(); + Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict"); + Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(conflict.toExpr()); Dump("bv-algebraic") << CheckSatCommand(); - Dump("bv-algebraic") << PopCommand(); + Dump("bv-algebraic") << PopCommand(); } - + ++(d_statistics.d_numSimplifiesToFalse); ++(d_numSolved); return false; @@ -331,7 +341,7 @@ bool AlgebraicSolver::check(Theory::Effort e) { worklist.resize(w); - + if(Debug.isOn("bv-subtheory-algebraic")) { Debug("bv-subtheory-algebraic") << "Assertions post-substitutions " << worklist.size() << ":\n"; for (unsigned i = 0; i < worklist.size(); ++i) { @@ -339,7 +349,7 @@ bool AlgebraicSolver::check(Theory::Effort e) { } } - + // all facts solved to true if (worklist.empty()) { Debug("bv-subtheory-algebraic") << " SAT: everything simplifies to true.\n"; @@ -355,13 +365,13 @@ bool AlgebraicSolver::check(Theory::Effort e) { d_isComplete.set(false); return true; } - + d_quickSolver->clearSolver(); d_quickSolver->push(); std::vector facts; for (unsigned i = 0; i < worklist.size(); ++i) { - facts.push_back(worklist[i].node); + facts.push_back(worklist[i].node); } bool ok = quickCheck(facts); @@ -378,7 +388,7 @@ bool AlgebraicSolver::quickCheck(std::vector& facts) { ++(d_statistics.d_numUnknown); return true; } - + if (res == SAT_VALUE_TRUE) { Debug("bv-subtheory-algebraic") << " Sat.\n"; ++(d_statistics.d_numSat); @@ -390,20 +400,19 @@ bool AlgebraicSolver::quickCheck(std::vector& facts) { Assert (res == SAT_VALUE_FALSE); Assert (d_quickSolver->inConflict()); d_isComplete.set(true); - Debug("bv-subtheory-algebraic") << " Unsat.\n"; ++(d_numSolved); ++(d_statistics.d_numUnsat); - + Node conflict = d_quickSolver->getConflict(); Debug("bv-subtheory-algebraic") << " Conflict: " << conflict << "\n"; // singleton conflict if (conflict.getKind() != kind::AND) { Assert (d_ids.find(conflict) != d_ids.end()); - unsigned id = d_ids[conflict]; - Assert (id < d_explanations.size()); + unsigned id = d_ids[conflict]; + Assert (id < d_explanations.size()); Node theory_confl = d_explanations[id]; d_bv->setConflict(theory_confl); return false; @@ -416,18 +425,18 @@ bool AlgebraicSolver::quickCheck(std::vector& facts) { conflict = d_quickXplain->minimizeConflict(conflict); Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck minimized conflict size " << conflict.getNumChildren() << "\n"; } - + vector theory_confl; for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { TNode c = conflict[i]; - Assert (d_ids.find(c) != d_ids.end()); + Assert (d_ids.find(c) != d_ids.end()); unsigned c_id = d_ids[c]; Assert (c_id < d_explanations.size()); TNode c_expl = d_explanations[c_id]; theory_confl.push_back(c_expl); } - + Node confl = BooleanSimplification::simplify(utils::mkAnd(theory_confl)); Debug("bv-subtheory-algebraic") << " Out Conflict: " << confl << "\n"; @@ -451,7 +460,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { TNode left = fact[0]; TNode right = fact[1]; - + if (left.isVar() && !right.hasSubterm(left)) { bool changed = subst.addSubstitution(left, right, reason); return changed; @@ -466,14 +475,14 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { left.getKind() == kind::BITVECTOR_XOR) { TNode var = left[0]; if (var.getMetaKind() != kind::metakind::VARIABLE) - return false; + return false; // simplify xor with same variable on both sides if (right.hasSubterm(var)) { std::vector right_children; for (unsigned i = 0; i < right.getNumChildren(); ++i) { if (right[i] != var) - right_children.push_back(right[i]); + right_children.push_back(right[i]); } Assert (right_children.size()); Node new_right = right_children.size() > 1 ? utils::mkNode(kind::BITVECTOR_XOR, right_children) @@ -488,7 +497,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { bool changed = subst.addSubstitution(fact, new_fact, reason); return changed; } - + NodeBuilder<> nb(kind::BITVECTOR_XOR); for (unsigned i = 1; i < left.getNumChildren(); ++i) { nb << left[i]; @@ -499,14 +508,14 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { if (Dump.isOn("bv-algebraic")) { Node query = utils::mkNot(utils::mkNode(kind::IFF, fact, utils::mkNode(kind::EQUAL, var, new_right))); - Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); - Dump("bv-algebraic") << PushCommand(); + Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); + Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(query.toExpr()); Dump("bv-algebraic") << CheckSatCommand(); - Dump("bv-algebraic") << PopCommand(); + Dump("bv-algebraic") << PopCommand(); } - + return changed; } @@ -519,9 +528,9 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { Node zero = utils::mkConst(utils::getSize(var), 0u); Node new_fact = utils::mkNode(kind::EQUAL, zero, new_left); bool changed = subst.addSubstitution(fact, new_fact, reason); - return changed; + return changed; } - + if (right.getKind() == kind::BITVECTOR_XOR && left.getMetaKind() == kind::metakind::VARIABLE && right.hasSubterm(left)) { @@ -530,7 +539,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { Node zero = utils::mkConst(utils::getSize(var), 0u); Node new_fact = utils::mkNode(kind::EQUAL, zero, new_right); bool changed = subst.addSubstitution(fact, new_fact, reason); - return changed; + return changed; } // (a xor b = 0) <=> (a = b) @@ -540,18 +549,18 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { right.getConst() == BitVector(utils::getSize(left), 0u)) { Node new_fact = utils::mkNode(kind::EQUAL, left[0], left[1]); bool changed = subst.addSubstitution(fact, new_fact, reason); - return changed; + return changed; } - + return false; -} +} bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) { if (node.getMetaKind() == kind::metakind::VARIABLE && !in.hasSubterm(node)) return true; - return false; + return false; } void AlgebraicSolver::processAssertions(std::vector& worklist, SubstitutionEx& subst) { @@ -567,9 +576,9 @@ void AlgebraicSolver::processAssertions(std::vector& worklist, worklist[i] = WorklistElement(Rewriter::rewrite(current), current_id); // explanation for this assertion Node old_expl = d_explanations[current_id]; - Node new_expl = mergeExplanations(subst_expl, old_expl); + Node new_expl = mergeExplanations(subst_expl, old_expl); storeExplanation(current_id, new_expl); - + // use the new substitution to solve if(solve(worklist[i].node, new_expl, subst)) { changed = true; @@ -580,49 +589,52 @@ void AlgebraicSolver::processAssertions(std::vector& worklist, for (unsigned i = 0; i < worklist.size(); ++i) { TNode fact = worklist[i].node; unsigned current_id = worklist[i].id; - - if (fact.getKind() != kind::EQUAL) + + if (fact.getKind() != kind::EQUAL) { continue; + } TNode left = fact[0]; TNode right = fact[1]; if (left.getKind() != kind::BITVECTOR_CONCAT || right.getKind() != kind::BITVECTOR_CONCAT || - left.getNumChildren() != right.getNumChildren()) + left.getNumChildren() != right.getNumChildren()) { continue; + } bool can_slice = true; for (unsigned j = 0; j < left.getNumChildren(); ++j) { if (utils::getSize(left[j]) != utils::getSize(right[j])) can_slice = false; } - - if (!can_slice) - continue; - + + if (!can_slice) { + continue; + } + for (unsigned j = 0; j < left.getNumChildren(); ++j) { Node eq_j = utils::mkNode(kind::EQUAL, left[j], right[j]); unsigned id = d_explanations.size(); TNode expl = d_explanations[current_id]; storeExplanation(expl); worklist.push_back(WorklistElement(eq_j, id)); - d_ids[eq_j] = id; + d_ids[eq_j] = id; } worklist[i] = WorklistElement(utils::mkTrue(), worklist[i].id); changed = true; } - Assert (d_explanations.size() == worklist.size()); + Assert (d_explanations.size() == worklist.size()); } } void AlgebraicSolver::storeExplanation(unsigned id, TNode explanation) { - Assert (checkExplanation(explanation)); + Assert (checkExplanation(explanation)); d_explanations[id] = explanation; } void AlgebraicSolver::storeExplanation(TNode explanation) { Assert (checkExplanation(explanation)); - d_explanations.push_back(explanation); + d_explanations.push_back(explanation); } bool AlgebraicSolver::checkExplanation(TNode explanation) { @@ -635,18 +647,18 @@ bool AlgebraicSolver::checkExplanation(TNode explanation) { return false; } } - return true; + return true; } bool AlgebraicSolver::isComplete() { - return d_isComplete.get(); + return d_isComplete.get(); } bool AlgebraicSolver::useHeuristic() { if (d_numCalls == 0) return true; - + double success_rate = double(d_numSolved)/double(d_numCalls); d_statistics.d_useHeuristic.setData(success_rate); return success_rate > 0.8; @@ -665,7 +677,7 @@ EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) { - Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n"; + Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n"; AlwaysAssert (!d_quickSolver->inConflict()); set termSet; d_bv->computeRelevantTerms(termSet); @@ -675,7 +687,7 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) { std::vector variables; std::vector values; for (set::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { - TNode term = *it; + TNode term = *it; if (term.getType().isBitVector() && (term.getMetaKind() == kind::metakind::VARIABLE || Theory::theoryOf(term) != THEORY_BV)) { @@ -704,7 +716,7 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) { // may be a shared term that did not appear in the current assertions if (!value.isNull()) { Debug("bitvector-model") << " " << var << " => " << value << "\n"; - Assert (value.getKind() == kind::CONST_BITVECTOR); + Assert (value.getKind() == kind::CONST_BITVECTOR); d_modelMap->addSubstitution(var, value); } } @@ -713,16 +725,16 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) { for (unsigned i = 0; i < variables.size(); ++i) { TNode current = values[i]; TNode subst = Rewriter::rewrite(d_modelMap->apply(current)); - Debug("bitvector-model") << "AlgebraicSolver: " << variables[i] << " => " << subst << "\n"; + Debug("bitvector-model") << "AlgebraicSolver: " << variables[i] << " => " << subst << "\n"; // Doesn't have to be constant as it may be irrelevant - Assert (subst.getKind() == kind::CONST_BITVECTOR); + Assert (subst.getKind() == kind::CONST_BITVECTOR); model->assertEquality(variables[i], subst, true); } } Node AlgebraicSolver::getModelValue(TNode node) { - return Node::null(); + return Node::null(); } AlgebraicSolver::Statistics::Statistics() @@ -763,12 +775,13 @@ bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) { return true; } - if (seen.find(fact) != seen.end()) + if (seen.find(fact) != seen.end()) { return false; - - if (fact.getNumChildren() == 0) + } + + if (fact.getNumChildren() == 0) { return false; - + } for (unsigned i = 0; i < fact.getNumChildren(); ++i) { bool difficult = hasExpensiveBVOperatorsRec(fact[i], seen); if (difficult) @@ -787,15 +800,15 @@ void ExtractSkolemizer::skolemize(std::vector& facts) { TNodeSet seen; for (unsigned i = 0; i < facts.size(); ++i) { TNode current = facts[i].node; - collectExtracts(current, seen); + collectExtracts(current, seen); } for (VarExtractMap::iterator it = d_varToExtract.begin(); it != d_varToExtract.end(); ++it) { ExtractList& el = it->second; - TNode var = it->first; + TNode var = it->first; Base& base = el.base; - unsigned bw = utils::getSize(var); + unsigned bw = utils::getSize(var); // compute decomposition std::vector cuts; for (unsigned i = 1; i <= bw; ++i) { @@ -813,7 +826,7 @@ void ExtractSkolemizer::skolemize(std::vector& facts) { Assert (size > 0); Node sk = utils::mkVar(size); skolems.push_back(sk); - previous = current; + previous = current; } if (current < bw -1) { int size = bw - current; @@ -824,7 +837,7 @@ void ExtractSkolemizer::skolemize(std::vector& facts) { NodeBuilder<> skolem_nb(kind::BITVECTOR_CONCAT); for (int i = skolems.size() - 1; i >= 0; --i) { - skolem_nb << skolems[i]; + skolem_nb << skolems[i]; } Node skolem_concat = skolems.size() == 1 ? (Node)skolems[0] : (Node) skolem_nb; @@ -838,10 +851,10 @@ void ExtractSkolemizer::skolemize(std::vector& facts) { Node skolem_extract = Rewriter::rewrite(utils::mkExtract(skolem_concat, h, l)); Assert (skolem_extract.getMetaKind() == kind::metakind::VARIABLE || skolem_extract.getKind() == kind::BITVECTOR_CONCAT); - storeSkolem(extract, skolem_extract); + storeSkolem(extract, skolem_extract); } } - + for (unsigned i = 0; i < facts.size(); ++i) { facts[i] = WorklistElement(skolemize(facts[i].node), facts[i].id); } @@ -851,7 +864,7 @@ Node ExtractSkolemizer::mkSkolem(Node node) { Assert (node.getKind() == kind::BITVECTOR_EXTRACT && node[0].getMetaKind() == kind::metakind::VARIABLE); Assert (!d_skolemSubst.hasSubstitution(node)); - return utils::mkVar(utils::getSize(node)); + return utils::mkVar(utils::getSize(node)); } void ExtractSkolemizer::unSkolemize(std::vector& facts) { @@ -862,16 +875,16 @@ void ExtractSkolemizer::unSkolemize(std::vector& facts) { void ExtractSkolemizer::storeSkolem(TNode node, TNode skolem) { d_skolemSubst.addSubstitution(node, skolem); - d_modelMap->addSubstitution(node, skolem); + d_modelMap->addSubstitution(node, skolem); d_skolemSubstRev.addSubstitution(skolem, node); } Node ExtractSkolemizer::unSkolemize(TNode node) { - return d_skolemSubstRev.apply(node); + return d_skolemSubstRev.apply(node); } Node ExtractSkolemizer::skolemize(TNode node) { - return d_skolemSubst.apply(node); + return d_skolemSubst.apply(node); } void ExtractSkolemizer::ExtractList::addExtract(Extract& e) { @@ -890,12 +903,12 @@ void ExtractSkolemizer::storeExtract(TNode var, unsigned high, unsigned low) { Extract e(high, low); el.addExtract(e); } - + void ExtractSkolemizer::collectExtracts(TNode node, TNodeSet& seen) { if (seen.find(node) != seen.end()) { return; } - + if (node.getKind() == kind::BITVECTOR_EXTRACT && node[0].getMetaKind() == kind::metakind::VARIABLE) { unsigned high = utils::getExtractHigh(node); @@ -912,7 +925,7 @@ void ExtractSkolemizer::collectExtracts(TNode node, TNodeSet& seen) { for (unsigned i = 0; i < node.getNumChildren(); ++i) { collectExtracts(node[i], seen); } - seen.insert(node); + seen.insert(node); } ExtractSkolemizer::ExtractSkolemizer(theory::SubstitutionMap* modelMap) @@ -926,39 +939,44 @@ ExtractSkolemizer::ExtractSkolemizer(theory::SubstitutionMap* modelMap) ExtractSkolemizer::~ExtractSkolemizer() { } -Node CVC4::theory::bv::mergeExplanations(const std::vector& expls) { +Node mergeExplanations(const std::vector& expls) { TNodeSet literals; for (unsigned i = 0; i < expls.size(); ++i) { - TNode expl = expls[i]; - Assert (expl.getType().isBoolean()); + TNode expl = expls[i]; + Assert (expl.getType().isBoolean()); if (expl.getKind() == kind::AND) { for (unsigned i = 0; i < expl.getNumChildren(); ++i) { TNode child = expl[i]; if (child == utils::mkTrue()) continue; - literals.insert(child); + literals.insert(child); } } else if (expl != utils::mkTrue()) { literals.insert(expl); } } - if (literals.size() == 0) + + if (literals.size() == 0) { return utils::mkTrue(); + }else if (literals.size() == 1) { + return *literals.begin(); + } - if (literals.size() == 1) - return *literals.begin(); - - NodeBuilder<> nb(kind::AND); + NodeBuilder<> nb(kind::AND); for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) { - nb << *it; + nb << *it; } - return nb; + return nb; } -Node CVC4::theory::bv::mergeExplanations(TNode expl1, TNode expl2) { +Node mergeExplanations(TNode expl1, TNode expl2) { std::vector expls; expls.push_back(expl1); expls.push_back(expl2); - return mergeExplanations(expls); + return mergeExplanations(expls); } + +} /* namespace CVC4::theory::bv */ +} /* namespace CVc4::theory */ +} /* namespace CVC4 */ -- 2.30.2