diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 62 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 14 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 512 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 4 | ||||
| -rw-r--r-- | src/theory/theory_model.cpp | 5 | ||||
| -rw-r--r-- | src/theory/uf/options | 2 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
8 files changed, 305 insertions, 301 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ad878e0f3..f4019450d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -506,6 +506,7 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one); Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], d_one); return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); + //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one); break; } @@ -530,6 +531,7 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]); Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]); return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); + //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]); break; } @@ -687,9 +689,9 @@ bool TheoryStrings::doPreprocess( Node atom ) { } plem = Rewriter::rewrite( plem ); Trace("strings-assert") << "(assert " << plem << ")" << std::endl; - Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess" << std::endl; + Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess reduction" << std::endl; d_out->lemma( plem ); - Trace("strings-pp-lemma") << "Preprocess reduce lemma : " << plem << std::endl; + Trace("strings-pp-lemma") << "Preprocess reduction lemma : " << plem << std::endl; Trace("strings-pp-lemma") << "...from " << atom << std::endl; }else{ Trace("strings-assertion-debug") << "...preprocess ok." << std::endl; @@ -700,6 +702,7 @@ bool TheoryStrings::doPreprocess( Node atom ) { Trace("strings-assertion-debug") << "...new nodes : " << nnlem << std::endl; Trace("strings-pp-lemma") << "Preprocess lemma : " << nnlem << std::endl; Trace("strings-pp-lemma") << "...from " << atom << std::endl; + Trace("strings-lemma") << "Strings::Lemma " << nnlem << " by preprocess" << std::endl; Trace("strings-assert") << "(assert " << nnlem << ")" << std::endl; d_out->lemma( nnlem ); } @@ -1291,12 +1294,12 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, } return true; } -Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit ){ +Node TheoryStrings::mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit ){ //return mkSkolemS( c, isLenSplit ); - std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( isLenSplit ); + std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( id ); if( it==d_skolem_cache[a][b].end() ){ Node sk = mkSkolemS( c, isLenSplit ); - d_skolem_cache[a][b][isLenSplit] = sk; + d_skolem_cache[a][b][id] = sk; return sk; }else{ return it->second; @@ -1410,10 +1413,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() ); Node xnz = other_str.eqNode(d_emptyString).negate(); antec.push_back( xnz ); - //Node sk = mkSkolemS( "c_spt" ); Node conc; - if( normal_forms[nconst_k].size() > nconst_index_k + 1 && - normal_forms[nconst_k][nconst_index_k + 1].isConst() ) { + if( normal_forms[nconst_k].size() > nconst_index_k + 1 && normal_forms[nconst_k][nconst_index_k + 1].isConst() ) { CVC4::String stra = const_str.getConst<String>(); CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>(); CVC4::String stra1 = stra.substr(1); @@ -1421,14 +1422,14 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms size_t p2 = stra1.find(strb); p = p2==std::string::npos? p : ( p>p2+1? p2+1 : p ); Node prea = p==stra.size()? const_str : NodeManager::currentNM()->mkConst(stra.substr(0, p)); - Node sk = mkSkolemSplit( other_str, prea, "c_spt" ); + Node sk = mkSkolemCached( other_str, prea, sk_id_c_spt, "c_spt" ); conc = other_str.eqNode( mkConcat(prea, sk) ); Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << std::endl; } else { // normal v/c split Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); - Node sk = mkSkolemSplit( other_str, firstChar, "c_spt" ); + Node sk = mkSkolemCached( other_str, firstChar, sk_id_vc_spt, "c_spt" ); conc = other_str.eqNode( mkConcat(firstChar, sk) ); Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (normal) " << std::endl; } @@ -1460,8 +1461,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms } } - //Node sk = mkSkolemS( "v_spt", 1 ); - Node sk = mkSkolemSplit( normal_forms[i][index_i], normal_forms[j][index_j], "v_spt", 1 ); + Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 ); Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) ); Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) ); conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 )); @@ -1777,18 +1777,16 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { } antec_new_lits.push_back( li.eqNode( lj ).negate() ); std::vector< Node > conc; - Node sk1 = mkSkolemS( "x_dsplit" ); - Node sk2 = mkSkolemS( "y_dsplit" ); - Node sk3 = mkSkolemS( "z_dsplit", 1 ); + Node sk1 = mkSkolemCached( i, j, sk_id_deq_x, "x_dsplit" ); + Node sk2 = mkSkolemCached( i, j, sk_id_deq_y, "y_dsplit" ); + Node sk3 = mkSkolemCached( i, j, sk_id_deq_z, "z_dsplit", 1 ); //Node nemp = sk3.eqNode(d_emptyString).negate(); //conc.push_back(nemp); Node lsk1 = getLength( sk1 ); conc.push_back( lsk1.eqNode( li ) ); Node lsk2 = getLength( sk2 ); conc.push_back( lsk2.eqNode( lj ) ); - conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, - j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); - + conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" ); ++(d_statistics.d_deq_splits); return true; @@ -1954,25 +1952,9 @@ bool TheoryStrings::registerTerm( Node n ) { d_registered_terms_cache.insert(n); Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl; if(n.getType().isString()) { - if(n.getKind() == kind::STRING_SUBSTR_TOTAL) { - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), - NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); - Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero); - Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, n[2], d_zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node sk1 = mkSkolemS( "ss1", 2 ); - Node sk3 = mkSkolemS( "ss3", 2 ); - Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) ); - Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) ); - Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ), - n.eqNode(d_emptyString))); - Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl; - Trace("strings-assert") << "(assert " << lemma << ")" << std::endl; - d_out->lemma(lemma); - } + //register length information: + // for variables, split on empty vs positive length + // for concat/const, introduce proxy var and state length relation if( n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) { if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) { sendLengthLemma( n ); @@ -3947,6 +3929,8 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { return; } } + //}else if( hasTerm( nrc ) && !areEqual( nrc, n ) ){ + // Trace("strings-extf-debug") << "Reduction inference : " << nrc << " " << n << std::endl; TODO? }else{ if( effort==1 ){ Trace("strings-extf") << " cannot rewrite extf : " << nrc << std::endl; @@ -4063,8 +4047,8 @@ void TheoryStrings::checkPosContains( std::vector< Node >& posContains ) { Node s = atom[1]; if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) { if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) { - Node sk1 = mkSkolemS( "sc1" ); - Node sk2 = mkSkolemS( "sc2" ); + Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); + Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); sendLemma( atom, eq, "POS-INC" ); d_pos_ctn_cached.insert( atom ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ce2422faf..7e09a8e5b 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -360,9 +360,19 @@ protected: void printConcat( std::vector< Node >& n, const char * c ); void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ); - + + enum { + sk_id_c_spt, + sk_id_vc_spt, + sk_id_v_spt, + sk_id_ctn_pre, + sk_id_ctn_post, + sk_id_deq_x, + sk_id_deq_y, + sk_id_deq_z, + }; std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache; - Node mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit = 0 ); + Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 ); private: // Special String Functions diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index e9b144a23..4e2b00fb1 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -212,8 +212,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" ); Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) ); Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + Node lenc = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) ); Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ), + NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ), t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) )); new_nodes.push_back( lemma ); d_cache[t] = t; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index fc17198c2..6356277ed 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1084,262 +1084,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } - } else if( node.getKind() == kind::STRING_STRCTN ){ - if( node[0] == node[1] ) { - retNode = NodeManager::currentNM()->mkConst( true ); - } else if( node[0].isConst() && node[1].isConst() ) { - CVC4::String s = node[0].getConst<String>(); - CVC4::String t = node[1].getConst<String>(); - if( s.find(t) != std::string::npos ){ - retNode = NodeManager::currentNM()->mkConst( true ); - }else{ - retNode = NodeManager::currentNM()->mkConst( false ); - } - }else if( node[0].getKind()==kind::STRING_CONCAT ) { - //component-wise containment - unsigned n1 = node[0].getNumChildren(); - std::vector< Node > nc1; - getConcat( node[1], nc1 ); - unsigned n2 = nc1.size(); - if( n1>n2 ){ - bool flag = false; - unsigned diff = n1-n2; - for(unsigned i=0; i<diff; i++) { - if( node[0][i]==nc1[0] ){ - flag = true; - for(unsigned j=1; j<n2; j++) { - if( node[0][i+j]!=nc1[j] ){ - flag = false; - break; - } - } - if(flag) { - break; - } - } - } - if( flag ){ - retNode = NodeManager::currentNM()->mkConst( true ); - } - } - if( retNode==node ){ - if( node[1].isConst() ){ - CVC4::String t = node[1].getConst<String>(); - for(unsigned i=0; i<node[0].getNumChildren(); i++) { - //constant contains - if( node[0][i].isConst() ){ - CVC4::String s = node[0][i].getConst<String>(); - if( s.find(t)!=std::string::npos ) { - retNode = NodeManager::currentNM()->mkConst( true ); - break; - }else{ - //if no overlap, we can split into disjunction - // if first child, only require no left overlap - // if last child, only require no right overlap - if( i==0 || i==node[0].getNumChildren()-1 || t.find(s)==std::string::npos ){ - bool do_split = false; - int sot = s.overlap( t ); - Trace("strings-ext-rewrite") << "Overlap " << s << " " << t << " is " << sot << std::endl; - if( sot==0 ){ - do_split = i==0; - } - if( !do_split && ( i==(node[0].getNumChildren()-1) || sot==0 ) ){ - int tos = t.overlap( s ); - Trace("strings-ext-rewrite") << "Overlap " << t << " " << s << " is " << tos << std::endl; - if( tos==0 ){ - do_split = true; - } - } - if( do_split ){ - std::vector< Node > nc0; - getConcat( node[0], nc0 ); - std::vector< Node > spl[2]; - if( i>0 ){ - spl[0].insert( spl[0].end(), nc0.begin(), nc0.begin()+i ); - } - if( i<nc0.size()-1 ){ - spl[1].insert( spl[1].end(), nc0.begin()+i+1, nc0.end() ); - } - retNode = NodeManager::currentNM()->mkNode( kind::OR, - NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[0] ), node[1] ), - NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[1] ), node[1] ) ); - break; - } - } - } - } - } - } - } - }else if( node[0].isConst() ){ - if( node[1].getKind()==kind::STRING_CONCAT ){ - //must find constant components in order - size_t pos = 0; - CVC4::String t = node[0].getConst<String>(); - for(unsigned i=0; i<node[1].getNumChildren(); i++) { - if( node[1][i].isConst() ){ - CVC4::String s = node[1][i].getConst<String>(); - size_t new_pos = t.find(s,pos); - if( new_pos==std::string::npos ) { - retNode = NodeManager::currentNM()->mkConst( false ); - break; - }else{ - pos = new_pos + s.size(); - } - } - } - } - } + }else if( node.getKind() == kind::STRING_STRCTN ){ + retNode = rewriteContains( node ); }else if( node.getKind()==kind::STRING_STRIDOF ){ - std::vector< Node > children; - getConcat( node[0], children ); - //std::vector< Node > children1; - //getConcat( node[1], children1 ); TODO - std::size_t start = 0; - std::size_t val2 = 0; - if( node[2].isConst() ){ - CVC4::Rational RMAXINT(LONG_MAX); - if( node[2].getConst<Rational>()>RMAXINT ){ - Assert(node[2].getConst<Rational>() <= RMAXINT, "Number exceeds LONG_MAX in string index_of"); - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); - }else if( node[2].getConst<Rational>().sgn()==-1 ){ - //constant negative - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); - }else{ - val2 = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); - start = val2; - } - } - if( retNode==node ){ - bool prefixNoOverlap = false; - CVC4::String t; - if( node[1].isConst() ){ - t = node[1].getConst<String>(); - } - //unsigned ch1_index = 0; - for( unsigned i=0; i<children.size(); i++ ){ - bool do_splice = false; - if( children[i].isConst() ){ - CVC4::String s = children[i].getConst<String>(); - if( node[1].isConst() ){ - if( i==0 ){ - std::size_t ret = s.find( t, start ); - if( ret!=std::string::npos ) { - //exact if start value was constant - if( node[2].isConst() ){ - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((unsigned) ret) ); - break; - } - }else{ - //exact if we scanned the entire string - if( node[0].isConst() ){ - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); - break; - }else{ - prefixNoOverlap = (s.overlap(t)==0); - Trace("strings-rewrite-debug") << "Prefix no overlap : " << s << " " << t << " " << prefixNoOverlap << std::endl; - } - } - }else if( !node[2].isConst() ){ - break; - }else{ - std::size_t ret = s.find(t, start); - //remove remaining children after finding the string - if( ret!=std::string::npos ){ - Assert( ret+t.size()<=s.size() ); - children[i] = NodeManager::currentNM()->mkConst( ::CVC4::String( s.substr(0,ret+t.size()) ) ); - do_splice = true; - }else{ - //if no overlap on last child, can remove - if( t.overlap( s )==0 && i==children.size()-1 ){ - std::vector< Node > spl; - spl.insert( spl.end(), children.begin(), children.begin()+i ); - retNode = NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ); - break; - } - } - } - } - //decrement the start index - if( start>0 ){ - if( s.size()>start ){ - start = 0; - }else{ - start = start - s.size(); - } - } - }else if( !node[2].isConst() ){ - break; - }else{ - if( children[i]==node[1] && start==0 ){ - //can remove beyond this - do_splice = true; - } - } - if( do_splice ){ - std::vector< Node > spl; - //since we definitely will find the string, we can safely add the length of the constant non-overlapping prefix - if( prefixNoOverlap ){ - Node pl = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, children[0] ) ); - Assert( pl.isConst() ); - Assert( node[2].isConst() ); - int new_start = val2 - pl.getConst<Rational>().getNumerator().toUnsignedInt(); - if( new_start<0 ){ - new_start = 0; - } - spl.insert( spl.end(), children.begin()+1, children.begin()+i+1 ); - retNode = NodeManager::currentNM()->mkNode( kind::PLUS, pl, - NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], NodeManager::currentNM()->mkConst( Rational(new_start) ) ) ); - }else{ - spl.insert( spl.end(), children.begin(), children.begin()+i+1 ); - retNode = NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ); - } - break; - } - } - } + retNode = rewriteIndexof( node ); }else if( node.getKind() == kind::STRING_STRREPL ){ - if( node[1]==node[2] ){ - retNode = node[0]; - }else{ - std::vector< Node > children; - getConcat( node[0], children ); - if( children[0].isConst() && node[1].isConst() ){ - CVC4::String s = children[0].getConst<String>(); - CVC4::String t = node[1].getConst<String>(); - std::size_t p = s.find(t); - if( p != std::string::npos ) { - if( node[2].isConst() ){ - CVC4::String r = node[2].getConst<String>(); - CVC4::String ret = s.replace(t, r); - retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) ); - } else { - CVC4::String s1 = s.substr(0, (int)p); - CVC4::String s3 = s.substr((int)p + (int)t.size()); - Node ns1 = NodeManager::currentNM()->mkConst( ::CVC4::String(s1) ); - Node ns3 = NodeManager::currentNM()->mkConst( ::CVC4::String(s3) ); - retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 ); - } - if( children.size()>1 ){ - children[0] = retNode; - retNode = mkConcat( kind::STRING_CONCAT, children ); - } - }else{ - //could not find replacement string - if( node[0].isConst() ){ - retNode = node[0]; - }else{ - //check for overlap, if none, we can remove the prefix - if( s.overlap(t)==0 ){ - std::vector< Node > spl; - spl.insert( spl.end(), children.begin()+1, children.end() ); - retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, children[0], - NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ) ); - } - } - } - } - } + retNode = rewriteReplace( node ); }else if( node.getKind() == kind::STRING_PREFIX ){ if( node[0].isConst() && node[1].isConst() ){ CVC4::String s = node[1].getConst<String>(); @@ -1629,6 +1379,260 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } + +Node TheoryStringsRewriter::rewriteContains( Node node ) { + if( node[0] == node[1] ){ + return NodeManager::currentNM()->mkConst( true ); + }else if( node[0].isConst() && node[1].isConst() ){ + CVC4::String s = node[0].getConst<String>(); + CVC4::String t = node[1].getConst<String>(); + if( s.find(t) != std::string::npos ){ + return NodeManager::currentNM()->mkConst( true ); + }else{ + return NodeManager::currentNM()->mkConst( false ); + } + }else if( node[0].getKind()==kind::STRING_CONCAT ){ + //component-wise containment + unsigned n1 = node[0].getNumChildren(); + std::vector< Node > nc1; + getConcat( node[1], nc1 ); + unsigned n2 = nc1.size(); + if( n1>n2 ){ + unsigned diff = n1-n2; + for(unsigned i=0; i<diff; i++) { + if( node[0][i]==nc1[0] ){ + bool flag = true; + for(unsigned j=1; j<n2; j++) { + if( node[0][i+j]!=nc1[j] ){ + flag = false; + break; + } + } + if(flag) { + return NodeManager::currentNM()->mkConst( true ); + } + } + } + } + if( node[1].isConst() ){ + CVC4::String t = node[1].getConst<String>(); + for(unsigned i=0; i<node[0].getNumChildren(); i++){ + //constant contains + if( node[0][i].isConst() ){ + CVC4::String s = node[0][i].getConst<String>(); + if( s.find(t)!=std::string::npos ) { + return NodeManager::currentNM()->mkConst( true ); + }else{ + //if no overlap, we can split into disjunction + // if first child, only require no left overlap + // if last child, only require no right overlap + if( i==0 || i==node[0].getNumChildren()-1 || t.find(s)==std::string::npos ){ + bool do_split = false; + int sot = s.overlap( t ); + Trace("strings-ext-rewrite") << "Overlap " << s << " " << t << " is " << sot << std::endl; + if( sot==0 ){ + do_split = i==0; + } + if( !do_split && ( i==(node[0].getNumChildren()-1) || sot==0 ) ){ + int tos = t.overlap( s ); + Trace("strings-ext-rewrite") << "Overlap " << t << " " << s << " is " << tos << std::endl; + if( tos==0 ){ + do_split = true; + } + } + if( do_split ){ + std::vector< Node > nc0; + getConcat( node[0], nc0 ); + std::vector< Node > spl[2]; + if( i>0 ){ + spl[0].insert( spl[0].end(), nc0.begin(), nc0.begin()+i ); + } + if( i<nc0.size()-1 ){ + spl[1].insert( spl[1].end(), nc0.begin()+i+1, nc0.end() ); + } + return NodeManager::currentNM()->mkNode( kind::OR, + NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[0] ), node[1] ), + NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[1] ), node[1] ) ); + } + } + } + } + } + } + }else if( node[0].isConst() ){ + if( node[1].getKind()==kind::STRING_CONCAT ){ + //must find constant components in order + size_t pos = 0; + CVC4::String t = node[0].getConst<String>(); + for(unsigned i=0; i<node[1].getNumChildren(); i++) { + if( node[1][i].isConst() ){ + CVC4::String s = node[1][i].getConst<String>(); + size_t new_pos = t.find(s,pos); + if( new_pos==std::string::npos ) { + return NodeManager::currentNM()->mkConst( false ); + }else{ + pos = new_pos + s.size(); + } + } + } + } + } + return node; +} + +Node TheoryStringsRewriter::rewriteIndexof( Node node ) { + std::vector< Node > children; + getConcat( node[0], children ); + //std::vector< Node > children1; + //getConcat( node[1], children1 ); TODO + std::size_t start = 0; + std::size_t val2 = 0; + if( node[2].isConst() ){ + CVC4::Rational RMAXINT(LONG_MAX); + if( node[2].getConst<Rational>()>RMAXINT ){ + Assert(node[2].getConst<Rational>() <= RMAXINT, "Number exceeds LONG_MAX in string index_of"); + return NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); + }else if( node[2].getConst<Rational>().sgn()==-1 ){ + //constant negative + return NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); + }else{ + val2 = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + start = val2; + } + } + bool prefixNoOverlap = false; + CVC4::String t; + if( node[1].isConst() ){ + t = node[1].getConst<String>(); + } + //unsigned ch1_index = 0; + for( unsigned i=0; i<children.size(); i++ ){ + bool do_splice = false; + if( children[i].isConst() ){ + CVC4::String s = children[i].getConst<String>(); + if( node[1].isConst() ){ + if( i==0 ){ + std::size_t ret = s.find( t, start ); + if( ret!=std::string::npos ) { + //exact if start value was constant + if( node[2].isConst() ){ + return NodeManager::currentNM()->mkConst( ::CVC4::Rational((unsigned) ret) ); + } + }else{ + //exact if we scanned the entire string + if( node[0].isConst() ){ + return NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); + }else{ + prefixNoOverlap = (s.overlap(t)==0); + Trace("strings-rewrite-debug") << "Prefix no overlap : " << s << " " << t << " " << prefixNoOverlap << std::endl; + } + } + }else if( !node[2].isConst() ){ + break; + }else{ + std::size_t ret = s.find(t, start); + //remove remaining children after finding the string + if( ret!=std::string::npos ){ + Assert( ret+t.size()<=s.size() ); + children[i] = NodeManager::currentNM()->mkConst( ::CVC4::String( s.substr(0,ret+t.size()) ) ); + do_splice = true; + }else{ + //if no overlap on last child, can remove + if( t.overlap( s )==0 && i==children.size()-1 ){ + std::vector< Node > spl; + spl.insert( spl.end(), children.begin(), children.begin()+i ); + return NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ); + } + } + } + } + //decrement the start index + if( start>0 ){ + if( s.size()>start ){ + start = 0; + }else{ + start = start - s.size(); + } + } + }else if( !node[2].isConst() ){ + break; + }else{ + if( children[i]==node[1] && start==0 ){ + //can remove beyond this + do_splice = true; + } + } + if( do_splice ){ + std::vector< Node > spl; + //since we definitely will find the string, we can safely add the length of the constant non-overlapping prefix + if( prefixNoOverlap ){ + Node pl = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, children[0] ) ); + Assert( pl.isConst() ); + Assert( node[2].isConst() ); + int new_start = val2 - pl.getConst<Rational>().getNumerator().toUnsignedInt(); + if( new_start<0 ){ + new_start = 0; + } + spl.insert( spl.end(), children.begin()+1, children.begin()+i+1 ); + return NodeManager::currentNM()->mkNode( kind::PLUS, pl, + NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], NodeManager::currentNM()->mkConst( Rational(new_start) ) ) ); + }else{ + spl.insert( spl.end(), children.begin(), children.begin()+i+1 ); + return NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ); + } + } + } + return node; +} + +Node TheoryStringsRewriter::rewriteReplace( Node node ) { + if( node[1]==node[2] ){ + return node[0]; + }else{ + std::vector< Node > children; + getConcat( node[0], children ); + if( children[0].isConst() && node[1].isConst() ){ + CVC4::String s = children[0].getConst<String>(); + CVC4::String t = node[1].getConst<String>(); + std::size_t p = s.find(t); + if( p != std::string::npos ) { + Node retNode; + if( node[2].isConst() ){ + CVC4::String r = node[2].getConst<String>(); + CVC4::String ret = s.replace(t, r); + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) ); + } else { + CVC4::String s1 = s.substr(0, (int)p); + CVC4::String s3 = s.substr((int)p + (int)t.size()); + Node ns1 = NodeManager::currentNM()->mkConst( ::CVC4::String(s1) ); + Node ns3 = NodeManager::currentNM()->mkConst( ::CVC4::String(s3) ); + retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 ); + } + if( children.size()>1 ){ + children[0] = retNode; + return mkConcat( kind::STRING_CONCAT, children ); + }else{ + return retNode; + } + }else{ + //could not find replacement string + if( node[0].isConst() ){ + return node[0]; + }else{ + //check for overlap, if none, we can remove the prefix + if( s.overlap(t)==0 ){ + std::vector< Node > spl; + spl.insert( spl.end(), children.begin()+1, children.end() ); + return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, children[0], + NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ) ); + } + } + } + } + } + return node; +} + void TheoryStringsRewriter::getConcat( Node n, std::vector< Node >& c ) { if( n.getKind()==kind::STRING_CONCAT || n.getKind()==kind::REGEXP_CONCAT ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 2a8258a09..f8b420904 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -54,6 +54,10 @@ public: static inline void init() {} static inline void shutdown() {} + static Node rewriteContains( Node n ); + static Node rewriteIndexof( Node n ); + static Node rewriteReplace( Node n ); + static void getConcat( Node n, std::vector< Node >& c ); static Node mkConcat( Kind k, std::vector< Node >& c ); static Node splitConstant( Node a, Node b, int& index, bool isRev ); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index cde3aef1c..c62a0dd4a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -104,7 +104,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). // However, if the Decision Engine stops us early, there might be a // quantifier that isn't assigned. In conjunction with miniscoping, this @@ -193,9 +193,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) { ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator()); } - if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ - //do nothing - } d_modelCache[n] = ret; return ret; } diff --git a/src/theory/uf/options b/src/theory/uf/options index d9e4c9477..cb6ddc0fa 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -36,7 +36,7 @@ option ufssCliqueSplits --uf-ss-clique-splits bool :default false option ufssSymBreak --uf-ss-sym-break bool :default false finite model finding symmetry breaking techniques -option ufssFairness --uf-ss-fair bool :default false +option ufssFairness --uf-ss-fair bool :default true use fair strategy for finite model finding multiple sorts endmodule diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 858761078..95671d6ec 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -124,6 +124,10 @@ void TheoryUF::check(Effort level) { ss << "Try using a logic containing \"UFC\"." << std::endl; throw Exception( ss.str() ); } + //needed for models + if( options::produceModels() && atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ + d_equalityEngine.assertPredicate(atom, polarity, fact); + } } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } |