From: Andrew Reynolds Date: Wed, 5 Feb 2014 10:23:47 +0000 (-0600) Subject: Bug fix for theory strings related to old cycle detection code (was leading to bogus... X-Git-Tag: cvc5-1.0.0~7105 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ef5d5880ad48d3659db33477c08a45eba44aab0d;p=cvc5.git Bug fix for theory strings related to old cycle detection code (was leading to bogus model). Minor cleanup of QCF. --- diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 96ea46b6b..25a62a4e8 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -271,7 +271,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor //} } //now, generate the trigger... - int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + int matchOption = 0; Trigger* tr = NULL; if( d_is_single_trigger[ patTerms[0] ] ){ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 95744a651..4a5c92c7e 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -125,12 +125,12 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) { if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){ if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ //literals - if( n.getKind()==APPLY_UF ){ - flatten( n ); - }else if( n.getKind()==EQUAL ){ + if( n.getKind()==EQUAL ){ for( unsigned i=0; i& assign eqc_count[index]++; Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl; if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){ + //if( currIndex==0 ){ + // Assert( p->areEqual( p->d_model_basis[unassigned_tn[r][index]], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ); + // d_match_term[unassigned[r][index]] = p->d_model_basis[unassigned_tn[r][index]]; + //}else{ + d_match_term[unassigned[r][index]] = TNode::null(); + //} Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl; index++; }else{ @@ -559,14 +565,11 @@ void QuantInfo::debugPrintMatch( const char * c ) { } -/* -struct MatchGenSort { - MatchGen * d_mg; - bool operator() (int i,int j) { - return d_mg->d_children[i].d_typed_children[j].d_type; - } -}; -*/ +//void QuantInfo::addFuncParent( int v, Node f, int arg ) { +// if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){ +// d_f_parent[v][f].push_back( arg ); +// } +//} MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl; @@ -580,12 +583,15 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ d_type = typ_var; d_type_not = false; d_n = n; + //Node f = getOperator( n ); for( unsigned j=0; jisVar( nn ) ){ - Trace("qcf-qregister-debug") << " is var #" << qi->d_var_num[nn] << std::endl; - d_qni_var_num[d_qni_size] = qi->d_var_num[nn]; + int v = qi->d_var_num[nn]; + Trace("qcf-qregister-debug") << " is var #" << v << std::endl; + d_qni_var_num[d_qni_size] = v; + //qi->addFuncParent( v, f, j ); }else{ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl; d_qni_gterm[d_qni_size] = nn; @@ -640,10 +646,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ }else{ d_type = typ_invalid; //literals - if( d_n.getKind()==APPLY_UF ){ - Assert( qi->isVar( d_n ) ); - d_type = typ_pred; - }else if( d_n.getKind()==EQUAL ){ + if( d_n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){ Assert( qi->isVar( d_n[i] ) ); @@ -652,6 +655,11 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ } } d_type = typ_eq; + }else if( isHandledUfTerm( d_n ) ){ + Assert( qi->isVar( d_n ) ); + d_type = typ_pred; + }else{ + Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl; } } }else{ @@ -812,12 +820,13 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { } }else if( d_type==typ_var ){ Assert( isHandledUfTerm( d_n ) ); - Node f = d_n.getOperator(); + Node f = getOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f ); if( qni!=NULL ){ d_qn.push_back( qni ); } + d_matched_basis = false; }else if( d_type==typ_pred || d_type==typ_eq ){ //add initial constraint Node nn[2]; @@ -986,6 +995,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { //if not successful, clean up the variables you bound if( !success ){ if( d_type==typ_eq || d_type==typ_pred ){ + //clean up the constraints you added for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){ if( !it->second.isNull() ){ Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl; @@ -998,7 +1008,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_qni_bound_cons_var.clear(); d_qni_bound.clear(); }else{ - //clean up the match : remove equalities/disequalities + //clean up the matches you set for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){ Debug("qcf-match") << " Clean up bound var " << it->second << std::endl; Assert( it->secondgetNumVars() ); @@ -1007,6 +1017,17 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { } d_qni_bound.clear(); } + /* + if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){ + d_matched_basis = true; + Node f = getOperator( d_n ); + TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f ); + if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){ + success = true; + d_qni_bound[0] = d_qni_var_num[0]; + } + } + */ } Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl; return success; @@ -1124,7 +1145,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { if( d_qn.size()==d_qni.size()+1 ) { int index = (int)d_qni.size(); //initialize - Node val; + TNode val; std::map< int, int >::iterator itv = d_qni_var_num.find( index ); if( itv!=d_qni_var_num.end() ){ //get the representative variable this variable is equal to @@ -1213,7 +1234,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { //Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() ); //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl; Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() ); - Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first; + TNode t = d_qni[d_qni.size()-1]->second.d_children.begin()->first; Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl; //set the match terms for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){ @@ -1260,10 +1281,10 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledUfTerm( TNode n ) { - return n.getKind()==APPLY_UF; + return n.getKind()==APPLY_UF;// || n.getKind()==GEQ; } -Node MatchGen::getFunction( Node n ) { +Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { if( isHandledUfTerm( n ) ){ return n.getOperator(); }else{ @@ -1333,7 +1354,7 @@ int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) { //else if( d_effort>QuantConflictFind::effort_conflict ){ // ret = -1; //} - }else if( n.getKind()==APPLY_UF ){ //predicate + }else if( MatchGen::isHandledUfTerm( n ) ){ //predicate Node nn = evaluateTerm( n ); Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl; if( areEqual( nn, d_true ) ){ @@ -1402,7 +1423,7 @@ bool QuantConflictFind::isPropagationSet() { } bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) { - //if( d_effort==QuantConflictFind::effort_prop_deq ){ + //if( d_effort==QuantConflictFind::effort_mc ){ // return n1==n2 || !areDisequal( n1, n2 ); //}else{ return n1==n2; @@ -1449,17 +1470,18 @@ Node QuantConflictFind::getRepresentative( Node n ) { } Node QuantConflictFind::evaluateTerm( Node n ) { if( MatchGen::isHandledUfTerm( n ) ){ + Node f = MatchGen::getOperator( this, n ); Node nn; if( getEqualityEngine()->hasTerm( n ) ){ computeArgReps( n ); - nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] ); + nn = d_uf_terms[f].existsTerm( n, d_arg_reps[n] ); }else{ std::vector< TNode > args; for( unsigned i=0; i >::iterator itt = d_eqcs.find( rtn ); + if( itt==d_eqcs.end() ){ + Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn ); + if( !getEqualityEngine()->hasTerm( mb ) ){ + Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl; + Assert( false ); + } + Node mbr = getRepresentative( mb ); + if( mbr!=r ){ + d_eqcs[rtn].push_back( mbr ); + } + d_eqcs[rtn].push_back( r ); + d_model_basis[rtn] = mb; + }else{ + itt->second.push_back( r ); + } + }else{ + d_eqcs[rtn].push_back( r ); + } //EqcInfo * eqcir = getEqcInfo( r, false ); //get relevant nodes that we are disequal from /* @@ -1786,12 +1829,13 @@ void QuantConflictFind::computeRelevantEqr() { std::map< TNode, std::vector< TNode > >::iterator it_na; TNode fn; if( MatchGen::isHandledUfTerm( n ) ){ + Node f = MatchGen::getOperator( this, n ); computeArgReps( n ); it_na = d_arg_reps.find( n ); Assert( it_na!=d_arg_reps.end() ); - Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] ); + Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] ); isRedundant = (nadd!=n); - d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] ); + d_uf_terms[f].addTerm( n, d_arg_reps[n] ); }else{ isRedundant = false; } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 2663ff0b9..80e56acbd 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -65,6 +65,7 @@ private: std::map< int, int > d_qni_bound_cons_var; std::map< int, int >::iterator d_binding_it; //std::vector< int > d_independent; + bool d_matched_basis; bool d_binding; //int getVarBindingVar(); std::map< int, Node > d_ground_eval; @@ -99,7 +100,7 @@ public: // is this term treated as UF application? static bool isHandledUfTerm( TNode n ); - static Node getFunction( Node n ); + static Node getOperator( QuantConflictFind * p, Node n ); }; //info for quantifiers @@ -139,6 +140,9 @@ public: bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned ); void debugPrintMatch( const char * c ); bool isConstrainedVar( int v ); +//public: //optimization : relevant domain + //std::map< int, std::map< Node, std::vector< int > > > d_f_parent; + //void addFuncParent( int v, Node f, int arg ); }; class QuantConflictFind : public QuantifiersModule @@ -195,6 +199,7 @@ private: //for equivalence classes QcfNodeIndex * getQcfNodeIndex( Node f ); // type -> list(eqc) std::map< TypeNode, std::vector< TNode > > d_eqcs; + std::map< TypeNode, Node > d_model_basis; //mapping from UF terms to representatives of their arguments std::map< TNode, std::vector< TNode > > d_arg_reps; //compute arg reps diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 58344964c..4fa37a732 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -62,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); - + d_all_warning = true; d_regexp_incomplete = false; d_opt_regexp_gcd = true; @@ -285,7 +285,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { } ////step 2 : assign arbitrary values for unknown lengths? //for( unsigned i=0; imkConst( Rational( lvalue ) ); @@ -423,7 +423,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_out->requirePhase( n_len_eq_z, true ); } // FMF - if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && + if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && if( std::find(d_in_vars.begin(), d_in_vars.end(), n) == d_in_vars.end() ) { d_in_vars.push_back( n ); } @@ -673,29 +673,34 @@ void TheoryStrings::doPendingLemmas() { bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) { Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; - // EqcItr - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ) { - Node n = (*eqc_i); - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { - Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; - std::vector nf_n; - std::vector nf_exp_n; + // EqcItr + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { + Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; + std::vector nf_n; + std::vector nf_exp_n; bool result = true; - if( n.getKind() == kind::CONST_STRING ){ - if( n!=d_emptyString ) { - nf_n.push_back( n ); - } - } else if( n.getKind() == kind::STRING_CONCAT ) { - for( unsigned i=0; i nf_temp; - std::vector< Node > nf_exp_temp; - Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; - bool nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); - if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return true; - } + if( n.getKind() == kind::CONST_STRING ){ + if( n!=d_emptyString ) { + nf_n.push_back( n ); + } + } else if( n.getKind() == kind::STRING_CONCAT ) { + for( unsigned i=0; i nf_temp; + std::vector< Node > nf_exp_temp; + Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + bool nresult = false; + if( nr==eqc ){ + nf_temp.push_back( nr ); + }else{ + nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return true; + } + } //successfully computed normal form if( nf.size()!=1 || nf[0]!=d_emptyString ) { for( unsigned r=0; r & visited, std nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); } if( !nresult ){ - //Trace("strings-process-debug") << "....Caused already asserted + //Trace("strings-process-debug") << "....Caused already asserted for( unsigned j=i+1; j & visited, std break; } } + } + } + //if not equal to self + //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){ + if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { + if( nf_n.size()>1 ){ + Trace("strings-process-debug") << "Check for cycle lemma for normal form "; + printConcat(nf_n,"strings-process-debug"); + Trace("strings-process-debug") << "..." << std::endl; + for( unsigned i=0; i ant; + if( nf_n[i]!=n ){ + ant.push_back( nf_n[i].eqNode( n ) ); } + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + std::vector< Node > cc; + for( unsigned j=0; j empty_vec; + Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); + sendLemma( mkExplain( ant ), conc, "CYCLE" ); + return true; + } } - if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { - if( nf_n.size()>1 ){ - Trace("strings-process-debug") << "Check for cycle lemma for normal form "; - printConcat(nf_n,"strings-process-debug"); - Trace("strings-process-debug") << "..." << std::endl; - for( unsigned i=0; i ant; - if( nf_n[i]!=n ){ - ant.push_back( nf_n[i].eqNode( n ) ); - } - ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); - std::vector< Node > cc; - for( unsigned j=0; j empty_vec; - Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); - sendLemma( mkExplain( ant ), conc, "CYCLE" ); - return true; - } - } - } - if( !result ) { - //we have a normal form that will cause a component lemma at a higher level - normal_forms.clear(); - normal_forms_exp.clear(); - normal_form_src.clear(); - } - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); - if( !result ){ - return false; - } - } else { - Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; - //Assert( areEqual( nf_n[0], eqc ) ); - if( !areEqual( nn, eqc ) ){ - std::vector< Node > ant; - ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); - ant.push_back( n.eqNode( eqc ) ); - Node conc = nn.eqNode( eqc ); - sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); - return true; - } - } + } + if( !result ) { + 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(); + normal_form_src.clear(); + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + if( !result ){ + return false; + } + } else { + Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; + //Assert( areEqual( nf_n[0], eqc ) ); + if( !areEqual( nn, eqc ) ){ + std::vector< Node > ant; + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + ant.push_back( n.eqNode( eqc ) ); + Node conc = nn.eqNode( eqc ); + sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); + return true; + } } - ++eqc_i; + //} } + ++eqc_i; + } // Test the result if( !normal_forms.empty() ) { @@ -805,6 +814,14 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std } 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; } return true; } @@ -831,7 +848,7 @@ void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) { } bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, - int i, int j, int index_i, int index_j, + int i, int j, int index_i, int index_j, int &loop_in_i, int &loop_in_j) { int has_loop[2] = { -1, -1 }; if( options::stringLB() != 2 ) { @@ -859,7 +876,7 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms } } //xs(zy)=t(yz)xr -bool TheoryStrings::processLoop(std::vector< Node > &antec, +bool TheoryStrings::processLoop(std::vector< Node > &antec, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, int i, int j, int loop_n_index, int other_n_index, @@ -867,7 +884,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, Node conc; Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl; Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl; - + Trace("strings-loop") << " ... T(Y.Z)= "; std::vector< Node > vec_t; for(int lp=index; lp &antec, Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; //special case - str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) ); conc = str_in_re; @@ -963,13 +980,13 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, vec_r.insert(vec_r.begin(), sk_z); Node conc2 = s_zy.eqNode( mkConcat( vec_r ) ); Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) ); - str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - + //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); - + 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); @@ -1042,7 +1059,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms //check length(normal_forms[i][index]) == length(normal_forms[j][index]) if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) && - normal_forms[i][index_i].getKind()!=kind::CONST_STRING && + normal_forms[i][index_i].getKind()!=kind::CONST_STRING && normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) { //length terms are equal, merge equivalence classes if not already done so Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); @@ -1071,7 +1088,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms if(options::stringLB() == 0) { flag_lb = true; } else { - if(processLoop(c_lb_exp, normal_forms, normal_form_src, + if(processLoop(c_lb_exp, normal_forms, normal_form_src, c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) { return true; } @@ -1147,7 +1164,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms } } if(flag_lb) { - if(processLoop(c_lb_exp, normal_forms, normal_form_src, + if(processLoop(c_lb_exp, normal_forms, normal_form_src, c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) { return true; } @@ -1229,7 +1246,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); sendInfer( eq_exp, eq, "LengthEq" ); return true; - } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || + } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) { Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl; Node conc; @@ -1388,7 +1405,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { if( revRet!=0 ){ return revRet==-1; } - + nfi.clear(); nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); nfj.clear(); @@ -1410,7 +1427,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { Node lj = getLength( j ); if( areDisequal(li, lj) ){ //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){ - + Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl; //must add lemma std::vector< Node > antec; @@ -1436,7 +1453,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { conc.push_back( lsk2.eqNode( lj ) ); conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); - + sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" ); ++(d_statistics.d_deq_splits); return true; @@ -1771,7 +1788,7 @@ bool TheoryStrings::checkSimple() { Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" ); d_statistics.d_new_skolems += 2; - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] ); Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); @@ -1786,7 +1803,7 @@ bool TheoryStrings::checkSimple() { Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" ); d_statistics.d_new_skolems += 2; - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + 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); @@ -2244,7 +2261,7 @@ bool TheoryStrings::unrollStar( Node atom ) { } //|x|>|xp| - Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, + Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) ); @@ -2398,7 +2415,7 @@ bool TheoryStrings::checkNegContains() { argTypes.push_back(NodeManager::currentNM()->stringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->stringType()), "uf substr", @@ -2597,7 +2614,7 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) { //add the others as lemmas sendLemma( d_true, sdc[i], "RegExp-DEF"); } - + conc = sdc[0]; } } @@ -2683,7 +2700,7 @@ Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node d_var_split_graph_lhs[sk] = lhs; d_var_split_graph_rhs[sk] = rhs; //d_var_split_eq[sk] = eq; - + //int mpl = getMaxPossibleLength( sk ); Trace("strings-progress") << "Strings::Progress: Because of " << eq << std::endl; Trace("strings-progress") << "Strings::Progress: \t" << lhs << "(up:" << getMaxPossibleLength(lhs) << ") is removed" << std::endl;