diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/theory/bv/theory_bv.cpp | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 433 |
1 files changed, 354 insertions, 79 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 5d5e0a97c..117a3e552 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -1,32 +1,36 @@ /********************* */ /*! \file theory_bv.cpp - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters, Liana Hadarean - ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - +** \verbatim +** Original author: Dejan Jovanovic +** Major contributors: Morgan Deters, Liana Hadarean +** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "smt/options.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/bv/slicer.h" #include "theory/valuation.h" -#include "theory/bv/bitblaster.h" #include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/bv/bv_subtheory_core.h" #include "theory/bv/bv_subtheory_inequality.h" +#include "theory/bv/bv_subtheory_algebraic.h" #include "theory/bv/bv_subtheory_bitblast.h" +#include "theory/bv/bv_eager_solver.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/theory_model.h" +#include "theory/bv/abstraction.h" using namespace CVC4; using namespace CVC4::theory; @@ -48,24 +52,45 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_propagatedBy(c) - { - if (options::bvEquality()) { - SubtheorySolver* core_solver = new CoreSolver(c, this); - 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); - d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; - } + 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(); + return; + } - SubtheorySolver* bb_solver = new BitblastSolver(c, this); - d_subtheories.push_back(bb_solver); - d_subtheoryMap[SUB_BITBLAST] = bb_solver; + if (options::bitvectorEqualitySolver()) { + SubtheorySolver* core_solver = new CoreSolver(c, this); + 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); + d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; } + if (options::bitvectorAlgebraicSolver()) { + SubtheorySolver* alg_solver = new AlgebraicSolver(c, this); + d_subtheories.push_back(alg_solver); + d_subtheoryMap[SUB_ALGEBRAIC] = alg_solver; + } + + BitblastSolver* bb_solver = new BitblastSolver(c, this); + if (options::bvAbstraction()) { + bb_solver->setAbstraction(d_abstractionModule); + } + d_subtheories.push_back(bb_solver); + d_subtheoryMap[SUB_BITBLAST] = bb_solver; +} + + TheoryBV::~TheoryBV() { for (unsigned i = 0; i < d_subtheories.size(); ++i) { delete d_subtheories[i]; @@ -73,7 +98,10 @@ TheoryBV::~TheoryBV() { } void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { - if (options::bvEquality()) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + return; + } + if (options::bitvectorEqualitySolver()) { dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); } } @@ -84,7 +112,8 @@ TheoryBV::Statistics::Statistics(): d_solveTimer("theory::bv::solveTimer"), d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0), d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0), - d_weightComputationTimer("theory::bv::weightComputationTimer") + d_weightComputationTimer("theory::bv::weightComputationTimer"), + d_numMultSlice("theory::bv::NumMultSliceApplied", 0) { StatisticsRegistry::registerStat(&d_avgConflictSize); StatisticsRegistry::registerStat(&d_solveSubstitutions); @@ -92,6 +121,7 @@ TheoryBV::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort); StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort); StatisticsRegistry::registerStat(&d_weightComputationTimer); + StatisticsRegistry::registerStat(&d_numMultSlice); } TheoryBV::Statistics::~Statistics() { @@ -101,6 +131,7 @@ TheoryBV::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort); StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort); StatisticsRegistry::unregisterStat(&d_weightComputationTimer); + StatisticsRegistry::unregisterStat(&d_numMultSlice); } Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { @@ -133,6 +164,83 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { } +void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) { + if (seen.find(term) != seen.end()) + return; + if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UDIV) { + unsigned size = utils::getSize(term[0]); + if (d_BVDivByZeroAckerman.find(size) == d_BVDivByZeroAckerman.end()) { + d_BVDivByZeroAckerman[size] = TNodeSet(); + } + d_BVDivByZeroAckerman[size].insert(term[0]); + 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); + } + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + collectNumerators(term[i], seen); + } +} + +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; + for (unsigned i = 0; i < assertions.size(); ++i) { + 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) { + const TNodeSet& numerators= it->second; + for (TNodeSet::const_iterator i = numerators.begin(); i != numerators.end(); ++i) { + TNodeSet::const_iterator j = i; + j++; + for (; j != numerators.end(); ++j) { + TNode arg1 = *i; + TNode arg2 = *j; + TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1); + 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); + } + } + } + // process remainder UF + Debug("bv-ackermanize") << "Process remainder UF...\n"; + for (WidthToNumerators::const_iterator it = d_BVRemByZeroAckerman.begin(); it != d_BVRemByZeroAckerman.end(); ++it) { + const TNodeSet& numerators= it->second; + for (TNodeSet::const_iterator i = numerators.begin(); i != numerators.end(); ++i) { + TNodeSet::const_iterator j = i; + j++; + for (; j != numerators.end(); ++j) { + TNode arg1 = *i; + TNode arg2 = *j; + TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1); + 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); + } + } + } +} + Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl; @@ -147,15 +255,29 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { case kind::BITVECTOR_UREM: { NodeManager* nm = NodeManager::currentNM(); unsigned width = node.getType().getBitVectorSize(); - Node divByZero = getBVDivByZero(node.getKind(), width); + + 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]); + } + TNode num = node[0], den = node[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL, num, den); - node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - logicRequest.widenLogic(THEORY_UF); - return 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 = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen); + return node; + } else { + Node divByZero = getBVDivByZero(node.getKind(), width); + Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); + node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + logicRequest.widenLogic(THEORY_UF); + return node; + } } break; @@ -169,13 +291,24 @@ 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 + if (!d_eagerSolver->isInitialized()) { + d_eagerSolver->initialize(); + } - if (options::bitvectorEagerBitblast()) { - // don't use the equality engine in the eager bit-blasting - d_subtheoryMap[SUB_BITBLAST]->preRegister(node); - return; + if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) { + Node formula = node[0]; + d_eagerSolver->assertFormula(formula); + } + // nothing to do for the other terms + return; } + for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->preRegister(node); } @@ -212,8 +345,8 @@ void TheoryBV::checkForLemma(TNode fact) { TNode divisor = urem[1]; Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); Node divisor_eq_0 = mkNode(kind::EQUAL, - divisor, - mkConst(BitVector(getSize(divisor), 0u))); + divisor, + mkConst(BitVector(getSize(divisor), 0u))); Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } @@ -224,10 +357,38 @@ void TheoryBV::checkForLemma(TNode fact) { void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - if (options::bitvectorEagerBitblast()) { + + // if we are using the eager solver + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + // this can only happen on an empty benchmark + if (!d_eagerSolver->isInitialized()) { + d_eagerSolver->initialize(); + } + if (!Theory::fullEffort(e)) + return; + + std::vector<TNode> assertions; + while (!done()) { + TNode fact = get().assertion; + Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM); + assertions.push_back(fact); + } + Assert (d_eagerSolver->hasAssertions(assertions)); + + bool ok = d_eagerSolver->checkSat(); + if (!ok) { + if (assertions.size() == 1) { + d_out->conflict(assertions[0]); + return; + } + Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions); + d_out->conflict(conflict); + return; + } return; } - + + if (Theory::fullEffort(e)) { ++(d_statistics.d_numCallsToCheckFullEffort); } else { @@ -241,6 +402,7 @@ void TheoryBV::check(Effort e) while (!done()) { TNode fact = get().assertion; + checkForLemma(fact); for (unsigned i = 0; i < d_subtheories.size(); ++i) { @@ -270,7 +432,7 @@ void TheoryBV::check(Effort e) void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); - // Assert (fullModel); // can only query full model + for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { d_subtheories[i]->collectModelInfo(m, fullModel); @@ -291,9 +453,8 @@ Node TheoryBV::getModelValue(TNode var) { void TheoryBV::propagate(Effort e) { Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; - - if (options::bitvectorEagerBitblast()) { - return; + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + return; } if (inConflict()) { @@ -321,22 +482,62 @@ void TheoryBV::propagate(Effort e) { Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: - - 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])) { - ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitution(in[1], in[0]); - return PP_ASSERT_STATUS_SOLVED; + { + 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])) { + ++(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())) { + 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(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); + } else { + unsigned skolem1_size = low; + unsigned skolem2_size = var_bitwidth - high - 1; + Node skolem1 = utils::mkVar(skolem1_size); + Node skolem2 = utils::mkVar(skolem2_size); + children.push_back(skolem2); + children.push_back(c); + children.push_back(skolem1); + } + Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children); + Assert (utils::getSize(concat) == utils::getSize(extract[0])); + outSubstitutions.addSubstitution(extract[0], concat); + return PP_ASSERT_STATUS_SOLVED; + } + } } - // to do constant propagations - - break; - case kind::NOT: break; + case kind::BITVECTOR_ULT: + case kind::BITVECTOR_SLT: + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_SLE: + default: // TODO other predicates break; @@ -346,28 +547,65 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { + Node res = t; if (RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); - return Rewriter::rewrite(result); - } - - if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { + res = Rewriter::rewrite(result); + } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) { std::vector<Node> equalities; Slicer::splitEqualities(t, equalities); - return utils::mkAnd(equalities); - } - - return t; + res = utils::mkAnd(equalities); + } + + // 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))) { + // // 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)); + + // // the simplification can cause the formula to blow up + // // only apply if formula reduced + // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { + // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; + // uint64_t old_size = bv->computeAtomWeight(t); + // Assert (old_size); + // uint64_t new_size = bv->computeAtomWeight(new_eq); + // double ratio = ((double)new_size)/old_size; + // if (ratio <= 0.4) { + // ++(d_statistics.d_numMultSlice); + // 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); + } + return res; } void TheoryBV::presolve() { Debug("bitvector") << "TheoryBV::presolve" << endl; } +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++; + // If already in conflict, no more propagation if (d_conflict) { Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl; @@ -425,7 +663,7 @@ Node TheoryBV::explain(TNode node) { return utils::mkTrue(); } // return the explanation - Node explanation = mkAnd(assumptions); + Node explanation = utils::mkAnd(assumptions); Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; return explanation; } @@ -434,7 +672,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (!options::bitvectorEagerBitblast() && options::bvEquality()) { + if (options::bitvectorEqualitySolver()) { for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->addSharedTerm(t); } @@ -444,10 +682,7 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - if (options::bitvectorEagerBitblast()) { - return EQUALITY_UNKNOWN; - } - + 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) { @@ -457,3 +692,43 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) return EQUALITY_UNKNOWN; ; } + +void TheoryBV::enableCoreTheorySlicer() { + Assert (!d_calledPreregister); + d_isCoreTheory = true; + if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) { + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + core->enableSlicer(); + } +} + + +void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {} + +bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { + bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); + if (changed && + options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && + options::bitvectorAig()) { + // disable AIG mode + AlwaysAssert (!d_eagerSolver->isInitialized()); + d_eagerSolver->turnOffAig(); + d_eagerSolver->initialize(); + } + return changed; +} + +void TheoryBV::setConflict(Node conflict) { + if (options::bvAbstraction()) { + 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])); + } + } + d_conflict = true; + d_conflictNode = conflict; +} |