From f45bad0112192abb47cd350abdb5414e385c38b1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 15 Nov 2019 17:52:15 -0800 Subject: Remove static --- src/CMakeLists.txt | 2 + src/proof/arith_proof.cpp | 8 +- src/proof/arith_proof.h | 13 +- src/proof/array_proof.cpp | 11 +- src/proof/array_proof.h | 13 +- src/proof/bitvector_proof.cpp | 12 +- src/proof/bitvector_proof.h | 4 +- src/proof/clausal_bitvector_proof.cpp | 5 +- src/proof/clausal_bitvector_proof.h | 24 ++- src/proof/proof_manager.cpp | 20 ++- src/proof/proof_manager.h | 32 ++-- src/proof/proof_utils.cpp | 12 +- src/proof/proof_utils.h | 5 +- src/proof/resolution_bitvector_proof.cpp | 4 +- src/proof/resolution_bitvector_proof.h | 8 +- src/proof/theory_proof.cpp | 65 ++++--- src/proof/theory_proof.h | 58 +++--- src/proof/uf_proof.cpp | 8 +- src/proof/uf_proof.h | 13 +- src/prop/cnf_stream.cpp | 30 ++-- src/prop/cnf_stream.h | 17 +- src/prop/prop_engine.cpp | 34 ++-- src/prop/prop_engine.h | 24 ++- src/smt/smt_engine.cpp | 23 ++- src/theory/arith/theory_arith.cpp | 16 +- src/theory/arith/theory_arith.h | 112 ++++++------ src/theory/arith/theory_arith_private.cpp | 9 +- src/theory/arith/theory_arith_private.h | 82 +++++---- src/theory/arrays/theory_arrays.cpp | 5 +- src/theory/arrays/theory_arrays.h | 9 +- src/theory/booleans/theory_bool.h | 15 +- src/theory/builtin/theory_builtin.h | 13 +- src/theory/bv/bitblast/aig_bitblaster.cpp | 4 +- src/theory/bv/bitblast/aig_bitblaster.h | 2 +- src/theory/bv/bitblast/bitblaster.h | 11 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 18 +- src/theory/bv/bitblast/eager_bitblaster.h | 4 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 21 +-- src/theory/bv/bitblast/lazy_bitblaster.h | 3 +- src/theory/bv/bv_eager_solver.cpp | 11 +- src/theory/bv/bv_eager_solver.h | 7 +- src/theory/bv/bv_quick_check.cpp | 12 +- src/theory/bv/bv_quick_check.h | 65 +++---- src/theory/bv/bv_subtheory.h | 11 +- src/theory/bv/bv_subtheory_algebraic.cpp | 15 +- src/theory/bv/bv_subtheory_algebraic.h | 4 +- src/theory/bv/bv_subtheory_bitblast.cpp | 10 +- src/theory/bv/bv_subtheory_bitblast.h | 5 +- src/theory/bv/bv_subtheory_core.cpp | 29 ++- src/theory/bv/bv_subtheory_core.h | 7 +- src/theory/bv/bv_subtheory_inequality.h | 26 +-- src/theory/bv/theory_bv.cpp | 15 +- src/theory/bv/theory_bv.h | 22 ++- src/theory/bv/theory_bv_utils.cpp | 16 +- src/theory/bv/theory_bv_utils.h | 5 +- src/theory/datatypes/theory_datatypes.cpp | 5 +- src/theory/datatypes/theory_datatypes.h | 8 +- src/theory/fp/theory_fp.cpp | 11 +- src/theory/fp/theory_fp.h | 8 +- src/theory/idl/theory_idl.cpp | 13 +- src/theory/idl/theory_idl.h | 11 +- src/theory/quantifiers/theory_quantifiers.cpp | 9 +- src/theory/quantifiers/theory_quantifiers.h | 7 +- src/theory/sep/theory_sep.cpp | 25 +-- src/theory/sep/theory_sep.h | 7 +- src/theory/sets/theory_sets.cpp | 5 +- src/theory/sets/theory_sets.h | 3 +- src/theory/strings/theory_strings.cpp | 5 +- src/theory/strings/theory_strings.h | 7 +- src/theory/term_registration_visitor.cpp | 38 ++-- src/theory/term_registration_visitor.h | 51 +++--- src/theory/theory.cpp | 2 + src/theory/theory.h | 3 +- src/theory/theory_engine.cpp | 242 ++++++++++++++++++++++---- src/theory/theory_engine.h | 68 ++++++-- src/theory/uf/theory_uf.cpp | 8 +- src/theory/uf/theory_uf.h | 8 +- 77 files changed, 1023 insertions(+), 550 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4f64760e0..09388c5ef 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -229,6 +229,8 @@ libcvc4_add_sources( smt/command_list.h smt/dump.cpp smt/dump.h + smt/environment.cpp + smt/environment.h smt/logic_exception.h smt/logic_request.cpp smt/logic_request.h diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 77f4b1630..65e16c8f3 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -654,8 +654,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, } } -ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe) - : TheoryProof(arith, pe), d_recorder(), d_realMode(false) +ArithProof::ArithProof(Environment* env, + theory::arith::TheoryArith* arith, + TheoryProofEngine* pe) + : TheoryProof(env, arith, pe), d_recorder(), d_realMode(false) { arith->setProofRecorder(&d_recorder); } @@ -688,7 +690,7 @@ void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM // !d_realMode <--> term.getType().isInteger() - Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARITH); + Assert(d_env->theoryOf(term) == theory::THEORY_ARITH); switch (term.getKind()) { case kind::CONST_RATIONAL: diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index a1df24fac..71e03657f 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -72,16 +72,21 @@ protected: theory::TheoryId getTheoryId() override; public: - ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine); + ArithProof(Environment* env, + theory::arith::TheoryArith* arith, + TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; }; class LFSCArithProof : public ArithProof { public: - LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine) - : ArithProof(arith, proofEngine) - {} + LFSCArithProof(Environment* env, + theory::arith::TheoryArith* arith, + TheoryProofEngine* proofEngine) + : ArithProof(env, arith, proofEngine) + { + } void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) override; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index ec2f85829..013e7e5f4 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -1076,8 +1076,10 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } } -ArrayProof::ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* pe) - : TheoryProof(arrays, pe) +ArrayProof::ArrayProof(Environment* env, + theory::arrays::TheoryArrays* arrays, + TheoryProofEngine* pe) + : TheoryProof(env, arrays, pe) {} theory::TheoryId ArrayProof::getTheoryId() { return theory::THEORY_ARRAYS; } @@ -1124,9 +1126,10 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) { } void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { - Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS); + Assert(d_env->theoryOf(term) == theory::THEORY_ARRAYS); - if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) { + if (d_env->theoryOf(term) != theory::THEORY_ARRAYS) + { // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term // hiding as a subterm of an array term. In that case, send it back to the dispatcher. d_proofEngine->printBoundTerm(term, os, map); diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 372ad1f67..9660fbe50 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -82,7 +82,9 @@ protected: theory::TheoryId getTheoryId() override; public: - ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine); + ArrayProof(Environment* env, + theory::arrays::TheoryArrays* arrays, + TheoryProofEngine* proofEngine); std::string skolemToLiteral(Expr skolem); @@ -91,9 +93,12 @@ protected: class LFSCArrayProof : public ArrayProof { public: - LFSCArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) - : ArrayProof(arrays, proofEngine) - {} + LFSCArrayProof(Environment* env, + theory::arrays::TheoryArrays* arrays, + TheoryProofEngine* proofEngine) + : ArrayProof(env, arrays, proofEngine) + { + } void printOwnedTerm(Expr term, std::ostream& os, diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 98f57e25f..baba3b0a3 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -25,9 +25,10 @@ namespace CVC4 { namespace proof { -BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, +BitVectorProof::BitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : TheoryProof(bv, proofEngine), + : TheoryProof(env, bv, proofEngine), d_declarations(), d_seenBBTerms(), d_bbTerms(), @@ -59,7 +60,7 @@ void BitVectorProof::registerTermBB(Expr term) // sees it, if it belongs to another theory, it won't register it with this // proof. So, we need to tell the engine to inform us. - if (theory::Theory::theoryOf(term) != theory::THEORY_BV) + if (d_env->theoryOf(term) != theory::THEORY_BV) { Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl; @@ -127,10 +128,9 @@ void BitVectorProof::printOwnedTerm(Expr term, { Debug("pf::bv") << std::endl << "(pf::bv) BitVectorProof::printOwnedTerm( " << term - << " ), theory is: " << theory::Theory::theoryOf(term) - << std::endl; + << " ), theory is: " << d_env->theoryOf(term) << std::endl; - Assert(theory::Theory::theoryOf(term) == theory::THEORY_BV); + Assert(d_env->theoryOf(term) == theory::THEORY_BV); // peel off eager bit-blasting trick if (term.getKind() == kind::BITVECTOR_EAGER_ATOM) { diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index f0a0717fa..878d7d5a6 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -74,7 +74,9 @@ typedef std::unordered_map ExprToString; class BitVectorProof : public TheoryProof { protected: - BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); + BitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine); virtual ~BitVectorProof(){}; // Set of BV variables in the input. (e.g. "a" in [ a = 000 ] ^ [ a == 001 ]) diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index bb9213b4b..f3ec13a99 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -41,9 +41,10 @@ namespace CVC4 { namespace proof { -ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv, +ClausalBitVectorProof::ClausalBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : BitVectorProof(bv, proofEngine), + : BitVectorProof(env, bv, proofEngine), d_clauses(), d_originalClauseIndices(), d_binaryDratProof(), diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h index 2047e325c..b4683ac99 100644 --- a/src/proof/clausal_bitvector_proof.h +++ b/src/proof/clausal_bitvector_proof.h @@ -42,7 +42,8 @@ namespace proof { class ClausalBitVectorProof : public BitVectorProof { public: - ClausalBitVectorProof(theory::bv::TheoryBV* bv, + ClausalBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); ~ClausalBitVectorProof() = default; @@ -123,9 +124,10 @@ class ClausalBitVectorProof : public BitVectorProof class LfscClausalBitVectorProof : public ClausalBitVectorProof { public: - LfscClausalBitVectorProof(theory::bv::TheoryBV* bv, + LfscClausalBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : ClausalBitVectorProof(bv, proofEngine) + : ClausalBitVectorProof(env, bv, proofEngine) { } @@ -144,9 +146,10 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof class LfscDratBitVectorProof : public LfscClausalBitVectorProof { public: - LfscDratBitVectorProof(theory::bv::TheoryBV* bv, + LfscDratBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : LfscClausalBitVectorProof(bv, proofEngine) + : LfscClausalBitVectorProof(env, bv, proofEngine) { } @@ -159,9 +162,10 @@ class LfscDratBitVectorProof : public LfscClausalBitVectorProof class LfscLratBitVectorProof : public LfscClausalBitVectorProof { public: - LfscLratBitVectorProof(theory::bv::TheoryBV* bv, + LfscLratBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : LfscClausalBitVectorProof(bv, proofEngine) + : LfscClausalBitVectorProof(env, bv, proofEngine) { } @@ -174,8 +178,10 @@ class LfscLratBitVectorProof : public LfscClausalBitVectorProof class LfscErBitVectorProof : public LfscClausalBitVectorProof { public: - LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : LfscClausalBitVectorProof(bv, proofEngine) + LfscErBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(env, bv, proofEngine) { } diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index fa4c1ecb5..fd563a92e 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -58,8 +58,11 @@ std::string append(const std::string& str, uint64_t num) { return os.str(); } -ProofManager::ProofManager(context::Context* context, ProofFormat format) - : d_context(context), +ProofManager::ProofManager(Environment* env, + context::Context* context, + ProofFormat format) + : d_env(env), + d_context(context), d_satProof(NULL), d_cnfProof(NULL), d_theoryProof(NULL), @@ -88,6 +91,7 @@ const Proof& ProofManager::getProof(SmtEngine* smt) { Assert(currentPM()->d_format == LFSC); currentPM()->d_fullProof.reset(new LFSCProof( + currentPM()->d_env, smt, static_cast(getSatProof()), static_cast(getCnfProof()), @@ -177,7 +181,7 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream, void ProofManager::initTheoryProofEngine() { Assert(currentPM()->d_theoryProof == NULL); Assert(currentPM()->d_format == LFSC); - currentPM()->d_theoryProof = new LFSCTheoryProofEngine(); + currentPM()->d_theoryProof = new LFSCTheoryProofEngine(currentPM()->d_env); } std::string ProofManager::getInputClauseName(ClauseId id, @@ -549,11 +553,13 @@ void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } -LFSCProof::LFSCProof(SmtEngine* smtEngine, +LFSCProof::LFSCProof(Environment* env, + SmtEngine* smtEngine, CoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory) - : d_satProof(sat), + : d_env(env), + d_satProof(sat), d_cnfProof(cnf), d_theoryProof(theory), d_smtEngine(smtEngine) @@ -658,7 +664,7 @@ void LFSCProof::toStream(std::ostream& out) const { // For arithmetic: these literals are not normalized, causing an error // in Arith. - if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) + if (d_env->theoryOf(*it) == theory::THEORY_ARITH) { d_cnfProof->ensureLiteral( *it, @@ -680,7 +686,7 @@ void LFSCProof::toStream(std::ostream& out) const it != used_assertions.end(); ++it) { - utils::collectAtoms(*it, atoms); + utils::collectAtoms(d_env, *it, atoms); } std::set::iterator atomIt; diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index ec845e41d..704d8c45d 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -31,6 +31,7 @@ #include "proof/proof.h" #include "proof/proof_utils.h" #include "proof/skolemization_manager.h" +#include "smt/environment.h" #include "theory/logic_info.h" #include "theory/substitutions.h" #include "util/proof.h" @@ -141,6 +142,8 @@ private: }; class ProofManager { + Environment* d_env; + context::Context* d_context; CoreSatProof* d_satProof; @@ -172,36 +175,39 @@ class ProofManager { protected: LogicInfo d_logic; -public: - ProofManager(context::Context* context, ProofFormat format = LFSC); + public: + ProofManager(Environment* env, + context::Context* context, + ProofFormat format = LFSC); ~ProofManager(); static ProofManager* currentPM(); // initialization - void initSatProof(Minisat::Solver* solver); - static void initCnfProof(CVC4::prop::CnfStream* cnfStream, - context::Context* ctx); - static void initTheoryProofEngine(); + void initSatProof(Minisat::Solver* solver); + static void initCnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx); + static void initTheoryProofEngine(); // getting various proofs static const Proof& getProof(SmtEngine* smt); - static CoreSatProof* getSatProof(); - static CnfProof* getCnfProof(); + static CoreSatProof* getSatProof(); + static CnfProof* getCnfProof(); static TheoryProofEngine* getTheoryProofEngine(); - static TheoryProof* getTheoryProof( theory::TheoryId id ); + static TheoryProof* getTheoryProof(theory::TheoryId id); static UFProof* getUfProof(); static proof::ResolutionBitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); static ArithProof* getArithProof(); - static SkolemizationManager *getSkolemizationManager(); + static SkolemizationManager* getSkolemizationManager(); // iterators over data shared by proofs typedef ExprSet::const_iterator assertions_iterator; // iterate over the assertions (these are arbitrary boolean formulas) - assertions_iterator begin_assertions() const { + assertions_iterator begin_assertions() const + { return d_inputFormulas.begin(); } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } @@ -350,7 +356,8 @@ public: class LFSCProof : public Proof { public: - LFSCProof(SmtEngine* smtEngine, + LFSCProof(Environment* env, + SmtEngine* smtEngine, CoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory); @@ -367,6 +374,7 @@ class LFSCProof : public Proof void checkUnrewrittenAssertion(const NodeSet& assertions) const; + Environment* d_env; CoreSatProof* d_satProof; LFSCCnfProof* d_cnfProof; LFSCTheoryProofEngine* d_theoryProof; diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index 3342d421a..84eefc17e 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -21,16 +21,18 @@ namespace CVC4 { namespace utils { -void collectAtoms(TNode node, std::set& seen) { +void collectAtoms(Environment* env, TNode node, std::set& seen) +{ if (seen.find(node) != seen.end()) return; - if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) { - seen.insert(node); - return; + if (env->theoryOf(node) != theory::THEORY_BOOL || node.isVar()) + { + seen.insert(node); + return; } for (unsigned i = 0; i < node.getNumChildren(); ++i) { - collectAtoms(node[i], seen); + collectAtoms(env, node[i], seen); } } diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index 66e20069d..a8173fc8b 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -25,6 +25,7 @@ #include #include "expr/node_manager.h" +#include "smt/environment.h" namespace CVC4 { @@ -225,8 +226,6 @@ inline const bool getBit(Expr expr, unsigned i) { return (bit == 1u); } -void collectAtoms(TNode node, std::set& seen); - - +void collectAtoms(Environment* env, TNode node, std::set& seen); } } diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index f4ced1748..5b4847544 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -42,8 +42,8 @@ namespace CVC4 { namespace proof { ResolutionBitVectorProof::ResolutionBitVectorProof( - theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : BitVectorProof(bv, proofEngine), + Environment* env, theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : BitVectorProof(env, bv, proofEngine), d_resolutionProof(), d_isAssumptionConflict(false) { diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index 5fd11092f..eac469ff7 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -48,7 +48,8 @@ namespace proof { class ResolutionBitVectorProof : public BitVectorProof { public: - ResolutionBitVectorProof(theory::bv::TheoryBV* bv, + ResolutionBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); /** @@ -90,9 +91,10 @@ class ResolutionBitVectorProof : public BitVectorProof class LfscResolutionBitVectorProof : public ResolutionBitVectorProof { public: - LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv, + LfscResolutionBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : ResolutionBitVectorProof(bv, proofEngine) + : ResolutionBitVectorProof(env, bv, proofEngine) { } void printTheoryLemmaProof(std::vector& lemma, diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 1f3e6abf1..248cfa972 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -53,11 +53,10 @@ using proof::ResolutionBitVectorProof; unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; -TheoryProofEngine::TheoryProofEngine() - : d_registrationCache() - , d_theoryProofTable() +TheoryProofEngine::TheoryProofEngine(Environment* env) + : d_env(env), d_registrationCache(), d_theoryProofTable() { - d_theoryProofTable[theory::THEORY_BOOL] = new LFSCBooleanProof(this); + d_theoryProofTable[theory::THEORY_BOOL] = new LFSCBooleanProof(d_env, this); } TheoryProofEngine::~TheoryProofEngine() { @@ -76,7 +75,8 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl; if (id == theory::THEORY_UF) { - d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); + d_theoryProofTable[id] = + new LFSCUFProof(d_env, (theory::uf::TheoryUF*)th, this); return; } @@ -90,17 +90,17 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { { case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT: { - bvp = new proof::LfscDratBitVectorProof(thBv, this); + bvp = new proof::LfscDratBitVectorProof(d_env, thBv, this); break; } case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT: { - bvp = new proof::LfscLratBitVectorProof(thBv, this); + bvp = new proof::LfscLratBitVectorProof(d_env, thBv, this); break; } case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER: { - bvp = new proof::LfscErBitVectorProof(thBv, this); + bvp = new proof::LfscErBitVectorProof(d_env, thBv, this); break; } default: @@ -113,19 +113,21 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { else { proof::BitVectorProof* bvp = - new proof::LfscResolutionBitVectorProof(thBv, this); + new proof::LfscResolutionBitVectorProof(d_env, thBv, this); d_theoryProofTable[id] = bvp; } return; } if (id == theory::THEORY_ARRAYS) { - d_theoryProofTable[id] = new LFSCArrayProof((theory::arrays::TheoryArrays*)th, this); + d_theoryProofTable[id] = + new LFSCArrayProof(d_env, (theory::arrays::TheoryArrays*)th, this); return; } if (id == theory::THEORY_ARITH) { - d_theoryProofTable[id] = new LFSCArithProof((theory::arith::TheoryArith*)th, this); + d_theoryProofTable[id] = + new LFSCArithProof(d_env, (theory::arith::TheoryArith*)th, this); return; } @@ -172,8 +174,9 @@ void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Assert(c1.isConst()); Assert(c2.isConst()); - Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2)); - getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2, globalLetMap); + Assert(d_env->theoryOf(c1) == d_env->theoryOf(c2)); + getTheoryProof(d_env->theoryOf(c1)) + ->printConstantDisequalityProof(os, c1, c2, globalLetMap); } void TheoryProofEngine::registerTerm(Expr term) { @@ -185,7 +188,7 @@ void TheoryProofEngine::registerTerm(Expr term) { Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; - theory::TheoryId theory_id = theory::Theory::theoryOf(term); + theory::TheoryId theory_id = d_env->theoryOf(term); Debug("pf::tp::register") << "Term's theory( " << term << " ) = " << theory_id << std::endl; @@ -284,7 +287,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { } void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) { - theory::TheoryId theory_id = theory::Theory::theoryOf(term); + theory::TheoryId theory_id = d_env->theoryOf(term); // boolean terms and ITEs are special because they // are common to all theories @@ -390,13 +393,13 @@ void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, Node n1 = it->first; Node n2 = it->second; Assert(n1.toExpr() == utils::mkFalse() - || theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + || d_env->theoryOf(n1) == d_env->theoryOf(n2)); std::ostringstream rewriteRule; rewriteRule << ".lrr" << d_assertionToRewrite.size(); os << "(th_let_pf _ "; - getTheoryProof(theory::Theory::theoryOf(n1))->printRewriteProof(os, n1, n2); + getTheoryProof(d_env->theoryOf(n1))->printRewriteProof(os, n1, n2); os << "(\\ " << rewriteRule.str() << "\n"; d_assertionToRewrite[it->first] = rewriteRule.str(); @@ -1021,13 +1024,22 @@ void TheoryProof::printTheoryLemmaProof(std::vector& lemma, Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; if (d_theory->getId()==theory::THEORY_UF) { - th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, + th = new theory::uf::TheoryUF(d_env, + &fakeContext, + &fakeContext, + oc, + v, ProofManager::currentPM()->getLogicInfo(), "replay::"); } else if (d_theory->getId()==theory::THEORY_ARRAYS) { - th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, - ProofManager::currentPM()->getLogicInfo(), - "replay::"); + th = new theory::arrays::TheoryArrays( + d_env, + &fakeContext, + &fakeContext, + oc, + v, + ProofManager::currentPM()->getLogicInfo(), + "replay::"); } else if (d_theory->getId() == theory::THEORY_ARITH) { Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl; os << " (clausify_false trust)"; @@ -1044,8 +1056,9 @@ void TheoryProof::printTheoryLemmaProof(std::vector& lemma, MyPreRegisterVisitor preRegVisitor(th); for (unsigned i=0; igetId() == theory::Theory::theoryOf(strippedLit)) { + if (strippedLit.getKind() == kind::EQUAL + || d_theory->getId() == d_env->theoryOf(strippedLit)) + { Node lit = Node::fromExpr( lemma[i] ).negate(); Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl; NodeVisitor::run(preRegVisitor, lit); @@ -1115,12 +1128,12 @@ bool TheoryProofEngine::printsAsBool(const Node &n) { return false; } - theory::TheoryId theory_id = theory::Theory::theoryOf(n); + theory::TheoryId theory_id = d_env->theoryOf(n); return getTheoryProof(theory_id)->printsAsBool(n); } -BooleanProof::BooleanProof(TheoryProofEngine* proofEngine) - : TheoryProof(NULL, proofEngine) +BooleanProof::BooleanProof(Environment* env, TheoryProofEngine* proofEngine) + : TheoryProof(env, NULL, proofEngine) {} void BooleanProof::registerTerm(Expr term) { diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index b487b62a8..7d58a8c1a 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -28,6 +28,7 @@ #include "proof/clause_id.h" #include "proof/proof_utils.h" #include "prop/sat_solver_types.h" +#include "smt/environment.h" #include "theory/uf/equality_engine.h" #include "util/proof.h" namespace CVC4 { @@ -47,19 +48,8 @@ typedef std::set TheoryIdSet; typedef std::map ExprToTheoryIds; class TheoryProofEngine { -protected: - ExprSet d_registrationCache; - TheoryProofTable d_theoryProofTable; - ExprToTheoryIds d_exprToTheoryIds; - - /** - * Returns whether the theory is currently supported in proof - * production mode. - */ - bool supportedTheory(theory::TheoryId id); -public: - - TheoryProofEngine(); + public: + TheoryProofEngine(Environment* env); virtual ~TheoryProofEngine(); /** @@ -155,13 +145,25 @@ public: virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; bool printsAsBool(const Node &n); + + protected: + Environment* d_env; + ExprSet d_registrationCache; + TheoryProofTable d_theoryProofTable; + ExprToTheoryIds d_exprToTheoryIds; + + /** + * Returns whether the theory is currently supported in proof + * production mode. + */ + bool supportedTheory(theory::TheoryId id); }; class LFSCTheoryProofEngine : public TheoryProofEngine { void bind(Expr term, ProofLetMap& map, Bindings& let_order); -public: - LFSCTheoryProofEngine() - : TheoryProofEngine() {} + + public: + LFSCTheoryProofEngine(Environment* env) : TheoryProofEngine(env) {} void printTheoryTerm(Expr term, std::ostream& os, @@ -194,7 +196,7 @@ public: void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os); -private: + private: static void dumpTheoryLemmas(const IdToSatClause& lemmas); // TODO: this function should be moved into the BV prover. @@ -203,17 +205,20 @@ private: }; class TheoryProof { -protected: + protected: + Environment* d_env; // Pointer to the theory for this proof theory::Theory* d_theory; TheoryProofEngine* d_proofEngine; virtual theory::TheoryId getTheoryId() = 0; public: - TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine) - : d_theory(th) - , d_proofEngine(proofEngine) - {} + TheoryProof(Environment* env, + theory::Theory* th, + TheoryProofEngine* proofEngine) + : d_env(env), d_theory(th), d_proofEngine(proofEngine) + { + } virtual ~TheoryProof() {}; /** * Print a term belonging some theory, not necessarily this one. @@ -366,16 +371,17 @@ protected: theory::TheoryId getTheoryId() override; public: - BooleanProof(TheoryProofEngine* proofEngine); + BooleanProof(Environment* env, TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; }; class LFSCBooleanProof : public BooleanProof { public: - LFSCBooleanProof(TheoryProofEngine* proofEngine) - : BooleanProof(proofEngine) - {} + LFSCBooleanProof(Environment* env, TheoryProofEngine* proofEngine) + : BooleanProof(env, proofEngine) + { + } void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) override; diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index b88f7dc33..9e5b82232 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -581,8 +581,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, } } -UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe) - : TheoryProof(uf, pe) +UFProof::UFProof(Environment* env, + theory::uf::TheoryUF* uf, + TheoryProofEngine* pe) + : TheoryProof(env, uf, pe) {} theory::TheoryId UFProof::getTheoryId() { return theory::THEORY_UF; } @@ -626,7 +628,7 @@ void UFProof::registerTerm(Expr term) { void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; - Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF); + Assert(d_env->theoryOf(term) == theory::THEORY_UF); if (term.getKind() == kind::VARIABLE || term.getKind() == kind::SKOLEM || diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index ca8b3f90e..16755e528 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -65,16 +65,21 @@ protected: theory::TheoryId getTheoryId() override; public: - UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine); + UFProof(Environment* env, + theory::uf::TheoryUF* uf, + TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; }; class LFSCUFProof : public UFProof { public: - LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine) - : UFProof(uf, proofEngine) - {} + LFSCUFProof(Environment* env, + theory::uf::TheoryUF* uf, + TheoryProofEngine* proofEngine) + : UFProof(env, uf, proofEngine) + { + } void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) override; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 7df5fb492..1d622cd1b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -42,10 +42,14 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, bool fullLitToNodeMap, +CnfStream::CnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + bool fullLitToNodeMap, std::string name) - : d_satSolver(satSolver), + : d_env(env), + d_satSolver(satSolver), d_booleanVariables(context), d_nodeToLiteralMap(context), d_literalToNodeMap(context), @@ -54,13 +58,17 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, d_registrar(registrar), d_name(name), d_cnfProof(NULL), - d_removable(false) { + d_removable(false) +{ } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, +TseitinCnfStream::TseitinCnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, context::Context* context, - bool fullLitToNodeMap, std::string name) - : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name) + bool fullLitToNodeMap, + std::string name) + : CnfStream(env, satSolver, registrar, context, fullLitToNodeMap, name) {} void CnfStream::assertClause(TNode node, SatClause& c) { @@ -155,8 +163,8 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { n = n[0]; } - if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL && - !n.isVar() ) { + if (d_env->theoryOf(n) == theory::THEORY_BOOL && !n.isVar()) + { // If we were called with something other than a theory atom (or // Boolean variable), we get a SatLiteral that is definitionally // equal to it. @@ -166,7 +174,9 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // These may already exist d_literalToNodeMap.insert_safe(lit, n); d_literalToNodeMap.insert_safe(~lit, n.notNode()); - } else { + } + else + { // We have a theory atom or variable. lit = convertAtom(n, noPreregistration); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a9b786615..3a4cfe209 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -31,6 +31,7 @@ #include "proof/proof_manager.h" #include "prop/registrar.h" #include "prop/theory_proxy.h" +#include "smt/environment.h" #include "smt_util/lemma_channels.h" namespace CVC4 { @@ -54,6 +55,8 @@ class CnfStream { NodeToLiteralMap; protected: + Environment* d_env; + /** The SAT solver we will be using */ SatSolver* d_satSolver; @@ -171,8 +174,11 @@ class CnfStream { * @param name string identifier to distinguish between different instances * even for non-theory literals. */ - CnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, bool fullLitToNodeMap = false, + CnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + bool fullLitToNodeMap = false, std::string name = ""); /** @@ -257,8 +263,11 @@ class TseitinCnfStream : public CnfStream { * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, bool fullLitToNodeMap = false, + TseitinCnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + bool fullLitToNodeMap = false, std::string name = ""); /** diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 8a0cc9f15..abb90e569 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -74,19 +74,25 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, - Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels) : - d_inCheckSat(false), - d_theoryEngine(te), - d_decisionEngine(de), - d_context(satContext), - d_theoryProxy(NULL), - d_satSolver(NULL), - d_registrar(NULL), - d_cnfStream(NULL), - d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) +PropEngine::PropEngine(Environment* env, + TheoryEngine* te, + DecisionEngine* de, + Context* satContext, + Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* channels) + : d_env(env), + d_inCheckSat(false), + d_theoryEngine(te), + d_decisionEngine(de), + d_context(satContext), + d_theoryProxy(NULL), + d_satSolver(NULL), + d_registrar(NULL), + d_cnfStream(NULL), + d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -95,7 +101,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream( - d_satSolver, d_registrar, userContext, true); + d_env, d_satSolver, d_registrar, userContext, true); d_theoryProxy = new TheoryProxy( this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index aaa65b85a..735c82bde 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,6 +28,7 @@ #include "expr/node.h" #include "options/options.h" #include "proof/proof_manager.h" +#include "smt/environment.h" #include "smt_util/lemma_channels.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -54,6 +55,7 @@ class PropEngine; * solving the SAT problem and conversion to CNF (via the CnfStream). */ class PropEngine { + Environment* d_env; /** * Indicates that the SAT solver is currently solving something and we should @@ -93,14 +95,18 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); -public: - + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, - context::Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels); + PropEngine(Environment* env, + TheoryEngine*, + DecisionEngine*, + context::Context* satContext, + context::Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* channels); /** * Destructor. @@ -114,7 +120,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { } + void shutdown() {} /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -134,7 +140,11 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); + void assertLemma(TNode node, + bool negated, + bool removable, + ProofRule rule, + TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 073c2ebc5..5d2d48f34 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -421,6 +421,8 @@ class SmtEnginePrivate : public NodeManagerListener { typedef unordered_map NodeToNodeHashMap; typedef unordered_map NodeToBoolHashMap; + Environment d_env; + /** * Manager for limiting time and abstract resource usage. */ @@ -651,6 +653,8 @@ class SmtEnginePrivate : public NodeManagerListener { d_smt.d_nodeManager->unsubscribeEvents(this); } + Environment* getEnvironment() { return &d_env; } + void cleanupPreprocessingPasses() { d_passes.clear(); } ResourceManager* getResourceManager() { return d_resourceManager; } @@ -893,7 +897,7 @@ SmtEngine::SmtEngine(ExprManager* em) // being parsed from the input file. Because of this, we cannot trust // that options::proof() is set correctly yet. #ifdef CVC4_PROOF - d_proofManager = new ProofManager(d_userContext); + d_proofManager = new ProofManager(d_private->getEnvironment(), d_userContext); #endif d_definedFunctions = new (true) DefinedFunctionMap(d_userContext); @@ -906,11 +910,13 @@ void SmtEngine::finishInit() Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_context, + d_theoryEngine = new TheoryEngine(d_private->getEnvironment(), + d_context, d_userContext, d_private->d_iteRemover, const_cast(d_logic), d_channels); + d_private->getEnvironment()->d_te = d_theoryEngine; // Add the theories for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { @@ -937,9 +943,14 @@ void SmtEngine::finishInit() d_decisionEngine->init(); // enable appropriate strategies Trace("smt-debug") << "Making prop engine..." << std::endl; - d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, - d_userContext, d_private->getReplayLog(), - d_replayStream, d_channels); + d_propEngine = new PropEngine(d_private->getEnvironment(), + d_theoryEngine, + d_decisionEngine, + d_context, + d_userContext, + d_private->getReplayLog(), + d_replayStream, + d_channels); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(d_propEngine); @@ -1569,8 +1580,10 @@ void SmtEngine::setDefaults() { if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() || (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) { Theory::setUninterpretedSortOwner(THEORY_ARRAYS); + d_theoryEngine->setUninterpretedSortOwner(THEORY_ARRAYS); } else { Theory::setUninterpretedSortOwner(THEORY_UF); + d_theoryEngine->setUninterpretedSortOwner(THEORY_UF); } // Turn on ite simplification for QF_LIA and QF_AUFBV diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6943c5546..07150f794 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -30,13 +30,17 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, +TheoryArith::TheoryArith(Environment* env, + 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)) - , d_ppRewriteTimer("theory::arith::ppRewriteTimer") - , d_proofRecorder(nullptr) + : Theory(THEORY_ARITH, env, c, u, out, valuation, logicInfo), + d_internal( + new TheoryArithPrivate(env, *this, c, u, out, valuation, logicInfo)), + d_ppRewriteTimer("theory::arith::ppRewriteTimer"), + d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); if (options::nlExt()) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index b39ab961f..5bfb44d22 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -34,7 +34,7 @@ namespace arith { * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ class TheoryArith : public Theory { -private: + private: friend class TheoryArithPrivate; TheoryArithPrivate* d_internal; @@ -47,59 +47,63 @@ private: proof::ArithProofRecorder * d_proofRecorder; public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); - virtual ~TheoryArith(); - - /** - * Does non-context dependent setup for a node connected to a theory. - */ - void preRegisterTerm(TNode n) override; - - Node expandDefinition(LogicRequest& logicRequest, Node node) override; - - void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - - void check(Effort e) override; - bool needsCheckLastEffort() override; - void propagate(Effort e) override; - Node explain(TNode n) override; - bool getCurrentSubstitution(int effort, - std::vector& vars, - std::vector& subs, - std::map >& exp) override; - bool isExtfReduced(int effort, - Node n, - Node on, - std::vector& exp) override; - - bool collectModelInfo(TheoryModel* m) override; - - void shutdown() override {} - - void presolve() override; - void notifyRestart() override; - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - Node ppRewrite(TNode atom) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; - - std::string identify() const override { return std::string("TheoryArith"); } - - EqualityStatus getEqualityStatus(TNode a, TNode b) override; - - void addSharedTerm(TNode n) override; - - Node getModelValue(TNode var) override; - - std::pair entailmentCheck( - TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out) override; - - void setProofRecorder(proof::ArithProofRecorder * proofRecorder) - { - d_proofRecorder = proofRecorder; - } + TheoryArith(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); + virtual ~TheoryArith(); + + /** + * Does non-context dependent setup for a node connected to a theory. + */ + void preRegisterTerm(TNode n) override; + + Node expandDefinition(LogicRequest& logicRequest, Node node) override; + + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; + + void check(Effort e) override; + bool needsCheckLastEffort() override; + void propagate(Effort e) override; + Node explain(TNode n) override; + bool getCurrentSubstitution(int effort, + std::vector& vars, + std::vector& subs, + std::map >& exp) override; + bool isExtfReduced(int effort, + Node n, + Node on, + std::vector& exp) override; + + bool collectModelInfo(TheoryModel* m) override; + + void shutdown() override {} + + void presolve() override; + void notifyRestart() override; + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + Node ppRewrite(TNode atom) override; + void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + + std::string identify() const override { return std::string("TheoryArith"); } + + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + + void addSharedTerm(TNode n) override; + + Node getModelValue(TNode var) override; + + std::pair entailmentCheck( + TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out) override; + + void setProofRecorder(proof::ArithProofRecorder* proofRecorder) + { + d_proofRecorder = proofRecorder; + } };/* class TheoryArith */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 62be1fcc1..6bcc14c94 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -81,13 +81,15 @@ namespace arith { static Node toSumNode(const ArithVariables& vars, const DenseMap& sum); static bool complexityBelow(const DenseMap& row, uint32_t cap); -TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, +TheoryArithPrivate::TheoryArithPrivate(Environment* env, + TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : d_containing(containing), + : d_env(env), + d_containing(containing), d_nlIncomplete(false), d_rowTracking(), d_constraintDatabase( @@ -1173,7 +1175,8 @@ Node TheoryArithPrivate::getModelValue(TNode term) { } Node TheoryArithPrivate::ppRewriteTerms(TNode n) { - if(Theory::theoryOf(n) != THEORY_ARITH) { + if (d_env->theoryOf(n) != THEORY_ARITH) + { return n; } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 03cb81785..5e933ea49 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -17,9 +17,10 @@ #pragma once +#include + #include #include -#include #include #include "context/cdhashset.h" @@ -32,18 +33,16 @@ #include "expr/node.h" #include "expr/node_builder.h" #include "options/arith_options.h" +#include "smt/environment.h" #include "smt/logic_exception.h" #include "smt_util/boolean_simplification.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/attempt_solution_simplex.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" -#include "theory/arith/constraint.h" -#include "theory/arith/delta_rational.h" #include "theory/arith/delta_rational.h" #include "theory/arith/dio_solver.h" #include "theory/arith/dual_simplex.h" @@ -51,10 +50,8 @@ #include "theory/arith/infer_bounds.h" #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" -#include "theory/arith/matrix.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" -#include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" #include "theory/arith/soi_simplex.h" #include "theory/arith/theory_arith.h" @@ -91,10 +88,11 @@ class NonlinearExtension; * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ class TheoryArithPrivate { -private: - + private: static const uint32_t RESET_START = 2; + Environment* d_env; + TheoryArith& d_containing; bool d_nlIncomplete; @@ -423,47 +421,57 @@ private: Node ppRewriteTerms(TNode atom); public: - TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); - ~TheoryArithPrivate(); - - /** - * Does non-context dependent setup for a node connected to a theory. - */ - void preRegisterTerm(TNode n); - Node expandDefinition(LogicRequest &logicRequest, Node node); - - void setMasterEqualityEngine(eq::EqualityEngine* eq); + TheoryArithPrivate(Environment* env, + TheoryArith& containing, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); + ~TheoryArithPrivate(); - void check(Theory::Effort e); - bool needsCheckLastEffort(); - void propagate(Theory::Effort e); - Node explain(TNode n); - bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); - bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ); + /** + * Does non-context dependent setup for a node connected to a theory. + */ + void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest& logicRequest, Node node); - Rational deltaValueForTotalOrder() const; + void setMasterEqualityEngine(eq::EqualityEngine* eq); - bool collectModelInfo(TheoryModel* m); + void check(Theory::Effort e); + bool needsCheckLastEffort(); + void propagate(Theory::Effort e); + Node explain(TNode n); + bool getCurrentSubstitution(int effort, + std::vector& vars, + std::vector& subs, + std::map >& exp); + bool isExtfReduced(int effort, Node n, Node on, std::vector& exp); - void shutdown(){ } + Rational deltaValueForTotalOrder() const; - void presolve(); - void notifyRestart(); - Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + bool collectModelInfo(TheoryModel* m); - std::string identify() const { return std::string("TheoryArith"); } + void shutdown() {} - EqualityStatus getEqualityStatus(TNode a, TNode b); + void presolve(); + void notifyRestart(); + Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); + void ppStaticLearn(TNode in, NodeBuilder<>& learned); - void addSharedTerm(TNode n); + std::string identify() const { return std::string("TheoryArith"); } - Node getModelValue(TNode var); + EqualityStatus getEqualityStatus(TNode a, TNode b); + void addSharedTerm(TNode n); - std::pair entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out); + Node getModelValue(TNode var); + std::pair entailmentCheck( + TNode lit, + const ArithEntailmentCheckParameters& params, + ArithEntailmentCheckSideEffects& out); private: diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f2beec0b8..67af54488 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -56,13 +56,14 @@ const bool d_solveWrite2 = false; //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, +TheoryArrays::TheoryArrays(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, std::string name) - : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name), + : Theory(THEORY_ARRAYS, env, c, u, out, valuation, logicInfo, name), d_numRow(name + "theory::arrays::number of Row lemmas", 0), d_numExt(name + "theory::arrays::number of Ext lemmas", 0), d_numProp(name + "theory::arrays::number of propagations", 0), diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 3d6d0692e..e694dcf5e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -138,9 +138,12 @@ class TheoryArrays : public Theory { unsigned d_reasonExt; public: - - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, + TheoryArrays(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, std::string name = ""); ~TheoryArrays(); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index abe024282..d400868bc 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -27,11 +27,16 @@ namespace theory { 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) - {} + public: + TheoryBool(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) + : Theory(THEORY_BOOL, env, c, u, out, valuation, logicInfo) + { + } PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 8a7d1bf7b..d11f3b246 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -26,11 +26,16 @@ namespace theory { namespace builtin { class TheoryBuiltin : public Theory { -public: - TheoryBuiltin(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, + public: + TheoryBuiltin(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} + : Theory(THEORY_BUILTIN, env, c, u, out, valuation, logicInfo) + { + } std::string identify() const override { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index c2bc9e6e8..c86b6888d 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -135,8 +135,8 @@ Abc_Aig_t* AigBitblaster::currentAigM() { return (Abc_Aig_t*)(currentAigNtk()->pManFunc); } -AigBitblaster::AigBitblaster() - : TBitblaster(), +AigBitblaster::AigBitblaster(Environment* env) + : TBitblaster(env), d_nullContext(new context::Context()), d_aigCache(), d_bbAtoms(), diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 4e11c0f36..0d420e473 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -43,7 +43,7 @@ namespace bv { class AigBitblaster : public TBitblaster { public: - AigBitblaster(); + AigBitblaster(Environment* env); ~AigBitblaster(); void makeVariable(TNode node, Bits& bits) override; diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index df7cc4f11..9684d1248 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -27,12 +27,12 @@ #include "proof/bitvector_proof.h" #include "prop/bv_sat_solver_notify.h" #include "prop/sat_solver_types.h" +#include "smt/environment.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" #include "util/resource_manager.h" - namespace CVC4 { namespace theory { namespace bv { @@ -58,6 +58,8 @@ class TBitblaster typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster*); typedef T (*AtomBBStrategy)(TNode, TBitblaster*); + Environment* d_env; + // caches and mappings TermDefMap d_termCache; ModelCache d_modelCache; @@ -79,7 +81,7 @@ class TBitblaster public: - TBitblaster(); + TBitblaster(Environment* env); virtual ~TBitblaster() {} virtual void bbAtom(TNode node) = 0; virtual void bbTerm(TNode node, Bits& bits) = 0; @@ -181,8 +183,9 @@ void TBitblaster::initTermBBStrategies() } template -TBitblaster::TBitblaster() - : d_termCache(), +TBitblaster::TBitblaster(Environment* env) + : d_env(env), + d_termCache(), d_modelCache(), d_nullContext(new context::Context()), d_cnfStream(), diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 9d43355cc..86696cfe4 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -29,8 +29,10 @@ namespace CVC4 { namespace theory { namespace bv { -EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) - : TBitblaster(), +EagerBitblaster::EagerBitblaster(Environment* env, + TheoryBV* theory_bv, + context::Context* c) + : TBitblaster(env), d_context(c), d_satSolver(), d_bitblastingRegistrar(new BitblastingRegistrar(this)), @@ -63,12 +65,12 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) default: Unreachable() << "Unknown SAT solver type"; } d_satSolver.reset(solver); - d_cnfStream.reset( - new prop::TseitinCnfStream(d_satSolver.get(), - d_bitblastingRegistrar.get(), - d_nullContext.get(), - options::proof(), - "EagerBitblaster")); + d_cnfStream.reset(new prop::TseitinCnfStream(d_env, + d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + options::proof(), + "EagerBitblaster")); } EagerBitblaster::~EagerBitblaster() {} diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index d407b8131..cc97f14ee 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -38,7 +38,9 @@ class TheoryBV; class EagerBitblaster : public TBitblaster { public: - EagerBitblaster(TheoryBV* theory_bv, context::Context* context); + EagerBitblaster(Environment* env, + TheoryBV* theory_bv, + context::Context* context); ~EagerBitblaster(); void addAtom(TNode atom); diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 2018590f7..afb0578be 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -58,11 +58,12 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen) } } -TLazyBitblaster::TLazyBitblaster(context::Context* c, +TLazyBitblaster::TLazyBitblaster(Environment* env, + context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify) - : TBitblaster(), + : TBitblaster(env), d_bv(bv), d_ctx(c), d_nullRegistrar(new prop::NullRegistrar()), @@ -79,12 +80,12 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolver.reset( prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); - d_cnfStream.reset( - new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - options::proof(), - "LazyBitblaster")); + d_cnfStream.reset(new prop::TseitinCnfStream(d_env, + d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + options::proof(), + "LazyBitblaster")); d_satSolverNotify.reset( d_emptyNotify @@ -545,7 +546,7 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) if (d_variables.find(var) == d_variables.end()) continue; - Assert(Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); + Assert(d_env->theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); // only shared terms could not have been bit-blasted Assert(hasBBTerm(var) || isSharedTerm(var)); @@ -579,7 +580,7 @@ void TLazyBitblaster::clearSolver() { d_satSolver.reset( prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); d_cnfStream.reset(new prop::TseitinCnfStream( - d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); + d_env, d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); d_satSolverNotify.reset( d_emptyNotify ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index ac5cd5c7f..d2a497bdd 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -45,7 +45,8 @@ class TLazyBitblaster : public TBitblaster void storeBBTerm(TNode node, const Bits& bits) override; bool hasBBAtom(TNode atom) const override; - TLazyBitblaster(context::Context* c, + TLazyBitblaster(Environment* env, + context::Context* c, TheoryBV* bv, const std::string name = "", bool emptyNotify = false); diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index dd0458a70..d725026cd 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -26,8 +26,11 @@ namespace CVC4 { namespace theory { namespace bv { -EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv) - : d_assertionSet(c), +EagerBitblastSolver::EagerBitblastSolver(Environment* env, + context::Context* c, + TheoryBV* bv) + : d_env(env), + d_assertionSet(c), d_assumptionSet(c), d_context(c), d_bitblaster(), @@ -49,12 +52,12 @@ void EagerBitblastSolver::initialize() { Assert(!isInitialized()); if (d_useAig) { #ifdef CVC4_USE_ABC - d_aigBitblaster.reset(new AigBitblaster()); + d_aigBitblaster.reset(new AigBitblaster(d_env)); #else Unreachable(); #endif } else { - d_bitblaster.reset(new EagerBitblaster(d_bv, d_context)); + d_bitblaster.reset(new EagerBitblaster(d_env, d_bv, d_context)); THEORY_PROOF(if (d_bvp) { d_bitblaster->setProofLog(d_bvp); d_bvp->setBitblaster(d_bitblaster.get()); diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 8e42d5cab..1d7f2e0bd 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "proof/resolution_bitvector_proof.h" +#include "smt/environment.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -39,7 +40,9 @@ class AigBitblaster; */ class EagerBitblastSolver { public: - EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv); + EagerBitblastSolver(Environment* env, + context::Context* c, + theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -51,6 +54,8 @@ class EagerBitblastSolver { void setProofLog(proof::BitVectorProof* bvp); private: + Environment* d_env; + context::CDHashSet d_assertionSet; context::CDHashSet d_assumptionSet; context::Context* d_context; diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index dbdeccfe5..8efda195e 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -26,11 +26,13 @@ namespace CVC4 { namespace theory { namespace bv { -BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv) - : d_ctx() - , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)) - , d_conflict() - , d_inConflict(&d_ctx, false) +BVQuickCheck::BVQuickCheck(Environment* env, + const std::string& name, + theory::bv::TheoryBV* bv) + : d_ctx(), + d_bitblaster(new TLazyBitblaster(env, &d_ctx, bv, name, true)), + d_conflict(), + d_inConflict(&d_ctx, false) {} diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 75f39b6e0..04ed0cd2c 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -19,12 +19,13 @@ #ifndef CVC4__BV_QUICK_CHECK_H #define CVC4__BV_QUICK_CHECK_H -#include #include +#include #include "context/cdo.h" #include "expr/node.h" #include "prop/sat_solver_types.h" +#include "smt/environment.h" #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" @@ -45,34 +46,36 @@ class BVQuickCheck { context::CDO d_inConflict; void setConflict(); -public: - BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv); + public: + BVQuickCheck(Environment* env, + const std::string& name, + theory::bv::TheoryBV* bv); ~BVQuickCheck(); bool inConflict(); Node getConflict() { return d_conflict; } - /** + /** * Checks the satisfiability for a given set of assumptions. - * + * * @param assumptions literals assumed true * @param budget max number of conflicts - * - * @return + * + * @return */ prop::SatValue checkSat(std::vector& assumptions, unsigned long budget); - /** + /** * Checks the satisfiability of given assertions. - * + * * @param budget max number of conflicts - * - * @return + * + * @return */ prop::SatValue checkSat(unsigned long budget); - - /** + + /** * Convert to CNF and assert the given literal. - * + * * @param assumption bv literal - * + * * @return false if a conflict has been found via bcp. */ bool addAssertion(TNode assumption); @@ -80,31 +83,31 @@ public: void push(); void pop(); void popToZero(); - /** + /** * Deletes the SAT solver and CNF stream, but maintains the - * bit-blasting term cache. - * + * bit-blasting term cache. + * */ - void clearSolver(); + void clearSolver(); - /** + /** * Computes the size of the circuit required to bit-blast - * atom, by not recounting the nodes in seen. - * - * @param node - * @param seen - * - * @return + * atom, by not recounting the nodes in seen. + * + * @param node + * @param seen + * + * @return */ uint64_t computeAtomWeight(TNode atom, NodeSet& seen); bool collectModelInfo(theory::TheoryModel* model, bool fullModel); - typedef std::unordered_set::const_iterator vars_iterator; - vars_iterator beginVars(); - vars_iterator endVars(); - - Node getVarValue(TNode var, bool fullModel); + typedef std::unordered_set::const_iterator + vars_iterator; + vars_iterator beginVars(); + vars_iterator endVars(); + Node getVarValue(TNode var, bool fullModel); }; diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 60660eda9..8dcc1835b 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -69,12 +69,15 @@ using AssertionQueue = context::CDQueue; */ class SubtheorySolver { public: - SubtheorySolver(context::Context* c, TheoryBV* bv) - : d_context(c), + SubtheorySolver(Environment* env, context::Context* c, TheoryBV* bv) + : d_env(env), + d_context(c), d_bv(bv), d_bvp(nullptr), d_assertionQueue(c), - d_assertionIndex(c, 0) {} + d_assertionIndex(c, 0) + { + } virtual ~SubtheorySolver() {} virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector& assumptions) = 0; @@ -102,6 +105,8 @@ class SubtheorySolver { } protected: + Environment* d_env; + /** The context we are using */ context::Context* d_context; diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 6f8804042..bfedced51 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -227,10 +227,12 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) { d_cache[from] = SubstitutionElement(to, reason); } -AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv) - : SubtheorySolver(c, bv), +AlgebraicSolver::AlgebraicSolver(Environment* env, + context::Context* c, + TheoryBV* bv) + : SubtheorySolver(env, c, bv), d_modelMap(), - d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)), + d_quickSolver(new BVQuickCheck(env, "theory::bv::algebraic", bv)), d_isComplete(c, false), d_isDifficult(c, false), d_budget(options::bitvectorAlgebraicBudget()), @@ -723,9 +725,10 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) std::vector values; for (set::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { TNode term = *it; - if (term.getType().isBitVector() && - (term.getMetaKind() == kind::metakind::VARIABLE || - Theory::theoryOf(term) != THEORY_BV)) { + if (term.getType().isBitVector() + && (term.getMetaKind() == kind::metakind::VARIABLE + || d_env->theoryOf(term) != THEORY_BV)) + { variables.push_back(term); values.push_back(term); } diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index de75ad859..8baa208c1 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -220,8 +220,8 @@ class AlgebraicSolver : public SubtheorySolver { */ bool quickCheck(std::vector& facts); -public: - AlgebraicSolver(context::Context* c, TheoryBV* bv); + public: + AlgebraicSolver(Environment* env, context::Context* c, TheoryBV* bv); ~AlgebraicSolver(); void preRegister(TNode node) override {} diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 94dfdee14..25a45236b 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -33,9 +33,11 @@ namespace CVC4 { namespace theory { namespace bv { -BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) - : SubtheorySolver(c, bv), - d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")), +BitblastSolver::BitblastSolver(Environment* env, + context::Context* c, + TheoryBV* bv) + : SubtheorySolver(env, c, bv), + d_bitblaster(new TLazyBitblaster(env, c, bv, "theory::bv::lazy")), d_bitblastQueue(c), d_statistics(), d_validModelCache(c, true), @@ -47,7 +49,7 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) { if (options::bitvectorQuickXplain()) { - d_quickCheck.reset(new BVQuickCheck("bb", bv)); + d_quickCheck.reset(new BVQuickCheck(env, "bb", bv)); d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get())); } } diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 0b0a9521b..50cd1cb5d 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -65,8 +65,9 @@ class BitblastSolver : public SubtheorySolver { std::unique_ptr d_quickXplain; // Node getModelValueRec(TNode node); void setConflict(TNode conflict); -public: - BitblastSolver(context::Context* c, TheoryBV* bv); + + public: + BitblastSolver(Environment* env, context::Context* c, TheoryBV* bv); ~BitblastSolver(); void preRegister(TNode node) override; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index bf9bfa480..bc796e7ab 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -32,17 +32,17 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; -CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) - : SubtheorySolver(c, bv), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::bv::ee", true), - d_slicer(new Slicer()), - d_isComplete(c, true), - d_lemmaThreshold(16), - d_useSlicer(false), - d_preregisterCalled(false), - d_checkCalled(false), - d_reasons(c) +CoreSolver::CoreSolver(Environment* env, context::Context* c, TheoryBV* bv) + : SubtheorySolver(env, c, bv), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::bv::ee", true), + d_slicer(new Slicer()), + d_isComplete(c, true), + d_lemmaThreshold(16), + d_useSlicer(false), + d_preregisterCalled(false), + d_checkCalled(false), + d_reasons(c) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); @@ -417,10 +417,9 @@ void CoreSolver::eqNotifyNewClass(TNode t) { } bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) { - if (d_useSlicer) - return utils::isCoreTerm(term, seen); - - return utils::isEqualityTerm(term, seen); + if (d_useSlicer) return utils::isCoreTerm(d_env, term, seen); + + return utils::isEqualityTerm(d_env, term, seen); } bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index e2026d4a5..b70518ab4 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -100,11 +100,12 @@ class CoreSolver : public SubtheorySolver { Node getBaseDecomposition(TNode a); bool isCompleteForTerm(TNode term, TNodeBoolMap& seen); Statistics d_statistics; -public: - CoreSolver(context::Context* c, TheoryBV* bv); + + public: + CoreSolver(Environment* env, context::Context* c, TheoryBV* bv); ~CoreSolver(); bool isComplete() override { return d_isComplete; } - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq); void preRegister(TNode node) override; bool check(Theory::Effort e) override; void explain(TNode literal, std::vector& assumptions) override; diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index e18c886df..f114b890e 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "expr/attribute.h" +#include "smt/environment.h" #include "theory/bv/bv_inequality_graph.h" #include "theory/bv/bv_subtheory.h" @@ -57,16 +58,21 @@ class InequalitySolver : public SubtheorySolver bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); Statistics d_statistics; -public: - InequalitySolver(context::Context* c, context::Context* u, TheoryBV* bv) - : SubtheorySolver(c, bv), - d_assertionSet(c), - d_inequalityGraph(c, u), - d_explanations(c), - d_isComplete(c, true), - d_ineqTerms(), - d_statistics() - {} + + public: + InequalitySolver(Environment* env, + context::Context* c, + context::Context* u, + TheoryBV* bv) + : SubtheorySolver(env, c, bv), + d_assertionSet(c), + d_inequalityGraph(c, u), + d_explanations(c), + d_isComplete(c, true), + d_ineqTerms(), + d_statistics() + { + } bool check(Theory::Effort e) override; void propagate(Theory::Effort e) override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 23ffabcd1..aa1aab6a6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -44,13 +44,14 @@ namespace CVC4 { namespace theory { namespace bv { -TheoryBV::TheoryBV(context::Context* c, +TheoryBV::TheoryBV(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, std::string name) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name), + : Theory(THEORY_BV, env, c, u, out, valuation, logicInfo, name), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), @@ -78,29 +79,29 @@ TheoryBV::TheoryBV(context::Context* c, getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT); getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver.reset(new EagerBitblastSolver(c, this)); + d_eagerSolver.reset(new EagerBitblastSolver(env, c, this)); return; } if (options::bitvectorEqualitySolver() && !options::proof()) { - d_subtheories.emplace_back(new CoreSolver(c, this)); + d_subtheories.emplace_back(new CoreSolver(env, c, this)); d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); } if (options::bitvectorInequalitySolver() && !options::proof()) { - d_subtheories.emplace_back(new InequalitySolver(c, u, this)); + d_subtheories.emplace_back(new InequalitySolver(env, c, u, this)); d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); } if (options::bitvectorAlgebraicSolver() && !options::proof()) { - d_subtheories.emplace_back(new AlgebraicSolver(c, this)); + d_subtheories.emplace_back(new AlgebraicSolver(env, c, this)); d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get(); } - BitblastSolver* bb_solver = new BitblastSolver(c, this); + BitblastSolver* bb_solver = new BitblastSolver(env, c, this); if (options::bvAbstraction()) { bb_solver->setAbstraction(d_abstractionModule.get()); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 7ca98f2ea..08325fc0e 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -64,10 +64,13 @@ class TheoryBV : public Theory { std::vector> d_subtheories; std::unordered_map > d_subtheoryMap; -public: - - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, + public: + TheoryBV(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, std::string name = ""); ~TheoryBV(); @@ -97,7 +100,7 @@ public: bool getCurrentSubstitution(int effort, std::vector& vars, std::vector& subs, - std::map >& exp) override; + std::map>& exp) override; int getReduction(int effort, Node n, Node& nr) override; PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; @@ -110,14 +113,15 @@ public: void presolve() override; - bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); + bool applyAbstraction(const std::vector& assertions, + std::vector& new_assertions); void setProofLog(proof::BitVectorProof* bvp); private: - - class Statistics { - public: + class Statistics + { + public: AverageStat d_avgConflictSize; IntStat d_solveSubstitutions; TimerStat d_solveTimer; diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index c0df9f35c..bd3f961e4 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -134,7 +134,10 @@ bool isBVPredicate(TNode node) || k == kind::BITVECTOR_REDAND; } -static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache) +static bool isCoreEqTerm(Environment* env, + bool iseq, + TNode term, + TNodeBoolMap& cache) { TNode t = term.getKind() == kind::NOT ? term[0] : term; @@ -156,8 +159,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache) continue; } - if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, n) - == theory::THEORY_BV) + if (env->theoryOf(theory::THEORY_OF_TERM_BASED, n) == theory::THEORY_BV) { Kind k = n.getKind(); Assert(k != kind::CONST_BITVECTOR); @@ -196,14 +198,14 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache) return cache[t]; } -bool isCoreTerm(TNode term, TNodeBoolMap& cache) +bool isCoreTerm(Environment* env, TNode term, TNodeBoolMap& cache) { - return isCoreEqTerm(false, term, cache); + return isCoreEqTerm(env, false, term, cache); } -bool isEqualityTerm(TNode term, TNodeBoolMap& cache) +bool isEqualityTerm(Environment* env, TNode term, TNodeBoolMap& cache) { - return isCoreEqTerm(true, term, cache); + return isCoreEqTerm(env, true, term, cache); } bool isBitblastAtom(Node lit) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 23eaab3f8..dfb6686d4 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -25,6 +25,7 @@ #include #include "expr/node_manager.h" +#include "smt/environment.h" namespace CVC4 { namespace theory { @@ -76,11 +77,11 @@ bool isBVPredicate(TNode node); * - not a THEORY_BV term * - a THEORY_BV \Sigma_core term, where * \Sigma_core = { concat, extract, =, bv constants, bv variables } */ -bool isCoreTerm(TNode term, TNodeBoolMap& cache); +bool isCoreTerm(Environment* env, TNode term, TNodeBoolMap& cache); /* Returns true if given term is a THEORY_BV \Sigma_equality term. * \Sigma_equality = { =, bv constants, bv variables } */ -bool isEqualityTerm(TNode term, TNodeBoolMap& cache); +bool isEqualityTerm(Environment* env, TNode term, TNodeBoolMap& cache); /* Returns true if given node is an atom that is bit-blasted. */ bool isBitblastAtom(Node lit); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 2d6aeae60..5961ab5de 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -39,12 +39,13 @@ namespace CVC4 { namespace theory { namespace datatypes { -TheoryDatatypes::TheoryDatatypes(Context* c, +TheoryDatatypes::TheoryDatatypes(Environment* env, + Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), + : Theory(THEORY_DATATYPES, env, c, u, out, valuation, logicInfo), d_infer(c), d_infer_exp(c), d_term_sk(u), diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index ba09ce89e..c417a399a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -26,6 +26,7 @@ #include "expr/attribute.h" #include "expr/datatype.h" #include "expr/node_trie.h" +#include "smt/environment.h" #include "theory/datatypes/sygus_extension.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -266,8 +267,11 @@ private: void computeCareGraph() override; public: - TheoryDatatypes(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, + TheoryDatatypes(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo); ~TheoryDatatypes(); diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index fa143a1d0..cfc75d671 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -99,12 +99,13 @@ Node buildConjunct(const std::vector &assumptions) { } // namespace helper /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ -TheoryFp::TheoryFp(context::Context *c, - context::UserContext *u, - OutputChannel &out, +TheoryFp::TheoryFp(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, Valuation valuation, - const LogicInfo &logicInfo) - : Theory(THEORY_FP, c, u, out, valuation, logicInfo), + const LogicInfo& logicInfo) + : Theory(THEORY_FP, env, c, u, out, valuation, logicInfo), d_notification(*this), d_equalityEngine(d_notification, c, "theory::fp::ee", true), d_registeredTerms(u), diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ad093f924..6aae5fbe2 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -35,8 +35,12 @@ namespace fp { class TheoryFp : public Theory { 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); + TheoryFp(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); Node expandDefinition(LogicRequest& lr, Node node) override; diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 12ac1e802..82056a6d4 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -30,12 +30,15 @@ namespace CVC4 { namespace theory { namespace idl { -TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, +TheoryIdl::TheoryIdl(Environment* env, + 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) + : Theory(THEORY_ARITH, env, c, u, out, valuation, logicInfo), + d_model(c), + d_assertionsDB(c) {} Node TheoryIdl::ppRewrite(TNode atom) { diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 1d48d0785..851226942 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -41,11 +41,14 @@ class TheoryIdl : public Theory { /** Process a new assertion, returns false if in conflict */ bool processAssertion(const IDLAssertion& assertion); -public: - + public: /** Theory constructor. */ - TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + TheoryIdl(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); /** Pre-processing of input atoms */ Node ppRewrite(TNode atom) override; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 1682b4d0c..512c903c9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,8 +34,13 @@ 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(Environment* env, + Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) + : Theory(THEORY_QUANTIFIERS, env, c, u, out, valuation, logicInfo) { out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index b5b07f2e6..ea688af96 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -34,8 +34,11 @@ namespace quantifiers { class TheoryQuantifiers : public Theory { public: - TheoryQuantifiers(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, + TheoryQuantifiers(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 1392f8fab..6a8b4771b 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -38,16 +38,21 @@ namespace CVC4 { namespace theory { namespace sep { -TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_SEP, c, u, out, valuation, logicInfo), - d_lemmas_produced_c(u), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::sep::ee", true), - d_conflict(c, false), - d_reduce(u), - d_infer(c), - d_infer_exp(c), - d_spatial_assertions(c) +TheorySep::TheorySep(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) + : Theory(THEORY_SEP, env, c, u, out, valuation, logicInfo), + d_lemmas_produced_c(u), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::sep::ee", true), + d_conflict(c, false), + d_reduce(u), + d_infer(c), + d_infer_exp(c), + d_spatial_assertions(c) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index ae044f6d7..dd3658fce 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -63,7 +63,12 @@ class TheorySep : public Theory { bool pol, bool hasPol, bool underSpatial ); public: - TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheorySep(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); ~TheorySep(); void setMasterEqualityEngine(eq::EqualityEngine* eq) override; diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 869cb8926..8e063219d 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -21,12 +21,13 @@ namespace CVC4 { namespace theory { namespace sets { -TheorySets::TheorySets(context::Context* c, +TheorySets::TheorySets(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_SETS, c, u, out, valuation, logicInfo), + : Theory(THEORY_SETS, env, c, u, out, valuation, logicInfo), d_internal(new TheorySetsPrivate(*this, c, u)) { // Do not move me to the header. diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 4c145aedb..7e5d23142 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -35,7 +35,8 @@ class TheorySets : public Theory { public: /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */ - TheorySets(context::Context* c, + TheorySets(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9fad39b6b..13d91bd17 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -85,12 +85,13 @@ Node TheoryStrings::TermIndex::add(TNode n, } } -TheoryStrings::TheoryStrings(context::Context* c, +TheoryStrings::TheoryStrings(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), + : Theory(THEORY_STRINGS, env, c, u, out, valuation, logicInfo), d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), d_state(c, d_equalityEngine, d_valuation), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8e2af8434..f016d9d72 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -97,8 +97,11 @@ class TheoryStrings : public Theory { typedef context::CDHashSet NodeSet; public: - TheoryStrings(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, + TheoryStrings(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo); ~TheoryStrings(); diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 3b11d8e54..3787ca8af 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -47,8 +47,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { return true; } - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); + TheoryId currentTheoryId = d_engine->theoryIdOf(current); + TheoryId parentTheoryId = d_engine->theoryIdOf(parent); d_theories = Theory::setInsert(currentTheoryId, d_theories); d_theories = Theory::setInsert(parentTheoryId, d_theories); @@ -62,10 +62,10 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers TypeNode type = current.getType(); useType = true; - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); } else { TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); if (typeTheoryId != currentTheoryId) { if (type.isInterpretedFinite()) { useType = true; @@ -88,7 +88,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { // The current theory has already visited it, so now it depends on the parent and the type if (Theory::setContains(parentTheoryId, visitedTheories)) { if (useType) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); + TheoryId typeTheoryId = d_engine->theoryIdOf(current.getType()); d_theories = Theory::setInsert(typeTheoryId, d_theories); return Theory::setContains(typeTheoryId, visitedTheories); } else { @@ -110,8 +110,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { } // Get the theories of the terms - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); + TheoryId currentTheoryId = d_engine->theoryIdOf(current); + TheoryId parentTheoryId = d_engine->theoryIdOf(parent); // Should we use the theory of the type bool useType = false; @@ -122,10 +122,10 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers TypeNode type = current.getType(); useType = true; - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); } else { TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); if (typeTheoryId != currentTheoryId) { if (type.isInterpretedFinite()) { useType = true; @@ -199,8 +199,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Theory::Set theories = (*find).second; - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); + TheoryId currentTheoryId = d_engine->theoryIdOf(current); + TheoryId parentTheoryId = d_engine->theoryIdOf(parent); // Should we use the theory of the type bool useType = false; @@ -211,10 +211,10 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers TypeNode type = current.getType(); useType = true; - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); } else { TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); if (typeTheoryId != currentTheoryId) { if (type.isInterpretedFinite()) { useType = true; @@ -227,10 +227,10 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers TypeNode type = current.getType(); useType = true; - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); } else { TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); if (typeTheoryId != currentTheoryId) { if (type.isInterpretedFinite()) { useType = true; @@ -262,8 +262,8 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { } // Get the theories of the terms - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); + TheoryId currentTheoryId = d_engine->theoryIdOf(current); + TheoryId parentTheoryId = d_engine->theoryIdOf(parent); // Should we use the theory of the type bool useType = false; @@ -274,10 +274,10 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers TypeNode type = current.getType(); useType = true; - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); } else { TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); + typeTheoryId = d_engine->theoryIdOf(type); if (typeTheoryId != currentTheoryId) { if (type.isInterpretedFinite()) { useType = true; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index cdb411c16..13a14881b 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -98,32 +98,13 @@ public: * been visited already, we need to visit it again, since we need to associate it with both atoms. */ class SharedTermsVisitor { - - /** The shared terms database */ - SharedTermsDatabase& d_sharedTerms; - - /** - * Cache from preprocessing of atoms. - */ - typedef std::unordered_map TNodeVisitedMap; - TNodeVisitedMap d_visited; - - /** - * String representation of the visited map, for debugging purposes. - */ - std::string toString() const; - - /** - * The initial atom. - */ - TNode d_atom; - public: - typedef void return_type; - SharedTermsVisitor(SharedTermsDatabase& sharedTerms) - : d_sharedTerms(sharedTerms) {} + SharedTermsVisitor(TheoryEngine* engine, SharedTermsDatabase& sharedTerms) + : d_engine(engine), d_sharedTerms(sharedTerms) + { + } /** * Returns true is current has already been pre-registered with both current and parent theories. @@ -149,7 +130,29 @@ public: * Clears the internal state. */ void clear(); -}; + private: + /** The engine */ + TheoryEngine* d_engine; + + /** The shared terms database */ + SharedTermsDatabase& d_sharedTerms; + + /** + * Cache from preprocessing of atoms. + */ + typedef std::unordered_map + TNodeVisitedMap; + TNodeVisitedMap d_visited; + /** + * String representation of the visited map, for debugging purposes. + */ + std::string toString() const; + + /** + * The initial atom. + */ + TNode d_atom; +}; } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 719239806..140f0de63 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -53,6 +53,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ }/* ostream& operator<<(ostream&, Theory::Effort) */ Theory::Theory(TheoryId id, + Environment* env, context::Context* satContext, context::UserContext* userContext, OutputChannel& out, @@ -71,6 +72,7 @@ Theory::Theory(TheoryId id, d_quantEngine(NULL), d_decManager(nullptr), d_extTheory(NULL), + d_env(env), d_checkTime(getStatsPrefix(id) + name + "::checkTime"), d_computeCareGraphTime(getStatsPrefix(id) + name + "::computeCareGraphTime"), diff --git a/src/theory/theory.h b/src/theory/theory.h index b133b878e..cc42e9788 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -139,7 +139,7 @@ private: ExtTheory* d_extTheory; protected: - + Environment* d_env; // === STATISTICS === /** time spent in check calls */ @@ -196,6 +196,7 @@ private: * w.r.t. the SmtEngine. */ Theory(TheoryId id, + Environment* env, context::Context* satContext, context::UserContext* userContext, OutputChannel& out, diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7a72367de..e7b044f81 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -310,15 +310,18 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ } } -TheoryEngine::TheoryEngine(context::Context* context, +TheoryEngine::TheoryEngine(Environment* env, + context::Context* context, context::UserContext* userContext, RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo, LemmaChannels* channels) - : d_propEngine(nullptr), + : d_env(env), + d_propEngine(nullptr), d_decisionEngine(nullptr), d_context(context), d_userContext(userContext), + d_uninterpretedSortOwner(THEORY_UF), d_logicInfo(logicInfo), d_sharedTerms(this, context), d_masterEqualityEngine(nullptr), @@ -352,7 +355,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), - d_sharedTermsVisitor(d_sharedTerms), + d_sharedTermsVisitor(this, d_sharedTerms), d_theoryAlternatives(), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) @@ -432,7 +435,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { Theory::Set theories = NodeVisitor::run(d_preRegistrationVisitor, preprocessed); theories = Theory::setRemove(THEORY_BOOL, theories); // Remove the top theory, if any more that means multiple theories were involved - bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories); + bool multipleTheories = + Theory::setRemove(theoryIdOf(preprocessed), theories); TheoryId i; // These checks don't work with finite model finding, because it // uses Rational constants to represent cardinality constraints, @@ -1070,11 +1074,12 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; - if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) && - Theory::theoryOf(atom) != THEORY_SAT_SOLVER) { + if (!d_logicInfo.isTheoryEnabled(theoryIdOf(atom)) + && theoryIdOf(atom) != THEORY_SAT_SOLVER) + { stringstream ss; ss << "The logic was specified as " << d_logicInfo.getLogicString() - << ", which doesn't include " << Theory::theoryOf(atom) + << ", which doesn't include " << theoryIdOf(atom) << ", but got a preprocessing-time fact for that theory." << endl << "The fact:" << endl << literal; @@ -1164,11 +1169,12 @@ Node TheoryEngine::preprocess(TNode assertion) { continue; } - if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) && - Theory::theoryOf(current) != THEORY_SAT_SOLVER) { + if (!d_logicInfo.isTheoryEnabled(theoryIdOf(current)) + && theoryIdOf(current) != THEORY_SAT_SOLVER) + { stringstream ss; ss << "The logic was specified as " << d_logicInfo.getLogicString() - << ", which doesn't include " << Theory::theoryOf(current) + << ", which doesn't include " << theoryIdOf(current) << ", but got a preprocessing-time fact for that theory." << endl << "The fact:" << endl << current; @@ -1176,7 +1182,8 @@ Node TheoryEngine::preprocess(TNode assertion) { } // If this is an atom, we preprocess its terms with the theory ppRewriter - if (Theory::theoryOf(current) != THEORY_BOOL) { + if (theoryIdOf(current) != THEORY_BOOL) + { Node ppRewritten = ppTheoryRewrite(current); d_ppCache[current] = ppRewritten; Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]); @@ -1332,7 +1339,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // We know that this is normalized, so just send it off to the theory if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // Is it preregistered - bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId; + bool preregistered = d_propEngine->isSatLiteral(assertion) + && theoryIdOf(assertion) == toTheoryId; // We assert it theoryOf(toTheoryId)->assertFact(assertion, preregistered); // Mark that we have more information @@ -1379,7 +1387,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // Try and assert (note that we assert the non-normalized one) if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // Check if has been pre-registered with the theory - bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId; + bool preregistered = d_propEngine->isSatLiteral(assertion) + && theoryIdOf(assertion) == toTheoryId; // Assert away theoryOf(toTheoryId)->assertFact(assertion, preregistered); d_factsAsserted = true; @@ -1427,7 +1436,10 @@ void TheoryEngine::assertFact(TNode literal) // to the assert the equality to the interested theories if (atom.getKind() == kind::EQUAL) { // Assert it to the the owning theory - assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); + assertToTheory(literal, + literal, + /* to */ theoryIdOf(atom), + /* from */ THEORY_SAT_SOLVER); // Shared terms manager will assert to interested theories directly, as the terms become shared assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER); @@ -1443,11 +1455,17 @@ void TheoryEngine::assertFact(TNode literal) } else { // Not an equality, just assert to the appropriate theory - assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); + assertToTheory(literal, + literal, + /* to */ theoryIdOf(atom), + /* from */ THEORY_SAT_SOLVER); } } else { // Assert the fact to the appropriate theory directly - assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); + assertToTheory(literal, + literal, + /* to */ theoryIdOf(atom), + /* from */ THEORY_SAT_SOLVER); } } @@ -1504,6 +1522,159 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { return !d_inConflict; } +theory::TheoryId TheoryEngine::theoryIdOf(TypeNode typeNode) const +{ + Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl; + TheoryId id; + if (typeNode.getKind() == kind::TYPE_CONSTANT) + { + id = typeConstantToTheoryId(typeNode.getConst()); + } + else + { + id = kindToTheoryId(typeNode.getKind()); + } + if (id == THEORY_BUILTIN) + { + Trace("theory::internal") + << "theoryOf(" << typeNode << ") == " << d_uninterpretedSortOwner + << std::endl; + return d_uninterpretedSortOwner; + } + return id; +} + +TheoryId TheoryEngine::theoryIdOf(TheoryOfMode mode, TNode node) const +{ + TheoryId tid = THEORY_BUILTIN; + switch (mode) + { + case THEORY_OF_TYPE_BASED: + // Constants, variables, 0-ary constructors + if (node.isVar()) + { + if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) + { + tid = THEORY_UF; + } + else + { + tid = theoryIdOf(node.getType()); + } + } + else if (node.isConst()) + { + tid = theoryIdOf(node.getType()); + } + else if (node.getKind() == kind::EQUAL) + { + // Equality is owned by the theory that owns the domain + tid = theoryIdOf(node[0].getType()); + } + else + { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); + } + break; + case THEORY_OF_TERM_BASED: + // Variables + if (node.isVar()) + { + if (theoryIdOf(node.getType()) != theory::THEORY_BOOL) + { + // We treat the variables as uninterpreted + tid = d_uninterpretedSortOwner; + } + else + { + if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) + { + // Boolean vars go to UF + tid = THEORY_UF; + } + else + { + // Except for the Boolean ones + tid = THEORY_BOOL; + } + } + } + else if (node.isConst()) + { + // Constants go to the theory of the type + tid = theoryIdOf(node.getType()); + } + else if (node.getKind() == kind::EQUAL) + { // Equality + // If one of them is an ITE, it's irelevant, since they will get + // replaced out anyhow + if (node[0].getKind() == kind::ITE) + { + tid = theoryIdOf(node[0].getType()); + } + else if (node[1].getKind() == kind::ITE) + { + tid = theoryIdOf(node[1].getType()); + } + else + { + TNode l = node[0]; + TNode r = node[1]; + TypeNode ltype = l.getType(); + TypeNode rtype = r.getType(); + if (ltype != rtype) + { + tid = theoryIdOf(l.getType()); + } + else + { + // If both sides belong to the same theory the choice is easy + TheoryId T1 = theoryIdOf(l); + TheoryId T2 = theoryIdOf(r); + if (T1 == T2) + { + tid = T1; + } + else + { + TheoryId T3 = theoryIdOf(ltype); + // This is a case of + // * x*y = f(z) -> UF + // * x = c -> UF + // * f(x) = read(a, y) -> either UF or ARRAY + // at least one of the theories has to be parametric, i.e. theory + // of the type is different from the theory of the term + if (T1 == T3) + { + tid = T2; + } + else if (T2 == T3) + { + tid = T1; + } + else + { + // If both are parametric, we take the smaller one (arbitrary) + tid = T1 < T2 ? T1 : T2; + } + } + } + } + } + else + { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); + } + break; + default: Unreachable(); + } + Trace("theory::internal") + << "theoryIdOf(" << mode << ", " << node << ") -> " << tid << std::endl; + return tid; +} + const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; } theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { @@ -1516,7 +1687,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return EQUALITY_FALSE_AND_PROPAGATED; } } - return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); + return theoryOf(theoryIdOf(a.getType()))->getEqualityStatus(a, b); } Node TheoryEngine::getModelValue(TNode var) { @@ -1526,7 +1697,7 @@ Node TheoryEngine::getModelValue(TNode var) { return var; } Assert(d_sharedTerms.isShared(var)); - return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); + return theoryOf(theoryIdOf(var.getType()))->getModelValue(var); } @@ -1733,25 +1904,28 @@ Node TheoryEngine::getExplanation(TNode node) { } struct AtomsCollect { - + const TheoryEngine* d_te; std::vector d_atoms; std::unordered_set d_visited; public: + AtomsCollect(const TheoryEngine* te) : d_te(te) {} - typedef void return_type; + typedef void return_type; - bool alreadyVisited(TNode current, TNode parent) { - // Check if already visited - if (d_visited.find(current) != d_visited.end()) return true; - // Don't visit non-boolean - if (!current.getType().isBoolean()) return true; - // New node - return false; - } + bool alreadyVisited(TNode current, TNode parent) + { + // Check if already visited + if (d_visited.find(current) != d_visited.end()) return true; + // Don't visit non-boolean + if (!current.getType().isBoolean()) return true; + // New node + return false; + } void visit(TNode current, TNode parent) { - if (Theory::theoryOf(current) != theory::THEORY_BOOL) { + if (d_te->theoryIdOf(current) != theory::THEORY_BOOL) + { d_atoms.push_back(current); } d_visited.insert(current); @@ -1823,7 +1997,8 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector& atoms, theory::The // If the theory is asking about a different form, or the form is ok but if will go to a different theory // then we must figure it out - if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) { + if (eqNormalized != eq || theoryIdOf(eq) != atomsTo) + { // If you get eqNormalized, send atoms[i] to atomsTo d_atomRequests.add(eqNormalized, eq, atomsTo); } @@ -1842,7 +2017,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl; - AtomsCollect collectAtoms; + AtomsCollect collectAtoms(this); NodeVisitor::run(collectAtoms, node); ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo); } @@ -2026,7 +2201,8 @@ void TheoryEngine::staticInitializeBVOptions( bv::utils::TNodeBoolMap cache; for (unsigned i = 0; i < assertions.size(); ++i) { - useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache); + useSlicer = + useSlicer && bv::utils::isCoreTerm(d_env, assertions[i], cache); } } @@ -2290,7 +2466,7 @@ std::pair TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T return std::pair(false, Node::null()); }else{ //it is a theory atom - theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); + theory::TheoryId tid = theoryIdOf(mode, atom); theory::Theory* th = theoryOf(tid); Assert(th != NULL); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index dd34ae16b..ca999f569 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -23,8 +23,8 @@ #include #include #include -#include #include +#include #include "base/check.h" #include "context/cdhashset.h" @@ -33,6 +33,7 @@ #include "options/smt_options.h" #include "prop/prop_engine.h" #include "smt/command.h" +#include "smt/environment.h" #include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" #include "theory/decision_manager.h" @@ -113,6 +114,8 @@ class TheoryEngine { friend class SharedTermsDatabase; friend class theory::quantifiers::TermDb; + Environment* d_env; + /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; @@ -131,6 +134,11 @@ class TheoryEngine { */ theory::Theory* d_theoryTable[theory::THEORY_LAST]; + /** + * The theory that owns the uninterpreted sort. + */ + theory::TheoryId d_uninterpretedSortOwner; + /** * A collection of theories that are "active" for the current run. * This set is provided by the user (as a logic string, say, in SMT-LIBv2 @@ -467,11 +475,13 @@ class TheoryEngine { /** Container for lemma input and output channels. */ LemmaChannels* d_channels; -public: - + public: /** Constructs a theory engine */ - TheoryEngine(context::Context* context, context::UserContext* userContext, - RemoveTermFormulas& iteRemover, const LogicInfo& logic, + TheoryEngine(Environment* env, + context::Context* context, + context::UserContext* userContext, + RemoveTermFormulas& iteRemover, + const LogicInfo& logic, LemmaChannels* channels); /** Destroys a theory engine */ @@ -487,12 +497,16 @@ public: * there is another theory it will be deleted. */ template - inline void addTheory(theory::TheoryId theoryId) { + 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_env, + d_context, + d_userContext, + *d_theoryOut[theoryId], + theory::Valuation(this), + d_logicInfo); } inline void setPropEngine(prop::PropEngine* propEngine) { @@ -508,6 +522,22 @@ public: /** Called when all initialization of options/logic is done */ void finishInit(); + /** + * Set the owner of the uninterpreted sort. + */ + void setUninterpretedSortOwner(theory::TheoryId theory) + { + d_uninterpretedSortOwner = theory; + } + + /** + * Get the owner of the uninterpreted sort. + */ + theory::TheoryId getUninterpretedSortOwner() + { + return d_uninterpretedSortOwner; + } + /** * Get a pointer to the underlying propositional engine. */ @@ -793,7 +823,7 @@ public: * of built-in type. */ inline theory::Theory* theoryOf(TNode node) const { - return d_theoryTable[theory::Theory::theoryOf(node)]; + return d_theoryTable[theoryIdOf(node)]; } /** @@ -806,6 +836,24 @@ public: return d_theoryTable[theoryId]; } + /** + * Return the ID of the theory responsible for the given type. + */ + theory::TheoryId theoryIdOf(TypeNode typeNode) const; + + /** + * Returns the ID of the theory responsible for the given node. + */ + theory::TheoryId theoryIdOf(theory::TheoryOfMode mode, TNode node) const; + + /** + * Returns the ID of the theory responsible for the given node. + */ + theory::TheoryId theoryIdOf(TNode node) const + { + return theoryIdOf(options::theoryOfMode(), node); + } + inline bool isTheoryEnabled(theory::TheoryId theoryId) const { return d_logicInfo.isTheoryEnabled(theoryId); } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 95e3f702b..be07334b7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -40,13 +40,14 @@ namespace theory { namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, +TheoryUF::TheoryUF(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, std::string instanceName) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName), + : Theory(THEORY_UF, env, c, u, out, valuation, logicInfo, instanceName), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ @@ -127,7 +128,8 @@ void TheoryUF::check(Effort level) { TNode fact = assertion.assertion; Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; - Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl; + Debug("uf") << "Term's theory: " << d_env->theoryOf(fact.toExpr()) + << std::endl; if (d_thss != NULL) { bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index dd69b2ee2..b7ef40e7d 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -186,8 +186,12 @@ 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(Environment* env, + context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, std::string instanceName = ""); ~TheoryUF(); -- cgit v1.2.3