Document inferences for strings (#1642)

2 files changed, 87 insertions, 27 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d0b3ec181..81b0118c5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -37,6 +37,23 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+std::ostream& operator<<(std::ostream& out, Inference i)
+{
+  switch (i)
+  {
+    case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
+    case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
+    case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
+    case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
+    case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break;
+    case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
+    case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
+    case INFER_FLOOP: out << "F-Loop"; break;
+    default: out << "?"; break;
+  }
+  return out;
+}
+
 Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) {
   if( index==n.getNumChildren() ){
     if( d_data.isNull() ){
@@ -2377,9 +2394,11 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
     Trace("strings-solve") << "Possible inferences (" << pinfer.size() << ") : " << std::endl;
     unsigned min_id = 9;
     unsigned max_index = 0;
-    for( unsigned i=0; i<pinfer.size(); i++ ){
+    for (unsigned i = 0, size = pinfer.size(); i < size; i++)
+    {
       Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev << ") : ";
-      Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].getId() << std::endl;
+      Trace("strings-solve")
+          << pinfer[i].d_conc << " by " << pinfer[i].d_id << std::endl;
       if( use_index==-1 || pinfer[i].d_id<min_id || ( pinfer[i].d_id==min_id && pinfer[i].d_index>max_index ) ){
         min_id = pinfer[i].d_id;
         max_index = pinfer[i].d_index;
@@ -2391,7 +2410,13 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
       Assert( !pinfer[use_index].d_nf_pair[1].isNull() );
       addNormalFormPair( pinfer[use_index].d_nf_pair[0], pinfer[use_index].d_nf_pair[1] );
     }
-    sendInference( pinfer[use_index].d_ant, pinfer[use_index].d_antn, pinfer[use_index].d_conc, pinfer[use_index].getId(), pinfer[use_index].sendAsLemma() );
+    std::stringstream ssi;
+    ssi << pinfer[use_index].d_id;
+    sendInference(pinfer[use_index].d_ant,
+                  pinfer[use_index].d_antn,
+                  pinfer[use_index].d_conc,
+                  ssi.str().c_str(),
+                  pinfer[use_index].sendAsLemma());
     for( std::map< int, std::vector< Node > >::iterator it = pinfer[use_index].d_new_skolem.begin(); it != pinfer[use_index].d_new_skolem.end(); ++it ){
       for( unsigned i=0; i<it->second.size(); i++ ){
         if( it->first==0 ){
@@ -2565,7 +2590,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
             //set info
             info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, length_eq, length_eq.negate() );
             info.d_pending_phase[ length_eq ] = true;
-            info.d_id = 3;
+            info.d_id = INFER_LEN_SPLIT;
             info_valid = true;
           }else{
             Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
@@ -2591,7 +2616,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                   Node eq = other_str.eqNode( d_emptyString );
                   //set info
                   info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
-                  info.d_id = 4;
+                  info.d_id = INFER_LEN_SPLIT_EMP;
                   info_valid = true;
                 }else{
                   if( !isRev ){  //FIXME
@@ -2634,7 +2659,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                         //set info
                         info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );
                         info.d_new_skolem[0].push_back( sk );
-                        info.d_id = 1;
+                        info.d_id = INFER_SSPLIT_CST_PROP;
                         info_valid = true;
                       }
                       /*  FIXME for isRev, speculative
@@ -2666,7 +2691,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                                                                            sk.eqNode( d_emptyString ).negate(),
                                                                            c_firstHalf.eqNode( isRev ? mkConcat( sk, other_str ) : mkConcat( other_str, sk ) ) ) );
                       info.d_new_skolem[0].push_back( sk );
-                      info.d_id = 5;
+                      info.d_id = INFER_SSPLIT_CST_BINARY;
                       info_valid = true;
                     }else{
                       // normal v/c split
@@ -2675,7 +2700,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                       Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl;
                       info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, firstChar ) : mkConcat(firstChar, sk) );
                       info.d_new_skolem[0].push_back( sk );
-                      info.d_id = 6;                    
+                      info.d_id = INFER_SSPLIT_CST;
                       info_valid = true;
                     }
                   }
@@ -2725,7 +2750,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                 if( lentTestSuccess!=-1 ){
                   info.d_antn.push_back( lentTestExp );
                   info.d_conc = lentTestSuccess==0 ? eq1 : eq2;
-                  info.d_id = 2;
+                  info.d_id = INFER_SSPLIT_VAR_PROP;
                   info_valid = true;
                 }else{
                   Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
@@ -2736,7 +2761,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                   }
                   //set info
                   info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                  info.d_id = 7;
+                  info.d_id = INFER_SSPLIT_VAR;
                   info_valid = true;
                 }
               }
@@ -2845,7 +2870,7 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form
       {
         // try to make t equal to empty to avoid loop
         info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
-        info.d_id = 4;
+        info.d_id = INFER_LEN_SPLIT_EMP;
         return true;
       }
       else
@@ -2965,7 +2990,7 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form
   if (options::stringProcessLoop())
   {
     info.d_conc = conc;
-    info.d_id = 8;
+    info.d_id = INFER_FLOOP;
     info.d_nf_pair[0] = normal_form_src[i];
     info.d_nf_pair[1] = normal_form_src[j];
     return true;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5dbbb93d6..2dcb3ebc8 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -44,6 +44,55 @@ namespace strings {
  *
  */
 
+/** Types of inferences used in the procedure
+ *
+ * These are variants of the inference rules in Figures 3-5 of Liang et al.
+ * "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
+ */
+enum Inference
+{
+  INFER_NONE,
+  // string split constant propagation, for example:
+  //     x = y, x = "abc", y = y1 ++ "b" ++ y2
+  //       implies y1 = "a" ++ y1'
+  INFER_SSPLIT_CST_PROP,
+  // string split variable propagation, for example:
+  //     x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
+  //       implies x1 = y1 ++ x1'
+  // This is inspired by Zheng et al CAV 2015.
+  INFER_SSPLIT_VAR_PROP,
+  // length split, for example:
+  //     len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
+  // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
+  INFER_LEN_SPLIT,
+  // length split empty, for example:
+  //     z = "" V z != ""
+  // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
+  INFER_LEN_SPLIT_EMP,
+  // string split constant binary, for example:
+  //     x1 = "aaaa" ++ x1' V "aaaa" = x1 ++ x1'
+  // This is inferred when, e.g. x = y, x = x1 ++ x2, y = "aaaaaaaa" ++ y2.
+  // This inference is disabled by default and is enabled by stringBinaryCsp().
+  INFER_SSPLIT_CST_BINARY,
+  // string split constant
+  //    x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
+  //      implies y1 = "c" ++ y1'
+  // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
+  INFER_SSPLIT_CST,
+  // string split variable, for example:
+  //    x = y, x = x1 ++ x2, y = y1 ++ y2
+  //      implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
+  // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
+  INFER_SSPLIT_VAR,
+  // flat form loop, for example:
+  //    x = y, x = x1 ++ z, y = z ++ y2
+  //      implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
+  //        for fresh u, u1, u2.
+  // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
+  INFER_FLOOP,
+};
+std::ostream& operator<<(std::ostream& out, Inference i);
+
 struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
@@ -300,23 +349,9 @@ private:
     std::vector< Node > d_antn;
     std::map< int, std::vector< Node > > d_new_skolem;
     Node d_conc;
-    unsigned d_id;
+    Inference d_id;
     std::map< Node, bool > d_pending_phase;
     unsigned d_index;
-    const char * getId() { 
-      switch( d_id ){
-      case 1:return "S-Split(CST-P)-prop";break;
-      case 2:return "S-Split(VAR)-prop";break;
-      case 3:return "Len-Split(Len)";break;
-      case 4:return "Len-Split(Emp)";break;
-      case 5:return "S-Split(CST-P)-binary";break;
-      case 6:return "S-Split(CST-P)";break;
-      case 7:return "S-Split(VAR)";break;
-      case 8:return "F-Loop";break;
-      default:break;
-      }
-      return "";
-    }
     Node d_nf_pair[2];
     bool sendAsLemma();
   };