Shared term database is proof producing. Simplifications to TheoryEngine in preparation for proofs, (commented out) assertions.

5 files changed, 92 insertions, 53 deletions

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index a13ac207a..6d87530cb 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -23,8 +23,11 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
+// below, proofs are enabled in d_pfee if we are provided a lazy proof
 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
-                                         context::Context* context)
+                                         context::Context* context,
+                                         context::UserContext* userContext,
+                ProofNodeManager* pnm, LazyCDProof* lcp)
     : ContextNotifyObj(context),
       d_statSharedTerms("theory::shared_terms", 0),
       d_addedSharedTermsSize(context, 0),
@@ -33,9 +36,11 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
       d_registeredEqualities(context),
       d_EENotify(*this),
       d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true),
+      d_pfee(context,userContext,d_equalityEngine,pnm, lcp!=nullptr),
       d_theoryEngine(theoryEngine),
       d_inConflict(context, false),
-      d_conflictPolarity() {
+      d_conflictPolarity(),
+      d_lazyPf(lcp) {
   smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
 }
 
@@ -198,7 +203,8 @@ void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode re
 {
   Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
   // Add it to the equality engine
-  d_equalityEngine.assertEquality(equality, polarity, reason);
+  //d_equalityEngine.assertEquality(equality, polarity, reason);
+  d_pfee.assertAssume(reason);
   // Check for conflict
   checkForConflict();
 }
@@ -237,10 +243,19 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 void SharedTermsDatabase::checkForConflict() {
   if (d_inConflict) {
     d_inConflict = false;
-    std::vector<TNode> assumptions;
-    d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
-    Node conflict = mkAnd(assumptions);
-    d_theoryEngine->conflict(conflict, THEORY_BUILTIN);
+    Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
+    if (!d_conflictPolarity)
+    {
+      conflict = conflict.notNode();
+    }
+    TrustNode trnc = d_pfee.assertConflict(conflict);
+    if (d_lazyPf!=nullptr)
+    {
+      // add the step to the proof
+      Node ckey = TrustNode::getConflictKeyValue(trnc.getNode());
+      d_lazyPf->addLazyStep(ckey, &d_pfee);
+    }
+    d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN);
     d_conflictLHS = d_conflictRHS = Node::null();
   }
 }
@@ -255,13 +270,9 @@ bool SharedTermsDatabase::isKnown(TNode literal) const {
   }
 }
 
-Node SharedTermsDatabase::explain(TNode literal) const {
-  bool polarity = literal.getKind() != kind::NOT;
-  TNode atom = polarity ? literal : literal[0];
-  Assert(atom.getKind() == kind::EQUAL);
-  std::vector<TNode> assumptions;
-  d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
-  return mkAnd(assumptions);
+theory::TrustNode SharedTermsDatabase::explain(TNode literal) {
+  TrustNode trn = d_pfee.explain(literal);
+  return trn;
 }
 
 } /* namespace CVC4 */
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 0c73195c5..ccee94c8d 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -23,7 +23,11 @@
 #include "expr/node.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
+#include "theory/trust_node.h"
+#include "expr/proof_node_manager.h"
 #include "util/statistics_registry.h"
+#include "expr/lazy_proof.h"
 
 namespace CVC4 {
 
@@ -114,6 +118,9 @@ private:
 
   /** Equality engine */
   theory::eq::EqualityEngine d_equalityEngine;
+  
+  /** Proof equality engine */
+  theory::eq::ProofEqEngine d_pfee;
 
   /**
    * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
@@ -157,7 +164,9 @@ private:
 
 public:
 
-  SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
+  SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context,
+                                         context::UserContext* userContext,
+                ProofNodeManager* pnm, LazyCDProof* lcp);
   ~SharedTermsDatabase();
 
   /**
@@ -173,7 +182,7 @@ public:
   /**
    * Returns an explanation of the propagation that came from the database.
    */
-  Node explain(TNode literal) const;
+  theory::TrustNode explain(TNode literal);
 
   /**
    * Add an equality to propagate.
@@ -249,6 +258,8 @@ public:
 
 protected:
 
+  /** Pointer to the lazy proof of TheoryEngine */
+  LazyCDProof* d_lazyPf;
   /**
    * This method gets called on backtracks from the context manager.
    */
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index a97ca0edf..cc73da8f2 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -792,6 +792,18 @@ Node CoreSolver::getConclusion(Node x,
     conc = x.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
                           : utils::mkNConcat(firstChar, sk));
   }
+  else if (rule==PfRule::CONCAT_CPROP)
+  {
+    // expect (str.++ z c1) and c2
+    Assert (x.getKind()==STRING_CONCAT && x.getNumChildren()==2);
+    Node z = x[isRev ? 1 : 0];
+    Node c1 = x[isRev ? 0 : 1];
+    Assert (c1.isConst());
+    Node c2 = y;
+    Assert (c2.isConst());
+    
+    
+  }
 
   return conc;
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b5c64bf3b..b2793fac9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -195,7 +195,10 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_context(context),
       d_userContext(userContext),
       d_logicInfo(logicInfo),
-      d_sharedTerms(this, context),
+      d_pchecker(new ProofChecker),
+      d_pNodeManager(new ProofNodeManager(d_pchecker.get())),
+      d_lazyProof(options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr),
+      d_sharedTerms(this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()),
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
@@ -243,18 +246,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
 
 #ifdef CVC4_PROOF
   ProofManager::currentPM()->initTheoryProofEngine();
-
-  // new proofs
-  d_pchecker.reset(new ProofChecker);
-  d_pNodeManager.reset(new ProofNodeManager(d_pchecker.get()));
-  // TODO: d_lazyProof could be owned by the owner of TheoryEngine
-  // The lazy proof is user-context-dependent
-  if (options::proofNew())
-  {
-    // no default generator
-    d_lazyProof.reset(
-        new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext));
-  }
 #endif
 
   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
@@ -1754,7 +1745,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
   // spendResource();
-
+  
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
@@ -1772,6 +1763,16 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                      << CheckSatCommand(n.toExpr());
   }
 
+  // if proofNew is enabled, then d_lazyProof contains a proof of n.
+  /*
+  Node lemma = node;
+  if (negated)
+  {
+    lemma = lemma.negate();
+  }
+  Assert (!options::proofNew() || d_lazyProof->hasStep(lemma));
+  */
+  
   AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
@@ -1784,7 +1785,6 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   d_tform_remover.run(additionalLemmas.ref(),
                       additionalLemmas.getIteSkolemMap());
   Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
-  additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0]));
 
   if(Debug.isOn("lemma-ites")) {
     Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
@@ -1799,10 +1799,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
-  for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
-    additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i]));
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
+  for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++ i) {
+    Node rewritten = Rewriter::rewrite(additionalLemmas[i]);
+    additionalLemmas.replace(i, rewritten);
+    d_propEngine->assertLemma(additionalLemmas[i], i==0 && negated, removable, rule, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1827,6 +1827,9 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
 
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
+  // if proofNew is enabled, then d_lazyProof contains a proof of conflict.negate()
+  //Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()));
+  
   Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
 
   Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
@@ -2048,21 +2051,21 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     }
 
     // It was produced by the theory, so ask for an explanation
-    Node explanation;
+    TrustNode texplanation;
     if (toExplain.d_theory == THEORY_BUILTIN)
     {
-      explanation = d_sharedTerms.explain(toExplain.d_node);
-      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
+      texplanation = d_sharedTerms.explain(toExplain.d_node);
+      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << texplanation.getNode() << std::endl;
     }
     else
     {
-      TrustNode texplanation =
+      texplanation =
           theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
-      explanation = texplanation.getNode();
       Debug("theory::explain") << "\tTerm was propagated by owner theory: "
                                << theoryOf(toExplain.d_theory)->getId()
-                               << ". Explanation: " << explanation << std::endl;
+                               << ". Explanation: " << texplanation.getNode() << std::endl;
     }
+    Node explanation = texplanation.getNode();
 
     Debug("theory::explain")
         << "TheoryEngine::explain(): got explanation " << explanation
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e45e4bfcc..cd3e8e122 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -143,6 +143,20 @@ class TheoryEngine {
    */
   const LogicInfo& d_logicInfo;
 
+  //--------------------------------- new proofs
+  /** For the new proofs module */
+  std::unique_ptr<ProofChecker> d_pchecker;
+
+  /** A proof node manager based on the above checker */
+  std::unique_ptr<ProofNodeManager> d_pNodeManager;
+
+  /** The lazy proof object
+   *
+   * This stores instructions for how to construct proofs for all theory lemmas.
+   */
+  std::shared_ptr<LazyCDProof> d_lazyProof;
+  //--------------------------------- end new proofs
+  
   /**
    * The database of shared terms.
    */
@@ -827,18 +841,6 @@ private:
 
  private:
   IntStat d_arithSubstitutionsAdded;
-
-  /** For the new proofs module */
-  std::unique_ptr<ProofChecker> d_pchecker;
-
-  /** A proof node manager based on the above checker */
-  std::unique_ptr<ProofNodeManager> d_pNodeManager;
-
-  /** The lazy proof object
-   *
-   * This stores instructions for how to construct proofs for all theory lemmas.
-   */
-  std::shared_ptr<LazyCDProof> d_lazyProof;
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */