(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

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 361b47c65ba1c991fefa862a4ed1a26022cef9e8..52090356265fef9233a92c629961ac27a771b816 100644 (file)
--- 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 77d4455ca5afaead0d5e5c876092d2e54a517775..3565d86b5b8fecd9e9aad7cf381948470cfefaf5 100644 (file)
--- 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<EagerProofGenerator> 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<EagerProofGenerator> 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 98427950ba32d151f3696beccc04d78e8e88191e..06ecb96187d87e8fe6a57c8a4acb447031088063 100644 (file)
--- 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 eb2d89de719da3f5f3ee9e45e499f6ede320d6b5..0afc0bc2ff20ad0dd40e29e042ea2b54ca46bb05 100644 (file)
--- 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 9324c94af3027b9b0fcc3e2cefb0d2032f161577..f16e0a297f2004263a1191492f58eed621b0cef6 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -205,6 +205,10 @@ std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
   std::pair<bool, Node> 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 25d3b1e4532c6f86a4d09313f408d970da78e5d5..e332646ffaf9d323c175365c1f10f98b368e33ec 100644 (file)
--- 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 74c35ff138a52abdb40be13de9d0a79ccf7f3f79..dfc51a6daed4720e8a6ad9db598acc8e295459ce 100644 (file)
--- 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<ProofNode>(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 298c989f44ffc438d3def5c42556faedcd4e1f16..6f6ca7fdfc2a431bfa296eb48ed2df40409a99e3 100644 (file)
--- 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<EagerProofGenerator> 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<Node> d_blackBoxConflict;
-public:
+  /** For holding the proof of the above conflict node. */
+  context::CDO<std::shared_ptr<ProofNode>> d_blackBoxConflictPf;
 
+ public:
   /**
    * This adds the constraint a to the queue of conflicts in d_conflicts.
    * Both a and ~a must have a proof.