(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)

This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular

    we add a proof checker for nl-ext
    we add a CDProofSet for nl-ext

7 files changed, 168 insertions, 8 deletions

diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index d850ff34e..5da5319a1 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -26,14 +26,21 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-ExtState::ExtState(InferenceManager& im, NlModel& model, context::Context* c)
-    : d_im(im), d_model(model)
+ExtState::ExtState(InferenceManager& im,
+                   NlModel& model,
+                   ProofNodeManager* pnm,
+                   context::UserContext* c)
+    : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c)
 {
   d_false = NodeManager::currentNM()->mkConst(false);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+  if (d_pnm != nullptr)
+  {
+    d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-ext"));
+  }
 }
 
 void ExtState::init(const std::vector<Node>& xts)
@@ -89,6 +96,14 @@ void ExtState::init(const std::vector<Node>& xts)
   Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl;
 }
 
+bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; }
+
+CDProof* ExtState::getProof()
+{
+  Assert(isProofEnabled());
+  return d_proof->allocateProof(d_ctx);
+}
+
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index adf576c8b..863b3f879 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -18,7 +18,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof.h"
+#include "expr/proof_set.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"
@@ -30,10 +30,22 @@ namespace nl {
 
 struct ExtState
 {
-  ExtState(InferenceManager& im, NlModel& model, context::Context* c);
+  ExtState(InferenceManager& im,
+           NlModel& model,
+           ProofNodeManager* pnm,
+           context::UserContext* c);
 
   void init(const std::vector<Node>& xts);
 
+  /**
+   * Checks whether proofs are enabled.
+   */
+  bool isProofEnabled() const;
+  /**
+   * Creates and returns a new LazyCDProof that can be used to prove some lemma.
+   */
+  CDProof* getProof();
+
   Node d_false;
   Node d_true;
   Node d_zero;
@@ -44,6 +56,17 @@ struct ExtState
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
+  /**
+   * Pointer to the current proof node manager. nullptr, if proofs are
+   * disabled.
+   */
+  ProofNodeManager* d_pnm;
+  /** The user context. */
+  context::UserContext* d_ctx;
+  /**
+   * A CDProofSet that hands out CDProof objects for lemmas.
+   */
+  std::unique_ptr<CDProofSet<CDProof>> d_proof;
 
   // information about monomials
   std::vector<Node> d_ms;
diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
new file mode 100644
index 000000000..57ef378b6
--- /dev/null
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of NlExt proof checker
+ **/
+
+#include "theory/arith/nl/ext/proof_checker.h"
+
+#include "expr/sequence.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+void ExtProofRuleChecker::registerTo(ProofChecker* pc)
+{
+}
+
+Node ExtProofRuleChecker::checkInternal(PfRule id,
+                                        const std::vector<Node>& children,
+                                        const std::vector<Node>& args)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  auto zero = nm->mkConst<Rational>(0);
+  auto one = nm->mkConst<Rational>(1);
+  auto mone = nm->mkConst<Rational>(-1);
+  auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
+  auto mpi = nm->mkNode(Kind::MULT, mone, pi);
+  Trace("nl-ext-checker") << "Checking " << id << std::endl;
+  for (const auto& c : children)
+  {
+    Trace("nl-ext-checker") << "\t" << c << std::endl;
+  }
+  return Node::null();
+}
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h
new file mode 100644
index 000000000..88df46110
--- /dev/null
+++ b/src/theory/arith/nl/ext/proof_checker.h
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief NlExt proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
+#define CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+/**
+ * A checker for NlExt proofs
+ *
+ * This proof checker takes care of all proofs for lemmas from the ext
+ * subsolver.
+ */
+class ExtProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  ExtProofRuleChecker() = default;
+  ~ExtProofRuleChecker() = default;
+
+  /** Register all rules owned by this rule checker in pc. */
+  void registerTo(ProofChecker* pc) override;
+
+ protected:
+  /** Return the conclusion of the given proof step, or null if it is invalid */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index dff43e568..e4a71b34d 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -35,7 +35,8 @@ namespace nl {
 
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        ArithState& state,
-                                       eq::EqualityEngine* ee)
+                                       eq::EqualityEngine* ee,
+                                       ProofNodeManager* pnm)
     : d_containing(containing),
       d_im(containing.getInferenceManager()),
       d_needsLastCall(false),
@@ -47,7 +48,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                   containing.getOutputChannel()),
       d_model(containing.getSatContext()),
       d_trSlv(d_im, d_model),
-      d_extState(d_im, d_model, containing.getSatContext()),
+      d_extState(d_im, d_model, pnm, containing.getUserContext()),
       d_factoringSlv(d_im, d_model),
       d_monomialBoundsSlv(&d_extState),
       d_monomialSlv(&d_extState),
@@ -67,6 +68,12 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    d_proofChecker.registerTo(pc);
+  }
 }
 
 NonlinearExtension::~NonlinearExtension() {}
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 2de5daeb6..77031ee1c 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -29,6 +29,7 @@
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 #include "theory/arith/nl/ext/monomial_check.h"
+#include "theory/arith/nl/ext/proof_checker.h"
 #include "theory/arith/nl/ext/split_zero_check.h"
 #include "theory/arith/nl/ext/tangent_plane_check.h"
 #include "theory/arith/nl/ext_theory_callback.h"
@@ -76,7 +77,10 @@ class NonlinearExtension
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  NonlinearExtension(TheoryArith& containing, ArithState& state, eq::EqualityEngine* ee);
+  NonlinearExtension(TheoryArith& containing,
+                     ArithState& state,
+                     eq::EqualityEngine* ee,
+                     ProofNodeManager* pnm);
   ~NonlinearExtension();
   /**
    * Does non-context dependent setup for a node connected to a theory.
@@ -252,6 +256,8 @@ class NonlinearExtension
    * transcendental functions.
    */
   transcendental::TranscendentalSolver d_trSlv;
+  /** The proof checker for proofs of the nlext. */
+  ExtProofRuleChecker d_proofChecker;
   /**
    * Holds common lookup data for the checks implemented in the "nl-ext"
    * solvers (from Cimatti et al., TACAS 2017).
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b8cead4fc..d1dd4bb63 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -82,7 +82,7 @@ void TheoryArith::finishInit()
   if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
   {
     d_nonlinearExtension.reset(
-        new nl::NonlinearExtension(*this, d_astate, d_equalityEngine));
+        new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm));
   }
   // finish initialize internally
   d_internal->finishInit();