Allow to pass ProofGenerator to arithmetic inference manager. (#5488)

This PR prepares the addition of proofs for the arithmetic theory by making addPendingArithLemma() accept a ProofGenerator*.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 43359c4602519d6474aa752355f9b74d59c3ca0b..08d2231375462baa83ad1e3ba44be34ecc7653f0 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -68,10 +68,11 @@ void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
 }
 void InferenceManager::addPendingArithLemma(const Node& lemma,
                                             InferenceId inftype,
+                                            ProofGenerator* pg,
                                             bool isWaiting)
 {
   addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(
-                           lemma, LemmaProperty::NONE, nullptr, inftype)),
+                           lemma, LemmaProperty::NONE, pg, inftype)),
                        isWaiting);
 }
 

diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index f2784ed89ace9990510c9244b1f6d44892e2aa1a..66710cd7b977b0fde7c9935d419512ec53499570 100644 (file)
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -37,7 +37,7 @@ class TheoryArith;
  * arithmetic theory.
  *
  * It adds some convenience methods to send ArithLemma and adds a mechanism for
- * waiting lemmas that can be flushed into the pending lemmas of the this
+ * waiting lemmas that can be flushed into the pending lemmas of this
  * buffered inference manager.
  * It also extends the caching mechanism of TheoryInferenceManager to cache
  * preprocessing lemmas and non-preprocessing lemmas separately. For the former,
@@ -51,29 +51,30 @@ class InferenceManager : public InferenceManagerBuffered
   InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
 
   /**
-   * Add a lemma as pending lemma to the this inference manager.
+   * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
   void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
                             bool isWaiting = false);
   /**
-   * Add a lemma as pending lemma to the this inference manager.
+   * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
   void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false);
   /**
-   * Add a lemma as pending lemma to the this inference manager.
+   * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
   void addPendingArithLemma(const Node& lemma,
                             InferenceId inftype,
+                            ProofGenerator* pg = nullptr,
                             bool isWaiting = false);
 
   /**
-   * Flush all waiting lemmas to the this inference manager (as pending
+   * Flush all waiting lemmas to this inference manager (as pending
    * lemmas). To actually send them, call doPendingLemmas() afterwards.
    */
   void flushWaitingLemmas();
@@ -84,8 +85,8 @@ class InferenceManager : public InferenceManagerBuffered
   void clearWaitingLemmas();
 
   /**
-   * Checks whether we have made any progress, that is whether a conflict, lemma
-   * or fact was added or whether a lemma or fact is pending.
+   * Checks whether we have made any progress, that is whether a conflict,
+   * lemma or fact was added or whether a lemma or fact is pending.
    */
   bool hasUsed() const;
 

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index fe4b1b83ae789c91e12fed681a91aa5cb66ede67..de6a3c65dc0fd0bdbfff39e22df86c6c0f645bc4 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -320,7 +320,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
             // Trace("nl-ext-bound-lemma") << "       intro new
             // monomials = " << introNewTerms << std::endl;
             d_data->d_im.addPendingArithLemma(
-                iblem, InferenceId::NL_INFER_BOUNDS_NT, introNewTerms);
+                iblem, InferenceId::NL_INFER_BOUNDS_NT, nullptr, introNewTerms);
           }
         }
       }
@@ -497,4 +497,4 @@ void MonomialBoundsCheck::checkResBounds()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
\ No newline at end of file
+}  // namespace CVC4

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 5235b7d430d813b11891f9455a77936b9d403a2d..3849c84242358776781c4d201c10984005be566c 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -133,7 +133,7 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
               Trace("nl-ext-tplanes")
                   << "Tangent plane lemma : " << tlem << std::endl;
               d_data->d_im.addPendingArithLemma(
-                  tlem, InferenceId::NL_TANGENT_PLANE, asWaitingLemmas);
+                  tlem, InferenceId::NL_TANGENT_PLANE, nullptr, asWaitingLemmas);
             }
           }
         }
@@ -145,4 +145,4 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
\ No newline at end of file
+}  // namespace CVC4

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 30441a8f48faa14ba3a7f562de1e90b8fa93d1f4..e33cfa6cddd2f0b567efcb279819470d51c9435b 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -151,7 +151,8 @@ void IAndSolver::checkFullRefine()
         Node lem = sumBasedLemma(i);  // add lemmas based on sum mode
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl;
-        d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_SUM_REFINE, true);
+        d_im.addPendingArithLemma(
+            lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true);
       }
       else if (options::iandMode() == options::IandMode::BITWISE)
       {
@@ -163,7 +164,8 @@ void IAndSolver::checkFullRefine()
         Node lem = valueBasedLemma(i);
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
-        d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_VALUE_REFINE, true);
+        d_im.addPendingArithLemma(
+            lem, InferenceId::NL_IAND_VALUE_REFINE, nullptr, true);
       }
     }
   }

diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp
index b3248119b64f80782e8ded19256d2cfc6418547d..2e25f1642b585041c02a25005567a8e89b69986e 100644 (file)
--- a/src/theory/arith/nl/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental_solver.cpp
@@ -875,7 +875,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf,
         << "*** Tangent plane lemma : " << lem << std::endl;
     Assert(d_model.computeAbstractModelValue(lem) == d_false);
     // Figure 3 : line 9
-    d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, true);
+    d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true);
   }
   else if (is_secant)
   {