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 | |
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')
36 files changed, 394 insertions, 314 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index f39006788..1cd617b64 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -53,7 +53,6 @@ #pragma once -#include "expr/result.h" #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "theory/arith/error_set.h" @@ -61,6 +60,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" #include "util/dense_map.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1e3b21b17..3c5c1c414 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -28,9 +28,11 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) - , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) +TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) + , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) {} TheoryArith::~TheoryArith(){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index a0a8e2c89..d26a120ae 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -46,7 +46,9 @@ private: KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); virtual ~TheoryArith(); /** diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ab800f10d..bf1810331 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,7 +33,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() @@ -70,6 +69,7 @@ #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" +#include "util/result.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 0c2a704e8..32c12eba7 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -31,7 +31,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/arith_options.h" #include "smt/logic_exception.h" @@ -67,6 +66,7 @@ #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 2863fad8a..ab57eb260 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -51,50 +51,52 @@ const bool d_solveWrite2 = false; //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo), - d_numRow("theory::arrays::number of Row lemmas", 0), - d_numExt("theory::arrays::number of Ext lemmas", 0), - d_numProp("theory::arrays::number of propagations", 0), - d_numExplain("theory::arrays::number of explanations", 0), - d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), - d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true), - d_ppFacts(u), - // d_ppCache(u), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true), - d_conflict(c, false), - d_backtracker(c), - d_infoMap(c, &d_backtracker), - d_mergeQueue(c), - d_mergeInProgress(false), - d_RowQueue(c), - d_RowAlreadyAdded(u), - d_sharedArrays(c), - d_sharedOther(c), - d_sharedTerms(c, false), - d_reads(c), - d_constReadsList(c), - d_constReadsContext(new context::Context()), - d_contextPopper(c, d_constReadsContext), - d_skolemIndex(c, 0), - d_decisionRequests(c), - d_permRef(c), - d_modelConstraints(c), - d_lemmasSaved(c), - d_defValues(c), - d_readTableContext(new context::Context()), - d_arrayMerges(c), - d_inCheckModel(false) +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals), + d_numRow("theory::arrays::number of Row lemmas", 0), + d_numExt("theory::arrays::number of Ext lemmas", 0), + d_numProp("theory::arrays::number of propagations", 0), + d_numExplain("theory::arrays::number of explanations", 0), + d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), + d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), + d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true), + d_ppFacts(u), + // d_ppCache(u), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_isPreRegistered(c), + d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true), + d_conflict(c, false), + d_backtracker(c), + d_infoMap(c, &d_backtracker), + d_mergeQueue(c), + d_mergeInProgress(false), + d_RowQueue(c), + d_RowAlreadyAdded(u), + d_sharedArrays(c), + d_sharedOther(c), + d_sharedTerms(c, false), + d_reads(c), + d_constReadsList(c), + d_constReadsContext(new context::Context()), + d_contextPopper(c, d_constReadsContext), + d_skolemIndex(c, 0), + d_decisionRequests(c), + d_permRef(c), + d_modelConstraints(c), + d_lemmasSaved(c), + d_defValues(c), + d_readTableContext(new context::Context()), + d_arrayMerges(c), + d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); StatisticsRegistry::registerStat(&d_numExt); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 28d994835..98cba0420 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -126,7 +126,9 @@ class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index a4a3757cd..246f1e7e8 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -28,9 +28,11 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) { - } + TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals) + : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, globals) + {} PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index fa6e8ab5c..2fbc0e402 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -27,8 +27,10 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} + TheoryBuiltin(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, globals) {} std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ 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 { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3d70e9a9a..9ba20fcc9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -31,32 +31,34 @@ #include "theory/type_enumerator.h" #include "theory/valuation.h" - using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::datatypes; - - -TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), - //d_cycle_check(c), - d_hasSeenCycle(c, false), - d_infer(c), - d_infer_exp(c), - d_notify( *this ), - d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true), - d_labels( c ), - d_selector_apps( c ), - //d_consEqc( c ), - d_conflict( c, false ), - d_collectTermsCache( c ), - d_consTerms( c ), - d_selTerms( c ), - d_singleton_eq( u ){ +namespace CVC4 { +namespace theory { +namespace datatypes { + +TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + SmtGlobals* globals) + : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, globals), + //d_cycle_check(c), + d_hasSeenCycle(c, false), + d_infer(c), + d_infer_exp(c), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true), + d_labels( c ), + d_selector_apps( c ), + //d_consEqc( c ), + d_conflict( c, false ), + d_collectTermsCache( c ), + d_consTerms( c ), + d_selTerms( c ), + d_singleton_eq( u ) +{ // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); @@ -2044,3 +2046,7 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& } return false; } + +} /* namepsace CVC4::theory::datatypes */ +} /* namepsace CVC4::theory */ +} /* namepsace CVC4 */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index bbbf799bd..fc6e435cc 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -180,31 +180,40 @@ private: /** sygus utilities */ SygusSplit * d_sygus_split; SygusSymBreak * d_sygus_sym_break; + private: /** singleton lemmas (for degenerate co-datatype case) */ std::map< TypeNode, Node > d_singleton_lemma[2]; + /** Cache for singleton equalities processed */ BoolMap d_singleton_eq; -private: + /** assert fact */ void assertFact( Node fact, Node exp ); + /** flush pending facts */ void flushPendingFacts(); + /** do pending merged */ void doPendingMerges(); + /** get or make eqc info */ EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); + /** has eqc info */ bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); } + /** get eqc constructor */ TNode getEqcConstructor( TNode r ); + protected: /** compute care graph */ void computeCareGraph(); + public: TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, SmtGlobals* globals); ~TheoryDatatypes(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 6400fec38..9a8d77844 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -51,13 +51,11 @@ namespace removeToFPGeneric { /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ -TheoryFp::TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo) : - Theory(THEORY_FP, c, u, out, valuation, logicInfo) { -}/* TheoryFp::TheoryFp() */ +TheoryFp::TheoryFp(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_FP, c, u, out, valuation, logicInfo, globals) +{}/* TheoryFp::TheoryFp() */ Node TheoryFp::expandDefinition(LogicRequest &, Node node) { diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 6fb41685f..fe3c377af 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -14,10 +14,11 @@ public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo); + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + SmtGlobals* globals); Node expandDefinition(LogicRequest &, Node node); diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 427ac577c..8cba51c8f 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -26,15 +26,16 @@ using namespace std; -using namespace CVC4; -using namespace theory; -using namespace idl; - -TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo) -: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) -, d_model(c) -, d_assertionsDB(c) +namespace CVC4 { +namespace theory { +namespace idl { + +TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) + , d_model(c) + , d_assertionsDB(c) {} Node TheoryIdl::ppRewrite(TNode atom) { @@ -148,3 +149,7 @@ bool TheoryIdl::processAssertion(const IDLAssertion& assertion) { // Everything fine, no conflict return true; } + +} /* namepsace CVC4::theory::idl */ +} /* namepsace CVC4::theory */ +} /* namepsace CVC4 */ diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 7c879e722..aa7267eb7 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -45,7 +45,8 @@ public: /** Theory constructor. */ TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); /** Pre-processing of input atoms */ Node ppRewrite(TNode atom); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 60d0e1d48..2113ea66e 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -86,8 +86,9 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint(uint64_t ammount) throw(Interrupted, UnsafeInterruptException, AssertionException) { - } + virtual void safePoint(uint64_t amount) + throw(Interrupted, UnsafeInterruptException, AssertionException) + {} /** * Indicate a theory conflict has arisen. diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e9ff60137..b808f4cd5 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,8 +34,8 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), +TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) : + Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals), d_masterEqualityEngine(0) { d_numInstantiations = 0; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 98f486145..f24c10fc0 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -46,10 +46,14 @@ private: int d_baseDecLevel; eq::EqualityEngine* d_masterEqualityEngine; + private: - void computeCareGraph(); + void computeCareGraph(); + public: - TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryQuantifiers(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index db93c597c..82ebb5bf8 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -25,10 +25,11 @@ TheorySets::TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) : - Theory(THEORY_SETS, c, u, out, valuation, logicInfo), - d_internal(new TheorySetsPrivate(*this, c, u)) { -} + const LogicInfo& logicInfo, + SmtGlobals* globals) + : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, globals), + d_internal(new TheorySetsPrivate(*this, c, u)) +{} TheorySets::~TheorySets() { delete d_internal; diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 6136fc8f8..7ff8abec6 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -40,11 +40,9 @@ public: * Constructs a new instance of TheorySets w.r.t. the provided * contexts. */ - TheorySets(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo); + TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); ~TheorySets(); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f200397bc..0c3171065 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -19,12 +19,12 @@ #include <boost/foreach.hpp> #include "expr/emptyset.h" -#include "expr/result.h" #include "options/sets_options.h" #include "theory/sets/expr_patterns.h" // ONLY included here #include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" #include "theory/theory_model.h" +#include "util/result.h" using namespace std; using namespace CVC4::expr::pattern; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index dfd3c4803..b68687d54 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,42 +55,44 @@ Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, No } -TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), - RMAXINT(LONG_MAX), - d_notify( *this ), - d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true), - d_conflict(c, false), - d_infer(c), - d_infer_exp(c), - d_nf_pairs(c), - d_loop_antec(u), - d_length_intro_vars(u), - d_pregistered_terms_cache(u), - d_registered_terms_cache(u), - d_preproc(u), - d_preproc_cache(u), - d_extf_infer_cache(c), - d_congruent(c), - d_proxy_var(u), - d_proxy_var_to_length(u), - d_neg_ctn_eqlen(c), - d_neg_ctn_ulen(c), - d_neg_ctn_cached(u), - d_ext_func_terms(c), - d_regexp_memberships(c), - d_regexp_ucached(u), - d_regexp_ccached(c), - d_pos_memberships(c), - d_neg_memberships(c), - d_inter_cache(c), - d_inter_index(c), - d_processed_memberships(c), - d_regexp_ant(c), - d_input_vars(u), - d_input_var_lsum(u), - d_cardinality_lits(u), - d_curr_cardinality(c, 0) +TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, globals), + RMAXINT(LONG_MAX), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true), + d_conflict(c, false), + d_infer(c), + d_infer_exp(c), + d_nf_pairs(c), + d_loop_antec(u), + d_length_intro_vars(u), + d_pregistered_terms_cache(u), + d_registered_terms_cache(u), + d_preproc(u), + d_preproc_cache(u), + d_extf_infer_cache(c), + d_congruent(c), + d_proxy_var(u), + d_proxy_var_to_length(u), + d_neg_ctn_eqlen(c), + d_neg_ctn_ulen(c), + d_neg_ctn_cached(u), + d_ext_func_terms(c), + d_regexp_memberships(c), + d_regexp_ucached(u), + d_regexp_ccached(c), + d_pos_memberships(c), + d_neg_memberships(c), + d_inter_cache(c), + d_inter_index(c), + d_processed_memberships(c), + d_regexp_ant(c), + d_input_vars(u), + d_input_var_lsum(u), + d_cardinality_lits(u), + d_curr_cardinality(c, 0) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 40358649b..ddb800ee1 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -52,7 +52,9 @@ class TheoryStrings : public Theory { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryStrings(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals); ~TheoryStrings(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/theory.h b/src/theory/theory.h index 5f4c80cf2..d17d97f97 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -34,6 +34,7 @@ #include "options/theory_options.h" #include "options/theoryof_mode.h" #include "smt/logic_request.h" +#include "smt/smt_globals.h" #include "smt_util/command.h" #include "smt_util/dump.h" #include "theory/logic_info.h" @@ -245,7 +246,8 @@ protected: * Construct a Theory. */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw() + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals) throw() : d_id(id) , d_satContext(satContext) , d_userContext(userContext) @@ -261,6 +263,7 @@ protected: , d_out(&out) , d_valuation(valuation) , d_proofEnabled(false) + , d_globals(globals) { StatisticsRegistry::registerStat(&d_checkTime); StatisticsRegistry::registerStat(&d_computeCareGraphTime); @@ -313,6 +316,8 @@ protected: */ bool d_proofEnabled; + SmtGlobals* d_globals; + public: /** @@ -870,6 +875,10 @@ public: */ virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + + /** Returns a pointer to the globals copy the theory is using. */ + SmtGlobals* globals() { return d_globals; } + };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 52922e2ca..a55b3a1c9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -104,7 +104,8 @@ void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, - const LogicInfo& logicInfo) + const LogicInfo& logicInfo, + SmtGlobals* globals) : d_propEngine(NULL), d_decisionEngine(NULL), d_context(context), @@ -133,6 +134,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_false(), d_interrupted(false), d_resourceManager(NodeManager::currentResourceManager()), + d_globals(globals), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -1390,8 +1392,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable } // Share with other portfolio threads - if(options::lemmaOutputChannel() != NULL) { - options::lemmaOutputChannel()->notifyNewLemma(node.toExpr()); + if(d_globals->getLemmaOutputChannel() != NULL) { + d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); } // Run theory preprocessing, maybe diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2185f22ff..adc4daeee 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -30,6 +30,7 @@ #include "options/options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" +#include "smt/smt_globals.h" #include "smt_util/command.h" #include "theory/atom_requests.h" #include "theory/bv/bv_to_bool.h" @@ -206,6 +207,7 @@ class TheoryEngine { */ context::CDHashSet<Node, NodeHashFunction> d_hasPropagated; + /** * Statistics for a particular theory. */ @@ -476,10 +478,14 @@ class TheoryEngine { bool d_interrupted; ResourceManager* d_resourceManager; + /** Container for misc. globals. */ + SmtGlobals* d_globals; + public: /** Constructs a theory engine */ - TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic); + TheoryEngine(context::Context* context, context::UserContext* userContext, + RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals); /** Destroys a theory engine */ ~TheoryEngine(); @@ -498,7 +504,9 @@ public: inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo); + d_theoryTable[theoryId] = + new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], + theory::Valuation(this), d_logicInfo, d_globals); } inline void setPropEngine(prop::PropEngine* propEngine) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 31bee316a..e21b7ef7d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -30,18 +30,20 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_UF, c, u, out, valuation, logicInfo), - d_notify(*this), - /* The strong theory solver can be notified by EqualityEngine::init(), - * so make sure it's initialized first. */ - d_thss(NULL), - d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true), - d_conflict(c, false), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_functionsTerms(c), - d_symb(u) +TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals), + d_notify(*this), + /* The strong theory solver can be notified by EqualityEngine::init(), + * so make sure it's initialized first. */ + d_thss(NULL), + d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true), + d_conflict(c, false), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_functionsTerms(c), + d_symb(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 82597e286..aff78f53d 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -161,7 +161,9 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); ~TheoryUF(); |