Minor fixes to strings, add regressions.

diff --git a/src/theory/strings/options b/src/theory/strings/options
index eb49e686d68815415ca473334f472624374fe42d..858a9e21cc143f92ad0a18315f4c47860412ab30 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -42,5 +42,7 @@ option stringLenNorm strings-len-norm --strings-len-norm bool :default true
  strings length normalization lemma
 option stringSplitEmp strings-sp-emp --strings-sp-emp bool :default true
  strings split on empty string
+option stringInferSym strings-infer-sym --strings-infer-sym bool :default true
+ strings split on empty string
 
 endmodule

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d5b738fac0a5c44586ae58ba587759954c79d8d3..4a1001a0477e160232d8ef71a11f52ec0d18fb1e 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -616,10 +616,8 @@ void TheoryStrings::check(Effort e) {
       addedLemma = checkNormalForms();
       Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
       if(!d_conflict && !addedLemma) {
-        if( options::stringLenNorm() ){
-          addedLemma = checkLengthsEqc();
-          Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-        }
+        addedLemma = checkLengthsEqc();
+        Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
         if(!d_conflict && !addedLemma) {
           addedLemma = checkExtendedFuncs();
           Trace("strings-process") << "Done check extended functions, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
@@ -1208,11 +1206,11 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
   }
   return true;
 }
-Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c ){
-  std::map< Node, Node >::iterator it = d_skolem_cache[a].find( b );
-  if( it==d_skolem_cache[a].end() ){
-    Node sk = mkSkolemS( c );
-    d_skolem_cache[a][b] = sk;
+Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit ){
+  std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( isLenSplit );
+  if( it==d_skolem_cache[a][b].end() ){
+    Node sk = mkSkolemS( c, isLenSplit );
+    d_skolem_cache[a][b][isLenSplit] = sk;
     return sk;
   }else{
     return it->second;
@@ -1377,7 +1375,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                   }
 
                   //Node sk = mkSkolemS( "v_spt", 1 );
-                  Node sk = mkSkolemSplit( normal_forms[i][index_i], normal_forms[j][index_j], "v_spt" );
+                  Node sk = mkSkolemSplit( normal_forms[i][index_i], normal_forms[j][index_j], "v_spt", 1 );
                   Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
                   Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
                   conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ));
@@ -1949,17 +1947,18 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
     sendLemma( eq_exp, eq, c );
   } else {
     Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
-
-    std::vector< Node > vars;
-    std::vector< Node > subs;
-    std::vector< Node > unproc;
-    std::vector< Node > exps;
-    inferSubstitutionProxyVars( eq_exp, vars, subs, unproc, exps );
-    if( unproc.empty() ){
-      Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-      Trace("strings-lemma") << "Strings::Infer Alternate : " << eqs << std::endl;
-      sendLemma( mkAnd( exps ), eqs, c );
-      return;
+    if( options::stringInferSym() ){
+      std::vector< Node > vars;
+      std::vector< Node > subs;
+      std::vector< Node > unproc;
+      std::vector< Node > exps;
+      inferSubstitutionProxyVars( eq_exp, vars, subs, unproc, exps );
+      if( unproc.empty() ){
+        Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        Trace("strings-lemma") << "Strings::Infer Alternate : " << eqs << std::endl;
+        sendLemma( mkAnd( exps ), eqs, c );
+        return;
+      }
     }
     Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
     d_pending.push_back( eq );
@@ -2332,36 +2331,38 @@ void TheoryStrings::checkDeqNF() {
 
 bool TheoryStrings::checkLengthsEqc() {
   bool addedLemma = false;
-  std::vector< Node > nodes;
-  getEquivalenceClasses( nodes );
-  for( unsigned i=0; i<nodes.size(); i++ ){
-    if( d_normal_forms[nodes[i]].size()>1 ) {
-      Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl;
-      //check if there is a length term for this equivalence class
-      EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false );
-      Node lt = ei ? ei->d_length_term : Node::null();
-      if( !lt.isNull() ) {
-        Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
-        //now, check if length normalization has occurred
-        if( ei->d_normalized_length.get().isNull() ) {
-          //if not, add the lemma
-          std::vector< Node > ant;
-          ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
-          ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
-          Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
-          lc = Rewriter::rewrite( lc );
-          Node eq = llt.eqNode( lc );
-          ei->d_normalized_length.set( eq );
-          sendLemma( mkExplain( ant ), eq, "LEN-NORM" );
-          addedLemma = true;
+  if( options::stringLenNorm() ){
+    std::vector< Node > nodes;
+    getEquivalenceClasses( nodes );
+    for( unsigned i=0; i<nodes.size(); i++ ){
+      if( d_normal_forms[nodes[i]].size()>1 ) {
+        Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl;
+        //check if there is a length term for this equivalence class
+        EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false );
+        Node lt = ei ? ei->d_length_term : Node::null();
+        if( !lt.isNull() ) {
+          Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
+          //now, check if length normalization has occurred
+          if( ei->d_normalized_length.get().isNull() ) {
+            //if not, add the lemma
+            std::vector< Node > ant;
+            ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
+            ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
+            Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
+            lc = Rewriter::rewrite( lc );
+            Node eq = llt.eqNode( lc );
+            ei->d_normalized_length.set( eq );
+            sendLemma( mkExplain( ant ), eq, "LEN-NORM" );
+            addedLemma = true;
+          }
         }
+      } else {
+        Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
       }
-    } else {
-      Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
     }
-  }
-  if( addedLemma ){
-    doPendingLemmas();
+    if( addedLemma ){
+      doPendingLemmas();
+    }
   }
   return addedLemma;
 }
@@ -3307,6 +3308,8 @@ bool TheoryStrings::checkExtendedFuncsEval() {
             Trace("strings-extf-debug") << "  symbolic definition is trivial..." << std::endl;
             nrs = Node::null();
           }
+        }else{
+          Trace("strings-extf-debug") << "  could not infer symbolic definition." << std::endl;
         }
         Node conc;
         Node expl;
@@ -3320,18 +3323,18 @@ bool TheoryStrings::checkExtendedFuncsEval() {
               conc = nrs.eqNode( nrc );
             }
             exp.clear();
-            expl = mkAnd( exps );
-            //expl = d_true;
+            //expl = mkAnd( exps );
+            expl = d_true;
           }
         }else{
           if( !areEqual( n, nrc ) ){
+            expl = mkExplain( exp );
             if( n.getType().isBoolean() ){
-              exp.push_back( n.negate() );
+              exp.push_back( nrc==d_true ? n.negate() : n );
               conc = d_false;
             }else{
               conc = n.eqNode( nrc );
             }
-            expl = mkExplain( exp );
           }
         }
         if( !conc.isNull() ){
@@ -3343,6 +3346,9 @@ bool TheoryStrings::checkExtendedFuncsEval() {
             sendInfer( expl, conc, "EXTF" );
           }
           if( d_conflict ){
+            Trace("strings-extf") << "  conflict, return." << std::endl;
+            doPendingFacts();
+            doPendingLemmas();
             return true;
           }
         }

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 7ecfaa69b70beba666d880ffefeae8a6c3c704c2..fb52b6413261b5722ba7edb1b4291125f03239dc 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -329,8 +329,8 @@ protected:
 
   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc, std::vector< Node >& exp );
 
-  std::map< Node, std::map< Node, Node > > d_skolem_cache;
-  Node mkSkolemSplit( Node a, Node b, const char * c );
+  std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
+  Node mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit = 0 );
 private:
   Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero );
 

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index e880d3edcfe44f274ff1e62e393c7f7cf5328b77..716d413656a694be965cb00b720edc638b2f3e84 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -56,7 +56,9 @@ TESTS = \
   artemis-0512-nonterm.smt2 \
   indexof-sym-simp.smt2 \
   bug613.smt2 \
-  idof-triv.smt2
+  idof-triv.smt2 \
+  chapman150408.smt2 \
+  pierre150331.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/chapman150408.smt2 b/test/regress/regress0/strings/chapman150408.smt2
new file mode 100644 (file)
index 0000000..546c46e
--- /dev/null
+++ b/test/regress/regress0/strings/chapman150408.smt2
@@ -0,0 +1,10 @@
+(set-logic SLIA)\r
+(set-info :status sat)\r
+(set-option :strings-exp true)\r
+(set-option :rewrite-divk true)\r
+(declare-fun string () String)\r
+(assert (and\r
+     (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)\r
+     0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not\r
+     (not (= (ite (str.contains string "]") 1 0) 0)))))\r
+(check-sat)\r

diff --git a/test/regress/regress0/strings/pierre150331.smt2 b/test/regress/regress0/strings/pierre150331.smt2
new file mode 100644 (file)
index 0000000..88d5ec1
--- /dev/null
+++ b/test/regress/regress0/strings/pierre150331.smt2
@@ -0,0 +1,13 @@
+(set-logic SLIA)\r
+(set-info :status sat)\r
+(set-info :smt-lib-version 2.5)\r
+(set-option :strings-exp true)\r
+(define-fun stringEval ((?s String)) Bool (str.in.re ?s \r
+(re.union \r
+(str.to.re "H")\r
+(re.++ (re.loop (str.to.re "{") 2 2 ) (re.loop (re.union re.nostr (re.range "\1d" "]") (re.range "\ e" "^") ) 2 4 ) ) ) ) )\r
+(declare-fun s0() String)\r
+(declare-fun s1() String)\r
+(declare-fun s2() String)\r
+(assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )\r
+(check-sat)
\ No newline at end of file