move new functions under exp options

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c667aedf07ce7dd1777ea00558c7965571ec903b..aa3ab12c5e0e436d201656ecabe1f55c8c58c0eb 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2110,15 +2110,20 @@ bool TheoryStrings::checkInclusions() {
                                addedLemma = true;
                        } else {
                                if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
-                                       Node x = atom[0];
-                                       Node s = atom[1];
-                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for inclusion" );
-                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for inclusion" );
-                                       Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
-                                       Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) );
-                                       d_str_ctn_rewritten[ assertion ] = true;
-                                       sendLemma( antc, d_false, "negative inclusion" );
-                                       addedLemma = true;
+                                       if(options::stringExp()) {
+                                               Node x = atom[0];
+                                               Node s = atom[1];
+                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for inclusion" );
+                                               Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for inclusion" );
+                                               Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
+                                               Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) );
+                                               d_str_ctn_rewritten[ assertion ] = true;
+                                               sendLemma( antc, d_false, "negative inclusion" );
+                                               addedLemma = true;
+                                       } else {
+                                               Trace("strings-inc") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
+                                               is_unk = true;
+                                       }
                                }
                        }
                }

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ca48d2fef7425862b9a3d1eb74e89c1bf8ede328..3b854630460a6c40ad43943ea7a3051cadcbcd5c 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -117,9 +117,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                //}
        } else if( t.getKind() == kind::STRING_SUBSTR ){
                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 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 );
@@ -138,9 +138,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                }
        } else if( t.getKind() == kind::STRING_CHARAT ){
                if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1sym_$$", t.getType(), "created for charat" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2sym_$$", t.getType(), "created for charat" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3sym_$$", t.getType(), "created for charat" );
+                       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 );
@@ -158,12 +158,49 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        throw LogicException("string char at not supported in this release");
                }
        } else if( t.getKind() == kind::STRING_STRIDOF ){
-               //if(options::stringExp()) {
-               ////    d_cache[t] = t;
-               //      retNode = t;
-               //} else {
+               if(options::stringExp()) {
+                       Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
+                       Node sk2 = NodeManager::currentNM()->mkSkolem( "io2_$$", t[0].getType(), "created for indexof" );
+                       Node sk3 = NodeManager::currentNM()->mkSkolem( "io3_$$", t[0].getType(), "created for indexof" );
+                       Node sk4 = NodeManager::currentNM()->mkSkolem( "io4_$$", t[0].getType(), "created for indexof" );
+                       Node skk = NodeManager::currentNM()->mkSkolem( "iok_$$", t[2].getType(), "created for indexof" );
+                       Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
+                       new_nodes.push_back( eq );
+                       Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+                       Node krange = NodeManager::currentNM()->mkNode( kind::AND,
+                                                       NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone ),
+                                                       NodeManager::currentNM()->mkNode( kind::GT, 
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
+                                                               skk));
+                       new_nodes.push_back( krange );
+
+                       //str.len(s1) < y + str.len(s2)
+                       Node c1 = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )),
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ));
+                       //str.len(t1) = y
+                       Node c2 = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+                       //~contain(t234, s2)
+                       Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
+                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4), t[1] ).negate();
+                       //left
+                       Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, NodeManager::currentNM()->mkNode( kind::AND, c2, c3 ) );
+                       //t3 = s2
+                       Node c4 = t[1].eqNode( sk3 );
+                       //~contain(t2, s2)
+                       Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk2, t[1] ).negate();
+                       //k=str.len(s1, s2)
+                       Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
+                                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2 )));
+                       //right
+                       Node right = NodeManager::currentNM()->mkNode( kind::AND, c2, c4, c5, c6 );
+                       Node cond = skk.eqNode( negone );
+                       Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
+                       new_nodes.push_back( rr );
+                       d_cache[t] = skk;
+                       retNode = skk;
+               } else {
                        throw LogicException("string indexof not supported in this release");
-               //}
+               }
        } else if( t.getKind() == kind::STRING_STRREPL ){
                //if(options::stringExp()) {
                //      d_cache[t] = t;