diff options
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 108 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 7 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 217 |
4 files changed, 200 insertions, 134 deletions
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<n.getNumChildren(); i++ ){
flatten( n[i] );
}
+ }else if( MatchGen::isHandledUfTerm( n ) ){
+ flatten( n );
}
}
}
@@ -496,6 +496,12 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& 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_type<d_mg->d_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; j<d_n.getNumChildren(); j++ ){
Node nn = d_n[j];
Trace("qcf-qregister-debug") << " " << d_qni_size;
if( qi->isVar( 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->second<qi->getNumVars() );
@@ -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<n.getNumChildren(); i++ ){
Node c = evaluateTerm( n[i] );
args.push_back( c );
}
- nn = d_uf_terms[n.getOperator()].existsTerm( n, args );
+ nn = d_uf_terms[f].existsTerm( n, args );
}
if( !nn.isNull() ){
Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
@@ -1612,7 +1634,7 @@ void QuantConflictFind::check( Theory::Effort level ) { debugPrint("qcf-debug");
Trace("qcf-debug") << std::endl;
}
- short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;
+ short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc;
for( short e = effort_conflict; e<=end_e; e++ ){
d_effort = e;
if( e == effort_prop_eq ){
@@ -1706,7 +1728,7 @@ void QuantConflictFind::check( Theory::Effort level ) { double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
if( addedLemmas>0 ){
- Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );
+ Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );
Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
}
Trace("qcf-engine") << std::endl;
@@ -1734,6 +1756,7 @@ void QuantConflictFind::computeRelevantEqr() { d_uf_terms.clear();
d_eqc_uf_terms.clear();
d_eqcs.clear();
+ d_model_basis.clear();
d_arg_reps.clear();
double clSet = 0;
if( Trace.isOn("qcf-opt") ){
@@ -1751,7 +1774,27 @@ void QuantConflictFind::computeRelevantEqr() { while( !eqcs_i.isFinished() ){
nEqc++;
Node r = (*eqcs_i);
- d_eqcs[r.getType()].push_back( r );
+ TypeNode rtn = r.getType();
+ if( options::qcfMode()==QCF_MC ){
+ std::map< TypeNode, std::vector< TNode > >::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; 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 @@ -307,13 +307,13 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { } } 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 ) ); @@ -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<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++ ) { @@ -715,7 +720,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & 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<n.getNumChildren(); j++ ){ if( !areEqual( n[j], d_emptyString ) ){ nf_n.push_back( n[j] ); @@ -726,62 +731,66 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & 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<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() ) { @@ -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<loop_index; ++lp) { @@ -945,7 +962,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &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; |