1 files changed, 40 insertions, 26 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d1b18df13..942c8d216 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -38,8 +38,9 @@ TheoryStrings::TheoryStrings(context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
                              Valuation valuation,
-                             const LogicInfo& logicInfo)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+                             const LogicInfo& logicInfo,
+                             ProofNodeManager* pnm)
+    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
       d_notify(*this),
       d_statistics(),
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
@@ -189,18 +190,20 @@ bool TheoryStrings::propagate(TNode literal) {
   return ok;
 }
 
-
-Node TheoryStrings::explain( TNode literal ){
+TrustNode TheoryStrings::explain(TNode literal)
+{
   Debug("strings-explain") << "explain called on " << literal << std::endl;
   std::vector< TNode > assumptions;
   d_im->explain(literal, assumptions);
+  Node ret;
   if( assumptions.empty() ){
-    return d_true;
+    ret = d_true;
   }else if( assumptions.size()==1 ){
-    return assumptions[0];
+    ret = assumptions[0];
   }else{
-    return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
+    ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
   }
+  return TrustNode::mkTrustPropExp(literal, ret, nullptr);
 }
 
 bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars, 
@@ -577,7 +580,7 @@ void TheoryStrings::preRegisterTerm(TNode n)
   d_termReg.preRegisterTerm(n);
 }
 
-Node TheoryStrings::expandDefinition(Node node)
+TrustNode TheoryStrings::expandDefinition(Node node)
 {
   Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
 
@@ -593,14 +596,15 @@ Node TheoryStrings::expandDefinition(Node node)
     Node k = nm->mkBoundVar(nm->stringType());
     Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
     Node emp = Word::mkEmptyWord(node.getType());
-    node = nm->mkNode(
+    Node ret = nm->mkNode(
         WITNESS,
         bvl,
         nm->mkNode(
             ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
+    return TrustNode::mkTrustRewrite(node, ret, nullptr);
   }
 
-  return node;
+  return TrustNode::null();
 }
 
 void TheoryStrings::check(Effort e) {
@@ -712,11 +716,12 @@ void TheoryStrings::conflict(TNode a, TNode b){
   {
     Debug("strings-conflict") << "Making conflict..." << std::endl;
     d_state.setConflict();
-    Node conflictNode;
-    conflictNode = explain( a.eqNode(b) );
-    Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
+    TrustNode conflictNode = explain(a.eqNode(b));
+    Trace("strings-conflict")
+        << "CONFLICT: Eq engine conflict : " << conflictNode.getNode()
+        << std::endl;
     ++(d_statistics.d_conflictsEqEngine);
-    d_out->conflict( conflictNode );
+    d_out->conflict(conflictNode.getNode());
   }
 }
 
@@ -957,39 +962,48 @@ void TheoryStrings::checkRegisterTermsNormalForms()
   }
 }
 
-Node TheoryStrings::ppRewrite(TNode atom) {
+TrustNode TheoryStrings::ppRewrite(TNode atom)
+{
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
-  Node atomElim;
+  Node atomRet = atom;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
   {
     // aggressive elimination of regular expression membership
-    atomElim = d_regexp_elim.eliminate(atom);
+    Node atomElim = d_regexp_elim.eliminate(atomRet);
     if (!atomElim.isNull())
     {
       Trace("strings-ppr") << "  rewrote " << atom << " -> " << atomElim
                            << " via regular expression elimination."
                            << std::endl;
-      atom = atomElim;
+      atomRet = atomElim;
     }
   }
   if( !options::stringLazyPreproc() ){
     //eager preprocess here
     std::vector< Node > new_nodes;
     StringsPreprocess* p = d_esolver->getPreprocess();
-    Node ret = p->processAssertion(atom, new_nodes);
-    if( ret!=atom ){
-      Trace("strings-ppr") << "  rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; 
-      for( unsigned i=0; i<new_nodes.size(); i++ ){
-        Trace("strings-ppr") << "    lemma : " << new_nodes[i] << std::endl;
+    Node ret = p->processAssertion(atomRet, new_nodes);
+    if (ret != atomRet)
+    {
+      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << ret
+                           << ", with " << new_nodes.size() << " lemmas."
+                           << std::endl;
+      for (const Node& lem : new_nodes)
+      {
+        Trace("strings-ppr") << "    lemma : " << lem << std::endl;
         ++(d_statistics.d_lemmasEagerPreproc);
-        d_out->lemma( new_nodes[i] );
+        d_out->lemma(lem);
       }
-      return ret;
+      atomRet = ret;
     }else{
       Assert(new_nodes.empty());
     }
   }
-  return atom;
+  if (atomRet != atom)
+  {
+    return TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
+  }
+  return TrustNode::null();
 }
 
 /** run the given inference step */