dumpAssertions("post-bv-to-bool", d_assertions);
Trace("smt") << "POST bvToBool" << endl;
}
- if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
- dumpAssertions("pre-strings-pp", d_assertions);
- if( !options::stringLazyPreproc() ){
- ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
- }
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
- dumpAssertions("post-strings-pp", d_assertions);
- }
if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) {
//separation logic solver needs to register the entire input
((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() );
Assert( d_label_model.find( s_lbl )!=d_label_model.end() );
std::vector< Node > conc;
bool inst_success = true;
- if( options::sepExp() ){
- //old refinement lemmas
- for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){
- int sub_index = itl->first;
- std::map< Node, Node > visited;
- Node c = applyLabel( s_atom[itl->first], mvals[sub_index], visited );
- Trace("sep-process-debug") << " applied inst : " << c << std::endl;
- if( s_atom.getKind()==kind::SEP_STAR || sub_index==0 ){
- conc.push_back( c.negate() );
- }else{
- conc.push_back( c );
- }
- }
+ //new refinement
+ //instantiate the label
+ std::map< Node, Node > visited;
+ Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, tn, active_lbl );
+ Trace("sep-inst-debug") << " applied inst : " << inst << std::endl;
+ if( inst.isNull() ){
+ inst_success = false;
}else{
- //new refinement
- std::map< Node, Node > visited;
- Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, tn, active_lbl );
- Trace("sep-inst-debug") << " applied inst : " << inst << std::endl;
- if( inst.isNull() ){
+ inst = Rewriter::rewrite( inst );
+ if( inst==( polarity ? d_true : d_false ) ){
inst_success = false;
- }else{
- inst = Rewriter::rewrite( inst );
- if( inst==( polarity ? d_true : d_false ) ){
- inst_success = false;
- }
- conc.push_back( polarity ? inst : inst.negate() );
}
+ conc.push_back( polarity ? inst : inst.negate() );
}
if( inst_success ){
std::vector< Node > lemc;
pol_atom = atom.negate();
}
lemc.push_back( pol_atom );
+ //TODO: add disjointness assumption
+
//lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() );
//lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() );
lemc.insert( lemc.end(), conc.begin(), conc.end() );
Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc );
- if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){
+ if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){
d_refinement_lem[s_atom][s_lbl].push_back( lem );
Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem[s_atom][s_lbl].size() << ") : " << lem << std::endl;
Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl;
d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
- d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
- d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
- d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
- d_equalityEngine.addFunctionKind(kind::STRING_STOI);
if( options::stringLazyPreproc() ){
+ d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
+ d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
+ d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
+ d_equalityEngine.addFunctionKind(kind::STRING_STOI);
d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
atom = polarity ? fact : fact[0];
//run preprocess on memberships
+ /*
if( options::stringLazyPreproc() ){
checkReduction( atom, polarity ? 1 : -1, 0 );
doPendingLemmas();
}
+ */
//assert pending fact
assertPendingFact( atom, polarity, fact );
}
Assert( d_lemma_cache.empty() );
}
+bool TheoryStrings::needsCheckLastEffort() {
+ return false;
+}
+
void TheoryStrings::checkExtfReduction( int effort ) {
Trace("strings-process-debug") << "Checking preprocess at effort " << effort << ", #to process=" << d_ext_func_terms.size() << "..." << std::endl;
for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
//determine the effort level to process the extf at
// 0 - at assertion time, 1+ - after no other reduction is applicable
int r_effort = -1;
- if( atom.getKind()==kind::STRING_IN_REGEXP ){
- if( pol==1 && atom[1].getKind()==kind::REGEXP_RANGE ){
- r_effort = 0;
- }
- }else if( atom.getKind()==kind::STRING_STRCTN ){
+ if( atom.getKind()==kind::STRING_STRCTN ){
if( pol==1 ){
r_effort = 1;
}else{
std::vector< Node > lexp;
Node lenx = getLength( x, lexp );
Node lens = getLength( s, lexp );
- if( areEqual(lenx, lens) ){
+ if( areEqual( lenx, lens ) ){
d_ext_func_terms[atom] = false;
//we can reduce to disequality when lengths are equal
if( !areDisequal( x, s ) ){
}
}else if( !areDisequal( lenx, lens ) ){
//split on their lenths
- lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
- lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
+ lenx = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
+ lens = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, s );
sendSplit( lenx, lens, "NEG-CTN-SP" );
}else{
r_effort = 2;
if( options::stringLazyPreproc() ){
if( atom.getKind()==kind::STRING_SUBSTR ){
r_effort = 1;
- }else{
+ }else if( atom.getKind()!=kind::STRING_IN_REGEXP ){
r_effort = 2;
}
}
}
if( effort==r_effort ){
- if( d_preproc_cache.find( atom )==d_preproc_cache.end() ){
- d_preproc_cache[ atom ] = true;
- Trace("strings-process-debug") << "Process reduction for " << atom << std::endl;
- if( atom.getKind()==kind::STRING_IN_REGEXP ){
- if( atom[1].getKind()==kind::REGEXP_RANGE ){
- Node eq = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, atom[0]));
- std::vector< Node > exp_vec;
- exp_vec.push_back( atom );
- sendInference( d_empty_vec, exp_vec, eq, "RE-Range-Len", true );
- }
- }else if( atom.getKind()==kind::STRING_STRCTN ){
+ Node c_atom = pol==-1 ? atom.negate() : atom;
+ if( d_preproc_cache.find( c_atom )==d_preproc_cache.end() ){
+ d_preproc_cache[ c_atom ] = true;
+ Trace("strings-process-debug") << "Process reduction for " << atom << ", pol = " << pol << std::endl;
+ if( atom.getKind()==kind::STRING_STRCTN && pol==1 ){
Node x = atom[0];
Node s = atom[1];
- if( pol==1 ){
- //positive contains reduces to a equality
- Assert( !areEqual( s, d_emptyString ) && !areEqual( s, x ) );
- 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 ) ) );
- std::vector< Node > exp_vec;
- exp_vec.push_back( atom );
- sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true );
- }else{
- //negative contains reduces to forall
- Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
- Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
- Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
- Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
- Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
- NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
- Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
- Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
- Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b2, d_one);
-
- Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6);
-
- std::vector< Node > vec_nodes;
- Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
- vec_nodes.push_back(cc);
- cc = NodeManager::currentNM()->mkNode( kind::GT, lens, b2 );
- vec_nodes.push_back(cc);
-
- cc = s2.eqNode(s5).negate();
- vec_nodes.push_back(cc);
-
- Node conc = NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
- conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
- conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
- conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
- Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
- conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ) );
-
- std::vector< Node > exp;
- exp.push_back( atom.negate() );
- sendInference( d_empty_vec, exp, conc, "NEG-CTN-BRK", true );
- }
+ //positive contains reduces to a equality
+ 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 ) ) );
+ std::vector< Node > exp_vec;
+ exp_vec.push_back( atom );
+ sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true );
+ //we've reduced this atom
+ d_ext_func_terms[ atom ] = false;
}else{
- // for STRING_SUBSTR,
+ // for STRING_SUBSTR, STRING_STRCTN with pol=-1,
// STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
std::vector< Node > new_nodes;
- Node res = d_preproc.decompose( atom, new_nodes );
- Assert( res==atom );
- if( !new_nodes.empty() ){
- Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
- nnlem = Rewriter::rewrite( nnlem );
- Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
- Trace("strings-red-lemma") << "...from " << atom << std::endl;
- sendInference( d_empty_vec, nnlem, "Reduction", true );
- }
+ Node res = d_preproc.simplify( atom, new_nodes );
+ Assert( res!=atom );
+ new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, atom ) );
+ Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+ nnlem = Rewriter::rewrite( nnlem );
+ Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
+ Trace("strings-red-lemma") << "...from " << atom << std::endl;
+ sendInference( d_empty_vec, nnlem, "Reduction", true );
+ //we've reduced this atom
+ d_ext_func_terms[ atom ] = false;
}
}
}
if( n_pol!=0 ){
//add original to explanation
d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() );
- if( nr.getKind()==kind::STRING_STRCTN ){
+
+ //d_extf_infer_cache stores whether we have made the inferences associated with a node n,
+ // this may need to be generalized if multiple inferences apply
+
+ if( nr.getKind()==kind::STRING_IN_REGEXP ){
+ if( n_pol==1 && nr[1].getKind()==kind::REGEXP_RANGE ){
+ if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
+ d_extf_infer_cache.insert( nr );
+ //length of first argument is one
+ Node conc = d_one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nr[0]) );
+ sendInference( d_extf_exp[n], conc, "RE-Range-Len", true );
+ }
+ }
+ }else if( nr.getKind()==kind::STRING_STRCTN ){
if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){
if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
d_extf_infer_cache.insert( nr );
+
//one argument does (not) contain each of the components of the other argument
int index = n_pol==1 ? 1 : 0;
std::vector< Node > children;
d_ext_func_terms[conc] = false;
sendInference( d_extf_exp[n], n_pol==1 ? conc : conc.negate(), "CTN_Decompose" );
}
+
}
}else{
//store this (reduced) assertion
//explain why other components up to now are empty
for( unsigned t=0; t<2; t++ ){
Node c = t==0 ? a : b;
- int jj = t==0 ? d_flat_form_index[a][count] : ( inf_type==2 ? ( r==0 ? c.getNumChildren() : -1 ) : d_flat_form_index[b][count] );
+ int jj;
+ if( inf_type==3 || ( t==1 && inf_type==2 ) ){
+ //explain all the empty components for F_EndpointEq, all for the short end for F_EndpointEmp
+ jj = r==0 ? c.getNumChildren() : -1;
+ }else{
+ jj = t==0 ? d_flat_form_index[a][count] : d_flat_form_index[b][count];
+ }
if( r==0 ){
for( int j=0; j<jj; j++ ){
if( areEqual( c[j], d_emptyString ) ){
}
}
}
- //if( exp_n.empty() ){
- sendInference( exp, conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) );
- //}else{
- //}
+ //notice that F_EndpointEmp is not typically applied, since strict prefix equality ( a.b = a ) where a,b non-empty
+ // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) when len(b)!=0.
+ sendInference( exp, conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_EndpointEmp" : "F_EndpointEq" ) ) );
if( d_conflict ){
return;
}else{
Trace("strings-nf") << "**** Normal forms are : " << std::endl;
for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
Trace("strings-nf") << " N[" << it->second << "] = " << it->first << std::endl;
+ //Trace("strings-nf") << " exp: " << eqc_to_exp[it->first] << std::endl;
}
Trace("strings-nf") << std::endl;
}
Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
//now, check if length normalization has occurred
if( ei->d_normalized_length.get().isNull() ) {
+ Node nf = mkConcat( d_normal_forms[d_strings_eqc[i]] );
+ if( Trace.isOn("strings-process-debug") ){
+ Trace("strings-process-debug") << " normal form is " << nf << " from base " << d_normal_forms_base[d_strings_eqc[i]] << std::endl;
+ Trace("strings-process-debug") << " normal form exp is: " << std::endl;
+ for( unsigned j=0; j<d_normal_forms_exp[d_strings_eqc[i]].size(); j++ ){
+ Trace("strings-process-debug") << " " << d_normal_forms_exp[d_strings_eqc[i]][j] << std::endl;
+ }
+ }
+
//if not, add the lemma
std::vector< Node > ant;
ant.insert( ant.end(), d_normal_forms_exp[d_strings_eqc[i]].begin(), d_normal_forms_exp[d_strings_eqc[i]].end() );
ant.push_back( d_normal_forms_base[d_strings_eqc[i]].eqNode( lt ) );
- Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[d_strings_eqc[i]] ) );
+ Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf );
lc = Rewriter::rewrite( lc );
Node eq = llt.eqNode( lc );
if( llt!=lc ){
}
}
}
-
return Node::null();
}
+Node TheoryStrings::ppRewrite(TNode atom) {
+ Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+ if( !options::stringLazyPreproc() ){
+ //eager preprocess here
+ std::vector< Node > new_nodes;
+ std::map< Node, Node > visited;
+ Node ret = d_preproc.simplifyRec( atom, new_nodes, visited );
+ if( ret!=atom ){
+ Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl;
+ for( unsigned i=0; i<new_nodes.size(); i++ ){
+ Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl;
+ d_out->lemma( new_nodes[i] );
+ }
+ return ret;
+ }else{
+ Assert( new_nodes.empty() );
+ }
+ }
+ return atom;
+}
+
void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
if( visited.find( n )==visited.end() ){
visited[n] = true;
n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){
Trace("strings-extf-debug2") << "Found extended function : " << n << std::endl;
+ Assert( options::stringLazyPreproc() );
d_ext_func_terms[n] = true;
}
}
Node r = atom[1];
std::vector< Node > rnfexp;
- if(options::stringOpt1()) {
+ //if(options::stringOpt1()) {
+ if(true){
if(!x.isConst()) {
x = getNormalString( x, rnfexp);
changed = true;
Node expandDefinition(LogicRequest &logicRequest, Node n);
/** Check at effort e */
void check(Effort e);
+ /** needs check last effort */
+ bool needsCheckLastEffort();
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when a new equivalence class is created */
public:
//for finite model finding
Node getNextDecisionRequest();
-
+ //ppRewrite
+ Node ppRewrite(TNode atom);
public:
/** statistics class */
class Statistics {
namespace theory {
namespace strings {
-StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){
+StringsPreprocess::StringsPreprocess( context::UserContext* u ){
//Constants
d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+ d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
}
StringsPreprocess::~StringsPreprocess(){
}
-/*
-int StringsPreprocess::checkFixLenVar( Node t ) {
- int ret = 2;
- if(t.getKind() == kind::EQUAL) {
- if(t[0].getType().isInteger() && t[0].isConst() && t[1].getKind() == kind::STRING_LENGTH) {
- if(t[1][0].getKind() == kind::VARIABLE) {
- ret = 0;
- }
- } else if(t[1].getType().isInteger() && t[1].isConst() && t[0].getKind() == kind::STRING_LENGTH) {
- if(t[0][0].getKind() == kind::VARIABLE) {
- ret = 1;
- }
- }
- }
- if(ret != 2) {
- unsigned len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt();
- if(len < 2) {
- ret = 2;
+Node StringsPreprocess::getUfForNode( Node n ) {
+ //TODO: use this for eager preprocess
+ Kind k = n.getKind();
+ std::map< Kind, Node >::iterator it = d_uf.find( k );
+ if( it==d_uf.end() ){
+ std::vector< TypeNode > types;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ types.push_back( n[i].getType() );
}
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, n.getType() );
+ Node f = NodeManager::currentNM()->mkSkolem( "sop", typ, "op created for string op" );
+ d_uf[k] = f;
+ return f;
+ }else{
+ return it->second;
}
- if(!options::stringExp()) {
- ret = 2;
- }
- return ret;
}
-*/
-Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
- NodeNodeMap::const_iterator i = d_cache.find(t);
- if(i != d_cache.end()) {
- return (*i).second.isNull() ? t : (*i).second;
- }
- Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
+//returns an n such that t can be replaced by n, under the assumption of lemmas in new_nodes
+
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
+ unsigned prev_new_nodes = new_nodes.size();
+ Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl;
Node retNode = t;
- /*int c_id = checkFixLenVar(t);
- if( c_id != 2 ) {
- int v_id = 1 - c_id;
- int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
- if(len > 1) {
- Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
- std::vector< Node > vec;
- for(int i=0; i<len; i++) {
- Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
- //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
- Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one);
- vec.push_back(sk);
- Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ));
- new_nodes.push_back( cc );
- }
- Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
- lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
- new_nodes.push_back( lem );
- d_cache[t] = t;
- retNode = t;
- }
- } else */
if( t.getKind() == kind::STRING_SUBSTR ) {
- /*
- Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
- NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
- Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
- Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, t[2], d_zero);
- Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
- Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
- 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, lenc ),
- t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
- */
+ Node skt = NodeManager::currentNM()->mkSkolem( "sst", NodeManager::currentNM()->stringType(), "created for substr" );
Node t12 = NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] );
Node lt0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] );
//start point is greater than or equal zero
Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" );
Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" );
- Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk2 ) );
+ Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, skt, sk2 ) );
//length of first skolem is second argument
Node b12 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ).eqNode( t[1] );
//length of second skolem is abs difference between end point and end of string
NodeManager::currentNM()->mkNode( kind::MINUS, lt0, t12 ), d_zero ) );
Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 );
- Node b2 = t.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
-
+ Node b2 = skt.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) );
new_nodes.push_back( lemma );
- d_cache[t] = t;
+ retNode = skt;
} else if( t.getKind() == kind::STRING_STRIDOF ) {
Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
Node cond = skk.eqNode( negone );
Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
new_nodes.push_back( rr );
- if( options::stringLazyPreproc() ){
- new_nodes.push_back( t.eqNode( skk ) );
- d_cache[t] = Node::null();
- }else{
- d_cache[t] = skk;
- retNode = skk;
- }
+ retNode = skk;
} else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) {
//Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
// NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
// t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
Node num = t[0];
- Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
+ //Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
+ Node pret = NodeManager::currentNM()->mkSkolem( "itost", NodeManager::currentNM()->stringType(), "created for itos" );
Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
new_nodes.push_back( conc );*/
- if( options::stringLazyPreproc() && t!=pret ){
- new_nodes.push_back( t.eqNode( pret ) );
- d_cache[t] = Node::null();
- }else{
- d_cache[t] = pret;
- retNode = pret;
- }
- //don't rewrite processed
- if(t != pret) {
- d_cache[pret] = pret;
- }
+ retNode = pret;
} else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) {
Node str = t[0];
- Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str);
+ //Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str);
+ Node pret = NodeManager::currentNM()->mkSkolem( "stoit", NodeManager::currentNM()->integerType(), "created for stoi" );
Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str);
Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone),
NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
new_nodes.push_back( conc );
- if( options::stringLazyPreproc() && t!=pret ){
- new_nodes.push_back( t.eqNode( pret ) );
- d_cache[t] = Node::null();
- }else{
- d_cache[t] = pret;
- retNode = pret;
- }
- if(t != pret) {
- d_cache[pret] = pret;
- }
+ retNode = pret;
} else if( t.getKind() == kind::STRING_STRREPL ) {
Node x = t[0];
Node y = t[1];
new_nodes.push_back( rr );
rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
new_nodes.push_back( rr );
- if( options::stringLazyPreproc() ){
- new_nodes.push_back( t.eqNode( skw ) );
- d_cache[t] = Node::null();
- }else{
- d_cache[t] = skw;
- retNode = skw;
- }
+ retNode = skw;
} else if( t.getKind() == kind::STRING_STRCTN ){
- //TODO?
- d_cache[t] = Node::null();
- } else{
- d_cache[t] = Node::null();
+ Node x = t[0];
+ Node s = t[1];
+ //negative contains reduces to existential
+ Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+ Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
+ Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+ Node body = NodeManager::currentNM()->mkNode( kind::AND,
+ NodeManager::currentNM()->mkNode( kind::LEQ, d_zero, b1 ),
+ NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ),
+ NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s )
+ );
+ retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
}
- /*if( t.getNumChildren()>0 ) {
- std::vector< Node > cc;
- if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
- cc.push_back(t.getOperator());
- }
- bool changed = false;
- for( unsigned i=0; i<t.getNumChildren(); i++ ){
- Node tn = simplify( t[i], new_nodes );
- cc.push_back( tn );
- changed = changed || tn!=t[i];
- }
- if(changed) {
- Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
- d_cache[t] = n;
- retNode = n;
- } else {
- d_cache[t] = Node::null();
- retNode = t;
- }
- }*/
if( t!=retNode ){
- Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
+ Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
if(!new_nodes.empty()) {
- Trace("strings-preprocess-debug") << " ... new nodes (" << new_nodes.size() << "):\n";
- for(unsigned int i=0; i<new_nodes.size(); ++i) {
- Trace("strings-preprocess-debug") << "\t" << new_nodes[i] << "\n";
+ Trace("strings-preprocess") << " ... new nodes (" << (new_nodes.size()-prev_new_nodes) << "):" << std::endl;
+ for(unsigned int i=prev_new_nodes; i<new_nodes.size(); ++i) {
+ Trace("strings-preprocess") << " " << new_nodes[i] << std::endl;
}
}
}
return retNode;
}
-Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
- NodeNodeMap::const_iterator i = d_cache.find(t);
- if(i != d_cache.end()) {
- return (*i).second.isNull() ? t : (*i).second;
- }
-
- unsigned num = t.getNumChildren();
- if(num == 0) {
- return simplify(t, new_nodes);
+Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, std::map< Node, Node >& visited ){
+ std::map< Node, Node >::iterator it = visited.find(t);
+ if( it!=visited.end() ){
+ return it->second;
}else{
- bool changed = false;
- std::vector< Node > cc;
- if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
- cc.push_back(t.getOperator());
- }
- for(unsigned i=0; i<t.getNumChildren(); i++) {
- Node s = decompose(t[i], new_nodes);
- cc.push_back( s );
- if(s != t[i]) {
- changed = true;
+ Node retNode;
+ if( t.getNumChildren()==0 ){
+ retNode = simplify( t, new_nodes );
+ }else if( t.getKind()!=kind::FORALL ){
+ bool changed = false;
+ std::vector< Node > cc;
+ if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ cc.push_back( t.getOperator() );
}
+ for(unsigned i=0; i<t.getNumChildren(); i++) {
+ Node s = simplifyRec( t[i], new_nodes, visited );
+ cc.push_back( s );
+ if( s!=t[i] ) {
+ changed = true;
+ }
+ }
+ Node tmp = t;
+ if( changed ){
+ tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
+ }
+ retNode = simplify( tmp, new_nodes );
}
- if(changed) {
- Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
- return simplify(tmp, new_nodes);
- } else {
- return simplify(t, new_nodes);
- }
+ visited[t] = retNode;
+ return retNode;
}
}
-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
+ std::map< Node, Node > visited;
for( unsigned i=0; i<vec_node.size(); i++ ){
+ Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl;
+ //preprocess until fixed point
std::vector< Node > new_nodes;
- Node curr = decompose( vec_node[i], new_nodes );
- if( !new_nodes.empty() ){
- new_nodes.insert( new_nodes.begin(), curr );
- curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+ std::vector< Node > new_nodes_curr;
+ new_nodes_curr.push_back( vec_node[i] );
+ while( !new_nodes_curr.empty() ){
+ Node curr = new_nodes_curr.back();
+ new_nodes_curr.pop_back();
+ std::vector< Node > new_nodes_tmp;
+ curr = simplifyRec( curr, new_nodes_tmp, visited );
+ new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() );
+ new_nodes.push_back( curr );
}
- if( curr!=vec_node[i] ){
- curr = Rewriter::rewrite( curr );
- PROOF( ProofManager::currentPM()->addDependence(curr, vec_node[i]); );
- vec_node[i] = curr;
+ Node res = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+ if( res!=vec_node[i] ){
+ res = Rewriter::rewrite( res );
+ PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); );
+ vec_node[i] = res;
}
}
}
namespace strings {
class StringsPreprocess {
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
- NodeNodeMap d_cache;
//Constants
Node d_zero;
-private:
- //int checkFixLenVar( Node t );
- Node simplify( Node t, std::vector< Node > &new_nodes );
+ Node d_one;
+ //mapping from kinds to UF
+ std::map< Kind, Node > d_uf;
+ //get UF for node
+ Node getUfForNode( Node n );
public:
StringsPreprocess( context::UserContext* u );
~StringsPreprocess();
-
- Node decompose( Node t, std::vector< Node > &new_nodes );
- void simplify(std::vector< Node > &vec_node);
+ //simplify a node
+ Node simplify( Node t, std::vector< Node > &new_nodes );
+ //recursive simplify
+ Node simplifyRec( Node t, std::vector< Node > &new_nodes, std::map< Node, Node >& visited );
+ //simplify each node in vec_node
+ void processAssertions(std::vector< Node > &vec_node);
};
}/* CVC4::theory::strings namespace */
norn-31.smt2 \
strings-native-simple.cvc \
cmu-2db2-extf-reg.smt2 \
- norn-nel-bug-052116.smt2
+ norn-nel-bug-052116.smt2 \
+ cmu-disagree-0707-dd.smt2
FAILING_TESTS =
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun url () String)
+
+(assert
+(and
+(and
+(and
+(and
+
+(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0)
+
+(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http")))
+(> (str.indexof url ":" 0) 0))
+(>= (- (str.indexof url "#" 2) 2) 0))
+(>= (str.indexof url ":" 0) 0))
+)
+
+(check-sat)
+
projects / cvc5.git / commitdiff