disable substring in default mode

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 8bede6cae5bb41b6f964d36f5cceeb32f9712cfa..6f4355fb6045b356c6261ee7ec9b309cc23e24eb 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -17,4 +17,7 @@ option stringFMF strings-fmf --strings-fmf bool :default false :predicate CVC4::
 option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
  the strategy of LB rule application: 0-lazy, 1-eager, 2-no
 
+option stringExp strings-exp --strings-exp bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+ experimental features in the theory of strings
+
 endmodule

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 9da0e343dbfb5ea24c2dd786e89fac27072f1351..ff01b18879d108725df23ec5103e8746e5a3c7e7 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/strings/theory_strings_preprocess.h"
 #include "expr/kind.h"
+#include "theory/strings/options.h"
+#include "smt/logic_exception.h"
 
 namespace CVC4 {
 namespace theory {
@@ -114,22 +116,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
                //}
        } else if( t.getKind() == kind::STRING_SUBSTR ){
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" );
-               Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" );
-               Node x = simplify( t[0], new_nodes );
-               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
-               new_nodes.push_back( x_eq_123 );
-               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-               new_nodes.push_back( len_sk1_eq_i );
-               Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-               new_nodes.push_back( len_sk2_eq_j );
+               if(options::stringExp()) {
+                       Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" );
+                       Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" );
+                       Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" );
+                       Node x = simplify( t[0], new_nodes );
+                       Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+                       new_nodes.push_back( x_eq_123 );
+                       Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+                       new_nodes.push_back( len_sk1_eq_i );
+                       Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
+                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+                       new_nodes.push_back( len_sk2_eq_j );
 
-               d_cache[t] = sk2;
-               retNode = sk2;
+                       d_cache[t] = sk2;
+                       retNode = sk2;
+               } else {
+                       throw LogicException("substring not supported in this release");
+               }
        } else if( t.getNumChildren()>0 ){
                std::vector< Node > cc;
                if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index cd9db85c796daf65ea1a219a67cd4bc19310b607..0e37367bf1d6c5c89f1af0afa6f736dc216c8cf8 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -14,6 +14,8 @@
  ** Implementation of the theory of strings.
  **/
 #include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/options.h"
+#include "smt/logic_exception.h"
 
 using namespace std;
 using namespace CVC4;
@@ -339,17 +341,21 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
             }
         }
     } else if(node.getKind() == kind::STRING_SUBSTR) {
-               if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
-                       int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
-                       int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
-                       if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
-                               retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+               if(options::stringExp()) {
+                       if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
+                               int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+                               int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+                               if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
+                                       retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+                               } else {
+                                       // TODO: some issues, must be guarded by users
+                                       retNode = NodeManager::currentNM()->mkConst( false );
+                               }
                        } else {
-                               // TODO: some issues, must be guarded by users
-                               retNode = NodeManager::currentNM()->mkConst( false );
+                               //handled by preprocess
                        }
                } else {
-                       //handled by preprocess
+                       throw LogicException("substring not supported in this release");
                }
        } else if(node.getKind() == kind::STRING_IN_REGEXP) {
                retNode = rewriteMembership(node);

diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2
index b5ff587b2a952ff2620e2909c6084871824e0009..2b2ae9820cb45219d17e9801cb9597b352f1d714 100644 (file)
--- a/test/regress/regress0/strings/substr001.smt2
+++ b/test/regress/regress0/strings/substr001.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)\r
+(set-option :strings-exp true)\r
 (set-info :status sat)\r
 \r
 (declare-fun x () String)\r