Reg exp unfold, more eq proof

4 files changed, 75 insertions, 50 deletions

diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 226db01f6..191e0e16c 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -444,11 +444,11 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     SkolemCache sc;
     if (id == PfRule::RE_UNFOLD_POS)
     {
-      conc = RegExpOpr::reduceRegExpPos(atom[0], atom[1], &sc);
+      conc = RegExpOpr::reduceRegExpPos(children[0], &sc);
     }
     else
     {
-      conc = RegExpOpr::reduceRegExpNeg(atom[0], atom[1], &sc);
+      conc = RegExpOpr::reduceRegExpNeg(children[0], &sc);
     }
     return ProofSkolemCache::getWitnessForm(conc);
   }
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index fbd10b7a3..60be02bb2 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -845,51 +845,48 @@ Node RegExpOpr::simplify(Node t, bool polarity)
   Node str = t[0];
   Node re = t[1];
   Node conc;
-  std::pair<Node, Node> p(str, re);
-  std::map<std::pair<Node, Node>, Node>::const_iterator itr;
   if(polarity) {
-    itr = d_simpl_cache.find(p);
-    if (itr != d_simpl_cache.end())
+    conc = reduceRegExpPos(t, d_sc);
+    // we also immediately unfold the last disjunct for re.*
+    if (re.getKind() == REGEXP_STAR)
     {
-      conc = itr->second;
-    }
-    else
-    {
-      conc = reduceRegExpPos(str, re, d_sc);
-      // we also immediately unfold the last disjunct for re.*
-      if (re.getKind() == REGEXP_STAR)
-      {
-        Assert(conc.getKind() == OR && conc.getNumChildren() == 3);
-        std::vector<Node> newChildren;
-        newChildren.push_back(conc[0]);
-        newChildren.push_back(conc[1]);
-        Node starExpUnf = simplify(conc[2], true);
-        newChildren.push_back(starExpUnf);
-        conc = NodeManager::currentNM()->mkNode(OR, newChildren);
-      }
-      d_simpl_cache[p] = conc;
+      Assert(conc.getKind() == OR && conc.getNumChildren() == 3);
+      std::vector<Node> newChildren;
+      newChildren.push_back(conc[0]);
+      newChildren.push_back(conc[1]);
+      Node starExpUnf = simplify(conc[2], true);
+      newChildren.push_back(starExpUnf);
+      conc = NodeManager::currentNM()->mkNode(OR, newChildren);
     }
   }
   else
   {
-    itr = d_simpl_neg_cache.find(p);
-    if (itr != d_simpl_neg_cache.end())
-    {
-      conc = itr->second;
-    }
-    else
-    {
-      conc = reduceRegExpNeg(str, re, d_sc);
-      d_simpl_neg_cache[p] = conc;
-    }
+    Node tnot = t.notNode();
+    conc = reduceRegExpNeg(tnot, d_sc);
   }
   Trace("strings-regexp-simpl")
       << "RegExpOpr::simplify: returns " << conc << std::endl;
   return conc;
 }
 
-Node RegExpOpr::reduceRegExpNeg(Node s, Node r, SkolemCache* sc)
+/**
+ * Associating formulas with their "unfolded form".
+ */
+struct ReUnfoldAttributeId
+{
+};
+typedef expr::Attribute<ReUnfoldAttributeId, Node> ReUnfoldAttribute;
+
+Node RegExpOpr::reduceRegExpNeg(Node mem, SkolemCache* sc)
 {
+  Assert (mem.getKind()==NOT && mem[0].getKind()==STRING_IN_REGEXP);
+  ReUnfoldAttribute rua;
+  if (mem.hasAttribute(rua))
+  {
+    return mem.getAttribute(rua);
+  }
+  Node s = mem[0][0];
+  Node r = mem[0][1];
   NodeManager* nm = NodeManager::currentNM();
   Kind k = r.getKind();
   Node zero = nm->mkConst(Rational(0));
@@ -986,11 +983,24 @@ Node RegExpOpr::reduceRegExpNeg(Node s, Node r, SkolemCache* sc)
     conc = nm->mkNode(FORALL, b1v, conc);
     conc = nm->mkNode(AND, sne, conc);
   }
+  else
+  {
+    Assert(!utils::isRegExpKind(k));
+  }
+  mem.setAttribute(rua,conc);
   return conc;
 }
 
-Node RegExpOpr::reduceRegExpPos(Node s, Node r, SkolemCache* sc)
-{
+Node RegExpOpr::reduceRegExpPos(Node mem, SkolemCache* sc)
+{  
+  Assert ( mem.getKind()==STRING_IN_REGEXP);
+  ReUnfoldAttribute rua;
+  if (mem.hasAttribute(rua))
+  {
+    return mem.getAttribute(rua);
+  }
+  Node s = mem[0];
+  Node r = mem[1];
   NodeManager* nm = NodeManager::currentNM();
   Kind k = r.getKind();
   Node conc;
@@ -1000,7 +1010,6 @@ Node RegExpOpr::reduceRegExpPos(Node s, Node r, SkolemCache* sc)
     std::vector<Node> cc;
     // Look up skolems for each of the components. If sc has optimizations
     // enabled, this will return arguments of str.to_re.
-    Node mem = nm->mkNode(STRING_IN_REGEXP, s, r);
     for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; ++i)
     {
       Node index = nm->mkConst(Rational(i));
@@ -1037,6 +1046,7 @@ Node RegExpOpr::reduceRegExpPos(Node s, Node r, SkolemCache* sc)
   {
     Assert(!utils::isRegExpKind(k));
   }
+  mem.setAttribute(rua,conc);
   return conc;
 }
 
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index e69657a2c..fec87b350 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -73,8 +73,6 @@ class RegExpOpr {
   Node d_sigma;
   Node d_sigma_star;
 
-  std::map<PairNodes, Node> d_simpl_cache;
-  std::map<PairNodes, Node> d_simpl_neg_cache;
   std::map<Node, std::pair<int, Node> > d_delta_cache;
   std::map<PairNodeStr, Node> d_dv_cache;
   std::map<PairNodeStr, std::pair<Node, int> > d_deriv_cache;
@@ -128,13 +126,13 @@ class RegExpOpr {
    */
   Node simplify(Node t, bool polarity);
   /**
-   * Return the unfolded form of (str.in_re s r).
+   * Return the unfolded form of mem of the form (str.in_re s r).
    */
-  static Node reduceRegExpPos(Node s, Node r, SkolemCache* sc);
+  static Node reduceRegExpPos(Node mem, SkolemCache* sc);
   /**
-   * Return the unfolded form of (not (str.in_re s r)).
+   * Return the unfolded form of mem of the form (not (str.in_re s r)).
    */
-  static Node reduceRegExpNeg(Node s, Node r, SkolemCache* sc);
+  static Node reduceRegExpNeg(Node mem, SkolemCache* sc);
   /**
    * This method returns 1 if the empty string is in r, 2 if the empty string
    * is not in r, or 0 if it is unknown whether the empty string is in r.
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index f5004e90e..053aa0e9e 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -116,7 +116,8 @@ bool EqProof::foldTransitivityChildren(Node conclusion,
   unsigned termPos = 2, offending = size;
   for (unsigned i = 0; i < size; ++i)
   {
-    Assert(premises[i].getKind() == kind::EQUAL);
+    Trace("ajr-temp") << "Premise trans : "<< premises[i] << std::endl;
+    AlwaysAssert(premises[i].getKind() == kind::EQUAL);
     for (unsigned j = 0; j < 2; ++j)
     {
       if (premises[i][j].getKind() == kind::CONST_BOOLEAN
@@ -471,7 +472,8 @@ Node EqProof::addToProof(
   // refl
   if (d_id == MERGED_THROUGH_REFLEXIVITY)
   {
-    Assert(d_node.getKind() == kind::EQUAL);
+    Trace("ajr-temp") << "Refl node: " << d_node << std::endl;
+    AlwaysAssert(d_node.getKind() == kind::EQUAL);
     std::vector<Node> children;
     std::vector<Node> args{d_node[0]};
     if (!p->addStep(d_node, PfRule::REFL, children, args))
@@ -496,6 +498,10 @@ Node EqProof::addToProof(
     //
     // (= t1 c1)  (= t2 c2)
     // -------------------- MACRO_SR_PRED_INTRO
+    //  (= (= t1 t2) false)
+        
+    // The additional step is commented out below:
+    // -------------------- FALSE_ELIM
     //  (not (= t1 t2))
     //
     // First process the children proofs
@@ -522,7 +528,8 @@ Node EqProof::addToProof(
       // look in children
       for (unsigned j = 0; j < premises.size(); ++j)
       {
-        Assert(premises[j].getKind() == kind::EQUAL);
+        Trace("ajr-temp") << "Premise : "<< premises[j] << std::endl;
+        AlwaysAssert(premises[j].getKind() == kind::EQUAL);
         if (premises[j][0] == term)
         {
           Assert(premises[j][1].isConst());
@@ -539,14 +546,24 @@ Node EqProof::addToProof(
     Trace("eqproof-conv") << "EqProof::addToProof: adding "
                           << PfRule::MACRO_SR_PRED_INTRO << " step from "
                           << children << "\n";
-    Node conclusion = d_node[0].notNode();
-    if (!p->addStep(conclusion, PfRule::MACRO_SR_PRED_INTRO, children, {conclusion}))
+    if (!p->addStep(d_node, PfRule::MACRO_SR_PRED_INTRO, children, {d_node}))
     {
       Assert(false) << "EqProof::addToProof: couldn't add "
                     << PfRule::MACRO_SR_PRED_INTRO << " rule\n";
     }
-    visited[d_node] = conclusion;
-    return conclusion;
+    /*
+    Node conclusion = d_node[0].notNode();
+    Trace("eqproof-conv") << "EqProof::addToProof: adding "
+                          << PfRule::FALSE_ELIM << " step from " << d_node
+                          << "\n";
+    if (!p->addStep(conclusion, PfRule::FALSE_ELIM, {d_node}, {}))
+    {
+      Assert(false) << "EqProof::addToProof: couldn't add "
+                    << PfRule::FALSE_ELIM << " rule\n";
+    }
+    */
+    visited[d_node] = d_node;
+    return d_node;
   }
   if (d_id == MERGED_THROUGH_TRANS)
   {