From 7736abe3b9c898033737865f033cc5cfe0f7922f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 24 Jun 2014 01:40:17 -0400 Subject: Squashed commit of the following: * Fix a bug in intersection * merging... * add delayed length lemmas * PreRegisterTerm is changed. * Bug fix for string-opt2 * PreRegisterTerm is changed. * add delayed length lemmas * Bug fix for string-opt2 * PreRegisterTerm is changed. * Bug fix for string-opt2 * PreRegisterTerm is changed. * Bug fix for string-opt2 * PreRegisterTerm is changed. --- src/theory/strings/regexp_operation.cpp | 11 + src/theory/strings/theory_strings.cpp | 574 ++++++++++++++++++-------------- src/theory/strings/theory_strings.h | 15 +- 3 files changed, 351 insertions(+), 249 deletions(-) (limited to 'src') diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 18df0f759..092c7e166 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1220,6 +1220,17 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se cset.clear(); firstChars(r1, cset, vset); std::vector< Node > vec_nodes; + Node delta_exp; + int flag = delta(r1, delta_exp); + int flag2 = delta(r2, delta_exp); + if(flag != 2 && flag2 != 2) { + if(flag == 1 && flag2 == 1) { + vec_nodes.push_back(d_emptySingleton); + } else { + //TODO + spflag = true; + } + } for(std::set::const_iterator itr = cset.begin(); itr != cset.end(); itr++) { CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0f9def3ea..f3134789f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -43,7 +43,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_nf_pairs(c), d_loop_antec(u), d_length_intro_vars(u), - d_prereg_cached(u), + d_registed_terms_cache(u), d_length_nodes(u), d_length_inst(u), d_str_pos_ctn(c), @@ -249,7 +249,7 @@ Node TheoryStrings::explain( TNode literal ){ void TheoryStrings::presolve() { - Trace("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl; + Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl; d_opt_fmf = options::stringFMF(); } @@ -273,14 +273,16 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { //step 1 : get all values for known lengths std::vector< Node > lts_values; std::map< unsigned, bool > values_used; - for( unsigned i=0; i0 ) Trace("strings-model") << ", "; + for( unsigned j=0; j0 ) { + Trace("strings-model") << ", "; + } Trace("strings-model") << col[i][j]; } Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl; - if( lts[i].isConst() ){ + if( lts[i].isConst() ) { lts_values.push_back( lts[i] ); unsigned lvalue = lts[i].getConst().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; @@ -388,19 +390,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { m->assertEquality( nodes[i], cc, true ); } } - Trace("strings-model") << "String Model : Assigned." << std::endl; - //check for negative contains - /* - Trace("strings-model") << "String Model : Check Neg Contains, size = " << d_str_neg_ctn.size() << std::endl; - for( unsigned i=0; igetValue(x); - //Node yv = m->getValue(y); - //Trace("strings-model") << "String Model : Check Neg contains Value: ~contains(" << xv << ", " << yv << ")." << std::endl; - } - */ + //Trace("strings-model") << "String Model : Assigned." << std::endl; Trace("strings-model") << "String Model : Finished." << std::endl; } @@ -408,8 +398,9 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// +/* void TheoryStrings::preRegisterTerm(TNode n) { - if(d_prereg_cached.find(n) == d_prereg_cached.end()) { + if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) { Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl; //collectTerms( n ); switch (n.getKind()) { @@ -466,7 +457,39 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } } - d_prereg_cached.insert(n); + 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); + break; + case kind::STRING_IN_REGEXP: + d_equalityEngine.addTriggerPredicate(n); + break; + //case kind::STRING_SUBSTR_TOTAL: + default: { + if( n.getType().isString() ) { + registerTerm(n); + // 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); + } + } + } + d_registed_terms_cache.insert(n); } } @@ -486,12 +509,10 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { } Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero); + Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one); + Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one); + Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], d_one); return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); break; } @@ -511,9 +532,8 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero); - Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero); + Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], d_zero); + Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]); Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]); @@ -530,8 +550,6 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { void TheoryStrings::check(Effort e) { - //Assert( d_pending.empty() ); - bool polarity; TNode atom; @@ -574,32 +592,36 @@ void TheoryStrings::check(Effort e) { } } doPendingFacts(); + d_terms_cache.clear(); bool addedLemma = false; if( e == EFFORT_FULL && !d_conflict ) { - addedLemma = checkSimple(); - Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if( !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; + //addedLemma = checkSimple(); + //Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + //if( !addedLemma ) { + addedLemma = checkNormalForms(); + Trace("strings-process") << "Done check normal forms, 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; - if( !d_conflict && !addedLemma ) { - addedLemma = checkMemberships(); - Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + 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; if( !d_conflict && !addedLemma ) { - addedLemma = checkCardinality(); - Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + 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; + } } } } - } + //} } + if(!d_conflict && !d_terms_cache.empty()) { + appendTermLemma(); } Trace("strings-check") << "Theory of strings, done check : " << e << std::endl; Assert( d_pending.empty() ); @@ -629,7 +651,7 @@ TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake /** Conflict when merging two constants */ void TheoryStrings::conflict(TNode a, TNode b){ if( !d_conflict ){ - Trace("strings-conflict-debug") << "Making conflict..." << std::endl; + Debug("strings-conflict") << "Making conflict..." << std::endl; d_conflict = true; Node conflictNode; if (a.getKind() == kind::CONST_BOOLEAN) { @@ -727,6 +749,8 @@ void TheoryStrings::assertPendingFact(Node fact, Node exp) { if (atom.getKind() == kind::EQUAL) { for( unsigned j=0; j<2; j++ ) { if( !d_equalityEngine.hasTerm( atom[j] ) ) { + //TODO: check!!! + registerTerm( atom[j] ); d_equalityEngine.addTerm( atom[j] ); } } @@ -762,6 +786,7 @@ void TheoryStrings::doPendingFacts() { d_pending.clear(); d_pending_exp.clear(); } + void TheoryStrings::doPendingLemmas() { if( !d_conflict && !d_lemma_cache.empty() ){ for( unsigned i=0; i & visited, std } //successfully computed normal form if( nf.size()!=1 || nf[0]!=d_emptyString ) { - for( unsigned r=0; rmkNode( kind::EQUAL, n[i], nr ) ); + nf_exp_n.push_back( n[i].eqNode( nr ) ); } if( !nresult ) { //Trace("strings-process-debug") << "....Caused already asserted @@ -871,7 +898,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std } } if( !result ) { - Trace("strings-process-debug") << "Will have cycle lemma at higher level!!!!!!!!!!!!!!!!" << std::endl; + Trace("strings-process-debug") << "Will have cycle lemma at higher level!" << std::endl; //we have a normal form that will cause a component lemma at a higher level normal_forms.clear(); normal_forms_exp.clear(); @@ -880,7 +907,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std normal_forms.push_back(nf_n); normal_forms_exp.push_back(nf_exp_n); normal_form_src.push_back(n); - if( !result ){ + if( !result ) { return false; } } else { @@ -901,35 +928,41 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std } // Test the result - if( !normal_forms.empty() ) { - Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; - for( unsigned i=0; i0) Trace("strings-solve") << ", "; - Trace("strings-solve") << normal_forms[i][j]; - } - Trace("strings-solve") << std::endl; - Trace("strings-solve") << " Explanation is : "; - if(normal_forms_exp[i].size() == 0) { - Trace("strings-solve") << "NONE"; - } else { - for( unsigned j=0; j0) Trace("strings-solve") << " AND "; - Trace("strings-solve") << normal_forms_exp[i][j]; + if(Trace.isOn("strings-solve")) { + if( !normal_forms.empty() ) { + Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; + for( unsigned i=0; i0) { + Trace("strings-solve") << ", "; + } + Trace("strings-solve") << normal_forms[i][j]; } + Trace("strings-solve") << std::endl; + Trace("strings-solve") << " Explanation is : "; + if(normal_forms_exp[i].size() == 0) { + Trace("strings-solve") << "NONE"; + } else { + for( unsigned j=0; j0) { + Trace("strings-solve") << " AND "; + } + Trace("strings-solve") << normal_forms_exp[i][j]; + } + } + Trace("strings-solve") << std::endl; } - Trace("strings-solve") << std::endl; + } else { + //std::vector< Node > nf; + //nf.push_back( eqc ); + //normal_forms.push_back(nf); + //std::vector< Node > nf_exp_def; + //normal_forms_exp.push_back(nf_exp_def); + //normal_form_src.push_back(eqc); + Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl; } - } else { - //std::vector< Node > nf; - //nf.push_back( eqc ); - //normal_forms.push_back(nf); - //std::vector< Node > nf_exp_def; - //normal_forms_exp.push_back(nf_exp_def); - //normal_form_src.push_back(eqc); - Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl; } return true; } @@ -1046,10 +1079,10 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, //require that x is non-empty if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){ //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop - sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop-X-E-Split" ); + sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Len-Split(Loop-X)" ); } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING ) { //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop - sendSplit( t_yz, d_emptyString, "Loop-YZ-E-SPlit" ); + sendSplit( t_yz, d_emptyString, "Len-Split(Loop-YZ)" ); } else { //need to break antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() ); @@ -1091,7 +1124,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, restr = mkConcat( z, y ); cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) )); } else { - cc = Rewriter::rewrite(s_zy.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z, y) )); + cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( z, y) )); } if(cc == d_false) { continue; @@ -1107,14 +1140,13 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, } conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc); } else { - Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl; + Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl; //right - Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); - Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); - d_statistics.d_new_skolems += 3; + Node sk_w= mkSkolemS( "w_loop" ); + Node sk_y= mkSkolemS( "y_loop", 1 ); + Node sk_z= mkSkolemS( "z_loop" ); //t1 * ... * tn = y * z - Node conc1 = t_yz.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + Node conc1 = t_yz.eqNode( mkConcat( sk_y, sk_z ) ); // s1 * ... * sk = z * y * r vec_r.insert(vec_r.begin(), sk_y); vec_r.insert(vec_r.begin(), sk_z); @@ -1128,8 +1160,8 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, std::vector< Node > vec_conc; vec_conc.push_back(conc1); vec_conc.push_back(conc2); vec_conc.push_back(conc3); vec_conc.push_back(str_in_re); - vec_conc.push_back(sk_y.eqNode(d_emptyString).negate()); - conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );//, len_x_gt_len_y + //vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems + conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc ); } // normal case //set its antecedant to ant, to say when it is relevant @@ -1137,11 +1169,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, d_regexp_ant[str_in_re] = ant; } - //if(conc.isNull() || conc == d_false || conc.getKind() == kind::OR) { - sendLemma( ant, conc, "LOOP-BREAK" ); - //} else { - //sendInfer( ant, conc, "LOOP-BREAK" ); - //} + sendLemma( ant, conc, "F-LOOP" ); ++(d_statistics.d_loop_lemmas); //we will be done @@ -1208,7 +1236,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl; //try to make the lengths equal via splitting on demand - sendSplit( length_term_i, length_term_j, "Length" ); + sendSplit( length_term_i, length_term_j, "Len-Split(Diseq)" ); length_eq = Rewriter::rewrite( length_eq ); d_pending_req_phase[ length_eq ] = true; return true; @@ -1251,98 +1279,37 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms Node other_str = normal_forms[nconst_k][nconst_index_k]; Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." ); Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." ); - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - //Opt - bool optflag = false; - if( normal_forms[nconst_k].size() > nconst_index_k + 1 && - normal_forms[nconst_k][nconst_index_k + 1].isConst() ) { - CVC4::String stra = const_str.getConst(); - CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst(); + if( !areDisequal(other_str, d_emptyString) ) { + sendSplit( other_str, d_emptyString, "Len-Split(CST)" ); + } else { + Assert(areDisequal(other_str, d_emptyString), "CST Split on empty Var"); + antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() ); + Node xnz = other_str.eqNode(d_emptyString).negate(); + antec.push_back( xnz ); + Node ant = mkExplain( antec ); + Node sk = mkSkolemS( "c_spt" ); Node conc; - Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" ); - if(stra == strb) { - conc = other_str.eqNode( d_emptyString ); + if( normal_forms[nconst_k].size() > nconst_index_k + 1 && + normal_forms[nconst_k][nconst_index_k + 1].isConst() ) { + CVC4::String stra = const_str.getConst(); + CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst(); CVC4::String stra1 = stra.substr(1); - std::size_t p = stra1.overlap(strb); - Node eq = p==0? other_str.eqNode( mkConcat(const_str, sk) ) - : other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, stra.size() - p) ), sk) ); - conc = NodeManager::currentNM()->mkNode(kind::OR, conc, eq); - Trace("strings-csp") << "Case 1: EQ " << stra << " = " << strb << std::endl; - } else if(stra.size() == 1) { - conc = other_str.eqNode( mkConcat(const_str, sk) ); - if(strb.size()>0 && stra[0] == strb[0]) { - conc = NodeManager::currentNM()->mkNode(kind::OR, conc, other_str.eqNode(d_emptyString)); - } - Trace("strings-csp") << "Case 8: Single Char " << stra << " vs " << strb << std::endl; + size_t p = stra.size() - stra1.overlap(strb); + size_t p2 = stra1.find(strb); + p = p2==std::string::npos? p : ( p>p2+1? p2+1 : p ); + Node prea = p==stra.size()? const_str : NodeManager::currentNM()->mkConst(stra.substr(0, p)); + conc = other_str.eqNode( mkConcat(prea, sk) ); + Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << std::endl; } else { - CVC4::String fc = strb.substr(0, 1); - std::size_t p; - if((p=stra.find(fc)) != std::string::npos) { - if( (p = stra.find(strb)) == std::string::npos ) { - if((p = stra.overlap(strb)) == 0) { - conc = other_str.eqNode( mkConcat(const_str, sk) ); - Trace("strings-csp") << "Case 2: No Substr/Overlap " << stra << " vs " << strb << std::endl; - } else { - conc = other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, stra.size() - p) ), sk) ); - Trace("strings-csp") << "Case 3: No Substr but Overlap " << stra << " vs " << strb << std::endl; - } - } else { - if(p == 0) { - conc = other_str.eqNode( d_emptyString ); - CVC4::String stra1 = stra.substr(1); - if((p = stra1.find(strb)) != std::string::npos) { - Node eq = other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, p + 1) ), sk) ); - conc = NodeManager::currentNM()->mkNode(kind::OR, conc, eq); - Trace("strings-csp") << "Case 4: Substr at beginning only " << stra << " vs " << strb << std::endl; - } else { - p = stra1.overlap(strb); - Node eq = p==0? other_str.eqNode( mkConcat(const_str, sk) ) - : other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, stra.size() - p) ), sk) ); - conc = NodeManager::currentNM()->mkNode(kind::OR, conc, eq); - Trace("strings-csp") << "Case 5: Substr again " << stra << " vs " << strb << std::endl; - } - } else { - conc = other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, p - 1) ), sk) ); - Trace("strings-csp") << "Case 6: Substr not at beginning " << stra << " vs " << strb << std::endl; - } - } - } else { - conc = other_str.eqNode( mkConcat(const_str, sk) ); - Trace("strings-csp") << "Case 7: No intersection " << stra << " vs " << strb << std::endl; - } + // normal v/c split + Node firstChar = const_str.getConst().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); + conc = other_str.eqNode( mkConcat(firstChar, sk) ); + Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (normal) " << std::endl; } - Node ant = mkExplain( antec ); - conc = Rewriter::rewrite( conc ); - //if(conc.getKind() == kind::OR) { - sendLemma(ant, conc, "CST-EPS-Split"); - //} else { - // sendInfer(ant, conc, "CST-EPS"); - //} - optflag = true; - /* - if( stra.find(fc) == std::string::npos || - (stra.find(strb) == std::string::npos && - !stra.overlap(strb)) ) { - Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" ); - Node eq = other_str.eqNode( mkConcat(const_str, sk) ); - Node ant = mkExplain( antec ); - sendLemma(ant, eq, "CST-EPS"); - optflag = true; - }*/ - } - if(!optflag) { - Node firstChar = const_str.getConst().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); - //split the string - Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); - Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false ); - d_pending_req_phase[ eq1 ] = true; - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - Node ant = mkExplain( antec ); - sendLemma( ant, conc, "CST-SPLIT" ); - ++(d_statistics.d_eq_splits); + conc = Rewriter::rewrite( conc ); + sendLemma(ant, conc, "S-Split(CST-P)"); } return true; } else { @@ -1367,13 +1334,14 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms } } - Node eq1 = mkSplitEq( "v_spt_l", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); - Node eq2 = mkSplitEq( "v_spt_r", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Node sk = mkSkolemS( "v_spt", 1 ); + Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) ); + Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) ); + conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 )); Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "VAR-SPLIT" ); - ++(d_statistics.d_eq_splits); + sendLemma( ant, conc, "S-Split(VAR)" ); + //++(d_statistics.d_eq_splits); return true; } } @@ -1493,6 +1461,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal conc = eqn[0].eqNode( eqn[1] ); Node ant = mkExplain( antec ); sendLemma( ant, conc, "ENDPOINT" ); + //sendInfer( ant, conc, "ENDPOINT" ); return true; }else{ index_i = normal_forms[i].size(); @@ -1557,6 +1526,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v for( unsigned i=0; i conc; - Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit", ni.getType(), "created for disequality normalization" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit", ni.getType(), "created for disequality normalization" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit", ni.getType(), "created for disequality normalization" ); - d_statistics.d_new_skolems += 3; - //Node nemp = sk1.eqNode(d_emptyString).negate(); + Node sk1 = mkSkolemS( "x_dsplit" ); + Node sk2 = mkSkolemS( "y_dsplit" ); + Node sk3 = mkSkolemS( "z_dsplit", 1 ); + //Node nemp = sk3.eqNode(d_emptyString).negate(); //conc.push_back(nemp); - //nemp = sk2.eqNode(d_emptyString).negate(); - //conc.push_back(nemp); - Node nemp = sk3.eqNode(d_emptyString).negate(); - conc.push_back(nemp); Node lsk1 = getLength( sk1 ); conc.push_back( lsk1.eqNode( li ) ); Node lsk2 = getLength( sk2 ); @@ -1693,14 +1658,14 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { Assert( !areDisequal( i, j ) ); //splitting on demand : try to make them disequal Node eq = i.eqNode( j ); - sendSplit( i, j, "D-EQL-Split" ); + sendSplit( i, j, "S-Split(DEQL)" ); eq = Rewriter::rewrite( eq ); d_pending_req_phase[ eq ] = false; return true; }else{ //splitting on demand : try to make lengths equal Node eq = li.eqNode( lj ); - sendSplit( li, lj, "D-UNK-Split" ); + sendSplit( li, lj, "D-Split" ); eq = Rewriter::rewrite( eq ); d_pending_req_phase[ eq ] = true; return true; @@ -1749,6 +1714,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); conc = Rewriter::rewrite( conc ); sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty"); + //sendInfer(mkExplain( ant ), conc, "Disequality Normalize Empty"); return -1; } else { Node i = nfi[index]; @@ -1844,6 +1810,73 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { return false; } +bool TheoryStrings::registerTerm( Node n ) { + if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) { + Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl; + if(n.getType().isString()) { + if(n.getKind() == kind::STRING_SUBSTR_TOTAL) { + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), + NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); + Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero); + Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, n[2], d_zero); + Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); + Node sk1 = mkSkolemS( "ss1", 2 ); + Node sk3 = mkSkolemS( "ss3", 2 ); + Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) ); + Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) ); + Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond, + NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ), + n.eqNode(d_emptyString))); + Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl; + d_out->lemma(lemma); + } + if( 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_statistics.d_splits); + d_out->lemma(n_len_geq_zero); + d_out->requirePhase( n_len_eq_z, true ); + d_length_intro_vars.insert(n); + } + } else { + if( d_length_nodes.find(n)==d_length_nodes.end() ) { + Node sk = mkSkolemS("lsym", 2); + Node eq = Rewriter::rewrite( sk.eqNode(n) ); + Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; + d_out->lemma(eq); + 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); + } + } + d_registed_terms_cache.insert(n); + return true; + } else { + AlwaysAssert(false, "String Terms only in registerTerm."); + } + } + return false; +} + void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { if( conc.isNull() || conc == d_false ) { d_out->conflict(ant); @@ -1884,12 +1917,60 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) { } Node TheoryStrings::mkConcat( Node n1, Node n2 ) { - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) ); + Node ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) ); + collectTerm(ret); + return ret; +} + +Node TheoryStrings::mkConcat( Node n1, Node n2, Node n3 ) { + Node ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2, n3 ) ); + collectTerm(ret); + return ret; +} + +Node TheoryStrings::mkConcat( const std::vector< Node >& c ) { + Node ret = Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) + : ( c.size()==1 ? c[0] : d_emptyString ) ); + collectTerm(ret); + return ret; +} + +//isLenSplit: 0-yes, 1-no, 2-ignore +Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) { + Node n = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), "string sko" ); + ++(d_statistics.d_new_skolems); + if(isLenSplit == 0) { + 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_statistics.d_splits); + d_out->lemma(n_len_geq_zero); + d_out->requirePhase( n_len_eq_z, true ); + } else if(isLenSplit == 1) { + d_equalityEngine.assertEquality(n.eqNode(d_emptyString), false, d_true); + Node len_n_gt_z = NodeManager::currentNM()->mkNode(kind::GT, + NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n), d_zero); + Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z << std::endl; + d_out->lemma(len_n_gt_z); + } + d_length_intro_vars.insert(n); + return n; } -Node TheoryStrings::mkConcat( std::vector< Node >& c ) { - Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); - return Rewriter::rewrite( cc ); +void TheoryStrings::collectTerm( Node n ) { + if(d_registed_terms_cache.find(n) == d_registed_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); + } } Node TheoryStrings::mkExplain( std::vector< Node >& a ) { @@ -1902,7 +1983,7 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) for( unsigned i=0; i& a, std::vector< Node >& an ) if( exp ) { unsigned ps = antec_exp.size(); explain(a[i], antec_exp); - Trace("strings-solve-debug") << "Done, explanation was : " << std::endl; + Debug("strings-explain") << "Done, explanation was : " << std::endl; for( unsigned j=ps; jmkNode( kind::STRING_CONCAT, nf ); + nf_term = mkConcat( nf ); } nf_term = Rewriter::rewrite( nf_term ); Trace("strings-debug") << "Make nf_term_exp..." << std::endl; @@ -2113,7 +2194,7 @@ bool TheoryStrings::checkNormalForms() { //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; //two equivalence classes have same normal form, merge Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] ); + Node eq = eqc.eqNode( nf_to_eqc[nf_term] ); sendInfer( eq_exp, eq, "Normal_Form" ); //d_equalityEngine.assertEquality( eq, true, eq_exp ); } else { @@ -2124,13 +2205,16 @@ bool TheoryStrings::checkNormalForms() { Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl; } - Trace("strings-nf-debug") << "**** 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-debug") << " normal_form(" << it->second << ") = " << it->first << std::endl; + if(Debug.isOn("strings-nf")) { + Debug("strings-nf") << "**** Normal forms are : " << std::endl; + for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){ + Debug("strings-nf") << " normal_form(" << it->second << ") = " << it->first << std::endl; + } + Debug("strings-nf") << std::endl; } - Trace("strings-nf-debug") << std::endl; - addedFact = !d_pending.empty(); - doPendingFacts(); + + addedFact = !d_pending.empty(); + doPendingFacts(); } while ( !d_conflict && d_lemma_cache.empty() && addedFact ); //process disequalities between equivalence classes @@ -2532,7 +2616,7 @@ bool TheoryStrings::checkMemberships() { vec_s2.push_back(x[s2i]); } Node s1 = x[0]; - Node s2 = vec_s2.size()==1? vec_s2[0]: NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, vec_s2); + Node s2 = mkConcat(vec_s2); for(unsigned int i=0; imkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first); Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second); @@ -2633,17 +2717,17 @@ bool TheoryStrings::checkMemberships() { }else{ Trace("strings-regexp-debug") << "Case 2\n"; std::vector< Node > conc_c; - Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" ); - Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" ); - Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" ); - Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" ); - conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12)); + Node s11 = mkSkolemS( "s11" ); + Node s12 = mkSkolemS( "s12" ); + Node s21 = mkSkolemS( "s21" ); + Node s22 = mkSkolemS( "s22" ); + conc = p1.eqNode( mkConcat(s11, s12) ); conc_c.push_back(conc); - conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22)); + conc = p2.eqNode( mkConcat(s21, s22) ); conc_c.push_back(conc); conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r); conc_c.push_back(conc); - conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]); + conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, mkConcat(s12, s21), r[0]); conc_c.push_back(conc); conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r); conc_c.push_back(conc); @@ -2675,7 +2759,7 @@ bool TheoryStrings::checkMemberships() { Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj); Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj)); Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate(); - Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]).negate(); + Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, mkConcat(s12, s21), r[0]).negate(); Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate(); conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3); conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc); @@ -2808,10 +2892,9 @@ bool TheoryStrings::checkPosContains() { Node s = atom[1]; if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) { if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1", s.getType(), "created for contain" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2", s.getType(), "created for contain" ); - d_statistics.d_new_skolems += 2; - Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) ); + Node sk1 = mkSkolemS( "sc1" ); + Node sk2 = mkSkolemS( "sc2" ); + Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); sendLemma( atom, eq, "POS-INC" ); addedLemma = true; d_pos_ctn_cached.insert( atom ); @@ -2977,6 +3060,7 @@ bool TheoryStrings::deriveRegExp( Node x, Node r, Node ant ) { CVC4::String c = s.substr(i, 1); Node dc2; int rt = d_regexp_opr.derivativeS(dc, c, dc2); + dc = dc2; if(rt == 0) { //TODO } else if(rt == 2) { @@ -2996,17 +3080,17 @@ bool TheoryStrings::deriveRegExp( Node x, Node r, Node ant ) { for(unsigned int i=1; imkNode( kind::STRING_CONCAT, vec_nodes ); + Node left = mkConcat( vec_nodes ); left = Rewriter::rewrite( left ); conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc ); - std::vector< Node > sdc; + /*std::vector< Node > sdc; d_regexp_opr.simplify(conc, sdc, true); if(sdc.size() == 1) { conc = sdc[0]; } else { conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc)); - } + }*/ } } sendLemma(ant, conc, "RegExp-Derive"); @@ -3204,19 +3288,15 @@ void TheoryStrings::assertNode( Node lit ) { } Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ) { - Node sk = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), info ); - d_statistics.d_new_skolems += 1; + Node sk = mkSkolemS( c, (lgtZero?1:0) ); //NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), info ); Node cc = mkConcat( rhs, sk ); - //if(rhs.isConst()) { - // d_length_inst[cc] = lhs; - //} - Node eq = lhs.eqNode( cc ); - eq = Rewriter::rewrite( eq ); + Node eq = Rewriter::rewrite( lhs.eqNode( cc ) ); + /* if( lgtZero ) { - Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); + Node sk_gt_zero = sk.eqNode(d_emptyString).negate(); Trace("strings-lemma") << "Strings::Lemma SK-NON-EMPTY: " << sk_gt_zero << std::endl; d_lemma_cache.push_back( sk_gt_zero ); - } + }*/ return eq; } @@ -3245,4 +3325,4 @@ TheoryStrings::Statistics::~Statistics(){ }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ -}/* CVC4 namespace */ +}/* CVC4 namespace */ \ No newline at end of file diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 2a33b400e..de5f62b1a 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -164,7 +164,11 @@ private: NodeSet d_loop_antec; NodeSet d_length_intro_vars; // preReg cache - NodeSet d_prereg_cached; + NodeSet d_registed_terms_cache; + // term cache + std::vector< Node > d_terms_cache; + void collectTerm( Node n ); + void appendTermLemma(); ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -271,12 +275,19 @@ protected: void doPendingFacts(); void doPendingLemmas(); + //register term + bool registerTerm( Node n ); + //send lemma void sendLemma( Node ant, Node conc, const char * c ); void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); /** mkConcat **/ inline Node mkConcat( Node n1, Node n2 ); - inline Node mkConcat( std::vector< Node >& c ); + inline Node mkConcat( Node n1, Node n2, Node n3 ); + inline Node mkConcat( const std::vector< Node >& c ); + //mkSkolem + inline Node mkSkolemS(const char * c, int isLenSplit = 0); + //inline Node mkSkolemI(const char * c); /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); -- cgit v1.2.3