if( !d_var_mg[j]->isValid() ){\r
d_mg->setInvalid();\r
break;\r
+ }else{\r
+ std::vector< int > bvars;\r
+ d_var_mg[j]->determineVariableOrder( this, bvars );\r
}\r
}\r
}\r
}\r
\r
void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {\r
+ Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;\r
if( n.getKind()==FORALL ){\r
registerNode( n[1], hasPol, pol );\r
}else{\r
- if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
+ if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){\r
if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
//literals\r
if( n.getKind()==EQUAL ){\r
}\r
}else if( MatchGen::isHandledUfTerm( n ) ){\r
flatten( n );\r
+ }else if( n.getKind()==ITE && !n[1].getType().isBoolean() ){\r
+ for( unsigned i=1; i<=2; i++ ){\r
+ flatten( n[i] );\r
+ }\r
}\r
}\r
}\r
}\r
\r
void QuantInfo::flatten( Node n ) {\r
+ Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;\r
if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
if( d_var_num.find( n )==d_var_num.end() ){\r
- //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;\r
+ Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;\r
d_var_num[n] = d_vars.size();\r
d_vars.push_back( n );\r
d_match.push_back( TNode::null() );\r
d_match_term.push_back( TNode::null() );\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- flatten( n[i] );\r
+ if( n.getKind()==ITE ){\r
+ registerNode( n, false, false );\r
+ }else{\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ flatten( n[i] );\r
+ }\r
}\r
+ }else{\r
+ Trace("qcf-qregister-debug2") << "...already processed" << std::endl;\r
}\r
+ }else{\r
+ Trace("qcf-qregister-debug2") << "...is ground." << std::endl;\r
}\r
}\r
\r
}\r
d_qni_size++;\r
}\r
+ }else if( n.getKind()==ITE ){\r
+ d_type = typ_ite_var;\r
+ d_type_not = false;\r
+ d_n = n;\r
+ d_children.push_back( MatchGen( qi, d_n[0] ) );\r
+ if( d_children[0].isValid() ){\r
+ d_type = typ_ite_var;\r
+ for( unsigned i=1; i<=2; i++ ){\r
+ Node nn = n.eqNode( n[i] );\r
+ d_children.push_back( MatchGen( qi, nn ) );\r
+ d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );\r
+ if( !d_children[d_children.size()-1].isValid() ){\r
+ setInvalid();\r
+ break;\r
+ }\r
+ }\r
+ }else{\r
+ d_type = typ_invalid;\r
+ }\r
}else{\r
//for now, unknown term\r
d_type = typ_invalid;\r
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
if( d_n.getKind()!=FORALL || i==1 ){\r
d_children.push_back( MatchGen( qi, d_n[i] ) );\r
- if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
+ if( !d_children[d_children.size()-1].isValid() ){\r
setInvalid();\r
break;\r
}\r
if( d_n.getKind()==EQUAL ){\r
for( unsigned i=0; i<2; i++ ){\r
if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
+ if( !qi->isVar( d_n[i] ) ){\r
+ Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;\r
+ }\r
Assert( qi->isVar( d_n[i] ) );\r
}else{\r
d_qni_gterm[i] = d_n[i];\r
}\r
}\r
if( isCom ){\r
- //first, do those that do not bind any new variables\r
- //second, do those with common variables\r
- //last, do those with no common variables\r
+ //children that bind the least number of unbound variables go first\r
do {\r
int min_score = -1;\r
int min_score_index = -1;\r
//if successful and non-redundant, store that we need to cleanup this\r
if( addc==1 ){\r
for( unsigned i=0; i<2; i++ ){\r
- if( vn[i]!=-1 ){\r
+ if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){\r
d_qni_bound[vn[i]] = vn[i];\r
}\r
}\r
}\r
Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
return success;\r
- }else if( d_type==typ_formula ){\r
+ }else if( d_type==typ_formula || d_type==typ_ite_var ){\r
if( d_child_counter!=-1 ){\r
bool success = false;\r
while( !success && d_child_counter>=0 ){\r
int index1 = d_child_counter==4 ? 1 : 0;\r
if( getChild( index1 )->getNextMatch( p, qi ) ){\r
d_child_counter++;\r
- getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, qi );\r
+ getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );\r
}else{\r
if( d_child_counter==4 ){\r
d_child_counter = -1;\r
}\r
}\r
if( d_child_counter%2==1 ){\r
- int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);\r
+ int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);\r
if( getChild( index2 )->getNextMatch( p, qi ) ){\r
success = true;\r
}else{\r
case typ_pred: Trace(c) << "pred";break;\r
case typ_formula: Trace(c) << "formula";break;\r
case typ_var: Trace(c) << "var";break;\r
+ case typ_ite_var: Trace(c) << "ite_var";break;\r
case typ_top: Trace(c) << "top";break;\r
}\r
}else{\r
case typ_pred: Debug(c) << "pred";break;\r
case typ_formula: Debug(c) << "formula";break;\r
case typ_var: Debug(c) << "var";break;\r
+ case typ_ite_var: Debug(c) << "ite_var";break;\r
case typ_top: Debug(c) << "top";break;\r
}\r
}\r
return ret;\r
}\r
\r
-bool QuantConflictFind::isPropagationSet() {\r
- return !d_prop_eq[0].isNull();\r
-}\r
-\r
bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {\r
//if( d_effort==QuantConflictFind::effort_mc ){\r
// return n1==n2 || !areDisequal( n1, n2 );\r
if( MatchGen::isHandledUfTerm( n ) ){\r
Node f = MatchGen::getOperator( this, n );\r
Node nn;\r
+ computeUfTerms( f );\r
if( getEqualityEngine()->hasTerm( n ) ){\r
computeArgReps( n );\r
nn = d_uf_terms[f].existsTerm( n, d_arg_reps[n] );\r
Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;\r
return n;\r
}\r
+ }else if( n.getKind()==ITE ){\r
+ int v = evaluate( n[0], false, false );\r
+ if( v==1 ){\r
+ return evaluateTerm( n[1] );\r
+ }else if( v==-1 ){\r
+ return evaluateTerm( n[2] );\r
+ }\r
}\r
return getRepresentative( n );\r
}\r
*/\r
\r
QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {\r
+ computeUfTerms( f );\r
std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );\r
if( itut==d_eqc_uf_terms.end() ){\r
return NULL;\r
}\r
\r
QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {\r
+ computeUfTerms( f );\r
std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );\r
if( itut!=d_uf_terms.end() ){\r
return &itut->second;\r
Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
computeRelevantEqr();\r
\r
+ //determine order for quantified formulas\r
+ std::vector< Node > qorder;\r
+ std::map< Node, bool > qassert;\r
+ //mark which are asserted\r
+ for( unsigned i=0; i<d_qassert.size(); i++ ){\r
+ qassert[d_qassert[i]] = true;\r
+ }\r
+ //add which ones are specified in the order\r
+ for( unsigned i=0; i<d_quant_order.size(); i++ ){\r
+ Node n = d_quant_order[i];\r
+ if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){\r
+ qorder.push_back( n );\r
+ }\r
+ }\r
+ d_quant_order.clear();\r
+ d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );\r
+ //add remaining\r
+ for( unsigned i=0; i<d_qassert.size(); i++ ){\r
+ Node n = d_qassert[i];\r
+ if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){\r
+ qorder.push_back( n );\r
+ }\r
+ }\r
+\r
+\r
+\r
if( Trace.isOn("qcf-debug") ){\r
Trace("qcf-debug") << std::endl;\r
debugPrint("qcf-debug");\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
- for( unsigned i=0; i<2; i++ ){\r
- d_prop_eq[i] = Node::null();\r
- }\r
- }\r
Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;\r
- for( unsigned j=0; j<d_qassert.size(); j++ ){\r
- Node q = d_qassert[j];\r
+ for( unsigned j=0; j<qorder.size(); j++ ){\r
+ Node q = qorder[j];\r
QuantInfo * qi = &d_qinfo[q];\r
Trace("qcf-check") << "Check quantified formula ";\r
debugPrintQuant("qcf-check", q);\r
Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
++addedLemmas;\r
if( e==effort_conflict ){\r
+ d_quant_order.insert( d_quant_order.begin(), q );\r
d_conflict.set( true );\r
++(d_statistics.d_conflict_inst);\r
break;\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
- clSet = double(clock())/double(CLOCKS_PER_SEC);\r
- }\r
+ //double clSet = 0;\r
+ //if( Trace.isOn("qcf-opt") ){\r
+ // clSet = double(clock())/double(CLOCKS_PER_SEC);\r
+ //}\r
\r
- long nTermst = 0;\r
- long nTerms = 0;\r
- long nEqc = 0;\r
+ //long nTermst = 0;\r
+ //long nTerms = 0;\r
+ //long nEqc = 0;\r
\r
//which nodes are irrelevant for disequality matches\r
std::map< TNode, bool > irrelevant_dnode;\r
//now, store matches\r
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
while( !eqcs_i.isFinished() ){\r
- nEqc++;\r
+ //nEqc++;\r
Node r = (*eqcs_i);\r
TypeNode rtn = r.getType();\r
if( options::qcfMode()==QCF_MC ){\r
}else{\r
d_eqcs[rtn].push_back( r );\r
}\r
+ //if( r.getType().isInteger() ){\r
+ // Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;\r
+ //}\r
//EqcInfo * eqcir = getEqcInfo( r, false );\r
//get relevant nodes that we are disequal from\r
/*\r
}\r
*/\r
//process disequalities\r
+ /*\r
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
while( !eqc_i.isFinished() ){\r
TNode n = (*eqc_i);\r
// std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;\r
// }\r
//}\r
-\r
- bool isRedundant;\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[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
- isRedundant = (nadd!=n);\r
- d_uf_terms[f].addTerm( n, d_arg_reps[n] );\r
+ if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){ //temporary\r
+\r
+ bool isRedundant;\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[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
+ isRedundant = (nadd!=n);\r
+ d_uf_terms[f].addTerm( n, d_arg_reps[n] );\r
+ }else{\r
+ isRedundant = false;\r
+ }\r
+ nTerms += isRedundant ? 0 : 1;\r
}else{\r
- isRedundant = false;\r
+ if( Debug.isOn("qcf-nground") ){\r
+ Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl;\r
+ Assert( false );\r
+ }\r
}\r
- nTerms += isRedundant ? 0 : 1;\r
}\r
++eqc_i;\r
}\r
- //process_eqc[r] = true;\r
+ */\r
++eqcs_i;\r
}\r
+ /*\r
if( Trace.isOn("qcf-opt") ){\r
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
Trace("qcf-opt") << "Compute rel eqc : " << std::endl;\r
Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;\r
Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;\r
}\r
+ */\r
}\r
\r
void QuantConflictFind::computeArgReps( TNode n ) {\r
}\r
}\r
\r
+void QuantConflictFind::computeUfTerms( TNode f ) {\r
+ if( d_uf_terms.find( f )==d_uf_terms.end() ){\r
+ d_uf_terms[f].clear();\r
+ unsigned nt = d_quantEngine->getTermDatabase()->d_op_map[f].size();\r
+ for( unsigned i=0; i<nt; i++ ){\r
+ Node n = d_quantEngine->getTermDatabase()->d_op_map[f][i];\r
+ if( !n.getAttribute(NoMatchAttribute()) ){\r
+ Assert( getEqualityEngine()->hasTerm( n ) );\r
+ Node r = getRepresentative( n );\r
+ computeArgReps( n );\r
+ d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
+ d_uf_terms[f].addTerm( n, d_arg_reps[n] );\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
//-------------------------------------------------- debugging\r
\r
\r
projects / cvc5.git / commitdiff