roll back to uf implementation for substr and charat

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3209a92ec86ae32175ed4497e89bcb26ec767024..2b1bb2b6340547e8b3b8603c3785f364cc1b6194 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -62,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
-
+       
        d_all_warning = true;
        d_regexp_incomplete = false;
        d_opt_regexp_gcd = true;
@@ -1709,6 +1709,21 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
 
 bool TheoryStrings::checkSimple() {
   bool addedLemma = false;
+
+  //Initialize UF
+  if(d_undefSubstr.isNull()) {
+       std::vector< TypeNode > argTypes;
+       argTypes.push_back(NodeManager::currentNM()->stringType());
+       argTypes.push_back(NodeManager::currentNM()->integerType());
+       argTypes.push_back(NodeManager::currentNM()->integerType());
+       d_undefSubstr = NodeManager::currentNM()->mkSkolem("__undefSS", 
+                                               NodeManager::currentNM()->mkFunctionType(
+                                                       argTypes, NodeManager::currentNM()->stringType()),
+                                               "undefined substr",
+                                               NodeManager::SKOLEM_EXACT_NAME);
+  }
+
+
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ) {
        Node eqc = (*eqcs_i);
@@ -1760,7 +1775,8 @@ bool TheoryStrings::checkSimple() {
                                                                Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
                                                                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
                                                                Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
+                                                               Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], d_one));
+                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf) );
                                                                Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
                                                                d_out->lemma(lemma);
                                                        } else if( n.getKind() == kind::STRING_SUBSTR ) {
@@ -1778,7 +1794,8 @@ bool TheoryStrings::checkSimple() {
 
                                                                Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
                                                                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
+                                                               Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], n[2]));
+                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf ) );
                                                                Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
                                                                d_out->lemma(lemma);
                                                        }

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index d15a76aad21ace4582f04b09f99d087035d5e4e9..81748d6076db77e1454789f576cc5fbbd66dd4b2 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -115,6 +115,7 @@ private:
     Node d_false;
     Node d_zero;
        Node d_one;
+       Node d_undefSubstr;
        // Options
        bool d_all_warning;
        bool d_opt_fmf;

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7bf016d2916cb72c1fd16d9736e524ab8f5966b3..1dc9cbe851472fbb20b8b6e07c689f41115c8b7b 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -353,7 +353,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
             }
         }
     } else if(node.getKind() == kind::STRING_SUBSTR) {
-               if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
+               Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+               if(node[2] == zero) {
+                       retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+               } else 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) ) {