summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r--src/theory/bv/theory_bv.cpp433
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;
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback