adds partial functions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 409c9b4dd491c21fc5818f60ae379bca85be2c9c..09de0d378d7a15d9e6a37fc7540582e1e0294895 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -277,9 +277,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_CONCAT: out << "str.++ "; break;
   case kind::STRING_IN_REGEXP: out << "str.in.re "; break;
   case kind::STRING_LENGTH: out << "str.len "; break;
-  case kind::STRING_SUBSTR: out << "str.substr "; break;
+  case kind::STRING_SUBSTR:
+  case kind::STRING_SUBSTR_TOTAL:
+         out << "str.substr "; break;
+  case kind::STRING_CHARAT:
+  case kind::STRING_CHARAT_TOTAL:
+         out << "str.at "; break;
   case kind::STRING_STRCTN: out << "str.contain "; break;
-  case kind::STRING_CHARAT: out << "str.at "; break;
   case kind::STRING_STRIDOF: out << "str.indexof "; break;
   case kind::STRING_STRREPL: out << "str.replace "; break;
   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3c3bbe97124ad0a808cc37a03ba5591996da72e4..761348890fed0e2b84c6b97acbac926a63ce14be 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -305,6 +305,13 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   hash_map<Node, Node, NodeHashFunction> d_abstractValues;
 
+  /**
+   * Function symbol used to implement uninterpreted undefined string
+   * semantics.  Needed to deal with partial charat/substr function.
+   */
+  Node d_charAtUndef;
+  Node d_substrUndef;
+
   /**
    * Function symbol used to implement uninterpreted division-by-zero
    * semantics.  Needed to deal with partial division function ("/").
@@ -433,6 +440,8 @@ public:
     d_fakeContext(),
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
+       d_charAtUndef(),
+       d_substrUndef(),
     d_divByZero(),
     d_intDivByZero(),
     d_modZero(),
@@ -1525,6 +1534,59 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         node = expandBVDivByZero(node);
         break;
 
+         case kind::STRING_CHARAT: {
+               if(d_charAtUndef.isNull()) {
+                       std::vector< TypeNode > argTypes;
+                       argTypes.push_back(NodeManager::currentNM()->stringType());
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef", 
+                                                               NodeManager::currentNM()->mkFunctionType(
+                                                                       argTypes,
+                                                                       NodeManager::currentNM()->stringType()),
+                                                               "partial charat undef",
+                                                               NodeManager::SKOLEM_EXACT_NAME);
+                       if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+                               d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+                               d_smt.d_logic.enableTheory(THEORY_UF);
+                               d_smt.d_logic.lock();
+                       }
+           }
+               TNode str = n[0], num = n[1];
+               Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
+               Node cond = nm->mkNode(kind::GT, lenx, num);
+               Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num);
+               Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num);
+               node = nm->mkNode(kind::ITE, cond, total, undef);
+         }
+               break;
+         case kind::STRING_SUBSTR: {
+               if(d_substrUndef.isNull()) {
+                       std::vector< TypeNode > argTypes;
+                       argTypes.push_back(NodeManager::currentNM()->stringType());
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       d_substrUndef = NodeManager::currentNM()->mkSkolem("substr_undef", 
+                                                               NodeManager::currentNM()->mkFunctionType(
+                                                                       argTypes,
+                                                                       NodeManager::currentNM()->stringType()),
+                                                               "partial substring undef",
+                                                               NodeManager::SKOLEM_EXACT_NAME);
+                       if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+                               d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+                               d_smt.d_logic.enableTheory(THEORY_UF);
+                               d_smt.d_logic.lock();
+                       }
+           }
+               TNode str = n[0];
+               Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
+               Node num = nm->mkNode(kind::PLUS, n[1], n[2]);
+               Node cond = nm->mkNode(kind::GEQ, lenx, num);
+               Node total = nm->mkNode(kind::STRING_SUBSTR_TOTAL, str, n[1], n[2]);
+               Node undef = nm->mkNode(kind::APPLY_UF, d_substrUndef, str, n[1], n[2]);
+               node = nm->mkNode(kind::ITE, cond, total, undef);
+         }
+               break;
+
       case kind::DIVISION: {
         // partial function: division
         if(d_divByZero.isNull()) {

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 9e0897c00eea8956be960c9ca37ff665d590d5e7..b30bf8f36d699aed6e887d250e526edf2ca3fd35 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -13,9 +13,11 @@ typechecker "theory/strings/theory_strings_type_rules.h"
 operator STRING_CONCAT 2: "string concat"
 operator STRING_IN_REGEXP 2 "membership"
 operator STRING_LENGTH 1 "string length"
-operator STRING_SUBSTR 3 "string substr"
+operator STRING_SUBSTR 3 "string substr (user symbol)"
+operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
+operator STRING_CHARAT 2 "string charat (user symbol)"
+operator STRING_CHARAT_TOTAL 2 "string charat (internal symbol)"
 operator STRING_STRCTN 2 "string contains"
-operator STRING_CHARAT 2 "string charat"
 operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
 
@@ -105,8 +107,10 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
+typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
+typerule STRING_CHARAT_TOTAL ::CVC4::theory::strings::StringCharAtTypeRule
+typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
 

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 543238d310a9e977bff5661ce23009f55187c674..11e206eebaf1a5b2b998b1bac7313b347e267d94 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -23,6 +23,9 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+StringsPreprocess::StringsPreprocess() {
+}
+
 void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
        int k = r.getKind();
        switch( k ) {
@@ -115,48 +118,47 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        // TODO
                //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
                //}
-       } else if( t.getKind() == kind::STRING_SUBSTR ){
-               if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", 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 );
+       } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ){
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" );
+               Node x = simplify( t[0], new_nodes );
+               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
+                                                       NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
+               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
 
-                       d_cache[t] = sk2;
-                       retNode = sk2;
-               } else {
-                       throw LogicException("substring not supported in this release");
-               }
-       } else if( t.getKind() == kind::STRING_CHARAT ){
-               if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" );
-                       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_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
-                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-                       new_nodes.push_back( len_sk2_eq_1 );
+               Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_j );
+               tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
+               new_nodes.push_back( tp );
 
-                       d_cache[t] = sk2;
-                       retNode = sk2;
-               } else {
-                       throw LogicException("string char at not supported in this release");
-               }
+               d_cache[t] = sk2;
+               retNode = sk2;
+       } else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" );
+               Node x = simplify( t[0], new_nodes );
+               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] );
+               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+
+               Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 );
+               tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
+               new_nodes.push_back( tp );
+
+               d_cache[t] = sk2;
+               retNode = sk2;
        } else if( t.getKind() == kind::STRING_STRIDOF ){
                if(options::stringExp()) {
                        Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
@@ -224,7 +226,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                } else {
                        throw LogicException("string replace not supported in this release");
                }
-       } else if( t.getNumChildren()>0 ){
+       } else if(t.getKind() == kind::STRING_CHARAT || t.getKind() == kind::STRING_SUBSTR) {
+               InternalError("CharAt and Substr should not be reached here.");
+       } else if( t.getNumChildren()>0 ) {
                std::vector< Node > cc;
                if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
                        cc.push_back(t.getOperator());

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 698ef6ba158ce72c0c8668a5fc250ea5b476da35..6d278cc7a606830f760603054f194ba9415682d5 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -36,6 +36,7 @@ private:
        Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
     void simplify(std::vector< Node > &vec_node);
+       StringsPreprocess();
 };
 
 }/* CVC4::theory::strings namespace */

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index d217548208cd56124d25fa2e30422abeffce111f..9f278aac2c276cab5db6d97fae2f1a199db0bd5a 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -340,15 +340,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
             }
         }
-    } else if(node.getKind() == kind::STRING_SUBSTR) {
+    } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
                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 if(node.getKind() == kind::STRING_STRCTN) {
@@ -363,14 +360,11 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
-       } else if(node.getKind() == kind::STRING_CHARAT) {
+       } else if(node.getKind() == kind::STRING_CHARAT_TOTAL) {
                if( node[0].isConst() && node[1].isConst() ) {
                        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
                        if( node[0].getConst<String>().size() > (unsigned) i ) {
                                retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, 1) );
-                       } else {
-                               // TODO: some issues, must be guarded by users
-                               retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
        } else if(node.getKind() == kind::STRING_STRIDOF) {

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index a5c6ae2f4e583fe7d2d4a007c6b1c6547d63e294..a2142eeb38e253331c47118b8c0e3cdce4f635ae 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -19,6 +19,7 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =        \
+  at001.smt2 \
   cardinality.smt2 \
   str001.smt2 \
   str002.smt2 \

diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2
new file mode 100644 (file)
index 0000000..8559574
--- /dev/null
+++ b/test/regress/regress0/strings/at001.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun i () Int)\r
+\r
+(assert (= (str.at x i) "b"))\r
+(assert (> i 5))\r
+(assert (< (str.len x) 4))\r
+(assert (> (str.len x) 2))\r
+\r
+(check-sat)\r

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