From 4b023ebf819e9d909d1542b79adc38fe1529a7fc Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 29 Sep 2020 09:39:11 -0700 Subject: [PATCH] (proof-new) Add proof managers and eager gens to arith (#5159) This commit threads ProofNodeManager, EagerProofGenerator, etc throughout the arith theory into the appropriate locations. These objects are currently unused, but will be used in future commits. Crediting Andy, since he set up some of this. Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com --- src/theory/arith/congruence_manager.cpp | 22 +++++++-- src/theory/arith/congruence_manager.h | 55 +++++++++++++++++++++-- src/theory/arith/constraint.cpp | 32 ++++++++----- src/theory/arith/constraint.h | 20 ++++++--- src/theory/arith/theory_arith.cpp | 4 ++ src/theory/arith/theory_arith.h | 2 + src/theory/arith/theory_arith_private.cpp | 27 +++++++++-- src/theory/arith/theory_arith_private.h | 15 ++++++- 8 files changed, 147 insertions(+), 30 deletions(-) diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 361b47c65..520903562 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -29,10 +29,12 @@ namespace arith { ArithCongruenceManager::ArithCongruenceManager( context::Context* c, + context::UserContext* u, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, - RaiseEqualityEngineConflict raiseConflict) + RaiseEqualityEngineConflict raiseConflict, + ProofNodeManager* pnm) : d_inConflict(c), d_raiseConflict(raiseConflict), d_notify(*this), @@ -42,7 +44,15 @@ ArithCongruenceManager::ArithCongruenceManager( d_constraintDatabase(cd), d_setupLiteral(setup), d_avariables(avars), - d_ee(nullptr) + d_ee(nullptr), + d_satContext(c), + d_userContext(u), + d_pnm(pnm), + d_pfGenEe( + new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")), + d_pfGenExplain(new EagerProofGenerator( + pnm, u, "ArithCongruenceManager::pfGenExplain")), + d_pfee(nullptr) { } @@ -55,7 +65,8 @@ bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi) return true; } -void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) +void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee, + eq::ProofEqEngine* pfee) { Assert(ee != nullptr); d_ee = ee; @@ -63,6 +74,9 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) d_ee->addFunctionKind(kind::EXPONENTIAL); d_ee->addFunctionKind(kind::SINE); d_ee->addFunctionKind(kind::IAND); + // have proof equality engine only if proofs are enabled + Assert(isProofEnabled() == (pfee != nullptr)); + d_pfee = pfee; } ArithCongruenceManager::Statistics::Statistics(): @@ -458,6 +472,8 @@ void ArithCongruenceManager::addSharedTerm(Node x){ d_ee->addTriggerTerm(x, THEORY_ARITH); } +bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; } + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 77d4455ca..3565d86b5 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,11 +24,15 @@ #include "context/cdo.h" #include "context/cdtrail_queue.h" #include "context/context.h" +#include "expr/proof_node_manager.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/partial_model.h" +#include "theory/eager_proof_generator.h" #include "theory/ee_setup_info.h" +#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/proof_equality_engine.h" #include "util/dense_map.h" #include "util/statistics_registry.h" @@ -96,10 +100,46 @@ private: /** The equality engine being used by this class */ eq::EqualityEngine* d_ee; + /** The sat context */ + context::Context* d_satContext; + /** The user context */ + context::UserContext* d_userContext; + + /** proof manager */ + ProofNodeManager* d_pnm; + /** A proof generator for storing proofs of facts that are asserted to the EQ + * engine. Note that these proofs **are not closed**, and assume the + * explanation of these facts. This is why this generator is separate from the + * TheoryArithPrivate generator, which stores closed proofs. + */ + std::unique_ptr d_pfGenEe; + /** A proof generator for TrustNodes sent to TheoryArithPrivate. + * + * When TheoryArithPrivate requests an explanation from + * ArithCongruenceManager, it can request a TrustNode for that explanation. + * This proof generator is the one used in that TrustNode: it stores the + * (closed) proofs of implications proved by the + * ArithCongruenceManager/EqualityEngine. + * + * It is insufficient to just use the ProofGenerator from the ProofEqEngine, + * since sometimes the ArithCongruenceManager needs to add some + * arith-specific reasoning to extend the proof (e.g. rewriting the result + * into a normal form). + * */ + std::unique_ptr d_pfGenExplain; + + /** Pointer to the proof equality engine of TheoryArith */ + theory::eq::ProofEqEngine* d_pfee; + void raiseConflict(Node conflict); -public: + /** + * Are proofs enabled? This is true if a non-null proof manager was provided + * to the constructor of this class. + */ + bool isProofEnabled() const; + public: bool inConflict() const; bool hasMorePropagations() const; @@ -133,7 +173,14 @@ private: Node explainInternal(TNode internal); public: - ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict); + public: + ArithCongruenceManager(context::Context* satContext, + context::UserContext* u, + ConstraintDatabase&, + SetupLiteralCallBack, + const ArithVariables&, + RaiseEqualityEngineConflict raiseConflict, + ProofNodeManager* pnm); ~ArithCongruenceManager(); //--------------------------------- initialization @@ -144,9 +191,9 @@ public: bool needsEqualityEngine(EeSetupInfo& esi); /** * Finish initialize. This class is instructed by TheoryArithPrivate to use - * the equality engine ee. + * the equality engine ee and proof equality engine pfee. */ - void finishInit(eq::EqualityEngine* ee); + void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee); //--------------------------------- end initialization Node explain(TNode literal); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 98427950b..06ecb9618 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -847,17 +847,25 @@ ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRa } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVariables& avars, ArithCongruenceManager& cm, RaiseConflict raiseConflict) - : d_varDatabases() - , d_toPropagate(satContext) - , d_antecedents(satContext, false) - , d_watches(new Watches(satContext, userContext)) - , d_avariables(avars) - , d_congruenceManager(cm) - , d_satContext(satContext) - , d_raiseConflict(raiseConflict) - , d_one(1) - , d_negOne(-1) +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, + context::Context* userContext, + const ArithVariables& avars, + ArithCongruenceManager& cm, + RaiseConflict raiseConflict, + EagerProofGenerator* pfGen, + ProofNodeManager* pnm) + : d_varDatabases(), + d_toPropagate(satContext), + d_antecedents(satContext, false), + d_watches(new Watches(satContext, userContext)), + d_avariables(avars), + d_congruenceManager(cm), + d_satContext(satContext), + d_pfGen(pfGen), + d_pnm(pnm), + d_raiseConflict(raiseConflict), + d_one(1), + d_negOne(-1) { } @@ -1722,6 +1730,8 @@ ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Cont void Constraint::setLiteral(Node n) { + Debug("arith::constraint") << "Mapping " << *this << " to " << n << std::endl; + Assert(Comparison::isNormalAtom(n)); Assert(!hasLiteral()); Assert(sanityChecking(n)); d_literal = n; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index eb2d89de7..0afc0bc2f 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -85,6 +85,7 @@ #include "context/cdqueue.h" #include "context/context.h" #include "expr/node.h" +#include "expr/proof_node_manager.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/congruence_manager.h" @@ -1086,6 +1087,10 @@ private: ArithCongruenceManager& d_congruenceManager; const context::Context * const d_satContext; + /** Owned by the TheoryArithPrivate, used here. */ + EagerProofGenerator* d_pfGen; + /** Owned by the TheoryArithPrivate, used here. */ + ProofNodeManager* d_pnm; RaiseConflict d_raiseConflict; @@ -1095,13 +1100,14 @@ private: friend class Constraint; -public: - - ConstraintDatabase( context::Context* satContext, - context::Context* userContext, - const ArithVariables& variables, - ArithCongruenceManager& dm, - RaiseConflict conflictCallBack); + public: + ConstraintDatabase(context::Context* satContext, + context::Context* userContext, + const ArithVariables& variables, + ArithCongruenceManager& dm, + RaiseConflict conflictCallBack, + EagerProofGenerator* pfGen, + ProofNodeManager* pnm); ~ConstraintDatabase(); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9324c94af..f16e0a297 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -205,6 +205,10 @@ std::pair TheoryArith::entailmentCheck(TNode lit) std::pair res = d_internal->entailmentCheck(lit, def, ase); return res; } +eq::ProofEqEngine* TheoryArith::getProofEqEngine() +{ + return d_inferenceManager.getProofEqEngine(); +} }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 25d3b1e45..e332646ff 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -112,6 +112,8 @@ class TheoryArith : public Theory { } private: + /** Get the proof equality engine */ + eq::ProofEqEngine* getProofEqEngine(); /** The state object wrapping TheoryArithPrivate */ ArithState d_astate; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 74c35ff13..dfc51a6da 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -34,6 +34,8 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() @@ -92,8 +94,16 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, : d_containing(containing), d_nlIncomplete(false), d_rowTracking(), - d_constraintDatabase( - c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)), + d_pnm(pnm), + d_checker(), + d_pfGen(new EagerProofGenerator(d_pnm, u)), + d_constraintDatabase(c, + u, + d_partialModel, + d_congruenceManager, + RaiseConflict(*this), + d_pfGen.get(), + d_pnm), d_qflraStatus(Result::SAT_UNKNOWN), d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), @@ -119,11 +129,14 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_tableauResetPeriod(10), d_conflicts(c), d_blackBoxConflict(c, Node::null()), + d_blackBoxConflictPf(c, std::shared_ptr(nullptr)), d_congruenceManager(c, + u, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, - RaiseEqualityEngineConflict(*this)), + RaiseEqualityEngineConflict(*this), + d_pnm), d_cmEnabled(c, true), d_dualSimplex( @@ -159,6 +172,11 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_statistics(), d_opElim(pnm, logicInfo) { + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + d_checker.registerTo(pc); + } } TheoryArithPrivate::~TheoryArithPrivate(){ @@ -174,8 +192,9 @@ bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi) void TheoryArithPrivate::finishInit() { eq::EqualityEngine* ee = d_containing.getEqualityEngine(); + eq::ProofEqEngine* pfee = d_containing.getProofEqEngine(); Assert(ee != nullptr); - d_congruenceManager.finishInit(ee); + d_congruenceManager.finishInit(ee, pfee); d_nonlinearExtension = d_containing.d_nonlinearExtension.get(); } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 298c989f4..6f6ca7fdf 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -31,6 +31,7 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" +#include "expr/proof_generator.h" #include "options/arith_options.h" #include "smt/logic_exception.h" #include "smt_util/boolean_simplification.h" @@ -51,10 +52,12 @@ #include "theory/arith/normal_form.h" #include "theory/arith/operator_elim.h" #include "theory/arith/partial_model.h" +#include "theory/arith/proof_checker.h" #include "theory/arith/simplex.h" #include "theory/arith/soi_simplex.h" #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private_forward.h" +#include "theory/eager_proof_generator.h" #include "theory/rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -101,6 +104,14 @@ private: BoundInfoMap d_rowTracking; + // For proofs + /** Manages the proof nodes of this theory. */ + ProofNodeManager* d_pnm; + /** Checks the proof rules of this theory. */ + ArithProofRuleChecker d_checker; + /** Stores proposition(node)/proof pairs. */ + std::unique_ptr d_pfGen; + /** * The constraint database associated with the theory. * This must be declared before ArithPartialModel. @@ -306,8 +317,10 @@ private: /** This is only used by simplex at the moment. */ context::CDO d_blackBoxConflict; -public: + /** For holding the proof of the above conflict node. */ + context::CDO> d_blackBoxConflictPf; + public: /** * This adds the constraint a to the queue of conflicts in d_conflicts. * Both a and ~a must have a proof. -- 2.30.2