diff options
35 files changed, 212 insertions, 105 deletions
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3f663726c..fbb21034a 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -65,7 +65,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) { theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id); } - + // Add the proof checkers for each theory + if (d_pnm) + { + d_theoryEngine->initializeProofChecker(d_pnm->getChecker()); + } Trace("smt-debug") << "Making prop engine..." << std::endl; /* force destruction of referenced PropEngine to enforce that statistics * are unregistered by the obsolete PropEngine object before registered diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 577aa0e6c..834a3d52d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -17,6 +17,7 @@ #include "theory/arith/theory_arith.h" +#include "expr/proof_checker.h" #include "expr/proof_rule.h" #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" @@ -65,6 +66,11 @@ TheoryArith::~TheoryArith(){ TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryArith::getProofChecker() +{ + return d_internal->getProofChecker(); +} + bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi) { return d_internal->needsEqualityEngine(esi); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 40abe21e0..0c1320b03 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -61,6 +61,8 @@ class TheoryArith : public Theory { //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if this theory needs an equality engine, which is assigned * to it (d_equalityEngine) by the equality engine manager during diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index b11bff768..d38dd881b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -172,11 +172,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_previousStatus(Result::SAT_UNKNOWN), d_statistics() { - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - d_checker.registerTo(pc); - } } TheoryArithPrivate::~TheoryArithPrivate(){ @@ -5507,6 +5502,11 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg } } +ArithProofRuleChecker* TheoryArithPrivate::getProofChecker() +{ + return &d_checker; +} + // InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const // inferbounds::InferBoundAlgorithm& param){ // Assert(param.findUpperBound()); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 929f40b56..ca2df4bd8 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -335,7 +335,7 @@ private: // inline void raiseConflict(const ConstraintCPVec& cv){ // d_conflicts.push_back(cv); // } - + // void raiseConflict(ConstraintCP a, ConstraintCP b); // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c); @@ -508,6 +508,9 @@ private: */ bool foundNonlinear() const; + /** get the proof checker of this theory */ + ArithProofRuleChecker* getProofChecker(); + private: /** The constant zero. */ DeltaRational d_DELTA_ZERO; @@ -759,7 +762,7 @@ private: static ConstraintCP vectorToIntHoleConflict(const ConstraintCPVec& conflict); static void intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict); - + // Returns true if the node contains a literal // that is an arithmetic literal and is not a sat literal // No caching is done so this should likely only diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 543d9833c..c51f4b98a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -131,11 +131,6 @@ TheoryArrays::TheoryArrays(context::Context* c, d_ppEqualityEngine.addFunctionKind(kind::SELECT); d_ppEqualityEngine.addFunctionKind(kind::STORE); - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - d_pchecker.registerTo(pc); - } // indicate we are using the default theory state object, and the arrays // inference manager d_theoryState = &d_state; @@ -167,6 +162,8 @@ TheoryArrays::~TheoryArrays() { TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; } + bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index e61c76089..24772a5f0 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -145,6 +145,8 @@ class TheoryArrays : public Theory { //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the @@ -349,7 +351,7 @@ class TheoryArrays : public Theory { NotifyClass d_notify; /** The proof checker */ - ArraysProofRuleChecker d_pchecker; + ArraysProofRuleChecker d_checker; /** Conflict when merging constants */ void conflict(TNode a, TNode b); diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index bea83ce40..933f1b1a1 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -14,6 +14,7 @@ #include "theory/bags/theory_bags.h" +#include "expr/proof_checker.h" #include "smt/logic_exception.h" #include "theory/bags/normal_form.h" #include "theory/rewriter.h" @@ -50,6 +51,8 @@ TheoryBags::~TheoryBags() {} TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; } + bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 7bb6111bd..7505f43bf 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -46,6 +46,8 @@ class TheoryBags : public Theory //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 74279f43c..04d6e77f6 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -29,8 +29,6 @@ #include "theory/valuation.h" #include "util/hash.h" -using namespace std; - namespace cvc5 { namespace theory { namespace booleans { @@ -43,12 +41,6 @@ TheoryBool::TheoryBool(context::Context* c, ProofNodeManager* pnm) : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm) { - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - // add checkers - d_bProofChecker.registerTo(pc); - } } Theory::PPAssertStatus TheoryBool::ppAssert( @@ -80,6 +72,12 @@ Theory::PPAssertStatus TheoryBool::ppAssert( return Theory::ppAssert(tin, outSubstitutions); } +TheoryRewriter* TheoryBool::getTheoryRewriter() { return &d_rewriter; } + +ProofRuleChecker* TheoryBool::getProofChecker() { return &d_checker; } + +std::string TheoryBool::identify() const { return std::string("TheoryBool"); } + } // namespace booleans } // namespace theory } // namespace cvc5 diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 05b169c24..042e487d6 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -37,18 +37,21 @@ class TheoryBool : public Theory { const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr); - TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } + /** get the official theory rewriter of this theory */ + TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; PPAssertStatus ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions) override; - std::string identify() const override { return std::string("TheoryBool"); } + std::string identify() const override; private: /** The theory rewriter for this theory. */ TheoryBoolRewriter d_rewriter; /** Proof rule checker */ - BoolProofRuleChecker d_bProofChecker; + BoolProofRuleChecker d_checker; };/* class TheoryBool */ } // namespace booleans diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index bd0374675..c2d9520d5 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -22,8 +22,6 @@ #include "theory/theory_model.h" #include "theory/valuation.h" -using namespace std; - namespace cvc5 { namespace theory { namespace builtin { @@ -36,14 +34,12 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c, ProofNodeManager* pnm) : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm) { - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - // add checkers - d_bProofChecker.registerTo(pc); - } } +TheoryRewriter* TheoryBuiltin::getTheoryRewriter() { return &d_rewriter; } + +ProofRuleChecker* TheoryBuiltin::getProofChecker() { return &d_checker; } + std::string TheoryBuiltin::identify() const { return std::string("TheoryBuiltin"); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index b4de83c02..fca05d7ff 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -37,7 +37,10 @@ class TheoryBuiltin : public Theory const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr); - TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } + /** get the official theory rewriter of this theory */ + TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; std::string identify() const override; @@ -48,7 +51,7 @@ class TheoryBuiltin : public Theory /** The theory rewriter for this theory. */ TheoryBuiltinRewriter d_rewriter; /** Proof rule checker */ - BuiltinProofRuleChecker d_bProofChecker; + BuiltinProofRuleChecker d_checker; }; /* class TheoryBuiltin */ } // namespace builtin diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index c96e8d0bc..7049044d4 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -74,10 +74,6 @@ BVSolverSimple::BVSolverSimple(TheoryState* s, d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "") : nullptr) { - if (pnm != nullptr) - { - d_bvProofChecker.registerTo(pnm->getChecker()); - } } void BVSolverSimple::addBBLemma(TNode fact) @@ -149,6 +145,8 @@ bool BVSolverSimple::collectModelValues(TheoryModel* m, return d_bitblaster->collectModelValues(m, termSet); } +BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; } + } // namespace bv } // namespace theory } // namespace cvc5 diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index 8983bddb2..843032bef 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -25,7 +25,6 @@ #include "theory/eager_proof_generator.h" namespace cvc5 { - namespace theory { namespace bv { @@ -63,6 +62,9 @@ class BVSolverSimple : public BVSolver bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; + /** get the proof checker of this theory */ + BVProofRuleChecker* getProofChecker(); + private: /** * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the @@ -75,8 +77,8 @@ class BVSolverSimple : public BVSolver /** Proof generator that manages proofs for lemmas generated by this class. */ std::unique_ptr<EagerProofGenerator> d_epg; - - BVProofRuleChecker d_bvProofChecker; + /** Proof rule checker */ + BVProofRuleChecker d_checker; }; } // namespace bv diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 8f9f88ea2..0587b8da0 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -15,6 +15,7 @@ #include "theory/bv/theory_bv.h" +#include "expr/proof_checker.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "theory/bv/bv_solver_bitblast.h" @@ -63,6 +64,15 @@ TheoryBV::~TheoryBV() {} TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryBV::getProofChecker() +{ + if (options::bvSolver() == options::BVSolver::SIMPLE) + { + return static_cast<BVSolverSimple*>(d_internal.get())->getProofChecker(); + } + return nullptr; +} + bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi) { bool need_ee = d_internal->needsEqualityEngine(esi); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c9ddaad11..c959aa5c1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -25,6 +25,9 @@ #include "theory/theory_state.h" namespace cvc5 { + +class ProofRuleChecker; + namespace theory { namespace bv { @@ -49,6 +52,8 @@ class TheoryBV : public Theory /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9d231f07d..3646c47b6 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -75,13 +75,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, // indicate we are using the default theory state object d_theoryState = &d_state; d_inferManager = &d_im; - - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - // add checkers - d_pchecker.registerTo(pc); - } } TheoryDatatypes::~TheoryDatatypes() { @@ -95,6 +88,8 @@ TheoryDatatypes::~TheoryDatatypes() { TheoryRewriter* TheoryDatatypes::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryDatatypes::getProofChecker() { return &d_checker; } + bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; @@ -141,10 +136,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak if( n.getKind()==APPLY_CONSTRUCTOR ){ ei->d_constructor = n; } - + //add to selectors d_selector_apps[n] = 0; - + return ei; }else{ return NULL; @@ -1018,7 +1013,7 @@ void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFact }else{ d_selector_apps_data[n].push_back( s ); } - + eqc->d_selectors = true; } if( assertFacts && !eqc->d_constructor.get().isNull() ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 34e865a50..e6df13348 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -199,6 +199,8 @@ private: //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the @@ -309,7 +311,7 @@ private: /** The notify class */ NotifyClass d_notify; /** Proof checker for datatypes */ - DatatypesProofRuleChecker d_pchecker; + DatatypesProofRuleChecker d_checker; };/* class TheoryDatatypes */ } // namespace datatypes diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 38444c7af..f647450c0 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -132,6 +132,8 @@ TheoryFp::TheoryFp(context::Context* c, TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryFp::getProofChecker() { return nullptr; } + bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notification; @@ -940,12 +942,11 @@ void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2) d_im.conflictEqConstantMerge(t1, t2); } - -bool TheoryFp::needsCheckLastEffort() -{ +bool TheoryFp::needsCheckLastEffort() +{ // only need to check if we have added to the abstraction map, otherwise // postCheck below is a no-op. - return !d_abstractionMap.empty(); + return !d_abstractionMap.empty(); } void TheoryFp::postCheck(Effort level) diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 87c63a231..6ed026567 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -51,6 +51,8 @@ class TheoryFp : public Theory //--------------------------------- initialization /** Get the official theory rewriter of this theory. */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index c3c3fe7b6..31b4f8c24 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -48,13 +48,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, out.handleUserAttribute( "quant-elim", this ); out.handleUserAttribute( "quant-elim-partial", this ); - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - // add the proof rules - d_qChecker.registerTo(pc); - } - // Finish initializing the term registry by hooking it up to the inference // manager. This is required due to a cyclic dependency between the term // database and the instantiate module. Term database needs inference manager @@ -82,6 +75,9 @@ TheoryQuantifiers::~TheoryQuantifiers() { } TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; } + +ProofRuleChecker* TheoryQuantifiers::getProofChecker() { return &d_checker; } + void TheoryQuantifiers::finishInit() { // quantifiers are not evaluated in getModelValue diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 21c30390c..716e8cdbd 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -47,6 +47,8 @@ class TheoryQuantifiers : public Theory { //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** finish initialization */ void finishInit() override; /** needs equality engine */ @@ -83,7 +85,7 @@ class TheoryQuantifiers : public Theory { /** The theory rewriter for this theory. */ QuantifiersRewriter d_rewriter; /** The proof rule checker */ - QuantifiersProofRuleChecker d_qChecker; + QuantifiersProofRuleChecker d_checker; /** The quantifiers state */ QuantifiersState d_qstate; /** The quantifiers registry */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index ab9b1b08d..6085c034d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -87,6 +87,8 @@ void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT) TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheorySep::getProofChecker() { return nullptr; } + bool TheorySep::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; @@ -174,7 +176,7 @@ void TheorySep::computeCareGraph() { void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << "Printing model for TheorySep..." << std::endl; - + std::vector< Node > sep_children; Node m_neq; Node m_heap; @@ -963,9 +965,15 @@ void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) { } //return cardinality -int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, - std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict, - bool pol, bool hasPol, bool underSpatial ) { +int TheorySep::processAssertion( + Node n, + std::map<int, std::map<Node, int> >& visited, + std::map<int, std::map<Node, std::vector<Node> > >& references, + std::map<int, std::map<Node, bool> >& references_strict, + bool pol, + bool hasPol, + bool underSpatial) +{ int index = hasPol ? ( pol ? 1 : -1 ) : 0; int card = 0; std::map< Node, int >::iterator it = visited[index].find( n ); @@ -975,7 +983,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& registerRefDataTypesAtom(n); if( hasPol && pol ){ references[index][n].clear(); - references_strict[index][n] = true; + references_strict[index][n] = true; }else{ card = 1; } @@ -993,7 +1001,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& references[index][n].push_back( n[0] ); } if( hasPol && pol ){ - references_strict[index][n] = true; + references_strict[index][n] = true; }else{ card = 1; } @@ -1055,7 +1063,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& }else{ card = it->second; } - + if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){ TypeNode tn = getReferenceType( n ); Assert(!tn.isNull()); @@ -1157,7 +1165,7 @@ void TheorySep::initializeBounds() { Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; unsigned n_emp = 0; if( d_bound_kind[tn] != bound_invalid ){ - n_emp = d_card_max[tn]; + n_emp = d_card_max[tn]; }else if( d_type_references[tn].empty() ){ //must include at least one constant TODO: remove? n_emp = 1; @@ -1213,12 +1221,13 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { } }else{ //break symmetries TODO - + d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() ); } //Assert( !d_type_references_all[tn].empty() ); - - if( d_bound_kind[tn]!=bound_invalid ){ + + if (d_bound_kind[tn] != bound_invalid) + { //construct bound d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] ); Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl; @@ -1247,7 +1256,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { } } } - + //assert that nil ref is not in base label Node nr = getNilRef( tn ); Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate(); @@ -1344,8 +1353,16 @@ Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) } } -Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, - TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) { +Node TheorySep::instantiateLabel(Node n, + Node o_lbl, + Node lbl, + Node lbl_v, + std::map<Node, Node>& visited, + std::map<Node, Node>& pto_model, + TypeNode rtn, + std::map<Node, bool>& active_lbl, + unsigned ind) +{ Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl; if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){ Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl; @@ -1420,7 +1437,8 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: for( unsigned i=0; i<children.size(); i++ ){ std::vector< Node > tchildren; Node mval = mvals[i]; - tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) ); + tchildren.push_back( + NodeManager::currentNM()->mkNode(kind::SUBSET, mval, lbl)); tchildren.push_back( children[i] ); std::vector< Node > rem_children; for( unsigned j=0; j<children.size(); j++ ){ @@ -1442,7 +1460,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: Node sub_lbl_0 = d_label_map[n][lbl][0]; Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn ); wchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval_0, lbl ).eqNode( empSet ).negate() ); - + //return the lemma wchildren.push_back( children[0].negate() ); wchildren.push_back( children[1] ); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index d52a3bca5..7d658352d 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -56,7 +56,7 @@ class TheorySep : public Theory { /** True node for predicates = false */ Node d_false; - + //whether bounds have been initialized bool d_bounds_init; @@ -68,9 +68,14 @@ class TheorySep : public Theory { Node mkAnd( std::vector< TNode >& assumptions ); - int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, - std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict, - bool pol, bool hasPol, bool underSpatial ); + int processAssertion( + Node n, + std::map<int, std::map<Node, int> >& visited, + std::map<int, std::map<Node, std::vector<Node> > >& references, + std::map<int, std::map<Node, bool> >& references_strict, + bool pol, + bool hasPol, + bool underSpatial); public: TheorySep(context::Context* c, @@ -93,6 +98,8 @@ class TheorySep : public Theory { //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the @@ -258,7 +265,7 @@ class TheorySep : public Theory { bound_invalid, }; std::map< TypeNode, unsigned > d_bound_kind; - + std::map< TypeNode, std::vector< Node > > d_type_references_card; std::map< Node, unsigned > d_type_ref_card_id; std::map< TypeNode, std::vector< Node > > d_type_references_all; @@ -328,8 +335,15 @@ class TheorySep : public Theory { void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ); void mergePto( Node p1, Node p2 ); void computeLabelModel( Node lbl ); - Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, - TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 ); + Node instantiateLabel(Node n, + Node o_lbl, + Node lbl, + Node lbl_v, + std::map<Node, Node>& visited, + std::map<Node, Node>& pto_model, + TypeNode rtn, + std::map<Node, bool>& active_lbl, + unsigned ind = 0); void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ); Node mkUnion( TypeNode tn, std::vector< Node >& locs ); diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index bd682ca57..eb2363eb7 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -55,6 +55,8 @@ TheoryRewriter* TheorySets::getTheoryRewriter() return d_internal->getTheoryRewriter(); } +ProofRuleChecker* TheorySets::getProofChecker() { return nullptr; } + bool TheorySets::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 16829bc6d..14f4b5699 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -53,6 +53,8 @@ class TheorySets : public Theory //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the @@ -102,7 +104,7 @@ class TheorySets : public Theory void eqNotifyNewClass(TNode t) override; void eqNotifyMerge(TNode t1, TNode t2) override; void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; - + private: TheorySetsPrivate& d_theory; }; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f2f584da7..2ce8adf95 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -84,12 +84,6 @@ TheoryStrings::TheoryStrings(context::Context* c, // set up the extended function callback d_extTheoryCb.d_esolver = &d_esolver; - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - // add checkers - d_sProofChecker.registerTo(pc); - } // use the state object as the official theory state d_theoryState = &d_state; // use the inference manager as the official inference manager @@ -102,6 +96,8 @@ TheoryStrings::~TheoryStrings() { TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryStrings::getProofChecker() { return &d_checker; } + bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index e1fc20d29..99a3f2c04 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -74,6 +74,8 @@ class TheoryStrings : public Theory { //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the @@ -273,7 +275,7 @@ class TheoryStrings : public Theory { /** The theory rewriter for this theory. */ StringsRewriter d_rewriter; /** The proof rule checker */ - StringProofRuleChecker d_sProofChecker; + StringProofRuleChecker d_checker; /** * The base solver, responsible for reasoning about congruent terms and * inferring constants for equivalence classes. diff --git a/src/theory/theory.h b/src/theory/theory.h index 4b06a5fa8..050fd51f7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -43,6 +43,7 @@ namespace cvc5 { class ProofNodeManager; class TheoryEngine; +class ProofRuleChecker; namespace theory { @@ -317,6 +318,10 @@ class Theory { */ virtual TheoryRewriter* getTheoryRewriter() = 0; /** + * @return The proof checker associated with this theory. + */ + virtual ProofRuleChecker* getProofChecker() = 0; + /** * Returns true if this theory needs an equality engine for checking * satisfiability. * diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6271f0afb..1482259e1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -24,6 +24,7 @@ #include "expr/lazy_proof.h" #include "expr/node_builder.h" #include "expr/node_visitor.h" +#include "expr/proof_checker.h" #include "expr/proof_ensure_closed.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -1894,4 +1895,17 @@ void TheoryEngine::spendResource(ResourceManager::Resource r) d_resourceManager->spendResource(r); } +void TheoryEngine::initializeProofChecker(ProofChecker* pc) +{ + for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; + ++id) + { + ProofRuleChecker* prc = d_theoryTable[id]->getProofChecker(); + if (prc) + { + prc->registerTo(pc); + } + } +} + } // namespace cvc5 diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7b91191f9..03c733451 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -46,6 +46,7 @@ namespace cvc5 { class ResourceManager; class OutputManager; class TheoryEngineProofGenerator; +class ProofChecker; /** * A pair of a theory and a node. This is used to mark the flow of @@ -322,6 +323,9 @@ class TheoryEngine { theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } + /** Register theory proof rule checkers to the given proof checker */ + void initializeProofChecker(ProofChecker* pc); + void setPropEngine(prop::PropEngine* propEngine) { d_propEngine = propEngine; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index f3c0a0ba0..e8ce7660a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -57,12 +57,6 @@ TheoryUF::TheoryUF(context::Context* c, d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); - - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) - { - d_ufProofChecker.registerTo(pc); - } // indicate we are using the default theory state and inference managers d_theoryState = &d_state; d_inferManager = &d_im; @@ -73,6 +67,8 @@ TheoryUF::~TheoryUF() { TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryUF::getProofChecker() { return &d_checker; } + bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index f6f4b3ee9..bae2a2544 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -111,6 +111,8 @@ private: //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the @@ -170,7 +172,7 @@ private: bool isHigherOrderType(TypeNode tn); TheoryUfRewriter d_rewriter; /** Proof rule checker */ - UfProofRuleChecker d_ufProofChecker; + UfProofRuleChecker d_checker; /** A (default) theory state object */ TheoryState d_state; /** A (default) inference manager */ diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index a26e039e4..f26bd0ff6 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -18,6 +18,7 @@ #include "expr/dtype_cons.h" #include "expr/node.h" #include "expr/node_manager.h" +#include "expr/proof_checker.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" @@ -169,7 +170,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel /* -------------------------------------------------------------------------- */ -class DymmyTheoryRewriter : public theory::TheoryRewriter +class DummyTheoryRewriter : public theory::TheoryRewriter { public: theory::RewriteResponse preRewrite(TNode n) override @@ -183,6 +184,22 @@ class DymmyTheoryRewriter : public theory::TheoryRewriter } }; +class DummyProofRuleChecker : public ProofRuleChecker +{ + public: + DummyProofRuleChecker() {} + ~DummyProofRuleChecker() {} + void registerTo(ProofChecker* pc) override {} + + protected: + Node checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) override + { + return Node::null(); + } +}; + /** Dummy Theory interface. */ template <theory::TheoryId theoryId> class DummyTheory : public theory::Theory @@ -202,6 +219,7 @@ class DummyTheory : public theory::Theory } theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } + ProofRuleChecker* getProofChecker() override { return &d_checker; } void registerTerm(TNode n) { @@ -244,7 +262,9 @@ class DummyTheory : public theory::Theory */ std::string d_id; /** The theory rewriter for this theory. */ - DymmyTheoryRewriter d_rewriter; + DummyTheoryRewriter d_rewriter; + /** The proof checker for this theory. */ + DummyProofRuleChecker d_checker; }; /* -------------------------------------------------------------------------- */ |