Merge branch 'stringsPf' into fix-eqproof3

7 files changed, 128 insertions, 112 deletions

diff --git a/src/expr/proof_skolem_cache.h b/src/expr/proof_skolem_cache.h
index aafba741d..e609492a3 100644
--- a/src/expr/proof_skolem_cache.h
+++ b/src/expr/proof_skolem_cache.h
@@ -25,7 +25,7 @@ namespace CVC4 {
 
 /**
  * A manager for skolems that can be used in proofs. This is designed to be
- * trusted interface to NodeManager::mkSkolem, where one
+ * a trusted interface to NodeManager::mkSkolem, where one
  * must provide a definition for the skolem they create in terms of a
  * predicate that the introduced variable is intended to witness.
  *
@@ -103,8 +103,9 @@ class ProofSkolemCache
                              const std::string& comment = "",
                              int flags = NodeManager::SKOLEM_DEFAULT);
   /**
-   * Same as above, but for special case for (witness ((x T)) (= x t))
-   * where T is the type of t. This skolem is unique for each t.
+   * Same as above, but for special case of (witness ((x T)) (= x t))
+   * where T is the type of t. This skolem is unique for each t, which we
+   * implement via an attribute on t.
    */
   static Node mkPurifySkolem(Node t,
                              const std::string& prefix,
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 f9f4a064f..cc73da8f2 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -717,6 +717,7 @@ Node CoreSolver::getConclusion(Node x,
   Trace("strings-csolver") << "CoreSolver::getConclusion: " << x << " " << y
                            << " " << rule << " " << isRev << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  Node conc;
   if (rule == PfRule::CONCAT_SPLIT || rule == PfRule::CONCAT_LPROP)
   {
     Node sk1;
@@ -757,7 +758,6 @@ Node CoreSolver::getConclusion(Node x,
         x.eqNode(isRev ? utils::mkNConcat(sk1, y) : utils::mkNConcat(y, sk1));
     // eq1 = nm->mkNode(AND, eq1, nm->mkNode(GEQ, sk1, d_one));
 
-    Node conc;
     if (rule == PfRule::CONCAT_LPROP)
     {
       conc = eq1;
@@ -769,19 +769,43 @@ Node CoreSolver::getConclusion(Node x,
       // eq2 = nm->mkNode(AND, eq2, nm->mkNode(GEQ, sk2, d_one));
       conc = nm->mkNode(OR, eq1, eq2);
     }
-    /*
     if (options::stringUnifiedVSpt())
     {
       // we can assume its length is greater than zero
       Node emp = Word::mkEmptyWord(sk1.getType());
       conc = nm->mkNode(AND, conc, sk1.eqNode(emp).negate(),
-    nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0))));
+      nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0))));
     }
-    */
-    return conc;
+  }
+  else if (rule==PfRule::CONCAT_CSPLIT)
+  {
+    Assert (y.isConst());
+    size_t yLen = Word::getLength(y);
+    Node firstChar = yLen == 1 ? y
+                                  : (isRev ? Word::suffix(y, 1)
+                                            : Word::prefix(y, 1));
+    Node sk = skc->mkSkolemCached(
+        x,
+        isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
+        "c_spt");
+    newSkolems.push_back(sk);
+    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 Node::null();
+  return conc;
 }
 
 void CoreSolver::getNormalForms(Node eqc,
@@ -1530,25 +1554,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // to start with the first character of the constant.
       //
       // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
-      Node stra = nfcv[index];
-      size_t straLen = Word::getLength(stra);
-      Node firstChar = straLen == 1 ? stra
-                                    : (isRev ? Word::suffix(stra, 1)
-                                             : Word::prefix(stra, 1));
       SkolemCache* skc = d_termReg.getSkolemCache();
-      Node sk = skc->mkSkolemCached(
-          nc,
-          isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
-          "c_spt");
-      Trace("strings-csp") << "Const Split: " << firstChar
-                           << " is removed from " << stra << " (serial) "
-                           << std::endl;
+      std::vector<Node> newSkolems;
+      iinfo.d_conc = getConclusion(nc,nfcv[index],PfRule::CONCAT_CSPLIT,isRev,skc,newSkolems);
       NormalForm::getExplanationForPrefixEq(
           nfi, nfj, index, index, iinfo.d_ant);
       iinfo.d_ant.push_back(expNonEmpty);
-      iinfo.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
-                                     : utils::mkNConcat(firstChar, sk));
-      iinfo.d_new_skolem[LENGTH_SPLIT].push_back(sk);
+      Assert(newSkolems.size()==1);
+      iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]);
       iinfo.d_id = Inference::SSPLIT_CST;
       iinfo.d_idRev = isRev;
       pinfer.push_back(info);
@@ -1637,7 +1650,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       if (options::stringUnifiedVSpt())
       {
         Assert(newSkolems.size() == 1);
-        iinfo.d_new_skolem[LENGTH_GEQ_ONE].push_back(newSkolems[0]);
+        iinfo.d_new_skolem[LENGTH_IGNORE].push_back(newSkolems[0]);
       }
     }
     else if (lentTestSuccess == 0)
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index b7cbf6037..a5a22dfa0 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -198,15 +198,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      // use skolem cache
-      SkolemCache skc(false);
-      std::vector<Node> newSkolems;
-      Node kt0 = ProofSkolemCache::getSkolemForm(t0);
-      Node ks0 = ProofSkolemCache::getSkolemForm(s0);
-      Node conc = CoreSolver::getConclusion(
-          kt0, ks0, PfRule::CONCAT_SPLIT, isRev, &skc, newSkolems);
-      conc = ProofSkolemCache::getWitnessForm(conc);
-      return conc;
     }
     else if (id == PfRule::CONCAT_CSPLIT)
     {
@@ -223,22 +214,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      Node c = isRev ? Word::suffix(s0, 1) : Word::prefix(s0, 1);
-      Node rbody =
-          isRev ? utils::mkPrefix(
-                      t0, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, t0), one))
-                : utils::mkSuffix(t0, one);
-      Node r = ProofSkolemCache::mkPurifySkolem(rbody, "r");
-      Node conc;
-      if (isRev)
-      {
-        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, r, c));
-      }
-      else
-      {
-        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, c, r));
-      }
-      return conc;
     }
     else if (id == PfRule::CONCAT_LPROP)
     {
@@ -251,15 +226,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      // use skolem cache
-      SkolemCache skc(false);
-      std::vector<Node> newSkolems;
-      Node kt0 = ProofSkolemCache::getSkolemForm(t0);
-      Node ks0 = ProofSkolemCache::getSkolemForm(s0);
-      Node conc = CoreSolver::getConclusion(
-          kt0, ks0, PfRule::CONCAT_LPROP, isRev, &skc, newSkolems);
-      conc = ProofSkolemCache::getWitnessForm(conc);
-      return conc;
     }
     else if (id == PfRule::CONCAT_CPROP)
     {
@@ -336,6 +302,15 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       }
       return conc;
     }
+    // use skolem cache
+    SkolemCache skc(false);
+    std::vector<Node> newSkolems;
+    Node kt0 = ProofSkolemCache::getSkolemForm(t0);
+    Node ks0 = ProofSkolemCache::getSkolemForm(s0);
+    Node conc = CoreSolver::getConclusion(
+        kt0, ks0, id, isRev, &skc, newSkolems);
+    conc = ProofSkolemCache::getWitnessForm(conc);
+    return conc;
   }
   else if (id == PfRule::CTN_NOT_EQUAL)
   {
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 */