diff options
author | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
commit | 5eabda0f55cee3be81aa7ae126269c32e818322f (patch) | |
tree | b873e4cb8e5d37ff3bb70596494bc5964aaef135 /src/theory/bv | |
parent | b717513e2a1d956c4456d13e0625957fc84c2449 (diff) |
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 55 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 7 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 4 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 3 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 38 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 168 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 20 |
8 files changed, 157 insertions, 140 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index b93d0561e..7b071b9e9 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -19,17 +19,17 @@ #ifndef __CVC4__BITBLASTER_TEMPLATE_H #define __CVC4__BITBLASTER_TEMPLATE_H - -#include "expr/node.h" -#include <vector> #include <ext/hash_map> +#include <vector> -#include "context/cdhashmap.h" #include "bitblast_strategies_template.h" +#include "context/cdhashmap.h" +#include "expr/node.h" #include "expr/resource_manager.h" #include "prop/sat_solver.h" -#include "theory/valuation.h" +#include "smt/smt_globals.h" #include "theory/theory_registrar.h" +#include "theory/valuation.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -84,25 +84,25 @@ protected: // caches and mappings TermDefMap d_termCache; ModelCache d_modelCache; - + void initAtomBBStrategies(); void initTermBBStrategies(); protected: /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; - AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; - virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; public: - TBitblaster(); + TBitblaster(); virtual ~TBitblaster() {} - virtual void bbAtom(TNode node) = 0; + virtual void bbAtom(TNode node) = 0; virtual void bbTerm(TNode node, Bits& bits) = 0; virtual void makeVariable(TNode node, Bits& bits) = 0; virtual T getBBAtom(TNode atom) const = 0; virtual bool hasBBAtom(TNode atom) const = 0; virtual void storeBBAtom(TNode atom, T atom_bb) = 0; - - + + bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; void storeBBTerm(TNode term, const Bits& bits); @@ -114,10 +114,10 @@ public: */ Node getTermModel(TNode node, bool fullModel); void invalidateModelCache(); -}; +}; -class TheoryBV; +class TheoryBV; class TLazyBitblaster : public TBitblaster<Node> { typedef std::vector<Node> Bits; @@ -127,19 +127,20 @@ class TLazyBitblaster : public TBitblaster<Node> { class MinisatNotify : public prop::BVSatSolverInterface::Notify { prop::CnfStream* d_cnf; TheoryBV *d_bv; - TLazyBitblaster* d_lazyBB; + TLazyBitblaster* d_lazyBB; public: MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv) : d_cnf(cnf) , d_bv(bv) , d_lazyBB(lbv) {} + bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); void spendResource(unsigned ammount); void safePoint(unsigned ammount); }; - + TheoryBV *d_bv; context::Context* d_ctx; @@ -155,24 +156,25 @@ class TLazyBitblaster : public TBitblaster<Node> { ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals. Only used when bvEagerPropagate option enabled. */ TNodeSet d_variables; - TNodeSet d_bbAtoms; + TNodeSet d_bbAtoms; AbstractionModule* d_abstraction; bool d_emptyNotify; context::CDO<bool> d_satSolverFullModel; - + void addAtom(TNode atom); bool hasValue(TNode a); - Node getModelFromSatSolver(TNode a, bool fullModel); + Node getModelFromSatSolver(TNode a, bool fullModel); + public: void bbTerm(TNode node, Bits& bits); void bbAtom(TNode node); Node getBBAtom(TNode atom) const; void storeBBAtom(TNode atom, Node atom_bb); - bool hasBBAtom(TNode atom) const; + bool hasBBAtom(TNode atom) const; TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); ~TLazyBitblaster() throw(); - /** + /** * Pushes the assumption literal associated with node to the SAT * solver assumption queue. * @@ -261,26 +263,27 @@ class EagerBitblaster : public TBitblaster<Node> { TNodeSet d_variables; Node getModelFromSatSolver(TNode a, bool fullModel); - bool isSharedTerm(TNode node); + bool isSharedTerm(TNode node); public: + EagerBitblaster(theory::bv::TheoryBV* theory_bv); + ~EagerBitblaster(); + void addAtom(TNode atom); void makeVariable(TNode node, Bits& bits); void bbTerm(TNode node, Bits& bits); void bbAtom(TNode node); Node getBBAtom(TNode node) const; - bool hasBBAtom(TNode atom) const; + bool hasBBAtom(TNode atom) const; void bbFormula(TNode formula); void storeBBAtom(TNode atom, Node atom_bb); - EagerBitblaster(theory::bv::TheoryBV* theory_bv); - ~EagerBitblaster(); bool assertToSat(TNode node, bool propagate = true); bool solve(); void collectModelInfo(TheoryModel* m, bool fullModel); }; class BitblastingRegistrar: public prop::Registrar { - EagerBitblaster* d_bitblaster; + EagerBitblaster* d_bitblaster; public: BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 37e1bd9ba..ff13867cc 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -33,15 +33,16 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; AssertionSet d_assertionSet; /** Bitblasters */ EagerBitblaster* d_bitblaster; AigBitblaster* d_aigBitblaster; bool d_useAig; - TheoryBV* d_bv; + TheoryBV* d_bv; + public: - EagerBitblastSolver(theory::bv::TheoryBV* bv); + EagerBitblastSolver(theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 261a0b1c4..8ef49f786 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -35,7 +35,7 @@ class TheoryModel; namespace bv { -class TLazyBitblaster; +class TLazyBitblaster; class TheoryBV; class BVQuickCheck { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 77461163c..0e066eefb 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -18,8 +18,8 @@ #pragma once -#include "theory/bv/bv_subtheory.h" #include "theory/bv/bitblaster_template.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -58,7 +58,7 @@ class BitblastSolver : public SubtheorySolver { BVQuickCheck* d_quickCheck; QuickXPlain* d_quickXplain; // Node getModelValueRec(TNode node); - void setConflict(TNode conflict); + void setConflict(TNode conflict); public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index ec2bfd9c0..39606ca7c 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -46,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_nullContext = new context::Context(); d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, + d_nullContext, d_bv->globals()); MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 3c2b4ed78..b8173cb8b 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -26,12 +26,13 @@ #include "theory/theory_model.h" #include "theory_bv_utils.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; +namespace CVC4 { +namespace theory { +namespace bv { -TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify) +TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, + const std::string name, bool emptyNotify) : TBitblaster<Node>() , d_bv(bv) , d_ctx(c) @@ -44,13 +45,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st , d_satSolverFullModel(c, false) , d_name(name) , d_statistics(name) { + d_satSolver = prop::SatSolverFactory::createMinisat(c, name); d_nullRegistrar = new prop::NullRegistrar(); d_nullContext = new context::Context(); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_nullRegistrar, - d_nullContext); - + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, + d_nullContext, d_bv->globals()); + d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); @@ -59,7 +60,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st } void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { - d_abstraction = abs; + d_abstraction = abs; } TLazyBitblaster::~TLazyBitblaster() throw() { @@ -103,8 +104,8 @@ void TLazyBitblaster::bbAtom(TNode node) { if (expansion.getKind() == kind::CONST_BOOLEAN) { atom_bb = expansion; } else { - Assert (expansion.getKind() == kind::AND); - std::vector<Node> atoms; + Assert (expansion.getKind() == kind::AND); + std::vector<Node> atoms; for (unsigned i = 0; i < expansion.getNumChildren(); ++i) { Node normalized_i = Rewriter::rewrite(expansion[i]); Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ? @@ -481,7 +482,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { } void TLazyBitblaster::clearSolver() { - Assert (d_ctx->getLevel() == 0); + Assert (d_ctx->getLevel() == 0); delete d_satSolver; delete d_satSolverNotify; delete d_cnfStream; @@ -492,16 +493,19 @@ void TLazyBitblaster::clearSolver() { d_bbAtoms.clear(); d_variables.clear(); d_termCache.clear(); - - invalidateModelCache(); + + invalidateModelCache(); // recreate sat solver d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_nullRegistrar, - d_nullContext); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, + d_nullContext, d_bv->globals()); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); d_satSolver->setNotify(d_satSolverNotify); } + +} /* namespace CVC4::theory::bv */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ 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 */ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 4b3649a86..8ded63c28 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,6 +23,7 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/statistics_registry.h" +#include "smt/smt_globals.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" @@ -35,10 +36,10 @@ namespace bv { class CoreSolver; class InequalitySolver; class AlgebraicSolver; -class BitblastSolver; +class BitblastSolver; class EagerBitblastSolver; - + class AbstractionModule; class TheoryBV : public Theory { @@ -49,14 +50,14 @@ class TheoryBV : public Theory { /** Context dependent set of atoms we already propagated */ context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; - - std::vector<SubtheorySolver*> d_subtheories; - __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; + std::vector<SubtheorySolver*> d_subtheories; + __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals); + ~TheoryBV(); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -80,13 +81,14 @@ public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); void enableCoreTheorySlicer(); - + Node ppRewrite(TNode t); void ppStaticLearn(TNode in, NodeBuilder<>& learned); - + void presolve(); - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + private: class Statistics { |