From d41b88cdec616e56310492efcda9c553008661d0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 27 Sep 2015 13:20:03 +0200 Subject: [PATCH] Improved handling of extended operators. Do preprocess on memberships eagerly, only process contains/memberships that have non-constant arguments. Cleanup. --- src/smt/smt_engine.cpp | 22 +- src/theory/strings/options | 3 + src/theory/strings/theory_strings.cpp | 586 ++++++++++------ src/theory/strings/theory_strings.h | 24 +- .../strings/theory_strings_preprocess.cpp | 638 +++++++++--------- .../strings/theory_strings_preprocess.h | 7 +- test/regress/regress0/strings/Makefile.am | 3 +- test/regress/regress0/strings/ilc-l-nt.smt2 | 14 + 8 files changed, 739 insertions(+), 558 deletions(-) create mode 100755 test/regress/regress0/strings/ilc-l-nt.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ae93176b2..337c5104c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3294,18 +3294,16 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } - if( !options::stringLazyPreproc() ){ - if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; - dumpAssertions("pre-strings-pp", d_assertions); - CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertions.ref() ); - //for (unsigned i = 0; i < d_assertions.size(); ++ i) { - // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); - //} - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; - dumpAssertions("post-strings-pp", d_assertions); - } + if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; + dumpAssertions("pre-strings-pp", d_assertions); + CVC4::theory::strings::StringsPreprocess sp; + sp.simplify( d_assertions.ref() ); + //for (unsigned i = 0; i < d_assertions.size(); ++ i) { + // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); + //} + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; + dumpAssertions("post-strings-pp", d_assertions); } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; diff --git a/src/theory/strings/options b/src/theory/strings/options index 8a839a118..21e1a7e4d 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -35,4 +35,7 @@ option stringIgnNegMembership strings-inm --strings-inm bool :default false option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true perform string preprocessing lazily +option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false + strings length greater than zero lemmas + endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 507c74c53..444115af4 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,6 +26,8 @@ #include "theory/strings/type_enumerator.h" #include +#define LAZY_ADD_MEMBERSHIP + using namespace std; using namespace CVC4::context; @@ -44,14 +46,14 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_nf_pairs(c), d_loop_antec(u), d_length_intro_vars(u), - d_registed_terms_cache(u), - d_length_inst(u), - d_str_pos_ctn(c), - d_str_neg_ctn(c), + d_registered_terms_cache(u), + d_preproc_cache(u), + d_proxy_var(u), d_neg_ctn_eqlen(u), d_neg_ctn_ulen(u), d_pos_ctn_cached(u), d_neg_ctn_cached(u), + d_ext_func_terms(c), d_regexp_memberships(c), d_regexp_ucached(u), d_regexp_ccached(c), @@ -330,7 +332,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { Trace("strings-model") << col[i][j] << " "; //check if col[i][j] has only variables EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false ); - Node cst = ei ? ei->d_const_term : Node::null(); + Node cst = ei ? ei->d_const_term : Node::null(); if( cst.isNull() ){ Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() ); if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){ @@ -414,72 +416,20 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// -/* + void TheoryStrings::preRegisterTerm(TNode n) { - if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) { - Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl; - //collectTerms( n ); - switch (n.getKind()) { - case kind::EQUAL: - d_equalityEngine.addTriggerEquality(n); - break; - case kind::STRING_IN_REGEXP: - //do not add trigger here - d_equalityEngine.addTriggerPredicate(n); - break; - case 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::GEQ, n[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" ); - d_statistics.d_new_skolems += 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; - d_out->lemma(lemma); - //d_equalityEngine.addTerm(n); - } - default: { - if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) { - if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) { - Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); - Node n_len_eq_z = n_len.eqNode( d_zero ); - n_len_eq_z = Rewriter::rewrite( n_len_eq_z ); - Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z, - NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); - Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl; - d_out->lemma(n_len_geq_zero); - d_out->requirePhase( n_len_eq_z, true ); - } - // FMF - if( n.getKind() == kind::VARIABLE && options::stringFMF() ) { - d_input_vars.insert(n); - } - } - if (n.getType().isBoolean()) { - // Get triggered for both equal and dis-equal - d_equalityEngine.addTriggerPredicate(n); - } else { - // Function applications/predicates - d_equalityEngine.addTerm(n); - } + if( d_registered_terms_cache.find(n) == d_registered_terms_cache.end() ) { + //check for logic exceptions + if( !options::stringExp() ){ + if( n.getKind()==kind::STRING_STRIDOF || + n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS || + n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 || + n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){ + std::stringstream ss; + ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp"; + throw LogicException(ss.str()); } } - d_registed_terms_cache.insert(n); - } -} -*/ - -void TheoryStrings::preRegisterTerm(TNode n) { - if( d_registed_terms_cache.find(n) == d_registed_terms_cache.end() ) { switch( n.getKind() ) { case kind::EQUAL: { d_equalityEngine.addTriggerEquality(n); @@ -509,7 +459,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } } - d_registed_terms_cache.insert(n); + d_registered_terms_cache.insert(n); } } @@ -600,20 +550,39 @@ void TheoryStrings::check(Effort e) { polarity = fact.getKind() != kind::NOT; atom = polarity ? fact : fact[0]; - //run preprocess + //run preprocess on memberships + bool addFact = true; if( options::stringLazyPreproc() ){ - std::map< Node, Node >::iterator itp = d_preproc_cache.find( atom ); - if( itp==d_preproc_cache.end() ){ + NodeBoolMap::const_iterator it = d_preproc_cache.find( atom ); + if( it==d_preproc_cache.end() ){ + d_preproc_cache[ atom ] = true; std::vector< Node > new_nodes; Node res = d_preproc.decompose( atom, new_nodes ); - d_preproc_cache[atom] = res; if( atom!=res ){ - Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl; - Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res ); - plem = Rewriter::rewrite( plem ); - d_out->lemma( plem ); - Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl; - Trace("strings-pp-lemma") << "...from " << fact << std::endl; + //check if reduction/deduction + std::vector< Node > subs_lhs; + std::vector< Node > subs_rhs; + subs_lhs.push_back( atom ); + subs_rhs.push_back( d_true ); + Node sres = res.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + sres = Rewriter::rewrite( sres ); + if( sres!=res ){ + Node plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres ); + plem = Rewriter::rewrite( plem ); + d_out->lemma( plem ); + Trace("strings-pp-lemma") << "Preprocess impl lemma : " << plem << std::endl; + Trace("strings-pp-lemma") << "...from " << fact << std::endl; + }else{ + Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl; + Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res ); + plem = Rewriter::rewrite( plem ); + d_out->lemma( plem ); + Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl; + Trace("strings-pp-lemma") << "...from " << fact << std::endl; + //reduced by preprocess + addFact = false; + d_preproc_cache[ atom ] = false; + } }else{ Trace("strings-assertion-debug") << "...preprocess ok." << std::endl; } @@ -625,26 +594,13 @@ void TheoryStrings::check(Effort e) { Trace("strings-pp-lemma") << "...from " << fact << std::endl; d_out->lemma( nnlem ); } + }else{ + addFact = (*it).second; } } - - //must record string in regular expressions - if ( atom.getKind() == kind::STRING_IN_REGEXP ) { - addMembership(assertion); - //if(polarity || !options::stringIgnNegMembership()) { - d_equalityEngine.assertPredicate(atom, polarity, fact); - //} - } else if (atom.getKind() == kind::STRING_STRCTN) { - if(polarity) { - d_str_pos_ctn.push_back( atom ); - } else { - d_str_neg_ctn.push_back( atom ); - } - d_equalityEngine.assertPredicate(atom, polarity, fact); - } else if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.assertEquality(atom, polarity, fact); - } else { - d_equalityEngine.assertPredicate(atom, polarity, fact); + //assert pending fact + if( addFact ){ + assertPendingFact( atom, polarity, fact ); } } doPendingFacts(); @@ -654,28 +610,28 @@ void TheoryStrings::check(Effort e) { bool addedLemma = false; if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) { Trace("strings-check") << "Theory of strings full effort check " << std::endl; - //addedLemma = checkSimple(); - //Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - //if( !addedLemma ) { + addedLemma = checkExtendedFuncsEval(); + Trace("strings-process") << "Done check extended functions eval, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if( !d_conflict && !addedLemma ){ addedLemma = checkNormalForms(); Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { addedLemma = checkLengthsEqc(); Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { - addedLemma = checkContains(); - Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + addedLemma = checkExtendedFuncs(); + Trace("strings-process") << "Done check extended functions, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !d_conflict && !addedLemma ) { - addedLemma = checkMemberships(); - Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if( !d_conflict && !addedLemma ) { - addedLemma = checkCardinality(); - Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - } + addedLemma = checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + //if( !d_conflict && !addedLemma ) { + // addedLemma = checkExtendedFuncsReduction(); + // Trace("strings-process") << "Done check extended functions reductions, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + //} } } } - //} + } Trace("strings-check") << "Theory of strings done full effort check " << addedLemma << " " << d_conflict << std::endl; } if(!d_conflict && !d_terms_cache.empty()) { @@ -801,32 +757,36 @@ void TheoryStrings::computeCareGraph(){ Theory::computeCareGraph(); } -void TheoryStrings::assertPendingFact(Node fact, Node exp) { - Trace("strings-pending") << "Assert pending fact : " << fact << " from " << exp << std::endl; - bool polarity = fact.getKind() != kind::NOT; - TNode atom = polarity ? fact : fact[0]; +void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { + Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl; Assert(atom.getKind() != kind::OR, "Infer error: a split."); - if (atom.getKind() == kind::EQUAL) { + if( atom.getKind()==kind::EQUAL ){ + //AJR : is this necessary? for( unsigned j=0; j<2; j++ ) { - if( !d_equalityEngine.hasTerm( atom[j] ) ) { + if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) { //TODO: check!!! - registerTerm( atom[j] ); - d_equalityEngine.addTerm( atom[j] ); + registerTerm( atom[j] ); } } d_equalityEngine.assertEquality( atom, polarity, exp ); } else { - if ( atom.getKind() == kind::STRING_IN_REGEXP ) { - addMembership(fact); - } else if (atom.getKind() == kind::STRING_STRCTN) { - if(polarity) { - d_str_pos_ctn.push_back( atom ); - } else { - d_str_neg_ctn.push_back( atom ); + if( atom.getKind()==kind::STRING_IN_REGEXP ) { +#ifdef LAZY_ADD_MEMBERSHIP + if( d_ext_func_terms.find( atom )==d_ext_func_terms.end() ){ + Trace("strings-extf-debug") << "Found extended function (membership) : " << atom << std::endl; + d_ext_func_terms[atom] = true; } +#else + addMembership( polarity ? atom : atom.negate() ); +#endif } d_equalityEngine.assertPredicate( atom, polarity, exp ); } + //collect extended function terms in the atom + if( options::stringExp() ){ + std::map< Node, bool > visited; + collectExtendedFuncTerms( atom, visited ); + } } void TheoryStrings::doPendingFacts() { @@ -836,10 +796,14 @@ void TheoryStrings::doPendingFacts() { Node exp = d_pending_exp[ fact ]; if(fact.getKind() == kind::AND) { for(size_t j=0; j > &normal //nf_exp is conjunction bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { - Trace("strings-process") << "Process equivalence class " << eqc << std::endl; + Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl; if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){ getConcatVec( eqc, nf ); - Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; + Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already visited." << std::endl; return false; } else if( areEqual( eqc, d_emptyString ) ) { eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); @@ -1602,7 +1566,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v ++eqc_i; } //do nothing - Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl; + Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl; d_normal_forms_base[eqc] = d_emptyString; d_normal_forms[eqc].clear(); d_normal_forms_exp[eqc].clear(); @@ -1646,9 +1610,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0]; d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() ); d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() ); - Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl; + Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl; } else { - Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl; + Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl; nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() ); nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() ); result = true; @@ -1880,7 +1844,7 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { } bool TheoryStrings::registerTerm( Node n ) { - if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) { + if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) { Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl; if(n.getType().isString()) { if(n.getKind() == kind::STRING_SUBSTR_TOTAL) { @@ -1910,6 +1874,7 @@ bool TheoryStrings::registerTerm( Node n ) { Node sk = mkSkolemS("lsym", 2); Node eq = Rewriter::rewrite( sk.eqNode(n) ); Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; + d_proxy_var[n] = sk; d_out->lemma(eq); Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); Node lsum; @@ -1932,7 +1897,7 @@ bool TheoryStrings::registerTerm( Node n ) { d_equalityEngine.assertEquality( ceq, true, d_true ); } } - d_registed_terms_cache.insert(n); + d_registered_terms_cache.insert(n); return true; } else { AlwaysAssert(false, "String Terms only in registerTerm."); @@ -1948,9 +1913,11 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict" << std::endl; d_conflict = true; } else { - Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); + Node lem; if( ant == d_true ) { lem = conc; + }else{ + lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); } Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl; Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl; @@ -1997,6 +1964,13 @@ void TheoryStrings::sendLengthLemma( Node n ){ d_out->lemma(n_len_geq_zero); d_out->requirePhase( n_len_eq_z, true ); d_out->requirePhase( n_len_eq_z_2, true ); + + //AJR: probably a good idea + if( options::stringLenGeqZ() ){ + Node n_len_geq = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero); + n_len_geq = Rewriter::rewrite( n_len_geq ); + d_out->lemma( n_len_geq ); + } } Node TheoryStrings::mkConcat( Node n1, Node n2 ) { @@ -2037,16 +2011,15 @@ Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) { } void TheoryStrings::collectTerm( Node n ) { - if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) { + if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) { d_terms_cache.push_back(n); } } void TheoryStrings::appendTermLemma() { - for(std::vector< Node >::const_iterator it=d_terms_cache.begin(); - it!=d_terms_cache.begin();it++) { - registerTerm(*it); + for(std::vector< Node >::const_iterator it=d_terms_cache.begin(); it!=d_terms_cache.begin();it++) { + registerTerm(*it); } } @@ -2124,64 +2097,6 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { c.push_back( n ); } } -/* -bool TheoryStrings::checkSimple() { - bool addedLemma = false; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ) { - Node eqc = (*eqcs_i); - if (eqc.getType().isString()) { - //EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); - //get the constant for the equivalence class - //int c_len = ...; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ) { - Node n = (*eqc_i); - //length axiom - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { - if( d_length_nodes.find(n)==d_length_nodes.end() ) { - Trace("strings-dassert-debug") << "get n: " << n << endl; - Node sk; - //if( d_length_inst.find(n)==d_length_inst.end() ) { - //Node nr = d_equalityEngine.getRepresentative( n ); - sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" ); - d_statistics.d_new_skolems += 1; - d_length_intro_vars.insert( sk ); - Node eq = sk.eqNode(n); - eq = Rewriter::rewrite(eq); - Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; - d_out->lemma(eq); - //} else { - // sk = d_length_inst[n]; - //} - Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node lsum; - if( n.getKind() == kind::STRING_CONCAT ) { - std::vector node_vec; - for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); - node_vec.push_back(lni); - } - lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); - } else if( n.getKind() == kind::CONST_STRING ) { - lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); - } - Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) ); - Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; - d_out->lemma(ceq); - addedLemma = true; - - d_length_nodes.insert(n); - } - } - ++eqc_i; - } - } - ++eqcs_i; - } - return addedLemma; -} - */ bool TheoryStrings::checkNormalForms() { Trace("strings-process") << "Normalize equivalence classes...." << std::endl; @@ -2244,7 +2159,7 @@ bool TheoryStrings::checkNormalForms() { getEquivalenceClasses( eqcs ); for( unsigned i=0; i visited; std::vector< Node > nf; std::vector< Node > nf_exp; @@ -2279,7 +2194,7 @@ bool TheoryStrings::checkNormalForms() { eqc_to_exp[eqc] = nf_term_exp; } } - Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl; + Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; } if(Debug.isOn("strings-nf")) { @@ -3279,21 +3194,222 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma return true; } -bool TheoryStrings::checkContains() { - bool addedLemma = checkPosContains(); +bool TheoryStrings::checkExtendedFuncsEval() { + bool addedLemma = false; + Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl; + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + if( (*it).second ){ + //check if all children are in eqc with a constant, if so, we can rewrite + Node n = (*it).first; + Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl; + std::vector< Node > children; + std::vector< Node > exp; + std::map< Node, Node > visited; + for( unsigned i=0; imkNode( n.getKind(), children ); + Node nrc = Rewriter::rewrite( nr ); + Assert( nrc.isConst() ); + Node nrs = getSymbolicDefinition( nr ); + Node conc; + if( !nrs.isNull() ){ + Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; + exp.clear(); + if( !areEqual( nrs, nrc ) ){ + //infer symbolic unit + if( n.getType().isBoolean() ){ + conc = nrc==d_true ? nrs : nrs.negate(); + }else{ + conc = nrs.eqNode( nrc ); + } + } + }else{ + if( !areEqual( n, nrc ) ){ + if( n.getType().isBoolean() ){ + exp.push_back( n ); + conc = d_false; + }else{ + conc = n.eqNode( nrc ); + } + } + } + if( !conc.isNull() ){ + Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; + if( n.getType().isInteger() || exp.empty() ){ + sendLemma( mkExplain( exp ), conc, "EXTF" ); + addedLemma = true; + }else{ + sendInfer( mkExplain( exp ), conc, "EXTF" ); + } + if( d_conflict ){ + return true; + } + } + }else{ + Trace("strings-extf-debug") << " unresolved ext function : " << n << std::endl; + } + } + } + doPendingFacts(); + if( addedLemma ){ + doPendingLemmas(); + return true; + }else{ + return false; + } +} + +Node TheoryStrings::inferConstantDefinition( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited ) { + if( n.isConst() ){ + return n; + }else{ + Node nr = getRepresentative( n ); + std::map< Node, Node >::iterator it = visited.find( nr ); + if( it==visited.end() ){ + visited[nr] = Node::null(); + if( nr.isConst() ){ + exp.push_back( n.eqNode( nr ) ); + visited[nr] = nr; + return nr; + }else{ + EqcInfo* ei = n.getType().isString() ? getOrMakeEqcInfo( nr, false ) : NULL; + if( ei && !ei->d_const_term.get().isNull() ){ + exp.push_back( n.eqNode( ei->d_const_term.get() ) ); + visited[nr] = ei->d_const_term.get(); + return ei->d_const_term.get(); + }else{ + //scan the equivalence class + if( d_equalityEngine.hasTerm( nr ) ){ + eq::EqClassIterator eqc_i = eq::EqClassIterator( nr, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + if( (*eqc_i).isConst() ){ + visited[nr] = *eqc_i; + return *eqc_i; + } + ++eqc_i; + } + } + if( n.getNumChildren()>0 ){ + std::vector< Node > children; + for( unsigned i=0; imkNode( n.getKind(), children ); + visited[nr] = ret; + return ret; + } + } + } + } + }else{ + return it->second; + } + } + return Node::null(); +} + +Node TheoryStrings::getSymbolicDefinition( Node n ) { + if( n.getNumChildren()==0 ){ + NodeNodeMap::const_iterator it = d_proxy_var.find( n ); + if( it==d_proxy_var.end() ){ + return Node::null(); + }else{ + return (*it).second; + } + }else{ + std::vector< Node > children; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back( n.getOperator() ); + } + for( unsigned i=0; imkNode( n.getKind(), children ); + } +} + +bool TheoryStrings::checkExtendedFuncs() { + std::map< bool, std::vector< Node > > pnContains; + std::map< bool, std::vector< Node > > pnMem; + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + if( (*it).second ){ + Node n = (*it).first; + if( n.getKind()==kind::STRING_STRCTN ) { + bool pol = areEqual( n, d_true ); + Assert( pol || areEqual( n, d_false ) ); + pnContains[pol].push_back( n ); + } +#ifdef LAZY_ADD_MEMBERSHIP + else if( n.getKind()==kind::STRING_IN_REGEXP ) { + bool pol = areEqual( n, d_true ); + Assert( pol || areEqual( n, d_false ) ); + pnMem[pol].push_back( n ); + } +#endif + } + } + + bool addedLemma = checkPosContains( pnContains[true] ); Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { - addedLemma = checkNegContains(); + addedLemma = checkNegContains( pnContains[false] ); Trace("strings-process") << "Done check negative contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if(!d_conflict && !addedLemma) { + Trace("strings-process") << "Adding memberships..." << std::endl; + //add all non-evaluated memberships +#ifdef LAZY_ADD_MEMBERSHIP + for( std::map< bool, std::vector< Node > >::iterator it=pnMem.begin(); it != pnMem.end(); ++it ){ + for( unsigned i=0; isecond.size(); i++ ){ + addMembership( it->first ? it->second[i] : it->second[i].negate() ); + } + } +#endif + addedLemma = checkMemberships(); + Trace("strings-process") << "Done check memberships, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + } } return addedLemma; } -bool TheoryStrings::checkPosContains() { +bool TheoryStrings::checkPosContains( std::vector< Node >& posContains ) { bool addedLemma = false; - for( unsigned i=0; i& negContains ) { bool addedLemma = false; //check for conflicts - for( unsigned i=0; imkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) ); @@ -3346,8 +3462,8 @@ bool TheoryStrings::checkNegContains() { if( !d_conflict ){ //check for lemmas if(options::stringExp()) { - for( unsigned i=0; i new_nodes; + Node res = d_preproc.decompose( n, new_nodes ); + Assert( res==n ); + 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-pp-lemma") << "Reduction lemma : " << nnlem << std::endl; + Trace("strings-pp-lemma") << "...from term " << n << std::endl; + d_out->lemma( nnlem ); + addedLemmas = true; + } + } + } + } + } + } + */ + return addedLemmas; +} + + CVC4::String TheoryStrings::getHeadConst( Node x ) { if( x.isConst() ) { return x.getConst< String >(); @@ -3730,6 +3878,24 @@ Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node return eq; } +void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==kind::STRING_SUBSTR_TOTAL || n.getKind()==kind::STRING_STRIDOF || + n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS || + n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 || + 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-debug") << "Found extended function : " << n << std::endl; + d_ext_func_terms[n] = true; + } + } + for( unsigned i=0; i d_terms_cache; void collectTerm( Node n ); void appendTermLemma(); // preprocess cache StringsPreprocess d_preproc; - std::map< Node, Node > d_preproc_cache; + NodeBoolMap d_preproc_cache; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -213,7 +213,7 @@ private: std::map< Node, EqcInfo* > d_eqc_info; EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); //maintain which concat terms have the length lemma instantiated - NodeNodeMap d_length_inst; + NodeNodeMap d_proxy_var; private: void mergeCstVec(std::vector< Node > &vec_strings); bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, @@ -264,9 +264,13 @@ private: bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp); - bool checkContains(); - bool checkPosContains(); - bool checkNegContains(); + bool checkExtendedFuncs(); + bool checkPosContains( std::vector< Node >& posContains ); + bool checkNegContains( std::vector< Node >& negContains ); + bool checkExtendedFuncsEval(); + Node inferConstantDefinition( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited ); + Node getSymbolicDefinition( Node n ); + bool checkExtendedFuncsReduction(); public: void preRegisterTerm(TNode n); @@ -288,7 +292,7 @@ protected: void computeCareGraph(); //do pending merges - void assertPendingFact(Node fact, Node exp); + void assertPendingFact(Node atom, bool polarity, Node exp); void doPendingFacts(); void doPendingLemmas(); @@ -327,12 +331,14 @@ private: Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ); // Special String Functions - NodeList d_str_pos_ctn; - NodeList d_str_neg_ctn; NodeSet d_neg_ctn_eqlen; NodeSet d_neg_ctn_ulen; NodeSet d_pos_ctn_cached; NodeSet d_neg_ctn_cached; + //extended string terms and whether they have been reduced + NodeBoolMap d_ext_func_terms; + //collect extended operator terms + void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ); // Symbolic Regular Expression private: diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 581e2be0a..787979faa 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -150,7 +150,7 @@ int StringsPreprocess::checkFixLenVar( Node t ) { } return ret; } -Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { +Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ) { std::hash_map::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; @@ -158,6 +158,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl; Node retNode = t; + if( options::stringLazyPreproc() ){ + //only process extended operators after preprocess + if( during_pp && ( t.getKind() == kind::STRING_SUBSTR_TOTAL || t.getKind() == kind::STRING_STRIDOF || + t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS || + t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 || + t.getKind() == kind::STRING_STRREPL ) ){ + return t; + } + } + /*int c_id = checkFixLenVar(t); if( c_id != 2 ) { int v_id = 1 - c_id; @@ -181,7 +191,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } } else */ if( t.getKind() == kind::STRING_IN_REGEXP ) { - Node t0 = simplify( t[0], new_nodes ); + Node t0 = simplify( t[0], new_nodes, during_pp ); //rewrite it std::vector< Node > ret; @@ -206,347 +216,329 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ), t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) )); new_nodes.push_back( lemma ); - retNode = t; d_cache[t] = t; } else if( t.getKind() == kind::STRING_STRIDOF ) { - if(options::stringExp()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" ); - 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 sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" ); - Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "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::GEQ, skk, negone ); - new_nodes.push_back( krange ); - krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) ); - new_nodes.push_back( krange ); - krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) ); - new_nodes.push_back( krange ); - krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ, - t[2], d_zero) ); - new_nodes.push_back( krange ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" ); + 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 sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" ); + Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "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::GEQ, skk, negone ); + new_nodes.push_back( krange ); + krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) ); + new_nodes.push_back( krange ); + krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) ); + new_nodes.push_back( krange ); + krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ, + t[2], d_zero) ); + new_nodes.push_back( krange ); - //str.len(s1) < y + str.len(s2) - Node c1 = Rewriter::rewrite(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 = Rewriter::rewrite(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, - NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2, - NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero, - NodeManager::currentNM()->mkNode(kind::MINUS, - NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]), - NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))), - 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 = Rewriter::rewrite(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 ); - if( options::stringLazyPreproc() ){ - new_nodes.push_back( t.eqNode( skk ) ); - d_cache[t] = Node::null(); - }else{ - d_cache[t] = skk; - retNode = skk; - } - } else { - throw LogicException("string indexof not supported in default mode, try --strings-exp"); + //str.len(s1) < y + str.len(s2) + Node c1 = Rewriter::rewrite(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 = Rewriter::rewrite(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, + NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2, + NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero, + NodeManager::currentNM()->mkNode(kind::MINUS, + NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]), + NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))), + 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 = Rewriter::rewrite(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 ); + if( options::stringLazyPreproc() ){ + new_nodes.push_back( t.eqNode( skk ) ); + d_cache[t] = Node::null(); + }else{ + d_cache[t] = skk; + retNode = skk; } } else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) { - if(options::stringExp()) { - //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 lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); + //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 lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); - Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero); - if(t.getKind()==kind::STRING_U16TOS) { - nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0])); - Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp); - new_nodes.push_back(lencond); - } else if(t.getKind()==kind::STRING_U32TOS) { - nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0])); - Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp); - new_nodes.push_back(lencond); - } + Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero); + if(t.getKind()==kind::STRING_U16TOS) { + nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0])); + Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp); + new_nodes.push_back(lencond); + } else if(t.getKind()==kind::STRING_U32TOS) { + nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0])); + Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp); + new_nodes.push_back(lencond); + } - Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(), - pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero) - ); - new_nodes.push_back(lem); + Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(), + pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero) + ); + new_nodes.push_back(lem); - //non-neg - 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::GT, lenp, b1 ) ) ); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); - Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); + //non-neg + 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::GT, lenp, b1 ) ) ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); + Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->integerType()); - Node ufP = NodeManager::currentNM()->mkSkolem("ufP", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->integerType()), - "uf type conv P"); - Node ufM = NodeManager::currentNM()->mkSkolem("ufM", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->integerType()), - "uf type conv M"); + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->integerType()); + Node ufP = NodeManager::currentNM()->mkSkolem("ufP", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf type conv P"); + Node ufM = NodeManager::currentNM()->mkSkolem("ufM", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf type conv M"); - lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)); - new_nodes.push_back( lem ); + lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)); + new_nodes.push_back( lem ); - Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1); - Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)); - Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1); - Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero); - Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS, - NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten), - NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) )); - cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1); - Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one)); - Node cc2 = ufx.eqNode(ufMx); - cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2); - // leading zero - Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate()); - Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero)); - //cc3 - Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); - Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); + Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1); + Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)); + Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1); + Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero); + Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS, + NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten), + NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) )); + cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1); + Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one)); + Node cc2 = ufx.eqNode(ufMx); + cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2); + // leading zero + Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate()); + Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero)); + //cc3 + Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); + Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); - Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); - Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22); + Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); + Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); + Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22); - Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode( - NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) )); - Node ch = - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), - NodeManager::currentNM()->mkConst(::CVC4::String("0")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), - NodeManager::currentNM()->mkConst(::CVC4::String("1")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))), - NodeManager::currentNM()->mkConst(::CVC4::String("2")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))), - NodeManager::currentNM()->mkConst(::CVC4::String("3")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))), - NodeManager::currentNM()->mkConst(::CVC4::String("4")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))), - NodeManager::currentNM()->mkConst(::CVC4::String("5")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))), - NodeManager::currentNM()->mkConst(::CVC4::String("6")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))), - NodeManager::currentNM()->mkConst(::CVC4::String("7")), - NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))), - NodeManager::currentNM()->mkConst(::CVC4::String("8")), - NodeManager::currentNM()->mkConst(::CVC4::String("9"))))))))))); - Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) ); - Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22)); - std::vector< Node > svec; - svec.push_back(cc1);svec.push_back(cc2); - svec.push_back(cc21); - svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5); - Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) ); - conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); - conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); - conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc ); - new_nodes.push_back( conc ); + Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode( + NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) )); + Node ch = + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), + NodeManager::currentNM()->mkConst(::CVC4::String("0")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), + NodeManager::currentNM()->mkConst(::CVC4::String("1")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))), + NodeManager::currentNM()->mkConst(::CVC4::String("2")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))), + NodeManager::currentNM()->mkConst(::CVC4::String("3")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))), + NodeManager::currentNM()->mkConst(::CVC4::String("4")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))), + NodeManager::currentNM()->mkConst(::CVC4::String("5")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))), + NodeManager::currentNM()->mkConst(::CVC4::String("6")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))), + NodeManager::currentNM()->mkConst(::CVC4::String("7")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))), + NodeManager::currentNM()->mkConst(::CVC4::String("8")), + NodeManager::currentNM()->mkConst(::CVC4::String("9"))))))))))); + Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) ); + Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22)); + std::vector< Node > svec; + svec.push_back(cc1);svec.push_back(cc2); + svec.push_back(cc21); + svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5); + Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) ); + conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); + conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); + conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc ); + new_nodes.push_back( conc ); - /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES, - NodeManager::currentNM()->mkNode(kind::LT, 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; - } - } else { - throw LogicException("string int.to.str not supported in default mode, try --strings-exp"); + /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES, + NodeManager::currentNM()->mkNode(kind::LT, 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; } } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) { - if(options::stringExp()) { - Node str = t[0]; - Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str); - Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str); + Node str = t[0]; + Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str); + Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str); - Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); - Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->integerType()); - Node ufP = NodeManager::currentNM()->mkSkolem("ufP", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->integerType()), - "uf type conv P"); - Node ufM = NodeManager::currentNM()->mkSkolem("ufM", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->integerType()), - "uf type conv M"); + Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); + Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->integerType()); + Node ufP = NodeManager::currentNM()->mkSkolem("ufP", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf type conv P"); + Node ufM = NodeManager::currentNM()->mkSkolem("ufM", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf type conv M"); - //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero); - //new_nodes.push_back(pret.eqNode(ufP0)); - //lemma - Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, - str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))), - pret.eqNode(negone)); + //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero); + //new_nodes.push_back(pret.eqNode(ufP0)); + //lemma + Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, + str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))), + pret.eqNode(negone)); + new_nodes.push_back(lem); + /*lem = NodeManager::currentNM()->mkNode(kind::IFF, + t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))), + t.eqNode(d_zero)); + new_nodes.push_back(lem);*/ + if(t.getKind()==kind::STRING_U16TOS) { + lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp); new_nodes.push_back(lem); - /*lem = NodeManager::currentNM()->mkNode(kind::IFF, - t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))), - t.eqNode(d_zero)); - new_nodes.push_back(lem);*/ - if(t.getKind()==kind::STRING_U16TOS) { - lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp); - new_nodes.push_back(lem); - } else if(t.getKind()==kind::STRING_U32TOS) { - lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp); - new_nodes.push_back(lem); - } - //cc1 - Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))); - //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1); - //cc2 - std::vector< Node > vec_n; - Node p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType()); - Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero); - vec_n.push_back(g); - g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p); + } else if(t.getKind()==kind::STRING_U32TOS) { + lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp); + new_nodes.push_back(lem); + } + //cc1 + Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))); + //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1); + //cc2 + std::vector< Node > vec_n; + Node p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType()); + Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero); + vec_n.push_back(g); + g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p); + vec_n.push_back(g); + Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one); + char chtmp[2]; + chtmp[1] = '\0'; + for(unsigned i=0; i<=9; i++) { + chtmp[0] = i + '0'; + std::string stmp(chtmp); + g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate(); vec_n.push_back(g); - Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one); - char chtmp[2]; - chtmp[1] = '\0'; - for(unsigned i=0; i<=9; i++) { - chtmp[0] = i + '0'; - std::string stmp(chtmp); - g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate(); - vec_n.push_back(g); - } - Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n)); - //cc3 - Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2); - Node g2 = NodeManager::currentNM()->mkNode(kind::AND, - NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero), - NodeManager::currentNM()->mkNode(kind::GT, lenp, b2)); - Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2); - Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one)); - Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2); - std::vector< Node > vec_c3; - std::vector< Node > vec_c3b; - //qx between 0 and 9 - Node c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); - vec_c3b.push_back(c3cc); - c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); - vec_c3b.push_back(c3cc); - Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one); - for(unsigned i=0; i<=9; i++) { - chtmp[0] = i + '0'; - std::string stmp(chtmp); - c3cc = NodeManager::currentNM()->mkNode(kind::IFF, - ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))), - sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp)))); - vec_c3b.push_back(c3cc); - } - //c312 - Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero); - c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, - ufx.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, - NodeManager::currentNM()->mkNode(kind::MULT, ufx1, ten), - ufMx))); + } + Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n)); + //cc3 + Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); + Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2); + Node g2 = NodeManager::currentNM()->mkNode(kind::AND, + NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero), + NodeManager::currentNM()->mkNode(kind::GT, lenp, b2)); + Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2); + Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one)); + Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2); + std::vector< Node > vec_c3; + std::vector< Node > vec_c3b; + //qx between 0 and 9 + Node c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); + vec_c3b.push_back(c3cc); + c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); + vec_c3b.push_back(c3cc); + Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one); + for(unsigned i=0; i<=9; i++) { + chtmp[0] = i + '0'; + std::string stmp(chtmp); + c3cc = NodeManager::currentNM()->mkNode(kind::IFF, + ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))), + sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp)))); vec_c3b.push_back(c3cc); - c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b); - c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) ); - c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc); - vec_c3.push_back(c3cc); - //unbound - c3cc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, d_zero)); - vec_c3.push_back(c3cc); - Node lstx = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, one); - Node upflstx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, lstx); - c3cc = upflstx.eqNode(pret); - vec_c3.push_back(c3cc); - Node cc3 = NodeManager::currentNM()->mkNode(kind::AND, vec_c3); - 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; - } - } else { - throw LogicException("string int.to.str not supported in default mode, try --strings-exp"); + } + //c312 + Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero); + c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, + ufx.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, + NodeManager::currentNM()->mkNode(kind::MULT, ufx1, ten), + ufMx))); + vec_c3b.push_back(c3cc); + c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b); + c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) ); + c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc); + vec_c3.push_back(c3cc); + //unbound + c3cc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, d_zero)); + vec_c3.push_back(c3cc); + Node lstx = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, one); + Node upflstx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, lstx); + c3cc = upflstx.eqNode(pret); + vec_c3.push_back(c3cc); + Node cc3 = NodeManager::currentNM()->mkNode(kind::AND, vec_c3); + 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; } } else if( t.getKind() == kind::STRING_STRREPL ) { - if(options::stringExp()) { - Node x = t[0]; - Node y = t[1]; - Node z = t[2]; - Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" ); - Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" ); - Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); - Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); - Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); - Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, - NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1, - NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero, - NodeManager::currentNM()->mkNode(kind::MINUS, - NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), - NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate(); - Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3), - skw.eqNode(x) ) ); - 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; - } - } else { - throw LogicException("string replace not supported in default mode, try --strings-exp"); + Node x = t[0]; + Node y = t[1]; + Node z = t[2]; + Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" ); + Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" ); + Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); + Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); + Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); + Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, + NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1, + NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero, + NodeManager::currentNM()->mkNode(kind::MINUS, + NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), + NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate(); + Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, + NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3), + skw.eqNode(x) ) ); + 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; } } else{ d_cache[t] = Node::null(); - retNode = t; } /*if( t.getNumChildren()>0 ) { @@ -581,7 +573,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return retNode; } -Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) { +Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) { std::hash_map::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; @@ -589,7 +581,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) { unsigned num = t.getNumChildren(); if(num == 0) { - return simplify(t, new_nodes); + return simplify(t, new_nodes, during_pp); } else { bool changed = false; std::vector< Node > cc; @@ -597,7 +589,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) { cc.push_back(t.getOperator()); } for(unsigned i=0; i & new_nodes) { } if(changed) { Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); - return simplify(tmp, new_nodes); + return simplify(tmp, new_nodes, during_pp); } else { - return simplify(t, new_nodes); + return simplify(t, new_nodes, during_pp); } } } @@ -615,7 +607,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) { void StringsPreprocess::simplify(std::vector< Node > &vec_node) { for( unsigned i=0; i new_nodes; - Node curr = decompose( vec_node[i], new_nodes ); + Node curr = decompose( vec_node[i], new_nodes, true ); if( !new_nodes.empty() ){ new_nodes.insert( new_nodes.begin(), curr ); curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index d96644bee..1255d93e0 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -37,11 +37,12 @@ private: bool checkStarPlus( Node t ); int checkFixLenVar( Node t ); void processRegExp( Node s, Node r, std::vector< Node > &ret ); - Node simplify( Node t, std::vector< Node > &new_nodes ); + Node simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ); public: - Node decompose( Node t, std::vector< Node > &new_nodes ); - void simplify(std::vector< Node > &vec_node); StringsPreprocess(); + + Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false ); + void simplify(std::vector< Node > &vec_node); }; }/* CVC4::theory::strings namespace */ diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index b796fc80b..79efee6e0 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -52,13 +52,14 @@ TESTS = \ reloop.smt2 \ unsound-0908.smt2 \ ilc-like.smt2 \ + ilc-l-nt.smt2 \ + artemis-0512-nonterm.smt2 \ indexof-sym-simp.smt2 \ bug613.smt2 FAILING_TESTS = EXTRA_DIST = $(TESTS) \ - artemis-0512-nonterm.smt2 \ fmf001.smt2 \ type002.smt2 diff --git a/test/regress/regress0/strings/ilc-l-nt.smt2 b/test/regress/regress0/strings/ilc-l-nt.smt2 new file mode 100755 index 000000000..32dfc0b1b --- /dev/null +++ b/test/regress/regress0/strings/ilc-l-nt.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :strings-exp true) + +(declare-fun s () String) +(assert (or (= s "Id like cookies.") (= s "Id not like cookies."))) + +(declare-fun target () String) +(assert (or (= target "l") (= target "m"))) + +(declare-fun location () Int) +(assert (= (* 2 location) (str.indexof s target 0))) + +(check-sat) \ No newline at end of file -- 2.30.2