TheoryEngineProofGenerator, proper explanations for getExplantaion

7 files changed, 209 insertions, 59 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2ac73f067..6deaea082 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -748,6 +748,8 @@ libcvc4_add_sources(
   theory/theory.h
   theory/theory_engine.cpp
   theory/theory_engine.h
+  theory/theory_engine_proof_generator.cpp
+  theory/theory_engine_proof_generator.h
   theory/theory_id.cpp
   theory/theory_id.h
   theory/theory_model.cpp
diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp
index 20dbd4ef0..82363ff9b 100644
--- a/src/theory/proof_engine_output_channel.cpp
+++ b/src/theory/proof_engine_output_channel.cpp
@@ -30,25 +30,8 @@ ProofEngineOutputChannel::ProofEngineOutputChannel(TheoryEngine* engine,
 void ProofEngineOutputChannel::trustedConflict(TrustNode pconf)
 {
   Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
-  Node conf = pconf.getNode();
-  if (d_lazyPf != nullptr)
-  {
-    Node ckey = pconf.getProven();
-    ProofGenerator* pfg = pconf.getGenerator();
-    // may or may not have supplied a generator
-    if (pfg != nullptr)
-    {
-      ++d_statistics.trustedConflicts;
-      // if we have, add it to the lazy proof object
-      d_lazyPf->addLazyStep(ckey, pfg);
-      Assert(pfg->hasProofFor(ckey));
-    }
-    else
-    {
-      // if none provided, do a very coarse-grained step
-      addTheoryLemmaStep(ckey);
-    }
-  }
+  d_engine->processTrustNode(pconf, d_theory);
+  TNode conf = pconf.getNode();
   // now, call the normal interface to conflict
   conflict(conf);
 }
@@ -59,25 +42,8 @@ LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem,
                                                    bool sendAtoms)
 {
   Assert(plem.getKind() == TrustNodeKind::LEMMA);
+  d_engine->processTrustNode(plem, d_theory);
   TNode lem = plem.getNode();
-  if (d_lazyPf != nullptr)
-  {
-    Node lkey = plem.getProven();
-    ProofGenerator* pfg = plem.getGenerator();
-    // may or may not have supplied a generator
-    if (pfg != nullptr)
-    {
-      ++d_statistics.trustedLemmas;
-      // if we have, add it to the lazy proof object
-      d_lazyPf->addLazyStep(lkey, pfg);
-      Assert(pfg->hasProofFor(lkey));
-    }
-    else
-    {
-      // if none provided, do a very coarse-grained step
-      addTheoryLemmaStep(lkey);
-    }
-  }
   // now, call the normal interface for lemma
   return OutputChannel::lemma(lem, removable, preprocess, sendAtoms);
 }
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 723e20a16..ac27a5820 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -230,7 +230,7 @@ void SharedTermsDatabase::checkForConflict() {
       conflict = conflict.notNode();
     }
     TrustNode trnc = d_pfee.assertConflict(conflict);
-    d_theoryEngine->processTrustNode(trnc);
+    d_theoryEngine->processTrustNode(trnc, THEORY_BUILTIN);
     d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN);
     d_conflictLHS = d_conflictRHS = Node::null();
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 93a3f286d..7a1e34bef 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -52,6 +52,7 @@
 #include "theory/theory_traits.h"
 #include "theory/uf/equality_engine.h"
 #include "util/resource_manager.h"
+#include "theory/theory_engine_proof_generator.h"
 
 using namespace std;
 
@@ -201,6 +202,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
           options::proofNew()
               ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext)
               : nullptr),
+      d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
       d_sharedTerms(
           this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()),
       d_masterEqualityEngine(nullptr),
@@ -1605,8 +1607,6 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe(
           proofRecipe->addStep(proofStep);
         }
       });
-    // it came directly from the theory, it is ready to be processed
-    processTrustNode(texplanation);
     return texplanation;
   }
 
@@ -1639,7 +1639,6 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe(
 
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
                            << texplanation.getNode() << endl;
-  // the trust node was processed within getExplanation
   return texplanation;
 }
 
@@ -1848,7 +1847,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
 }
 
-void TheoryEngine::processTrustNode(theory::TrustNode trn)
+void TheoryEngine::processTrustNode(theory::TrustNode trn,
+                            theory::TheoryId from)
 {
   if (d_lazyProof == nullptr)
   {
@@ -1856,15 +1856,29 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn)
     return;
   }
   ProofGenerator* pfg = trn.getGenerator();
+  Node p = trn.getProven();
   // may or may not have supplied a generator
   if (pfg != nullptr)
   {
-    Node p = trn.getProven();
     // if we have, add it to the lazy proof object
     d_lazyProof->addLazyStep(p, pfg);
     // generator should have a proof for p
     Assert(pfg->hasProofFor(p));
   }
+  else
+  {
+    // all BUILTIN should be handled
+    Assert (from!=THEORY_BUILTIN);
+    // untrusted theory lemma
+    std::vector<Node> children;
+    std::vector<Node> args;
+    args.push_back(p);
+    unsigned tid = static_cast<unsigned>(from);
+    Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
+    args.push_back(tidn);
+    // add the step, should always succeed;
+    d_lazyProof->addStep(p, PfRule::THEORY_LEMMA, children, args);
+  }
 }
 
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
@@ -1913,8 +1927,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     TrustNode tnc = getExplanation(vec, proofRecipe);
     PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
 
-    // FIXME: have ~( l1 ^ ... ^ ln ) and ( E1 ^ ... ^ En ) => l1 ^ ... ^ ln
-    // Prove ~( E1 ^ ... ^ En )
+    // FIXME: have ~( F ) and E => F, prove ~( E )
 
     Node fullConflict = tnc.getNode();
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
@@ -2009,7 +2022,9 @@ theory::TrustNode TheoryEngine::getExplanation(
   Assert(explanationVector.size() == 1);
 
   Node conclusion = explanationVector[0].d_node;
-  std::unique_ptr<LazyCDProof> lcp;
+  std::shared_ptr<LazyCDProof> lcp;
+  bool simpleExplain = true;
+  TrustNode simpleTrn;
   if (d_lazyProof != nullptr)
   {
     Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl;
@@ -2053,6 +2068,7 @@ theory::TrustNode TheoryEngine::getExplanation(
         args.push_back(toExplain.d_node);
         lcp->addStep(
             toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+        simpleExplain = false;
       }
       continue;
     }
@@ -2096,6 +2112,7 @@ theory::TrustNode TheoryEngine::getExplanation(
         args.push_back(mkMethodId(MethodId::SB_PREDICATE));
         lcp->addStep(
             toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+        simpleExplain = false;
       }
       ++ i;
       continue;
@@ -2138,6 +2155,7 @@ theory::TrustNode TheoryEngine::getExplanation(
             Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl;
             // does this ever happen?
             Assert(false);
+            simpleExplain = false;
           }
         }
         continue;
@@ -2196,6 +2214,20 @@ theory::TrustNode TheoryEngine::getExplanation(
         args.push_back(mkMethodId(MethodId::SB_PREDICATE));
         lcp->addStep(
             toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        if (simpleExplain)
+        {
+          if (simpleTrn.isNull())
+          {
+            // as an optimization, it may be a simple explanation, so we
+            // remember the trust node for now
+            simpleTrn = texplanation;
+          }
+          else
+          {
+            // multiple theories involved, not simple
+            simpleExplain = false;
+          }
+        }
       }
     }
     Node explanation = texplanation.getNode();
@@ -2269,18 +2301,20 @@ theory::TrustNode TheoryEngine::getExplanation(
 
   if (lcp != nullptr)
   {
-    Assert(lcp != nullptr);
-    // FIXME
-    // get the proof for conclusion
-    std::shared_ptr<ProofNode> pfConc = lcp->mkProof(conclusion);
-    std::vector<Node> scopeAssumps;
-    for (size_t k = 0, esize = explanationVector.size(); k < esize; ++k)
+    // doesn't work currently due to reordering of assumptions
+    /*
+    if (simpleExplain)
     {
-      scopeAssumps.push_back(explanationVector[k].d_node);
-    }
-    // call the scope method of proof node manager
-    std::shared_ptr<ProofNode> pf =
-        d_pNodeManager->mkScope(pfConc, scopeAssumps);
+      // single call to a theory's explain method, skip the proof generator
+      Assert (!simpleTrn.isNull());
+      Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << std::endl;
+      return simpleTrn;
+    }
+    */
+    // store in the proof generator
+    TrustNode trn = d_tepg->mkTrustExplain(conclusion,exp,lcp);
+    // return the trust node
+    return trn;
   }
 
   return theory::TrustNode::mkTrustLemma(exp, nullptr);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c3759ca52..de4b17f8c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -58,6 +58,7 @@ namespace CVC4 {
 class ResourceManager;
 class LemmaProofRecipe;
 class LazyCDProof;
+class TheoryEngineProofGenerator;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -156,6 +157,8 @@ class TheoryEngine {
    * This stores instructions for how to construct proofs for all theory lemmas.
    */
   std::shared_ptr<LazyCDProof> d_lazyProof;
+  /** The proof generator */
+  std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
   //--------------------------------- end new proofs
 
   /**
@@ -361,8 +364,19 @@ class TheoryEngine {
                             bool preprocess,
                             theory::TheoryId atomsTo);
 
-  /** Process trust node */
-  void processTrustNode(theory::TrustNode trn);
+  /** 
+   * Process trust node. This method ensures that the proof for the proven node
+   * of trn is stored as a lazy step in the lazy proof (d_lazyProof) maintained
+   * by this class, referencing the proof generator of the trust node. The
+   * argument from specifies the theory responsible for this trust node. If
+   * no generator is provided, then a (eager) THEORY_LEMMA step is added to
+   * the lazy proof.
+   * 
+   * @param trn The trust node to process
+   * @param from The id of the theory responsible for the trust node.
+   */
+  void processTrustNode(theory::TrustNode trn,
+                            theory::TheoryId from);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
new file mode 100644
index 000000000..af737e53b
--- /dev/null
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file theory_engine_proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 The theory engine proof generator
+ **/
+
+#include "theory/theory_engine_proof_generator.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 
+{
+
+TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u) : d_pnm(pnm), d_proofs(u)
+{
+  
+}
+
+theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
+{
+  theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit,exp,this);
+  Node p = trn.getProven();
+  // should not already be proven
+  NodeLazyCDProofMap::iterator it = d_proofs.find(p);
+  if (it!=d_proofs.end())
+  {
+    Assert(false);
+  }
+  else
+  {
+    // we will prove this
+    d_proofs.insert(p, lpf);
+  }
+  return trn;
+}
+
+std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f)
+{
+  Assert (f.getKind()==IMPLIES && f.getNumChildren()==2);
+  NodeLazyCDProofMap::iterator it = d_proofs.find(f);
+  if (it==d_proofs.end())
+  {
+    return nullptr;
+  }
+  std::shared_ptr<LazyCDProof> lcp = (*it).second;
+  // finalize it via scope
+  std::vector<Node> scopeAssumps;
+  if (f[0].getKind()==AND)
+  {
+    for (const Node& fc : f[0])
+    {
+      scopeAssumps.push_back(fc);
+    }
+  }
+  else
+  {
+    scopeAssumps.push_back(f[1]);
+  }
+  Node conclusion = f[1];
+
+  // get the proof for conclusion
+  std::shared_ptr<ProofNode> pfb = lcp->mkProof(conclusion);
+  // call the scope method of proof node manager
+  std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps);
+  return pf;
+}
+
+std::string TheoryEngineProofGenerator::identify() const
+{
+  return "TheoryEngineProofGenerator";
+}
+
+}
diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h
new file mode 100644
index 000000000..0dd6e0dd8
--- /dev/null
+++ b/src/theory/theory_engine_proof_generator.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file theory_engine.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 The theory engine proof generator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+
+#include <memory>
+
+#include "expr/lazy_proof.h"
+#include "expr/proof_node_manager.h"
+#include "expr/proof_generator.h"
+#include "context/cdhashmap.h"
+#include "context/context.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+
+class TheoryEngineProofGenerator : public ProofGenerator
+{
+  typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
+      NodeLazyCDProofMap;
+ public:
+  TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
+  ~TheoryEngineProofGenerator(){}
+  /** Set proof */
+  theory::TrustNode mkTrustExplain(TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf);
+  /** Get proof for */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+ private:
+  /** The proof manager, used for allocating new ProofNode objects */
+  ProofNodeManager* d_pnm;
+  /** Map from formulas to lazy CD proofs */
+  NodeLazyCDProofMap d_proofs;
+};
+  
+}
+
+#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */