clean some code

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index deb58d7d472cc7a2eec7ae7bffc4fe95d7bf711f..5f26b2f6a8013afbc8bdbc1ac09d58ae2e878d81 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2125,25 +2125,22 @@ bool TheoryStrings::checkInclusions() {
                                sendLemma( ant, conc, "inclusion conflict 2" );
                                addedLemma = true;
                        } else {
-                               if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
-                                       Node b1 = NodeManager::currentNM()->mkBoundVar( atom[0].getType() );
-                                       Node b2 = NodeManager::currentNM()->mkBoundVar( atom[0].getType() );
-                                       Node bvar = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, b1, b2 );
-                                       Node lena0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, atom[0] );
-                                       Node lena1 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, atom[1] );
-                                       Node len_eq = Rewriter::rewrite( lena0.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, lena1,
-                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, b1 ),
-                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, b2 ) ) ) );
-                                       Node conc = NodeManager::currentNM()->mkNode( kind::FORALL, bvar,
-                                                                       NodeManager::currentNM()->mkNode( kind::IMPLIES, len_eq,
-                                                                       atom[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, b1, atom[1], b2 ) ).negate() )
-                                                               );
-                                       d_str_ctn_rewritten[ assertion ] = true;
-                                       sendLemma( assertion, conc, "negative inclusion" );
-                                       addedLemma = true;
+                               if( getLogicInfo().isQuantified() ){
+                                       if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
+                                               Node b1 = NodeManager::currentNM()->mkBoundVar( atom[0].getType() );
+                                               Node b2 = NodeManager::currentNM()->mkBoundVar( atom[0].getType() );
+                                               Node bvar = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, b1, b2 );
+                                               Node conc = NodeManager::currentNM()->mkNode( kind::FORALL, bvar,
+                                                                               atom[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, b1, atom[1], b2 ) ).negate()
+                                                                       );
+                                               d_str_ctn_rewritten[ assertion ] = true;
+                                               sendLemma( assertion, conc, "negative inclusion" );
+                                               addedLemma = true;
+                                       }
+                               } else {
+                                       Trace("strings-inc") << "Inclusion is incomplete due to " << assertion << "." << std::endl;
+                                       is_unk = true;
                                }
-                               //Trace("strings-inc") << "Inclusion is incomplete due to " << assertion << "." << std::endl;
-                               //is_unk = true;
                        }
                }
        }

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 08ebe7f1005152fbd032f61eb80bc9d4d0b3bbfe..4d1643fbd6d0291f6ebf86e631f778e89dba07b5 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -136,43 +136,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                } else {
                        throw LogicException("substring not supported in this release");
                }
-       }
-       /* else if( t.getKind() == kind::STRING_STRCTN ){
-               if(options::stringExp()) {
-                       Node w = simplify( t[0], new_nodes );
-                       Node y = simplify( t[1], new_nodes );
-                       Node emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-                       std::vector< Node > or_vec;
-                       or_vec.push_back( w.eqNode(y) );
-                       Node x1 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node b1 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x1 );
-                       Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, b1, NodeManager::currentNM()->mkNode( kind::AND,
-                                                       x1.eqNode( emptyString ).negate(),
-                                                       w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x1, y ) )));
-                       or_vec.push_back( c1 );
-                       Node z2 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node b2 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, z2 );
-                       Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, b2, NodeManager::currentNM()->mkNode( kind::AND,
-                                                       z2.eqNode( emptyString ).negate(),
-                                                       w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, z2 ) )));
-                       or_vec.push_back( c2 );
-                       Node x3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node z3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node b3 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x3, z3 );
-                       Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, b3, NodeManager::currentNM()->mkNode( kind::AND,
-                                                       x3.eqNode( emptyString ).negate(), z3.eqNode( emptyString ).negate(),
-                                                       w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x3, y, z3 ) )));
-                       or_vec.push_back( c3 );
-
-                       Node cc = NodeManager::currentNM()->mkNode( kind::OR, or_vec );
-
-                       d_cache[t] = cc;
-                       retNode = cc;
-               } else {
-                       throw LogicException("string contain not supported in this release");
-               }
-       } */
-       else if( t.getKind() == kind::STRING_CHARAT ){
+       } 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" );