From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 8 Jan 2014 18:07:56 +0000 (-0600)
Subject: clean some code
X-Git-Tag: cvc5-1.0.0~7162
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9e376ab6c826c951a0c9e1bf3d07a902249b34fd;p=cvc5.git

clean some code
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index deb58d7d4..5f26b2f6a 100644
--- 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 08ebe7f10..4d1643fbd 100644
--- 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" );