(proof-new) Make CombinationEngine proof producing (#4955)

Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 9374e7ecbc680a27ad4ae655096e7d582c57578c..c390a4b251bb14b43ae9cf2badcff131c7bd0507 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -22,8 +22,10 @@ namespace CVC4 {
 namespace theory {
 
 CombinationCareGraph::CombinationCareGraph(
-    TheoryEngine& te, const std::vector<Theory*>& paraTheories)
-    : CombinationEngine(te, paraTheories)
+    TheoryEngine& te,
+    const std::vector<Theory*>& paraTheories,
+    ProofNodeManager* pnm)
+    : CombinationEngine(te, paraTheories, pnm)
 {
 }
 
@@ -62,7 +64,17 @@ void CombinationCareGraph::combineTheories()
         << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
 
     Node split = equality.orNode(equality.notNode());
-    sendLemma(split, carePair.d_theory);
+    TrustNode tsplit;
+    if (isProofEnabled())
+    {
+      // make proof of splitting lemma
+      tsplit = d_cmbsPg->mkTrustNode(split, PfRule::SPLIT, {equality});
+    }
+    else
+    {
+      tsplit = TrustNode::mkTrustLemma(split, nullptr);
+    }
+    sendLemma(tsplit, carePair.d_theory);
 
     // Could check the equality status here:
     //   EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);

diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h
index 0fbefb16addcf082103d08d9211f6117646ae103..78f892f5edc96bda5a75bc2df122ae1eb6f070d6 100644 (file)
--- a/src/theory/combination_care_graph.h
+++ b/src/theory/combination_care_graph.h
@@ -35,7 +35,8 @@ class CombinationCareGraph : public CombinationEngine
 {
  public:
   CombinationCareGraph(TheoryEngine& te,
-                       const std::vector<Theory*>& paraTheories);
+                       const std::vector<Theory*>& paraTheories,
+                       ProofNodeManager* pnm);
   ~CombinationCareGraph();
 
   bool buildModel() override;

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 83aae3f5413fd50d23cf3f0484643ed403c73fb6..e1317cf298c7d211d0777b999252261d6f02d270 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -26,12 +26,15 @@ namespace CVC4 {
 namespace theory {
 
 CombinationEngine::CombinationEngine(TheoryEngine& te,
-                                     const std::vector<Theory*>& paraTheories)
+                                     const std::vector<Theory*>& paraTheories,
+                                     ProofNodeManager* pnm)
     : d_te(te),
       d_logicInfo(te.getLogicInfo()),
       d_paraTheories(paraTheories),
       d_eemanager(nullptr),
-      d_mmanager(nullptr)
+      d_mmanager(nullptr),
+      d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
+                   : nullptr)
 {
 }
 
@@ -100,15 +103,17 @@ theory::TheoryModel* CombinationEngine::getModel()
   return d_mmanager->getModel();
 }
 
+bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
+
 eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
 {
   // by default, no notifications from model's equality engine
   return nullptr;
 }
 
-void CombinationEngine::sendLemma(TNode node, TheoryId atomsTo)
+void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
 {
-  d_te.lemma(node, RULE_INVALID, false, LemmaProperty::NONE, atomsTo);
+  d_te.lemma(trn.getNode(), RULE_INVALID, false, LemmaProperty::NONE, atomsTo);
 }
 
 void CombinationEngine::resetRound()

diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index cfe6562d42d231a2a331e0874c7adba6af06f0ae..3aabc549a060304d20cc78e9f626fdfb95cd0dd5 100644 (file)
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -20,6 +20,7 @@
 #include <vector>
 #include <memory>
 
+#include "theory/eager_proof_generator.h"
 #include "theory/ee_manager.h"
 #include "theory/model_manager.h"
 
@@ -39,7 +40,9 @@ namespace theory {
 class CombinationEngine
 {
  public:
-  CombinationEngine(TheoryEngine& te, const std::vector<Theory*>& paraTheories);
+  CombinationEngine(TheoryEngine& te,
+                    const std::vector<Theory*>& paraTheories,
+                    ProofNodeManager* pnm);
   virtual ~CombinationEngine();
 
   /** Finish initialization */
@@ -91,13 +94,15 @@ class CombinationEngine
   virtual void combineTheories() = 0;
 
  protected:
+  /** Is proof enabled? */
+  bool isProofEnabled() const;
   /**
    * Get model equality engine notify. Return the notification object for
    * who listens to the model's equality engine (if any).
    */
   virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify();
   /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
-  void sendLemma(TNode node, TheoryId atomsTo);
+  void sendLemma(TrustNode trn, TheoryId atomsTo);
   /** Reference to the theory engine */
   TheoryEngine& d_te;
   /** Logic info of theory engine (cached) */
@@ -114,6 +119,11 @@ class CombinationEngine
    * model.
    */
   std::unique_ptr<ModelManager> d_mmanager;
+  /**
+   * An eager proof generator, if proofs are enabled. This proof generator is
+   * responsible for proofs of splitting lemmas generated in combineTheories.
+   */
+  std::unique_ptr<EagerProofGenerator> d_cmbsPg;
 };
 
 }  // namespace theory

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0979d447b0910ed0fa3263bb0beaaa409f9ac3f1..bf74cd0162f41aaa8038ce5f001021b3534e9755 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -151,7 +151,7 @@ void TheoryEngine::finishInit() {
   // Initialize the theory combination architecture
   if (options::tcMode() == options::TcMode::CARE_GRAPH)
   {
-    d_tc.reset(new CombinationCareGraph(*this, paraTheories));
+    d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
   }
   else
   {
@@ -213,6 +213,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_context(context),
       d_userContext(userContext),
       d_logicInfo(logicInfo),
+      d_pnm(nullptr),
       d_sharedTerms(this, context),
       d_tc(nullptr),
       d_quantEngine(nullptr),

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 61ee30bc8f66656a8a149f136d42586a04f4277b..b1543ad0b257fcc7570010cb63dd3d4f669d2905 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -144,6 +144,11 @@ class TheoryEngine {
    */
   const LogicInfo& d_logicInfo;
 
+  //--------------------------------- new proofs
+  /** Proof node manager used by this theory engine, if proofs are enabled */
+  ProofNodeManager* d_pnm;
+  //--------------------------------- end new proofs
+
   /**
    * The database of shared terms.
    */