diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 168 |
1 files changed, 87 insertions, 81 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4039fceec..0505035c7 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -31,38 +31,40 @@ #include "theory/theory_model.h" #include "theory/valuation.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; using namespace CVC4::context; - -using namespace std; using namespace CVC4::theory::bv::utils; +using namespace std; -TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo), - d_context(c), - d_alreadyPropagatedSet(c), - d_sharedTermsSet(c), - d_subtheories(), - d_subtheoryMap(), - d_statistics(), - d_staticLearnCache(), - d_lemmasAdded(c, false), - d_conflict(c, false), - d_invalidateModelCache(c, true), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_propagatedBy(c), - d_eagerSolver(NULL), - d_abstractionModule(new AbstractionModule()), - d_isCoreTheory(false), - d_calledPreregister(false) +namespace CVC4 { +namespace theory { +namespace bv { + +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals), + d_context(c), + d_alreadyPropagatedSet(c), + d_sharedTermsSet(c), + d_subtheories(), + d_subtheoryMap(), + d_statistics(), + d_staticLearnCache(), + d_lemmasAdded(c, false), + d_conflict(c, false), + d_invalidateModelCache(c, true), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_propagatedBy(c), + d_eagerSolver(NULL), + d_abstractionModule(new AbstractionModule()), + d_isCoreTheory(false), + d_calledPreregister(false) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { d_eagerSolver = new EagerBitblastSolver(this); - return; + return; } if (options::bitvectorEqualitySolver()) { @@ -70,7 +72,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories.push_back(core_solver); d_subtheoryMap[SUB_CORE] = core_solver; } - + if (options::bitvectorInequalitySolver()) { SubtheorySolver* ineq_solver = new InequalitySolver(c, this); d_subtheories.push_back(ineq_solver); @@ -101,7 +103,7 @@ TheoryBV::~TheoryBV() { void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - return; + return; } if (options::bitvectorEqualitySolver()) { dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); @@ -179,31 +181,31 @@ void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) { d_BVDivByZeroAckerman[size] = TNodeSet(); } d_BVDivByZeroAckerman[size].insert(term[0]); - seen.insert(term); + seen.insert(term); } else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) { unsigned size = utils::getSize(term[0]); if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) { d_BVRemByZeroAckerman[size] = TNodeSet(); } d_BVRemByZeroAckerman[size].insert(term[0]); - seen.insert(term); + seen.insert(term); } for (unsigned i = 0; i < term.getNumChildren(); ++i) { - collectNumerators(term[i], seen); + collectNumerators(term[i], seen); } - seen.insert(term); + seen.insert(term); } void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n"; - + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); AlwaysAssert(!options::incrementalSolving()); - TNodeSet seen; + TNodeSet seen; for (unsigned i = 0; i < assertions.size(); ++i) { - collectNumerators(assertions[i], seen); + collectNumerators(assertions[i], seen); } - + // process division UF Debug("bv-ackermanize") << "Process division UF...\n"; for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) { @@ -215,13 +217,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { TNode arg1 = *i; TNode arg2 = *j; TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1); - TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); + TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2); Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2); Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq); Debug("bv-ackermanize") << " " << lemma << "\n"; - assertions.push_back(lemma); + assertions.push_back(lemma); } } } @@ -236,13 +238,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { TNode arg1 = *i; TNode arg2 = *j; TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1); - TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); + TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2); Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2); Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq); Debug("bv-ackermanize") << " " << lemma << "\n"; - assertions.push_back(lemma); + assertions.push_back(lemma); } } } @@ -265,7 +267,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { if (options::bitvectorDivByZeroConst()) { Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL; - return nm->mkNode(kind, node[0], node[1]); + return nm->mkNode(kind, node[0], node[1]); } TNode num = node[0], den = node[1]; @@ -275,9 +277,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // Ackermanize UF if using eager bit-blasting - Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); + Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen); - return node; + return node; } else { Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); @@ -300,7 +302,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { void TheoryBV::preRegisterTerm(TNode node) { d_calledPreregister = true; Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // the aig bit-blaster option is set heuristically // if bv abstraction is not used @@ -309,13 +311,13 @@ void TheoryBV::preRegisterTerm(TNode node) { } if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) { - Node formula = node[0]; + Node formula = node[0]; d_eagerSolver->assertFormula(formula); } // nothing to do for the other terms - return; + return; } - + for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->preRegister(node); } @@ -370,7 +372,7 @@ void TheoryBV::check(Effort e) Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound - d_invalidateModelCache.set(true); + d_invalidateModelCache.set(true); // if we are using the eager solver if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // this can only happen on an empty benchmark @@ -380,28 +382,28 @@ void TheoryBV::check(Effort e) if (!Theory::fullEffort(e)) return; - std::vector<TNode> assertions; + std::vector<TNode> assertions; while (!done()) { TNode fact = get().assertion; Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM); - assertions.push_back(fact); + assertions.push_back(fact); } - Assert (d_eagerSolver->hasAssertions(assertions)); - + Assert (d_eagerSolver->hasAssertions(assertions)); + bool ok = d_eagerSolver->checkSat(); if (!ok) { if (assertions.size() == 1) { d_out->conflict(assertions[0]); - return; + return; } Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions); d_out->conflict(conflict); - return; + return; } return; } - - + + if (Theory::fullEffort(e)) { ++(d_statistics.d_numCallsToCheckFullEffort); } else { @@ -446,7 +448,7 @@ void TheoryBV::check(Effort e) void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver->collectModelInfo(m, fullModel); + d_eagerSolver->collectModelInfo(m, fullModel); } for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { @@ -469,7 +471,7 @@ Node TheoryBV::getModelValue(TNode var) { void TheoryBV::propagate(Effort e) { Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - return; + return; } if (inConflict()) { @@ -508,29 +510,29 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } - Node node = Rewriter::rewrite(in); + Node node = Rewriter::rewrite(in); 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) { Node c = node[0].isConst() ? node[0] : node[1]; - + unsigned high = utils::getExtractHigh(extract); unsigned low = utils::getExtractLow(extract); unsigned var_bitwidth = utils::getSize(extract[0]); std::vector<Node> children; - + 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(skolem); children.push_back(c); } else if (high == var_bitwidth - 1) { unsigned skolem_size = low; Node skolem = utils::mkVar(skolem_size); children.push_back(c); - children.push_back(skolem); + children.push_back(skolem); } else { unsigned skolem1_size = low; unsigned skolem2_size = var_bitwidth - high - 1; @@ -541,7 +543,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu children.push_back(skolem1); } Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children); - Assert (utils::getSize(concat) == utils::getSize(extract[0])); + Assert (utils::getSize(concat) == utils::getSize(extract[0])); outSubstitutions.addSubstitution(extract[0], concat); return PP_ASSERT_STATUS_SOLVED; } @@ -552,7 +554,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu case kind::BITVECTOR_SLT: case kind::BITVECTOR_ULE: case kind::BITVECTOR_SLE: - + default: // TODO other predicates break; @@ -562,7 +564,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { - Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; + Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; Node res = t; if (RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); @@ -591,8 +593,8 @@ Node TheoryBV::ppRewrite(TNode t) } else { res = t; } - } - + } + // if(t.getKind() == kind::EQUAL && // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) || @@ -618,18 +620,18 @@ Node TheoryBV::ppRewrite(TNode t) // return new_eq; // } // } - + // if (new_eq.getKind() == kind::CONST_BOOLEAN) { // ++(d_statistics.d_numMultSlice); // return new_eq; // } // } // } - + if (options::bvAbstraction() && t.getType().isBoolean()) { - d_abstractionModule->addInputAtom(res); + d_abstractionModule->addInputAtom(res); } - Debug("bv-pp-rewrite") << "to " << res << "\n"; + Debug("bv-pp-rewrite") << "to " << res << "\n"; return res; } @@ -637,13 +639,13 @@ void TheoryBV::presolve() { Debug("bitvector") << "TheoryBV::presolve" << endl; } -static int prop_count = 0; +static int prop_count = 0; bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl; - prop_count++; - + prop_count++; + // If already in conflict, no more propagation if (d_conflict) { Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl; @@ -720,7 +722,7 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); if (status != EQUALITY_UNKNOWN) { @@ -736,7 +738,7 @@ void TheoryBV::enableCoreTheorySlicer() { d_isCoreTheory = true; if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) { CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - core->enableSlicer(); + core->enableSlicer(); } } @@ -746,7 +748,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { return; } d_staticLearnCache.insert(in); - + if (in.getKind() == kind::EQUAL) { if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) || (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) { @@ -754,7 +756,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; if(p.getNumChildren() == 2 - && p[0].getKind() == kind::BITVECTOR_SHL + && p[0].getKind() == kind::BITVECTOR_SHL && p[1].getKind() == kind::BITVECTOR_SHL ){ unsigned size = utils::getSize(s); Node one = utils::mkConst(size, 1u); @@ -796,14 +798,18 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector void TheoryBV::setConflict(Node conflict) { if (options::bvAbstraction()) { Node new_conflict = d_abstractionModule->simplifyConflict(conflict); - + std::vector<Node> lemmas; - lemmas.push_back(new_conflict); + 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])); + lemma(utils::mkNode(kind::NOT, lemmas[i])); } } d_conflict = true; d_conflictNode = conflict; } + +} /* namespace CVC4::theory::bv */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ |