diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-26 14:23:51 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-26 14:24:02 -0600 |
| commit | d0add0eb12cac4e9cbcf09fe60724d280889002d (patch) | |
| tree | 217528663e877f15832a5cb00005e5a15a69f2ee /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | 160572318e251a98a58b3f506c31fb233070d477 (diff) | |
More optimization of QCF. Fixed InstMatchTrie for caching instantiations. Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 1544 |
1 files changed, 782 insertions, 762 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 198ec3bbf..665ae5329 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -68,665 +68,8 @@ void QcfNodeIndex::debugPrint( const char * c, int t ) { }
}
-QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ),
-d_c( c ),
-d_conflict( c, false ),
-d_qassert( c ) {
- d_fid_count = 0;
- d_true = NodeManager::currentNM()->mkConst<bool>(true);
- d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {
- if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){
- index = 0;
- return n;
- }else if( isHandledUfTerm( n ) ){
- /*
- std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );
- if( it==d_op_node.end() ){
- std::vector< Node > children;
- children.push_back( n.getOperator() );
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- children.push_back( getFv( n[i].getType() ) );
- }
- Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
- d_op_node[n.getOperator()] = nn;
- return nn;
- }else{
- return it->second;
- }*/
- index = 1;
- return n.getOperator();
- }else{
- return Node::null();
- }
-}
-
-Node QuantConflictFind::mkEqNode( Node a, Node b ) {
- if( a.getType().isBoolean() ){
- return a.iffNode( b );
- }else{
- return a.eqNode( b );
- }
-}
-
-//-------------------------------------------------- registration
-
-void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {
- //qcf->d_node = n;
- bool recurse = true;
- 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 || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- flatten( q, n[i] );
- }
- }else if( n.getKind()==EQUAL ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- for( unsigned j=0; j<n[i].getNumChildren(); j++ ){
- flatten( q, n[i][j] );
- }
- }
- }
-
- */
-
- if( n.getKind()==APPLY_UF ){
- flatten( q, n );
- }else if( n.getKind()==EQUAL ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- flatten( q, n[i] );
- }
- }
-
- }else{
- Trace("qcf-qregister") << " RegisterGroundLit : " << n;
- }
- recurse = false;
- }
- if( recurse ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- //QcfNode * qcfc = new QcfNode( d_c );
- //qcfc->d_parent = qcf;
- //qcf->d_child[i] = qcfc;
- registerNode( q, n[i], newHasPol, newPol );
- }
- }
-}
-
-void QuantConflictFind::flatten( Node q, Node n ) {
- if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){
- if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){
- //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;
- d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();
- d_qinfo[q].d_vars.push_back( n );
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- flatten( q, n[i] );
- }
- }
-}
-
-void QuantConflictFind::registerQuantifier( Node q ) {
- d_quants.push_back( q );
- d_quant_id[q] = d_quants.size();
- Trace("qcf-qregister") << "Register ";
- debugPrintQuant( "qcf-qregister", q );
- Trace("qcf-qregister") << " : " << q << std::endl;
-
- //register the variables
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- d_qinfo[q].d_var_num[q[0][i]] = i;
- d_qinfo[q].d_vars.push_back( q[0][i] );
- }
-
- //make QcfNode structure
- Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
- //d_qinfo[q].d_cf = new QcfNode( d_c );
- registerNode( q, q[1], true, true );
-
- //debug print
- Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
- Trace("qcf-qregister") << " ";
- debugPrintQuantBody( "qcf-qregister", q, q[1] );
- Trace("qcf-qregister") << std::endl;
- if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
- Trace("qcf-qregister") << " with additional constraints : " << std::endl;
- for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
- Trace("qcf-qregister") << " ?x" << j << " = ";
- debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
- Trace("qcf-qregister") << std::endl;
- }
- }
-
- Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
- d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );
-
- for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
- d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );
- if( !d_qinfo[q].d_var_mg[j]->isValid() ){
- d_qinfo[q].d_mg->setInvalid();
- break;
- }
- }
-
- Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
-}
-
-int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
- int ret = 0;
- if( n.getKind()==EQUAL ){
- Node n1 = evaluateTerm( n[0] );
- Node n2 = evaluateTerm( n[1] );
- Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
- if( areEqual( n1, n2 ) ){
- ret = 1;
- }else if( areDisequal( n1, n2 ) ){
- ret = -1;
- }
- //else if( d_effort>QuantConflictFind::effort_conflict ){
- // ret = -1;
- //}
- }else if( n.getKind()==APPLY_UF ){ //predicate
- Node nn = evaluateTerm( n );
- Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
- if( areEqual( nn, d_true ) ){
- ret = 1;
- }else if( areEqual( nn, d_false ) ){
- ret = -1;
- }
- //else if( d_effort>QuantConflictFind::effort_conflict ){
- // ret = -1;
- //}
- }else if( n.getKind()==NOT ){
- return -evaluate( n[0] );
- }else if( n.getKind()==ITE ){
- int cev1 = evaluate( n[0] );
- int cevc[2] = { 0, 0 };
- for( unsigned i=0; i<2; i++ ){
- if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){
- cevc[i] = evaluate( n[i+1] );
- if( cev1!=0 ){
- ret = cevc[i];
- break;
- }else if( cevc[i]==0 ){
- break;
- }
- }
- }
- if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){
- ret = cevc[0];
- }
- }else if( n.getKind()==IFF ){
- int cev1 = evaluate( n[0] );
- if( cev1!=0 ){
- int cev2 = evaluate( n[1] );
- if( cev2!=0 ){
- ret = cev1==cev2 ? 1 : -1;
- }
- }
-
- }else{
- int ssval = 0;
- if( n.getKind()==OR ){
- ssval = 1;
- }else if( n.getKind()==AND ){
- ssval = -1;
- }
- bool isUnk = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- int cev = evaluate( n[i] );
- if( cev==ssval ){
- ret = ssval;
- break;
- }else if( cev==0 ){
- isUnk = true;
- }
- }
- if( ret==0 && !isUnk ){
- ret = -ssval;
- }
- }
- Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;
- return ret;
-}
-
-bool QuantConflictFind::isPropagationSet() {
- return !d_prop_eq[0].isNull();
-}
-
-bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
- //if( d_effort==QuantConflictFind::effort_prop_deq ){
- // return n1==n2 || !areDisequal( n1, n2 );
- //}else{
- return n1==n2;
- //}
-}
-
-bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
- //if( d_effort==QuantConflictFind::effort_conflict ){
- // return areDisequal( n1, n2 );
- //}else{
- return n1!=n2;
- //}
-}
-
-//-------------------------------------------------- handling assertions / eqc
-
-void QuantConflictFind::assertNode( Node q ) {
- Trace("qcf-proc") << "QCF : assertQuantifier : ";
- debugPrintQuant("qcf-proc", q);
- Trace("qcf-proc") << std::endl;
- d_qassert.push_back( q );
- //set the eqRegistries that this depends on to true
- //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
- // it->first->d_active.set( true );
- //}
-}
-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
- //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-}
-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
-}
-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
-}
-Node QuantConflictFind::getRepresentative( Node n ) {
- if( getEqualityEngine()->hasTerm( n ) ){
- return getEqualityEngine()->getRepresentative( n );
- }else{
- return n;
- }
-}
-Node QuantConflictFind::evaluateTerm( Node n ) {
- if( isHandledUfTerm( n ) ){
- Node nn;
- if( getEqualityEngine()->hasTerm( n ) ){
- computeArgReps( n );
- nn = d_uf_terms[n.getOperator()].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 );
- }
- if( !nn.isNull() ){
- Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
- return getRepresentative( nn );
- }else{
- Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
- return n;
- }
- }
- return getRepresentative( n );
-}
-
-/*
-QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {
- std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );
- if( it2==d_eqc_info.end() ){
- if( doCreate ){
- EqcInfo * eqci = new EqcInfo( d_c );
- d_eqc_info[n] = eqci;
- return eqci;
- }else{
- return NULL;
- }
- }
- return it2->second;
-}
-*/
-
-QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {
- std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );
- if( itut==d_eqc_uf_terms.end() ){
- return NULL;
- }else{
- if( eqc.isNull() ){
- return &itut->second;
- }else{
- std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );
- if( itute!=itut->second.d_children.end() ){
- return &itute->second;
- }else{
- return NULL;
- }
- }
- }
-}
-
-QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {
- std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );
- if( itut!=d_uf_terms.end() ){
- return &itut->second;
- }else{
- return NULL;
- }
-}
-
-/** new node */
-void QuantConflictFind::newEqClass( Node n ) {
- //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
- //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;
-}
-
-/** merge */
-void QuantConflictFind::merge( Node a, Node b ) {
- /*
- if( b.getKind()==EQUAL ){
- if( a==d_true ){
- //will merge anyways
- //merge( b[0], b[1] );
- }else if( a==d_false ){
- assertDisequal( b[0], b[1] );
- }
- }else{
- Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;
- EqcInfo * eqc_b = getEqcInfo( b, false );
- EqcInfo * eqc_a = NULL;
- if( eqc_b ){
- eqc_a = getEqcInfo( a );
- //move disequalities of b into a
- for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){
- if( (*it).second ){
- Node n = (*it).first;
- EqcInfo * eqc_n = getEqcInfo( n, false );
- Assert( eqc_n );
- if( !eqc_n->isDisequal( a ) ){
- Assert( !eqc_a->isDisequal( n ) );
- eqc_n->setDisequal( a );
- eqc_a->setDisequal( n );
- //setEqual( eqc_a, eqc_b, a, n, false );
- }
- eqc_n->setDisequal( b, false );
- }
- }
- ////move all previous EqcRegistry's regarding equalities within b
- //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){
- // if( (*it).second ){
- // eqc_a->d_rel_eqr_e[(*it).first] = true;
- // }
- //}
- }
- //process new equalities
- //setEqual( eqc_a, eqc_b, a, b, true );
- Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;
- }
- */
-}
-
-/** assert disequal */
-void QuantConflictFind::assertDisequal( Node a, Node b ) {
- /*
- a = getRepresentative( a );
- b = getRepresentative( b );
- Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;
- EqcInfo * eqc_a = getEqcInfo( a );
- EqcInfo * eqc_b = getEqcInfo( b );
- if( !eqc_a->isDisequal( b ) ){
- Assert( !eqc_b->isDisequal( a ) );
- eqc_b->setDisequal( a );
- eqc_a->setDisequal( b );
- //setEqual( eqc_a, eqc_b, a, b, false );
- }
- Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;
- */
-}
-
-//-------------------------------------------------- check function
-
-/** check */
-void QuantConflictFind::check( Theory::Effort level ) {
- Trace("qcf-check") << "QCF : check : " << level << std::endl;
- if( d_conflict ){
- Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
- if( level>=Theory::EFFORT_FULL ){
- Assert( false );
- }
- }else{
- int addedLemmas = 0;
- if( d_performCheck ){
- ++(d_statistics.d_inst_rounds);
- double clSet = 0;
- if( Trace.isOn("qcf-engine") ){
- clSet = double(clock())/double(CLOCKS_PER_SEC);
- Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
- }
- Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
- computeRelevantEqr();
-
- if( Trace.isOn("qcf-debug") ){
- Trace("qcf-debug") << std::endl;
- debugPrint("qcf-debug");
- Trace("qcf-debug") << std::endl;
- }
- short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;
- for( short e = effort_conflict; e<=end_e; e++ ){
- d_effort = e;
- if( e == effort_prop_eq ){
- for( unsigned i=0; i<2; i++ ){
- d_prop_eq[i] = Node::null();
- }
- }
- Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
- for( unsigned j=0; j<d_qassert.size(); j++ ){
- Node q = d_qassert[j];
- Trace("qcf-check") << "Check quantified formula ";
- debugPrintQuant("qcf-check", q);
- Trace("qcf-check") << " : " << q << "..." << std::endl;
-
- Assert( d_qinfo.find( q )!=d_qinfo.end() );
- if( d_qinfo[q].d_mg->isValid() ){
- d_qinfo[q].reset_round( this );
- //try to make a matches making the body false
- d_qinfo[q].d_mg->reset( this, false, q );
- while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){
-
- Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
- d_qinfo[q].debugPrintMatch("qcf-check");
- Trace("qcf-check") << std::endl;
-
- if( !d_qinfo[q].isMatchSpurious( this ) ){
- std::vector< int > assigned;
- if( d_qinfo[q].completeMatch( this, q, assigned ) ){
- InstMatch m;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- //Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );
- int repVar = d_qinfo[q].getCurrentRepVar( i );
- Node cv;
- std::map< int, Node >::iterator itmt = d_qinfo[q].d_match_term.find( repVar );
- if( itmt!=d_qinfo[q].d_match_term.end() ){
- cv = itmt->second;
- }else{
- cv = d_qinfo[q].d_match[repVar];
- }
-
-
- Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;
- m.set( d_quantEngine, q, i, cv );
- }
- if( Debug.isOn("qcf-check-inst") ){
- //if( e==effort_conflict ){
- Node inst = d_quantEngine->getInstantiation( q, m );
- Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
- Assert( evaluate( inst )!=1 );
- Assert( evaluate( inst )==-1 || e>effort_conflict );
- //}
- }
- if( d_quantEngine->addInstantiation( q, m ) ){
- Trace("qcf-check") << " ... Added instantiation" << std::endl;
- ++addedLemmas;
- if( e==effort_conflict ){
- d_conflict.set( true );
- ++(d_statistics.d_conflict_inst);
- break;
- }else if( e==effort_prop_eq ){
- ++(d_statistics.d_prop_inst);
- }
- }else{
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
- Assert( false );
- }
- //clean up assigned
- for( unsigned i=0; i<assigned.size(); i++ ){
- d_qinfo[q].d_match.erase( assigned[i] );
- }
- }else{
- Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
- }
- }else{
- Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;
- }
- }
- }
- if( d_conflict ){
- break;
- }
- }
- if( addedLemmas>0 ){
- d_quantEngine->flushLemmas();
- break;
- }
- }
- if( Trace.isOn("qcf-engine") ){
- 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") << ", addedLemmas = " << addedLemmas;
- }
- Trace("qcf-engine") << std::endl;
- }
- }
- Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
- }
-}
-
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {
- d_performCheck = false;
- if( !d_conflict ){
- if( level==Theory::EFFORT_LAST_CALL ){
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
- }else if( level==Theory::EFFORT_FULL ){
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
- }else if( level==Theory::EFFORT_STANDARD ){
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
- }
- }
- return d_performCheck;
-}
-
-void QuantConflictFind::computeRelevantEqr() {
- d_uf_terms.clear();
- d_eqc_uf_terms.clear();
- d_eqcs.clear();
- d_arg_reps.clear();
- double clSet = 0;
- if( Trace.isOn("qcf-opt") ){
- clSet = double(clock())/double(CLOCKS_PER_SEC);
- }
-
- long nTermst = 0;
- long nTerms = 0;
- long nEqc = 0;
-
- //which nodes are irrelevant for disequality matches
- std::map< TNode, bool > irrelevant_dnode;
- //now, store matches
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
- while( !eqcs_i.isFinished() ){
- nEqc++;
- Node r = (*eqcs_i);
- d_eqcs[r.getType()].push_back( r );
- //EqcInfo * eqcir = getEqcInfo( r, false );
- //get relevant nodes that we are disequal from
- /*
- std::vector< Node > deqc;
- if( eqcir ){
- for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){
- if( (*it).second ){
- //Node rd = (*it).first;
- //if( rd!=getRepresentative( rd ) ){
- // std::cout << "Bad rep!" << std::endl;
- // exit( 0 );
- //}
- deqc.push_back( (*it).first );
- }
- }
- }
- */
- //process disequalities
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
- while( !eqc_i.isFinished() ){
- TNode n = (*eqc_i);
- if( n.getKind()!=EQUAL ){
- nTermst++;
- //node_to_rep[n] = r;
- //if( n.getNumChildren()>0 ){
- // if( n.getKind()!=APPLY_UF ){
- // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;
- // }
- //}
-
- bool isRedundant;
- std::map< TNode, std::vector< TNode > >::iterator it_na;
- TNode fn;
- if( isHandledUfTerm( 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] );
- isRedundant = (nadd!=n);
- d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );
- if( !isRedundant ){
- int jindex;
- fn = getFunction( n, jindex );
- }
- }else{
- isRedundant = false;
- }
- nTerms += isRedundant ? 0 : 1;
- }
- ++eqc_i;
- }
- //process_eqc[r] = true;
- ++eqcs_i;
- }
- if( Trace.isOn("qcf-opt") ){
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
- Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;
- Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;
- Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;
- }
-}
-
-void QuantConflictFind::computeArgReps( TNode n ) {
- if( d_arg_reps.find( n )==d_arg_reps.end() ){
- Assert( isHandledUfTerm( n ) );
- for( unsigned j=0; j<n.getNumChildren(); j++ ){
- d_arg_reps[n].push_back( getRepresentative( n[j] ) );
- }
- }
-}
-bool QuantConflictFind::isHandledUfTerm( TNode n ) {
- return n.getKind()==APPLY_UF;
-}
-
-void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {
+void QuantInfo::reset_round( QuantConflictFind * p ) {
d_match.clear();
d_match_term.clear();
d_curr_var_deq.clear();
@@ -758,8 +101,8 @@ void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) { }
}
-int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {
- std::map< int, Node >::iterator it = d_match.find( v );
+int QuantInfo::getCurrentRepVar( int v ) {
+ std::map< int, TNode >::iterator it = d_match.find( v );
if( it!=d_match.end() ){
int vn = getVarNum( it->second );
if( vn!=-1 ){
@@ -772,12 +115,12 @@ int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) { return v;
}
-Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {
+TNode QuantInfo::getCurrentValue( TNode n ) {
int v = getVarNum( n );
if( v==-1 ){
return n;
}else{
- std::map< int, Node >::iterator it = d_match.find( v );
+ std::map< int, TNode >::iterator it = d_match.find( v );
if( it==d_match.end() ){
return n;
}else{
@@ -787,24 +130,27 @@ Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) { }
}
-bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n, bool chDiseq ) {
+bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {
//check disequalities
- for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){
- Node cv = getCurrentValue( it->first );
- Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
- if( cv==n ){
- return false;
- }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
- //they must actually be disequal if we are looking for conflicts
- if( !p->areDisequal( n, cv ) ){
+ std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
+ if( itd!=d_curr_var_deq.end() ){
+ for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
+ Node cv = getCurrentValue( it->first );
+ Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
+ if( cv==n ){
return false;
+ }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
+ //they must actually be disequal if we are looking for conflicts
+ if( !p->areDisequal( n, cv ) ){
+ return false;
+ }
}
}
}
return true;
}
-int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ) {
+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) {
v = getCurrentRepVar( v );
int vn = getVarNum( n );
vn = vn==-1 ? -1 : getCurrentRepVar( vn );
@@ -812,7 +158,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N return addConstraint( p, v, n, vn, polarity, false );
}
-int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ) {
+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) {
//for handling equalities between variables, and disequalities involving variables
Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
@@ -824,16 +170,16 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N if( doRemove ){
if( vn!=-1 ){
//if set to this in the opposite direction, clean up opposite instead
- std::map< int, Node >::iterator itmn = d_match.find( vn );
+ std::map< int, TNode >::iterator itmn = d_match.find( vn );
if( itmn!=d_match.end() && itmn->second==d_vars[v] ){
return addConstraint( p, vn, d_vars[v], v, true, true );
}else{
//unsetting variables equal
- std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( vn );
+ std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );
if( itd!=d_curr_var_deq.end() ){
//remove disequalities owned by this
- std::vector< Node > remDeq;
- for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
+ std::vector< TNode > remDeq;
+ for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
if( it->second==v ){
remDeq.push_back( it->first );
}
@@ -847,11 +193,11 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N d_match.erase( v );
return 1;
}else{
- std::map< int, Node >::iterator itm = d_match.find( v );
+ std::map< int, TNode >::iterator itm = d_match.find( v );
if( vn!=-1 ){
Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;
- std::map< int, Node >::iterator itmn = d_match.find( vn );
+ std::map< int, TNode >::iterator itmn = d_match.find( vn );
if( itm==d_match.end() ){
//setting variables equal
bool alreadySet = false;
@@ -861,9 +207,9 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N }
//copy or check disequalities
- std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( v );
+ std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
if( itd!=d_curr_var_deq.end() ){
- for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
+ for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
Node dv = getCurrentValue( it->first );
if( !alreadySet ){
if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
@@ -925,9 +271,9 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N }else{
if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
//check if it respects equality
- std::map< int, Node >::iterator itm = d_match.find( v );
+ std::map< int, TNode >::iterator itm = d_match.find( v );
if( itm!=d_match.end() ){
- Node nv = getCurrentValue( n );
+ TNode nv = getCurrentValue( n );
if( !p->areMatchDisequal( nv, itm->second ) ){
Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
return -1;
@@ -945,32 +291,28 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N }
}
-bool QuantConflictFind::QuantInfo::isConstrainedVar( int v ) {
- //if( options::qcfMode()==QCF_CONFLICT_ONLY ){
- // return true;
- //}else{
- if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
- return true;
- }else{
- Node vv = getVar( v );
- for( std::map< int, Node >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
- if( it->second==vv ){
- return true;
- }
+bool QuantInfo::isConstrainedVar( int v ) {
+ if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
+ return true;
+ }else{
+ Node vv = getVar( v );
+ for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
+ if( it->second==vv ){
+ return true;
}
- for( std::map< int, std::map< Node, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
- for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- if( it2->first==vv ){
- return true;
- }
+ }
+ for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
+ for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ if( it2->first==vv ){
+ return true;
}
}
- return false;
}
- //}
+ return false;
+ }
}
-bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node n ) {
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
if( getCurrentCanBeEqual( p, v, n ) ){
Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;
d_match[v] = n;
@@ -980,9 +322,9 @@ bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node }
}
-bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
+bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
for( int i=0; i<getNumVars(); i++ ){
- std::map< int, Node >::iterator it = d_match.find( i );
+ std::map< int, TNode >::iterator it = d_match.find( i );
if( it!=d_match.end() ){
if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){
return true;
@@ -992,7 +334,7 @@ bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false;
}
-bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ) {
+bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned ) {
//assign values for variables that were unassigned (usually not necessary, but handles corner cases)
Trace("qcf-check") << std::endl;
std::vector< int > unassigned[2];
@@ -1023,7 +365,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, if( !isConstrainedVar( unassigned[r][index] ) ){
eqc_count.push_back( -1 );
}else{
- d_var_mg[ unassigned[r][index] ]->reset( p, true, q );
+ d_var_mg[ unassigned[r][index] ]->reset( p, true, this );
eqc_count.push_back( 0 );
}
}else{
@@ -1034,7 +376,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){
Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;
index++;
- }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){
+ }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, this ) ){
Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;
index++;
}else{
@@ -1098,7 +440,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, }
}
-void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {
+void QuantInfo::debugPrintMatch( const char * c ) {
for( int i=0; i<getNumVars(); i++ ){
Trace(c) << " " << d_vars[i] << " -> ";
if( d_match.find( i )!=d_match.end() ){
@@ -1108,7 +450,7 @@ void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) { }
if( !d_curr_var_deq[i].empty() ){
Trace(c) << ", DEQ{ ";
- for( std::map< Node, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
+ for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
Trace(c) << it->first << " ";
}
Trace(c) << "}";
@@ -1119,14 +461,14 @@ void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) { /*
struct MatchGenSort {
- QuantConflictFind::MatchGen * d_mg;
+ MatchGen * d_mg;
bool operator() (int i,int j) {
return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;
}
};
*/
-QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){
+MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){
Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;
std::vector< Node > qni_apps;
d_qni_size = 0;
@@ -1231,11 +573,11 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo }
-void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {
+void MatchGen::reset_round( QuantConflictFind * p ) {
for( unsigned i=0; i<d_children.size(); i++ ){
d_children[i].reset_round( p );
}
- for( std::map< int, Node >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
+ for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
}
if( d_type==typ_ground ){
@@ -1254,7 +596,7 @@ void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) { }
}
-void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q ) {
+void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
d_tgt = d_type_not ? !tgt : tgt;
Debug("qcf-match") << " Reset for : " << d_n << ", type : ";
debugPrintType( "qcf-match", d_type );
@@ -1265,7 +607,9 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q d_child_counter = -1;
//set up processing matches
- if( d_type==typ_ground ){
+ if( d_type==typ_invalid ){
+ //d_child_counter = 0;
+ }else if( d_type==typ_ground ){
if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
d_child_counter = 0;
}
@@ -1282,22 +626,30 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q Node nn[2];
int vn[2];
if( d_type==typ_pred ){
- nn[0] = p->d_qinfo[q].getCurrentValue( d_n );
- vn[0] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[0] ) );
+ nn[0] = qi->getCurrentValue( d_n );
+ vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
vn[1] = -1;
d_tgt = true;
}else{
for( unsigned i=0; i<2; i++ ){
- nn[i] = p->d_qinfo[q].getCurrentValue( d_n[i] );
- vn[i] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[i] ) );
+ nn[i] = qi->getCurrentValue( d_n[i] );
+ vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );
}
}
bool success;
if( vn[0]==-1 && vn[1]==-1 ){
Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
//just compare values
- success = d_tgt ? p->areMatchEqual( nn[0], nn[1] ) : p->areMatchDisequal( nn[0], nn[1] );
+ if( d_tgt ){
+ success = p->areMatchEqual( nn[0], nn[1] );
+ }else{
+ if( p->d_effort==QuantConflictFind::effort_conflict ){
+ success = p->areDisequal( nn[0], nn[1] );
+ }else{
+ success = p->areMatchDisequal( nn[0], nn[1] );
+ }
+ }
}else{
//otherwise, add a constraint to a variable
if( vn[1]!=-1 && vn[0]==-1 ){
@@ -1310,7 +662,7 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q }
Debug("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
//add some constraint
- int addc = p->d_qinfo[q].addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
+ int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
success = addc!=-1;
//if successful and non-redundant, store that we need to cleanup this
if( addc==1 ){
@@ -1334,18 +686,18 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q }else{
//reset the first child to d_tgt
d_child_counter = 0;
- getChild( d_child_counter )->reset( p, d_tgt, q );
+ getChild( d_child_counter )->reset( p, d_tgt, qi );
}
}
d_binding = false;
Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
}
-bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) {
+bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
Debug("qcf-match") << " Get next match for : " << d_n << ", type = ";
debugPrintType( "qcf-match", d_type );
Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
- if( d_type==typ_ground ){
+ if( d_type==typ_invalid || d_type==typ_ground ){
if( d_child_counter==0 ){
d_child_counter = -1;
return true;
@@ -1359,7 +711,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) bool doReset = false;
bool doFail = false;
if( !d_binding ){
- if( doMatching( p, q ) ){
+ if( doMatching( p, qi ) ){
Debug("qcf-match-debug") << " - Matching succeeded" << std::endl;
d_binding = true;
d_binding_it = d_qni_bound.begin();
@@ -1383,14 +735,14 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) std::map< int, MatchGen * >::iterator itm;
if( !doFail ){
Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl;
- itm = p->d_qinfo[q].d_var_mg.find( d_binding_it->second );
+ itm = qi->d_var_mg.find( d_binding_it->second );
}
- if( doFail || ( d_binding_it->first!=0 && itm!=p->d_qinfo[q].d_var_mg.end() ) ){
+ if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){
Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
if( doReset ){
- itm->second->reset( p, true, q );
+ itm->second->reset( p, true, qi );
}
- if( doFail || !itm->second->getNextMatch( p, q ) ){
+ if( doFail || !itm->second->getNextMatch( p, qi ) ){
do {
if( d_binding_it==d_qni_bound.begin() ){
Debug("qcf-match-debug") << " failed." << std::endl;
@@ -1399,7 +751,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) Debug("qcf-match-debug") << " decrement..." << std::endl;
--d_binding_it;
}
- }while( success && ( d_binding_it->first==0 || p->d_qinfo[q].d_var_mg.find( d_binding_it->second )==p->d_qinfo[q].d_var_mg.end() ) );
+ }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );
doReset = false;
doFail = false;
}else{
@@ -1426,12 +778,12 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) //if not successful, clean up the variables you bound
if( !success ){
if( d_type==typ_eq || d_type==typ_pred ){
- for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
+ 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;
std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
- p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );
+ qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );
}
}
d_qni_bound_cons.clear();
@@ -1441,9 +793,9 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) //clean up the match : remove equalities/disequalities
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<p->d_qinfo[q].getNumVars() );
- p->d_qinfo[q].d_match.erase( it->second );
- p->d_qinfo[q].d_match_term.erase( it->second );
+ Assert( it->second<qi->getNumVars() );
+ qi->d_match.erase( it->second );
+ qi->d_match_term.erase( it->second );
}
d_qni_bound.clear();
}
@@ -1458,11 +810,11 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){
if( (d_n.getKind()==AND)==d_tgt ){
//all children must match simultaneously
- if( getChild( d_child_counter )->getNextMatch( p, q ) ){
+ if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
if( d_child_counter<(int)(getNumChildren()-1) ){
d_child_counter++;
Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl;
- getChild( d_child_counter )->reset( p, d_tgt, q );
+ getChild( d_child_counter )->reset( p, d_tgt, qi );
}else{
success = true;
}
@@ -1471,11 +823,11 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) }
}else{
//one child must match
- if( !getChild( d_child_counter )->getNextMatch( p, q ) ){
+ if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){
if( d_child_counter<(int)(getNumChildren()-1) ){
d_child_counter++;
Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;
- getChild( d_child_counter )->reset( p, d_tgt, q );
+ getChild( d_child_counter )->reset( p, d_tgt, qi );
}else{
d_child_counter = -1;
}
@@ -1486,20 +838,20 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) }else if( d_n.getKind()==IFF ){
//construct match based on both children
if( d_child_counter%2==0 ){
- if( getChild( 0 )->getNextMatch( p, q ) ){
+ if( getChild( 0 )->getNextMatch( p, qi ) ){
d_child_counter++;
- getChild( 1 )->reset( p, d_child_counter==1, q );
+ getChild( 1 )->reset( p, d_child_counter==1, qi );
}else{
if( d_child_counter==0 ){
d_child_counter = 2;
- getChild( 0 )->reset( p, !d_tgt, q );
+ getChild( 0 )->reset( p, !d_tgt, qi );
}else{
d_child_counter = -1;
}
}
}
if( d_child_counter%2==1 ){
- if( getChild( 1 )->getNextMatch( p, q ) ){
+ if( getChild( 1 )->getNextMatch( p, qi ) ){
success = true;
}else{
d_child_counter--;
@@ -1508,21 +860,21 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) }else if( d_n.getKind()==ITE ){
if( d_child_counter%2==0 ){
int index1 = d_child_counter==4 ? 1 : 0;
- if( getChild( index1 )->getNextMatch( p, q ) ){
+ if( getChild( index1 )->getNextMatch( p, qi ) ){
d_child_counter++;
- getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, q );
+ getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, qi );
}else{
if( d_child_counter==4 ){
d_child_counter = -1;
}else{
d_child_counter +=2;
- getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, q );
+ getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
}
}
}
if( d_child_counter%2==1 ){
int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);
- if( getChild( index2 )->getNextMatch( p, q ) ){
+ if( getChild( index2 )->getNextMatch( p, qi ) ){
success = true;
}else{
d_child_counter--;
@@ -1538,12 +890,13 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) return false;
}
-bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
+bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
if( !d_qn.empty() ){
if( d_qn[0]==NULL ){
d_qn.clear();
return true;
}else{
+ Assert( d_type==typ_var );
Assert( d_qni_size>0 );
bool invalidMatch;
do {
@@ -1556,11 +909,11 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { 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
- int repVar = p->d_qinfo[q].getCurrentRepVar( itv->second );
+ int repVar = qi->getCurrentRepVar( itv->second );
Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;
//get the value the rep variable
- std::map< int, Node >::iterator itm = p->d_qinfo[q].d_match.find( repVar );
- if( itm!=p->d_qinfo[q].d_match.end() ){
+ std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );
+ if( itm!=qi->d_match.end() ){
val = itm->second;
Assert( !val.isNull() );
Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;
@@ -1571,7 +924,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { if( it != d_qn[index]->d_children.end() ) {
d_qni.push_back( it );
//set the match
- if( p->d_qinfo[q].setMatch( p, d_qni_bound[index], it->first ) ){
+ if( qi->setMatch( p, d_qni_bound[index], it->first ) ){
Debug("qcf-match-debug") << " Binding variable" << std::endl;
if( d_qn.size()<d_qni_size ){
d_qn.push_back( &it->second );
@@ -1616,7 +969,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { d_qni[index]++;
if( d_qni[index]!=d_qn[index]->d_children.end() ){
success = true;
- if( p->d_qinfo[q].setMatch( p, itb->second, d_qni[index]->first ) ){
+ if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){
Debug("qcf-match-debug") << " Bind next variable" << std::endl;
if( d_qn.size()<d_qni_size ){
d_qn.push_back( &d_qni[index]->second );
@@ -1643,14 +996,14 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { //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;
- Debug("qcf-match-debug") << " We matched " << t << std::endl;
+ 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 ){
- if( it->second<(int)q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term
- Assert( it->first>0 );
- Assert( p->d_qinfo[q].d_match.find( it->second )!=p->d_qinfo[q].d_match.end() );
- Assert( p->areEqual( t[it->first-1], p->d_qinfo[q].d_match[ it->second ] ) );
- p->d_qinfo[q].d_match_term[it->second] = t[it->first-1];
+ Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
+ if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){ //if it is an actual variable, we are interested in knowing the actual term
+ Assert( qi->d_match.find( it->second )!=qi->d_match.end() );
+ Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
+ qi->d_match_term[it->second] = t[it->first-1];
}
}
}
@@ -1659,7 +1012,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { return !d_qn.empty();
}
-void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
+void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
if( isTrace ){
switch( typ ){
case typ_invalid: Trace(c) << "invalid";break;
@@ -1683,12 +1036,679 @@ void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, boo }
}
-void QuantConflictFind::MatchGen::setInvalid() {
+void MatchGen::setInvalid() {
d_type = typ_invalid;
d_children.clear();
}
+
+QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ),
+d_c( c ),
+d_conflict( c, false ),
+d_qassert( c ) {
+ d_fid_count = 0;
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {
+ if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){
+ index = 0;
+ return n;
+ }else if( isHandledUfTerm( n ) ){
+ /*
+ std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );
+ if( it==d_op_node.end() ){
+ std::vector< Node > children;
+ children.push_back( n.getOperator() );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ children.push_back( getFv( n[i].getType() ) );
+ }
+ Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ d_op_node[n.getOperator()] = nn;
+ return nn;
+ }else{
+ return it->second;
+ }*/
+ index = 1;
+ return n.getOperator();
+ }else{
+ return Node::null();
+ }
+}
+
+Node QuantConflictFind::mkEqNode( Node a, Node b ) {
+ if( a.getType().isBoolean() ){
+ return a.iffNode( b );
+ }else{
+ return a.eqNode( b );
+ }
+}
+
+//-------------------------------------------------- registration
+
+void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {
+ if( n.getKind()==FORALL ){
+ //do nothing
+ }else{
+ //qcf->d_node = n;
+ bool recurse = true;
+ 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 || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ flatten( q, n[i] );
+ }
+ }else if( n.getKind()==EQUAL ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ for( unsigned j=0; j<n[i].getNumChildren(); j++ ){
+ flatten( q, n[i][j] );
+ }
+ }
+ }
+
+ */
+
+ if( n.getKind()==APPLY_UF ){
+ flatten( q, n );
+ }else if( n.getKind()==EQUAL ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ flatten( q, n[i] );
+ }
+ }
+
+ }else{
+ Trace("qcf-qregister") << " RegisterGroundLit : " << n;
+ }
+ recurse = false;
+ }
+ if( recurse ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+ //QcfNode * qcfc = new QcfNode( d_c );
+ //qcfc->d_parent = qcf;
+ //qcf->d_child[i] = qcfc;
+ registerNode( q, n[i], newHasPol, newPol );
+ }
+ }
+ }
+}
+
+void QuantConflictFind::flatten( Node q, Node n ) {
+ if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){
+ if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){
+ //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;
+ d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();
+ d_qinfo[q].d_vars.push_back( n );
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ flatten( q, n[i] );
+ }
+ }
+}
+
+void QuantConflictFind::registerQuantifier( Node q ) {
+ d_quants.push_back( q );
+ d_quant_id[q] = d_quants.size();
+ d_qinfo[q].d_q = q;
+ Trace("qcf-qregister") << "Register ";
+ debugPrintQuant( "qcf-qregister", q );
+ Trace("qcf-qregister") << " : " << q << std::endl;
+
+ //register the variables
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ d_qinfo[q].d_var_num[q[0][i]] = i;
+ d_qinfo[q].d_vars.push_back( q[0][i] );
+ }
+
+ //make QcfNode structure
+ Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
+ //d_qinfo[q].d_cf = new QcfNode( d_c );
+ registerNode( q, q[1], true, true );
+
+ //debug print
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
+ Trace("qcf-qregister") << " ";
+ debugPrintQuantBody( "qcf-qregister", q, q[1] );
+ Trace("qcf-qregister") << std::endl;
+ if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
+ Trace("qcf-qregister") << " with additional constraints : " << std::endl;
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
+ Trace("qcf-qregister") << " ?x" << j << " = ";
+ debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
+ Trace("qcf-qregister") << std::endl;
+ }
+ }
+
+ Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
+ d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );
+
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
+ d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );
+ if( !d_qinfo[q].d_var_mg[j]->isValid() ){
+ d_qinfo[q].d_mg->setInvalid();
+ break;
+ }
+ }
+
+ Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+}
+
+int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
+ int ret = 0;
+ if( n.getKind()==EQUAL ){
+ Node n1 = evaluateTerm( n[0] );
+ Node n2 = evaluateTerm( n[1] );
+ Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
+ if( areEqual( n1, n2 ) ){
+ ret = 1;
+ }else if( areDisequal( n1, n2 ) ){
+ ret = -1;
+ }
+ //else if( d_effort>QuantConflictFind::effort_conflict ){
+ // ret = -1;
+ //}
+ }else if( n.getKind()==APPLY_UF ){ //predicate
+ Node nn = evaluateTerm( n );
+ Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
+ if( areEqual( nn, d_true ) ){
+ ret = 1;
+ }else if( areEqual( nn, d_false ) ){
+ ret = -1;
+ }
+ //else if( d_effort>QuantConflictFind::effort_conflict ){
+ // ret = -1;
+ //}
+ }else if( n.getKind()==NOT ){
+ return -evaluate( n[0] );
+ }else if( n.getKind()==ITE ){
+ int cev1 = evaluate( n[0] );
+ int cevc[2] = { 0, 0 };
+ for( unsigned i=0; i<2; i++ ){
+ if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){
+ cevc[i] = evaluate( n[i+1] );
+ if( cev1!=0 ){
+ ret = cevc[i];
+ break;
+ }else if( cevc[i]==0 ){
+ break;
+ }
+ }
+ }
+ if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){
+ ret = cevc[0];
+ }
+ }else if( n.getKind()==IFF ){
+ int cev1 = evaluate( n[0] );
+ if( cev1!=0 ){
+ int cev2 = evaluate( n[1] );
+ if( cev2!=0 ){
+ ret = cev1==cev2 ? 1 : -1;
+ }
+ }
+
+ }else{
+ int ssval = 0;
+ if( n.getKind()==OR ){
+ ssval = 1;
+ }else if( n.getKind()==AND ){
+ ssval = -1;
+ }
+ bool isUnk = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int cev = evaluate( n[i] );
+ if( cev==ssval ){
+ ret = ssval;
+ break;
+ }else if( cev==0 ){
+ isUnk = true;
+ }
+ }
+ if( ret==0 && !isUnk ){
+ ret = -ssval;
+ }
+ }
+ Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;
+ return ret;
+}
+
+bool QuantConflictFind::isPropagationSet() {
+ return !d_prop_eq[0].isNull();
+}
+
+bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
+ //if( d_effort==QuantConflictFind::effort_prop_deq ){
+ // return n1==n2 || !areDisequal( n1, n2 );
+ //}else{
+ return n1==n2;
+ //}
+}
+
+bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
+ //if( d_effort==QuantConflictFind::effort_conflict ){
+ // return areDisequal( n1, n2 );
+ //}else{
+ return n1!=n2;
+ //}
+}
+
+//-------------------------------------------------- handling assertions / eqc
+
+void QuantConflictFind::assertNode( Node q ) {
+ Trace("qcf-proc") << "QCF : assertQuantifier : ";
+ debugPrintQuant("qcf-proc", q);
+ Trace("qcf-proc") << std::endl;
+ d_qassert.push_back( q );
+ //set the eqRegistries that this depends on to true
+ //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
+ // it->first->d_active.set( true );
+ //}
+}
+
+eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
+ //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
+ return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+}
+bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
+ return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
+}
+bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {
+ return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
+}
+Node QuantConflictFind::getRepresentative( Node n ) {
+ if( getEqualityEngine()->hasTerm( n ) ){
+ return getEqualityEngine()->getRepresentative( n );
+ }else{
+ return n;
+ }
+}
+Node QuantConflictFind::evaluateTerm( Node n ) {
+ if( isHandledUfTerm( n ) ){
+ Node nn;
+ if( getEqualityEngine()->hasTerm( n ) ){
+ computeArgReps( n );
+ nn = d_uf_terms[n.getOperator()].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 );
+ }
+ if( !nn.isNull() ){
+ Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
+ return getRepresentative( nn );
+ }else{
+ Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
+ return n;
+ }
+ }
+ return getRepresentative( n );
+}
+
+/*
+QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {
+ std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );
+ if( it2==d_eqc_info.end() ){
+ if( doCreate ){
+ EqcInfo * eqci = new EqcInfo( d_c );
+ d_eqc_info[n] = eqci;
+ return eqci;
+ }else{
+ return NULL;
+ }
+ }
+ return it2->second;
+}
+*/
+
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {
+ std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );
+ if( itut==d_eqc_uf_terms.end() ){
+ return NULL;
+ }else{
+ if( eqc.isNull() ){
+ return &itut->second;
+ }else{
+ std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );
+ if( itute!=itut->second.d_children.end() ){
+ return &itute->second;
+ }else{
+ return NULL;
+ }
+ }
+ }
+}
+
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {
+ std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );
+ if( itut!=d_uf_terms.end() ){
+ return &itut->second;
+ }else{
+ return NULL;
+ }
+}
+
+/** new node */
+void QuantConflictFind::newEqClass( Node n ) {
+ //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
+ //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;
+}
+
+/** merge */
+void QuantConflictFind::merge( Node a, Node b ) {
+ /*
+ if( b.getKind()==EQUAL ){
+ if( a==d_true ){
+ //will merge anyways
+ //merge( b[0], b[1] );
+ }else if( a==d_false ){
+ assertDisequal( b[0], b[1] );
+ }
+ }else{
+ Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;
+ EqcInfo * eqc_b = getEqcInfo( b, false );
+ EqcInfo * eqc_a = NULL;
+ if( eqc_b ){
+ eqc_a = getEqcInfo( a );
+ //move disequalities of b into a
+ for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){
+ if( (*it).second ){
+ Node n = (*it).first;
+ EqcInfo * eqc_n = getEqcInfo( n, false );
+ Assert( eqc_n );
+ if( !eqc_n->isDisequal( a ) ){
+ Assert( !eqc_a->isDisequal( n ) );
+ eqc_n->setDisequal( a );
+ eqc_a->setDisequal( n );
+ //setEqual( eqc_a, eqc_b, a, n, false );
+ }
+ eqc_n->setDisequal( b, false );
+ }
+ }
+ ////move all previous EqcRegistry's regarding equalities within b
+ //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){
+ // if( (*it).second ){
+ // eqc_a->d_rel_eqr_e[(*it).first] = true;
+ // }
+ //}
+ }
+ //process new equalities
+ //setEqual( eqc_a, eqc_b, a, b, true );
+ Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;
+ }
+ */
+}
+
+/** assert disequal */
+void QuantConflictFind::assertDisequal( Node a, Node b ) {
+ /*
+ a = getRepresentative( a );
+ b = getRepresentative( b );
+ Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;
+ EqcInfo * eqc_a = getEqcInfo( a );
+ EqcInfo * eqc_b = getEqcInfo( b );
+ if( !eqc_a->isDisequal( b ) ){
+ Assert( !eqc_b->isDisequal( a ) );
+ eqc_b->setDisequal( a );
+ eqc_a->setDisequal( b );
+ //setEqual( eqc_a, eqc_b, a, b, false );
+ }
+ Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;
+ */
+}
+
+//-------------------------------------------------- check function
+
+/** check */
+void QuantConflictFind::check( Theory::Effort level ) {
+ Trace("qcf-check") << "QCF : check : " << level << std::endl;
+ if( d_conflict ){
+ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
+ if( level>=Theory::EFFORT_FULL ){
+ Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
+ //Assert( false );
+ }
+ }else{
+ int addedLemmas = 0;
+ if( d_performCheck ){
+ ++(d_statistics.d_inst_rounds);
+ double clSet = 0;
+ if( Trace.isOn("qcf-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
+ }
+ Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
+ computeRelevantEqr();
+
+ if( Trace.isOn("qcf-debug") ){
+ Trace("qcf-debug") << std::endl;
+ debugPrint("qcf-debug");
+ Trace("qcf-debug") << std::endl;
+ }
+ short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;
+ for( short e = effort_conflict; e<=end_e; e++ ){
+ d_effort = e;
+ if( e == effort_prop_eq ){
+ for( unsigned i=0; i<2; i++ ){
+ d_prop_eq[i] = Node::null();
+ }
+ }
+ Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
+ for( unsigned j=0; j<d_qassert.size(); j++ ){
+ Node q = d_qassert[j];
+ QuantInfo * qi = &d_qinfo[q];
+ Trace("qcf-check") << "Check quantified formula ";
+ debugPrintQuant("qcf-check", q);
+ Trace("qcf-check") << " : " << q << "..." << std::endl;
+
+ Assert( d_qinfo.find( q )!=d_qinfo.end() );
+ if( qi->d_mg->isValid() ){
+ qi->reset_round( this );
+ //try to make a matches making the body false
+ qi->d_mg->reset( this, false, qi );
+ while( qi->d_mg->getNextMatch( this, qi ) ){
+
+ Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-check");
+ Trace("qcf-check") << std::endl;
+
+ if( !qi->isMatchSpurious( this ) ){
+ std::vector< int > assigned;
+ if( qi->completeMatch( this, assigned ) ){
+ InstMatch m;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ //Node cv = qi->getCurrentValue( qi->d_match[i] );
+ int repVar = qi->getCurrentRepVar( i );
+ Node cv;
+ std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
+ if( itmt!=qi->d_match_term.end() ){
+ cv = itmt->second;
+ }else{
+ cv = qi->d_match[repVar];
+ }
+
+
+ Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;
+ m.set( d_quantEngine, q, i, cv );
+ }
+ if( Debug.isOn("qcf-check-inst") ){
+ //if( e==effort_conflict ){
+ Node inst = d_quantEngine->getInstantiation( q, m );
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+ Assert( evaluate( inst )!=1 );
+ Assert( evaluate( inst )==-1 || e>effort_conflict );
+ //}
+ }
+ if( d_quantEngine->addInstantiation( q, m ) ){
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;
+ ++addedLemmas;
+ if( e==effort_conflict ){
+ d_conflict.set( true );
+ ++(d_statistics.d_conflict_inst);
+ break;
+ }else if( e==effort_prop_eq ){
+ ++(d_statistics.d_prop_inst);
+ }
+ }else{
+ Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
+ //Assert( false );
+ }
+ //clean up assigned
+ for( unsigned i=0; i<assigned.size(); i++ ){
+ qi->d_match.erase( assigned[i] );
+ }
+ }else{
+ Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+ }
+ }else{
+ Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;
+ }
+ }
+ }
+ if( d_conflict ){
+ break;
+ }
+ }
+ if( addedLemmas>0 ){
+ d_quantEngine->flushLemmas();
+ break;
+ }
+ }
+ if( Trace.isOn("qcf-engine") ){
+ 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") << ", addedLemmas = " << addedLemmas;
+ }
+ Trace("qcf-engine") << std::endl;
+ }
+ }
+ Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
+ }
+}
+
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {
+ d_performCheck = false;
+ if( !d_conflict ){
+ if( level==Theory::EFFORT_LAST_CALL ){
+ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
+ }else if( level==Theory::EFFORT_FULL ){
+ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
+ }else if( level==Theory::EFFORT_STANDARD ){
+ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+ }
+ }
+ return d_performCheck;
+}
+
+void QuantConflictFind::computeRelevantEqr() {
+ d_uf_terms.clear();
+ d_eqc_uf_terms.clear();
+ d_eqcs.clear();
+ d_arg_reps.clear();
+ double clSet = 0;
+ if( Trace.isOn("qcf-opt") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ }
+
+ long nTermst = 0;
+ long nTerms = 0;
+ long nEqc = 0;
+
+ //which nodes are irrelevant for disequality matches
+ std::map< TNode, bool > irrelevant_dnode;
+ //now, store matches
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
+ while( !eqcs_i.isFinished() ){
+ nEqc++;
+ Node r = (*eqcs_i);
+ d_eqcs[r.getType()].push_back( r );
+ //EqcInfo * eqcir = getEqcInfo( r, false );
+ //get relevant nodes that we are disequal from
+ /*
+ std::vector< Node > deqc;
+ if( eqcir ){
+ for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){
+ if( (*it).second ){
+ //Node rd = (*it).first;
+ //if( rd!=getRepresentative( rd ) ){
+ // std::cout << "Bad rep!" << std::endl;
+ // exit( 0 );
+ //}
+ deqc.push_back( (*it).first );
+ }
+ }
+ }
+ */
+ //process disequalities
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
+ while( !eqc_i.isFinished() ){
+ TNode n = (*eqc_i);
+ if( n.getKind()!=EQUAL ){
+ nTermst++;
+ //node_to_rep[n] = r;
+ //if( n.getNumChildren()>0 ){
+ // if( n.getKind()!=APPLY_UF ){
+ // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;
+ // }
+ //}
+
+ bool isRedundant;
+ std::map< TNode, std::vector< TNode > >::iterator it_na;
+ TNode fn;
+ if( isHandledUfTerm( 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] );
+ isRedundant = (nadd!=n);
+ d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );
+ if( !isRedundant ){
+ int jindex;
+ fn = getFunction( n, jindex );
+ }
+ }else{
+ isRedundant = false;
+ }
+ nTerms += isRedundant ? 0 : 1;
+ }
+ ++eqc_i;
+ }
+ //process_eqc[r] = true;
+ ++eqcs_i;
+ }
+ if( Trace.isOn("qcf-opt") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
+ Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;
+ Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;
+ Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;
+ }
+}
+
+void QuantConflictFind::computeArgReps( TNode n ) {
+ if( d_arg_reps.find( n )==d_arg_reps.end() ){
+ Assert( isHandledUfTerm( n ) );
+ for( unsigned j=0; j<n.getNumChildren(); j++ ){
+ d_arg_reps[n].push_back( getRepresentative( n[j] ) );
+ }
+ }
+}
+bool QuantConflictFind::isHandledUfTerm( TNode n ) {
+ return n.getKind()==APPLY_UF;
+}
+
+
//-------------------------------------------------- debugging
|