if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
//literals\r
- if( n.getKind()==APPLY_UF ){\r
- flatten( n );\r
- }else if( n.getKind()==EQUAL ){\r
+ if( n.getKind()==EQUAL ){\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
flatten( n[i] );\r
}\r
+ }else if( MatchGen::isHandledUfTerm( n ) ){\r
+ flatten( n );\r
}\r
}\r
}\r
eqc_count[index]++;\r
Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;\r
if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){\r
+ //if( currIndex==0 ){\r
+ // Assert( p->areEqual( p->d_model_basis[unassigned_tn[r][index]], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) );\r
+ // d_match_term[unassigned[r][index]] = p->d_model_basis[unassigned_tn[r][index]];\r
+ //}else{\r
+ d_match_term[unassigned[r][index]] = TNode::null();\r
+ //}\r
Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl;\r
index++;\r
}else{\r
}\r
\r
\r
-/*\r
-struct MatchGenSort {\r
- MatchGen * d_mg;\r
- bool operator() (int i,int j) {\r
- return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;\r
- }\r
-};\r
-*/\r
+//void QuantInfo::addFuncParent( int v, Node f, int arg ) {\r
+// if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){\r
+// d_f_parent[v][f].push_back( arg );\r
+// }\r
+//}\r
\r
MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){\r
Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;\r
d_type = typ_var;\r
d_type_not = false;\r
d_n = n;\r
+ //Node f = getOperator( n );\r
for( unsigned j=0; j<d_n.getNumChildren(); j++ ){\r
Node nn = d_n[j];\r
Trace("qcf-qregister-debug") << " " << d_qni_size;\r
if( qi->isVar( nn ) ){\r
- Trace("qcf-qregister-debug") << " is var #" << qi->d_var_num[nn] << std::endl;\r
- d_qni_var_num[d_qni_size] = qi->d_var_num[nn];\r
+ int v = qi->d_var_num[nn];\r
+ Trace("qcf-qregister-debug") << " is var #" << v << std::endl;\r
+ d_qni_var_num[d_qni_size] = v;\r
+ //qi->addFuncParent( v, f, j );\r
}else{\r
Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
d_qni_gterm[d_qni_size] = nn;\r
}else{\r
d_type = typ_invalid;\r
//literals\r
- if( d_n.getKind()==APPLY_UF ){\r
- Assert( qi->isVar( d_n ) );\r
- d_type = typ_pred;\r
- }else if( d_n.getKind()==EQUAL ){\r
+ if( d_n.getKind()==EQUAL ){\r
for( unsigned i=0; i<2; i++ ){\r
if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
Assert( qi->isVar( d_n[i] ) );\r
}\r
}\r
d_type = typ_eq;\r
+ }else if( isHandledUfTerm( d_n ) ){\r
+ Assert( qi->isVar( d_n ) );\r
+ d_type = typ_pred;\r
+ }else{\r
+ Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;\r
}\r
}\r
}else{\r
}\r
}else if( d_type==typ_var ){\r
Assert( isHandledUfTerm( d_n ) );\r
- Node f = d_n.getOperator();\r
+ Node f = getOperator( p, d_n );\r
Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;\r
QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f );\r
if( qni!=NULL ){\r
d_qn.push_back( qni );\r
}\r
+ d_matched_basis = false;\r
}else if( d_type==typ_pred || d_type==typ_eq ){\r
//add initial constraint\r
Node nn[2];\r
//if not successful, clean up the variables you bound\r
if( !success ){\r
if( d_type==typ_eq || d_type==typ_pred ){\r
+ //clean up the constraints you added\r
for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
if( !it->second.isNull() ){\r
Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;\r
d_qni_bound_cons_var.clear();\r
d_qni_bound.clear();\r
}else{\r
- //clean up the match : remove equalities/disequalities\r
+ //clean up the matches you set\r
for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;\r
Assert( it->second<qi->getNumVars() );\r
}\r
d_qni_bound.clear();\r
}\r
+ /*\r
+ if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){\r
+ d_matched_basis = true;\r
+ Node f = getOperator( d_n );\r
+ TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f );\r
+ if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){\r
+ success = true;\r
+ d_qni_bound[0] = d_qni_var_num[0];\r
+ }\r
+ }\r
+ */\r
}\r
Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
return success;\r
if( d_qn.size()==d_qni.size()+1 ) {\r
int index = (int)d_qni.size();\r
//initialize\r
- Node val;\r
+ TNode val;\r
std::map< int, int >::iterator itv = d_qni_var_num.find( index );\r
if( itv!=d_qni_var_num.end() ){\r
//get the representative variable this variable is equal to\r
//Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
//Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;\r
Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
- Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;\r
+ TNode t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;\r
Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl;\r
//set the match terms\r
for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
}\r
\r
bool MatchGen::isHandledUfTerm( TNode n ) {\r
- return n.getKind()==APPLY_UF;\r
+ return n.getKind()==APPLY_UF;// || n.getKind()==GEQ;\r
}\r
\r
-Node MatchGen::getFunction( Node n ) {\r
+Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {\r
if( isHandledUfTerm( n ) ){\r
return n.getOperator();\r
}else{\r
//else if( d_effort>QuantConflictFind::effort_conflict ){\r
// ret = -1;\r
//}\r
- }else if( n.getKind()==APPLY_UF ){ //predicate\r
+ }else if( MatchGen::isHandledUfTerm( n ) ){ //predicate\r
Node nn = evaluateTerm( n );\r
Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;\r
if( areEqual( nn, d_true ) ){\r
}\r
\r
bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {\r
- //if( d_effort==QuantConflictFind::effort_prop_deq ){\r
+ //if( d_effort==QuantConflictFind::effort_mc ){\r
// return n1==n2 || !areDisequal( n1, n2 );\r
//}else{\r
return n1==n2;\r
}\r
Node QuantConflictFind::evaluateTerm( Node n ) {\r
if( MatchGen::isHandledUfTerm( n ) ){\r
+ Node f = MatchGen::getOperator( this, n );\r
Node nn;\r
if( getEqualityEngine()->hasTerm( n ) ){\r
computeArgReps( n );\r
- nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
+ nn = d_uf_terms[f].existsTerm( n, d_arg_reps[n] );\r
}else{\r
std::vector< TNode > args;\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
Node c = evaluateTerm( n[i] );\r
args.push_back( c );\r
}\r
- nn = d_uf_terms[n.getOperator()].existsTerm( n, args );\r
+ nn = d_uf_terms[f].existsTerm( n, args );\r
}\r
if( !nn.isNull() ){\r
Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;\r
debugPrint("qcf-debug");\r
Trace("qcf-debug") << std::endl;\r
}\r
- short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;\r
+ short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc;\r
for( short e = effort_conflict; e<=end_e; e++ ){\r
d_effort = e;\r
if( e == effort_prop_eq ){\r
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);\r
if( addedLemmas>0 ){\r
- Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );\r
+ Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );\r
Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;\r
}\r
Trace("qcf-engine") << std::endl;\r
d_uf_terms.clear();\r
d_eqc_uf_terms.clear();\r
d_eqcs.clear();\r
+ d_model_basis.clear();\r
d_arg_reps.clear();\r
double clSet = 0;\r
if( Trace.isOn("qcf-opt") ){\r
while( !eqcs_i.isFinished() ){\r
nEqc++;\r
Node r = (*eqcs_i);\r
- d_eqcs[r.getType()].push_back( r );\r
+ TypeNode rtn = r.getType();\r
+ if( options::qcfMode()==QCF_MC ){\r
+ std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );\r
+ if( itt==d_eqcs.end() ){\r
+ Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );\r
+ if( !getEqualityEngine()->hasTerm( mb ) ){\r
+ Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;\r
+ Assert( false );\r
+ }\r
+ Node mbr = getRepresentative( mb );\r
+ if( mbr!=r ){\r
+ d_eqcs[rtn].push_back( mbr );\r
+ }\r
+ d_eqcs[rtn].push_back( r );\r
+ d_model_basis[rtn] = mb;\r
+ }else{\r
+ itt->second.push_back( r );\r
+ }\r
+ }else{\r
+ d_eqcs[rtn].push_back( r );\r
+ }\r
//EqcInfo * eqcir = getEqcInfo( r, false );\r
//get relevant nodes that we are disequal from\r
/*\r
std::map< TNode, std::vector< TNode > >::iterator it_na;\r
TNode fn;\r
if( MatchGen::isHandledUfTerm( n ) ){\r
+ Node f = MatchGen::getOperator( this, n );\r
computeArgReps( n );\r
it_na = d_arg_reps.find( n );\r
Assert( it_na!=d_arg_reps.end() );\r
- Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );\r
+ Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
isRedundant = (nadd!=n);\r
- d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
+ d_uf_terms[f].addTerm( n, d_arg_reps[n] );\r
}else{\r
isRedundant = false;\r
}\r
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;
}
////step 2 : assign arbitrary values for unknown lengths?
//for( unsigned i=0; i<col.size(); i++ ){
- // if(
+ // if(
//}
Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
//step 3 : assign values to equivalence classes that are pure variables
}
}
Trace("strings-model") << "have length " << lts_values[i] << std::endl;
-
+
//assign a new length if necessary
if( !pure_eq.empty() ){
if( lts_values[i].isNull() ){
unsigned lvalue = 0;
while( values_used.find( lvalue )!=values_used.end() ){
- lvalue++;
+ lvalue++;
}
Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) );
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 );
}
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<Node> nf_n;
- std::vector<Node> 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<Node> nf_n;
+ std::vector<Node> 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<n.getNumChildren(); i++ ) {
- Node nr = d_equalityEngine.getRepresentative( n[i] );
- std::vector< Node > 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<n.getNumChildren(); i++ ) {
+ Node nr = d_equalityEngine.getRepresentative( n[i] );
+ std::vector< Node > 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<nf_temp.size(); r++ ) {
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<n.getNumChildren(); j++ ){
if( !areEqual( n[j], d_emptyString ) ){
nf_n.push_back( n[j] );
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<nf_n.size(); i++ ){
+ //if a component is equal to whole,
+ if( areEqual( nf_n[i], n ) ){
+ //all others must be empty
+ std::vector< Node > 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<nf_n.size(); j++ ){
+ if( i!=j ){
+ cc.push_back( nf_n[j].eqNode( d_emptyString ) );
+ }
+ }
+ std::vector< Node > 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<nf_n.size(); i++ ){
- //if a component is equal to whole,
- if( areEqual( nf_n[i], n ) ){
- //all others must be empty
- std::vector< Node > 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<nf_n.size(); j++ ){
- if( i!=j ){
- cc.push_back( nf_n[j].eqNode( d_emptyString ) );
- }
- }
- std::vector< Node > 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() ) {
}
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;
}
}
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 ) {
}
}
//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,
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<loop_index; ++lp) {
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;
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);
//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 );
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;
}
}
}
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;
}
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;
if( revRet!=0 ){
return revRet==-1;
}
-
+
nfi.clear();
nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
nfj.clear();
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;
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;
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 ));
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);
}
//|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 ) );
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",
//add the others as lemmas
sendLemma( d_true, sdc[i], "RegExp-DEF");
}
-
+
conc = sdc[0];
}
}
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;
projects / cvc5.git / commitdiff