From: Andrew Reynolds Date: Fri, 10 Jan 2014 08:04:51 +0000 (-0600) Subject: Add new method --quant-cf for finding conflicts eagerly for quantified formulas.... X-Git-Tag: cvc5-1.0.0~7155 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=841b7951f41f399859afab13a81e04599308da61;p=cvc5.git Add new method --quant-cf for finding conflicts eagerly for quantified formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup. --- diff --git a/src/Makefile.am b/src/Makefile.am index eda6acd6b..e5e1b9346 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -293,6 +293,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/symmetry_breaking.cpp \ theory/quantifiers/qinterval_builder.h \ theory/quantifiers/qinterval_builder.cpp \ + theory/quantifiers/quant_conflict_find.h \ + theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/options_handlers.h \ theory/rewriterules/theory_rewriterules_rules.h \ theory/rewriterules/theory_rewriterules_rules.cpp \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 014d3c603..3c3bbe971 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -77,6 +77,7 @@ #include "prop/options.h" #include "theory/arrays/options.h" #include "util/sort_inference.h" +#include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/macros.h" #include "theory/datatypes/options.h" #include "theory/quantifiers/first_order_reasoning.h" @@ -1149,6 +1150,10 @@ void SmtEngine::setLogicInternal() throw() { options::mbqiMode.set( quantifiers::MBQI_FMC ); } } + if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ + //must do pre-skolemization + options::preSkolemQuant.set( true ); + } if( options::ufssSymBreak() ){ options::sortInference.set( true ); } @@ -3042,35 +3047,35 @@ void SmtEnginePrivate::processAssertions() { d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); } } - - dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); - if( options::preSkolemQuant() ){ - //apply pre-skolemization to existential quantifiers - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Node prev = d_assertionsToPreprocess[i]; - vector< Node > fvs; - d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) ); - if( prev!=d_assertionsToPreprocess[i] ){ - Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; - Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; + if( d_smt.d_logic.isQuantified() ){ + dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); + if( options::preSkolemQuant() ){ + //apply pre-skolemization to existential quantifiers + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + Node prev = d_assertionsToPreprocess[i]; + vector< Node > fvs; + d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) ); + if( prev!=d_assertionsToPreprocess[i] ){ + Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; + Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; + } } } - } - dumpAssertions("post-skolem-quant", d_assertionsToPreprocess); - - if( options::macrosQuant() ){ - //quantifiers macro expansion - bool success; - do{ - QuantifierMacros qm; - success = qm.simplify( d_assertionsToPreprocess, true ); - }while( success ); - } + dumpAssertions("post-skolem-quant", d_assertionsToPreprocess); + if( options::macrosQuant() ){ + //quantifiers macro expansion + bool success; + do{ + QuantifierMacros qm; + success = qm.simplify( d_assertionsToPreprocess, true ); + }while( success ); + } - Trace("fo-rsn-enable") << std::endl; - if( options::foPropQuant() ){ - FirstOrderPropagation fop; - fop.simplify( d_assertionsToPreprocess ); + Trace("fo-rsn-enable") << std::endl; + if( options::foPropQuant() ){ + FirstOrderPropagation fop; + fop.simplify( d_assertionsToPreprocess ); + } } if( options::sortInference() ){ @@ -3078,6 +3083,10 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess ); } + //if( options::quantConflictFind() ){ + // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess ); + //} + dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 28485a979..d4faf41fe 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -198,10 +198,9 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, void BoundedIntegers::process( Node f, Node n, bool pol, std::map< int, std::map< Node, Node > >& bound_lit_map, std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){ - if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){ + if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){ for( unsigned i=0; igetNumTerms(); @@ -182,7 +182,7 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ //evaluate subterm int childDepIndex; - Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i]; + Node nn = n[i]; int eValT = evaluate( nn, childDepIndex, ri ); if( eValT==baseVal ){ if( eVal==baseVal ){ @@ -210,12 +210,12 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ }else{ return 0; } - }else if( n.getKind()==IFF || n.getKind()==XOR ){ + }else if( n.getKind()==IFF ){ int depIndex1; int eVal = evaluate( n[0], depIndex1, ri ); if( eVal!=0 ){ int depIndex2; - int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2, ri ); + int eVal2 = evaluate( n[1], depIndex2, ri ); if( eVal2!=0 ){ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; return eVal==eVal2 ? 1 : -1; diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 9cd12fbfb..600f8c0b9 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -233,7 +233,7 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ if( n.getKind()==NOT ){ process( n[0], !pol, args, f ); - }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){ + }else if( n.getKind()==AND || n.getKind()==OR ){ //bool favorPol = (n.getKind()==AND)==pol; //conditional? }else if( n.getKind()==ITE ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index cb63ccd45..493d54b53 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -929,13 +929,13 @@ Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, Node ret; if( n.getKind()==NOT ){ ret = getSelectionFormula( fn[0], n[0], !polarity, useOption ); - }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){ + }else if( n.getKind()==OR || n.getKind()==AND ){ //whether we only need to find one or all bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity ); std::vector< Node > children; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i]; - Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i]; + Node fnc = fn[i]; + Node nc = n[i]; Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); if( nn.isNull() && !favorPol ){ //cannot make selection formula @@ -993,8 +993,8 @@ Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){ ret = mkAndSelectionFormula( nc[0], nc[1] ); } - }else if( n.getKind()==IFF || n.getKind()==XOR ){ - bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF; + }else if( n.getKind()==IFF ){ + bool opPol = !polarity; for( int p=0; p<2; p++ ){ Node nn[2]; for( int i=0; i<2; i++ ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f314584cd..bc717bbbc 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -178,15 +178,17 @@ int ModelEngine::checkModel(){ it != fm->d_rep_set.d_type_reps.end(); ++it ){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - Trace("model-engine-debug") << " "; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); - for( size_t i=0; isecond.size(); i++ ){ - //Trace("model-engine-debug") << it->second[i] << " "; - Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); - Trace("model-engine-debug") << r << " "; + if( Trace.isOn("model-engine-debug") ){ + Trace("model-engine-debug") << " "; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + for( size_t i=0; isecond.size(); i++ ){ + //Trace("model-engine-debug") << it->second[i] << " "; + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Trace("model-engine-debug") << r << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; } - Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; } } } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 190c7ddc9..652526cc9 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -40,7 +40,7 @@ option clauseSplit --clause-split bool :default false # Whether to pre-skolemize quantifier bodies. # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to # forall x. P( x ) => f( S( x ) ) = x -option preSkolemQuant --pre-skolem-quant bool :default false +option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas option iteRemoveQuant --ite-remove-quant bool :default false apply ite removal to bodies of quantifiers @@ -119,5 +119,7 @@ option fmfBoundInt --fmf-bound-int bool :default false option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms +option quantConflictFind --quant-cf bool :default false + enable eager conflict find mechanism for quantifiers endmodule diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp new file mode 100755 index 000000000..58840989d --- /dev/null +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -0,0 +1,1712 @@ +/********************* */ +/*! \file quant_conflict_find.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief quant conflict find class + ** + **/ + +#include + +#include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/theory_engine.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace std; + +namespace CVC4 { + +Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) { + if( index==(int)n.getNumChildren() ){ + if( d_children.empty() ){ + if( doAdd ){ + d_children[ n ].clear(); + return n; + }else{ + return Node::null(); + } + }else{ + return d_children.begin()->first; + } + }else{ + Node r = qcf->getRepresentative( n[index] ); + return d_children[r].addTerm( qcf, n, doAdd, index+1 ); + } +} + +bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index ) { + if( index==(int)n1.getNumChildren() ){ + Node n = addTerm( qcf, n2 ); + return n==n2; + }else{ + Node r = qcf->getRepresentative( n1[index] ); + return d_children[r].addTermEq( qcf, n1, n2, index+1 ); + } +} + +void QcfNodeIndex::debugPrint( const char * c, int t ) { + for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ + if( !it->first.isNull() ){ + for( int j=0; jfirst << " : " << std::endl; + it->second.debugPrint( c, t+1 ); + } + } +} + +EqRegistry::EqRegistry( context::Context* c ) : d_active( c, false ){//: d_t_eqc( c ){ + +} + +void EqRegistry::debugPrint( const char * c, int t ) { + d_qni.debugPrint( c, t ); +} + +//QcfNode::QcfNode( context::Context* c ) : d_parent( NULL ){ +// d_reg[0] = NULL; +// d_reg[1] = NULL; +//} + +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(true); + d_false = NodeManager::currentNM()->mkConst(false); + getFunctionId( d_true ); + getFunctionId( d_false ); +} + +int QuantConflictFind::getFunctionId( Node f ) { + std::map< Node, int >::iterator it = d_fid.find( f ); + if( it==d_fid.end() ){ + d_fid[f] = d_fid_count; + d_fid_count++; + return d_fid[f]; + } + return it->second; +} + +bool QuantConflictFind::isLessThan( Node a, Node b ) { + Assert( a.getKind()==APPLY_UF ); + Assert( b.getKind()==APPLY_UF ); + /* + if( a.getOperator()==b.getOperator() ){ + for( unsigned i=0; ibcr ){ + return false; + } + } + return false; + }else{ + */ + return getFunctionId( a.getOperator() )::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; imkNode( APPLY_UF, children ); + d_op_node[n.getOperator()] = nn; + return nn; + }else{ + return it->second; + } + }else{ + //should be a variable + return Node::null(); + } +} + +Node QuantConflictFind::getFv( TypeNode tn ) { + if( d_fv.find( tn )==d_fv.end() ){ + std::stringstream ss; + ss << "_u"; + d_fv[tn] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is for QCF" ); + } + return d_fv[tn]; +} + +Node QuantConflictFind::mkEqNode( Node a, Node b ) { + if( a.getType().isBoolean() ){ + return a.iffNode( b ); + }else{ + return a.eqNode( b ); + } +} + +//-------------------------------------------------- registration + +/* +void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) { + for( unsigned i=0; id_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 + for( unsigned i=0; i<2; i++ ){ + if( !hasPol || ( pol!=(i==0) ) ){ + EqRegistry * eqr = getEqRegistry( i==0, n ); + if( eqr ){ + d_qinfo[q].d_rel_eqr[ eqr ] = true; + } + } + } + if( n.getKind()==APPLY_UF || + ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){ + flatten( q, n ); + }else{ + for( unsigned i=0; id_parent = qcf; + //qcf->d_child[i] = qcfc; + registerQuant( q, n[i], newHasPol, newPol ); + } + } +} + +void QuantConflictFind::flatten( Node q, Node n ) { + for( unsigned i=0; iq[0].getNumChildren() ){ + Trace("qcf-qregister") << " with additional constraints : " << std::endl; + for( unsigned j=q[0].getNumChildren(); j::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::getTerm( Node n ) { + if( n.getKind()==APPLY_UF ){ + Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false ); + if( !nn.isNull() ){ + return nn; + } + } + return n; +} + +QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) { + /* + NodeBoolMap::iterator it = d_eqc.find( n ); + if( it==d_eqc.end() ){ + if( doCreate ){ + d_eqc[n] = true; + }else{ + //equivalence class does not currently exist + return NULL; + } + }else{ + //should only ask for valid equivalence classes + Assert( (*it).second ); + } + */ + 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; +} + +/** 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; + }else{ + bool addedLemma = false; + if( level==Theory::EFFORT_FULL ){ + 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(); + + Trace("qcf-debug") << std::endl; + debugPrint("qcf-debug"); + Trace("qcf-debug") << std::endl; + + + Trace("qcf-check") << "Checking quantified formulas..." << std::endl; + for( unsigned j=0; jisValid() ){ + 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 : " << std::endl; + d_qinfo[q].debugPrintMatch("qcf-check"); + Trace("qcf-check") << std::endl; + + if( !d_qinfo[q].isMatchSpurious( this ) ){ + //assign values for variables that were unassigned (usually not necessary, but handles corner cases) + Trace("qcf-check") << std::endl; + std::vector< int > unassigned; + std::vector< TypeNode > unassigned_tn; + for( int i=0; i eqc_count; + do { + bool invalidMatch; + while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){ + invalidMatch = false; + if( index==(int)eqc_count.size() ){ + eqc_count.push_back( 0 ); + }else{ + Assert( index==(int)eqc_count.size()-1 ); + if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){ + int currIndex = eqc_count[index]; + eqc_count[index]++; + Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl; + if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){ + Trace("qcf-check-unassign") << "Succeeded match" << std::endl; + index++; + }else{ + Trace("qcf-check-unassign") << "Failed match" << std::endl; + invalidMatch = true; + } + }else{ + Trace("qcf-check-unassign") << "No more matches" << std::endl; + eqc_count.pop_back(); + index--; + } + } + } + success = index>=0; + if( success ){ + index = (int)unassigned.size()-1; + Trace("qcf-check-unassign") << " Try: " << std::endl; + for( unsigned i=0; i " << d_qinfo[q].d_match[ui] << std::endl; + } + } + }while( success && d_qinfo[q].isMatchSpurious( this ) ); + } + + if( success ){ + InstMatch m; + for( unsigned i=0; i " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl; + m.set( d_quantEngine, q, i, cv ); + } + if( Debug.isOn("qcf-check-inst") ){ + Node inst = d_quantEngine->getInstantiation( q, m ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( evaluate( inst )==-1 ); + } + if( d_quantEngine->addInstantiation( q, m ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + d_quantEngine->flushLemmas(); + d_conflict.set( true ); + addedLemma = true; + break; + }else{ + Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; + Assert( false ); + } + }else{ + Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; + } + for( unsigned i=0; i >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){ + for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + it2->second->clear(); + } + } + } + d_uf_terms.clear(); + d_eqc_uf_terms.clear(); + d_eqcs.clear(); + + //which nodes are irrelevant for disequality matches + std::map< Node, bool > irrelevant_dnode; + //which eqc we have processed + std::map< Node, bool > process_eqc; + //now, store matches + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); + while( !eqcs_i.isFinished() ){ + 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 we have processed the other direction + if( process_eqc.find( rd )!=process_eqc.end() ){ + eq::EqClassIterator eqcd_i = eq::EqClassIterator( rd, getEqualityEngine() ); + while( !eqcd_i.isFinished() ){ + Node nd = (*eqcd_i); + if( irrelevant_dnode.find( nd )==irrelevant_dnode.end() ){ + deqc.push_back( nd ); + } + ++eqcd_i; + } + } + } + } + } + //the relevant nodes in this eqc + std::vector< Node > eqc; + //process disequalities + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + bool isRedundant; + if( n.getKind()==APPLY_UF ){ + Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n ); + isRedundant = (nadd!=n); + d_uf_terms[n.getOperator()].addTerm( this, n ); + }else{ + isRedundant = false; + } + //process all relevant equalities and disequalities to n + for( unsigned index=0; index<2; index++ ){ + std::map< Node, std::map< Node, EqRegistry * > >::iterator itn[2]; + itn[0] = d_eqr[index].find( n ); + Node fn; + if( n.getKind()==APPLY_UF && !isRedundant ){ + fn = getFunction( n ); + itn[1] = d_eqr[index].find( fn ); + } + //for n, fn... + bool relevant = false; + for( unsigned j=0; j<2; j++ ){ + //if this node is relevant as an ground term or f-application + if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index].end() ){ + relevant = true; + std::vector< Node >& rel_nodes = index==0 ? eqc : deqc; + for( unsigned i=0; i::iterator itm = itn[j]->second.find( m ); + if( itm!=itn[j]->second.end() ){ + if( itm->second->d_qni.addTerm( this, n )==n ){ + Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; + Trace("qcf-reqr") << fn << " " << m << std::endl; + } + } + } + if( !fm.isNull() ){ + std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm ); + if( itm!=itn[j]->second.end() ){ + if( j==0 ){ + //n with fm + if( itm->second->d_qni.addTerm( this, m )==m ){ + Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; + Trace("qcf-reqr") << n << " " << fm << std::endl; + } + }else{ + //fn with fm + bool mltn = isLessThan( m, n ); + for( unsigned i=0; i<2; i++ ){ + if( i==0 || m.getOperator()==n.getOperator() ){ + Node am = ((i==0)==mltn) ? n : m; + Node an = ((i==0)==mltn) ? m : n; + if( itm->second->d_qni.addTermEq( this, an, am ) ){ + Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for "; + Trace("qcf-reqr") << fn << " " << fm << std::endl; + } + } + } + } + } + } + } + } + } + if( !relevant ){ + //if not relevant for disequalities, store it + if( index==1 ){ + irrelevant_dnode[n] = true; + } + }else{ + //if relevant for equalities, store it + if( index==0 ){ + eqc.push_back( n ); + } + } + } + ++eqc_i; + } + process_eqc[r] = true; + ++eqcs_i; + } +} + + +void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) { + d_match.clear(); + d_curr_var_deq.clear(); + //add built-in variable constraints + for( unsigned r=0; r<2; r++ ){ + for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin(); + it != d_var_constraint[r].end(); ++it ){ + for( unsigned j=0; jsecond.size(); j++ ){ + Node rr = it->second[j]; + if( !isVar( rr ) ){ + rr = p->getRepresentative( rr ); + } + if( addConstraint( p, it->first, rr, r==0 )==-1 ){ + d_var_constraint[0].clear(); + d_var_constraint[1].clear(); + //quantified formula is actually equivalent to true + Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl; + d_mg->d_children.clear(); + d_mg->d_n = NodeManager::currentNM()->mkConst( true ); + d_mg->d_type = MatchGen::typ_ground; + return; + } + } + } + } + d_mg->reset_round( p ); +} + +int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) { + std::map< int, Node >::iterator it = d_match.find( v ); + if( it!=d_match.end() ){ + int vn = getVarNum( it->second ); + if( vn!=-1 ){ + //int vr = getCurrentRepVar( vn ); + //d_match[v] = d_vars[vr]; + //return vr; + return getCurrentRepVar( vn ); + } + } + return v; +} + +Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) { + int v = getVarNum( n ); + if( v==-1 ){ + return n; + }else{ + std::map< int, Node >::iterator it = d_match.find( v ); + if( it==d_match.end() ){ + return n; + }else{ + Assert( getVarNum( it->second )!=v ); + return getCurrentValue( it->second ); + } + } +} + +bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n ) { + //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( !isVar( n ) && !isVar( cv ) ){ + //they must actually be disequal + if( !p->areDisequal( n, cv ) ){ + return false; + } + } + } + return true; +} + +int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ) { + v = getCurrentRepVar( v ); + int vn = getVarNum( n ); + vn = vn==-1 ? -1 : getCurrentRepVar( vn ); + n = getCurrentValue( 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 ) { + //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; + Assert( n==getCurrentValue( n ) ); + Assert( doRemove || v==getCurrentRepVar( v ) ); + Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) ); + if( polarity ){ + if( vn!=v ){ + 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 ); + if( itmn!=d_match.end() && itmn->second==d_vars[v] ){ + return addConstraint( p, vn, d_vars[v], v, true, true ); + }else{ + //unsetting variables equal + + //remove disequalities owned by this + std::vector< Node > remDeq; + for( std::map< Node, int >::iterator it = d_curr_var_deq[vn].begin(); it != d_curr_var_deq[vn].end(); ++it ){ + if( it->second==v ){ + remDeq.push_back( it->first ); + } + } + for( unsigned i=0; i::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 ); + if( itm==d_match.end() ){ + //setting variables equal + bool alreadySet = false; + if( itmn!=d_match.end() ){ + alreadySet = true; + Assert( !itmn->second.isNull() && !isVar( itmn->second ) ); + } + + //copy or check disequalities + std::vector< Node > addDeq; + for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){ + Node dv = getCurrentValue( it->first ); + if( !alreadySet ){ + if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){ + d_curr_var_deq[vn][dv] = v; + addDeq.push_back( dv ); + } + }else{ + if( itmn->second!=dv ){ + Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; + return -1; + } + } + } + if( alreadySet ){ + n = getCurrentValue( n ); + } + }else{ + if( itmn==d_match.end() ){ + Debug("qcf-match-debug") << " ...Reverse direction" << std::endl; + //set the opposite direction + return addConstraint( p, vn, d_vars[v], v, true, false ); + }else{ + Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl; + //are they currently equal + return itm->second==itmn->second ? 0 : -1; + } + } + }else{ + Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl; + if( itm==d_match.end() ){ + + }else{ + //compare ground values + Debug("qcf-match-debug") << " -> Ground value, compare " << itm->second << " "<< n << std::endl; + return itm->second==n ? 0 : -1; + } + } + if( setMatch( p, v, n ) ){ + Debug("qcf-match-debug") << " -> success" << std::endl; + return 1; + }else{ + Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; + return -1; + } + } + }else{ + Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl; + return 0; + } + }else{ + if( vn==v ){ + Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl; + return -1; + }else{ + if( doRemove ){ + Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() ); + d_curr_var_deq[v].erase( n ); + return 1; + }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 ); + if( itm!=d_match.end() ){ + if( getCurrentValue( n )==itm->second ){ + Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; + return -1; + } + } + d_curr_var_deq[v][n] = v; + Debug("qcf-match-debug") << " -> success" << std::endl; + return 1; + }else{ + Debug("qcf-match-debug") << " -> redundant disequality" << std::endl; + return 0; + } + } + } + } +} + +bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node 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; + return true; + }else{ + return false; + } +} + +bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) { + for( int i=0; i::iterator it = d_match.find( i ); + if( it!=d_match.end() ){ + if( !getCurrentCanBeEqual( p, i, it->second ) ){ + return true; + } + } + } + return false; +} + +void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) { + for( int i=0; i "; + if( d_match.find( i )!=d_match.end() ){ + Trace(c) << d_match[i]; + }else{ + Trace(c) << "(unassigned) "; + } + 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 ){ + Trace(c) << it->first << " "; + } + Trace(c) << "}"; + } + Trace(c) << std::endl; + } +} + + +struct MatchGenSort { + QuantConflictFind::MatchGen * d_mg; + bool operator() (int i,int j) { + return d_mg->d_children[i].d_typed_children[j].d_type; + } +}; + +QuantConflictFind::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; + if( isVar ){ + Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() ); + if( n.getKind()==APPLY_UF ){ + d_type = typ_var; + d_type_not = true; //implicit disequality, in disjunction at top level + d_n = n; + qni_apps.push_back( n ); + }else{ + //unknown term + d_type = typ_invalid; + } + }else{ + if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){ + //conjoin extra constraints based on flattening with quantifier body + d_children.push_back( MatchGen( p, q, n ) ); + if( d_children[0].d_type==typ_invalid ){ + d_children.clear(); + d_type = typ_invalid; + }else{ + d_type = typ_top; + } + d_type_not = false; + }else if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ + //we handle not immediately + d_n = n.getKind()==NOT ? n[0] : n; + d_type_not = n.getKind()==NOT; + if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){ + //non-literals + d_type = typ_valid; + for( unsigned i=0; id_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) ); + //make it a built-in constraint instead + for( unsigned i=0; i<2; i++ ){ + if( p->d_qinfo[q].isVar( cn[i] ) ){ + int v = p->d_qinfo[q].getVarNum( cn[i] ); + Node cno = cn[i==0 ? 1 : 0]; + p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno ); + break; + } + } + d_children.pop_back(); + } + } + }else{ + d_type = typ_invalid; + //literals + if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){ + //get the applications (in order) that will be matching + p->getEqRegistryApps( d_n, qni_apps ); + if( qni_apps.size()>0 ){ + d_type =typ_valid_lit; + }else if( d_n.getKind()==EQUAL ){ + bool isValid = true; + for( unsigned i=0; i<2; i++ ){ + if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) && !p->d_qinfo[q].isVar( d_n[i] ) ){ + isValid = false; + break; + } + } + if( isValid ){ + Assert( p->d_qinfo[q].isVar( d_n[0] ) || p->d_qinfo[q].isVar( d_n[1] ) ); + // variable equality + d_type = typ_var_eq; + } + } + } + } + }else{ + //we will just evaluate + d_n = n; + d_type = typ_ground; + } + if( d_type!=typ_invalid ){ + //determine an efficient children ordering + if( !d_children.empty() ){ + for( unsigned i=0; id_qinfo[q].d_vars.size(); j++ ){ + d_children.push_back( MatchGen( p, q, p->d_qinfo[q].d_vars[j], false, true ) ); + } + + //choose variable order for variables based on when they are bound + std::vector< int > varOrder; + varOrder.insert( varOrder.end(), d_children_order.begin(), d_children_order.end() ); + d_children_order.clear(); + std::map< int, bool > bound; + for( unsigned i=0; i::iterator it = d_children[curr].d_qni_var_num.begin(); + it != d_children[curr].d_qni_var_num.end(); ++it ){ + if( it->second>=(int)q[0].getNumChildren() && bound.find( it->second )==bound.end() ){ + bound[ it->second ] = true; + int var = base + it->second - (int)q[0].getNumChildren(); + d_children_order.push_back( var ); + Trace("qcf-qregister-debug") << "Var Order, bound : " << var << std::endl; + } + } + } + for( unsigned j=q[0].getNumChildren(); jd_qinfo[q].d_vars.size(); j++ ){ + if( bound.find( j )==bound.end() ){ + int var = base + j - (int)q[0].getNumChildren(); + d_children_order.push_back( var ); + Trace("qcf-qregister-debug") << "Var Order, remaining : " << j << std::endl; + } + } + } + } + } + if( d_type!=typ_invalid ){ + if( !qni_apps.empty() ){ + Trace("qcf-qregister-debug") << "Initialize matching..." << std::endl; + for( unsigned i=0; id_qinfo[q].isVar( nn ) ){ + Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl; + d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn]; + }else{ + Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl; + d_qni_gterm[d_qni_size] = nn; + } + d_qni_size++; + } + } + } + } + Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = "; + debugPrintType( "qcf-qregister-debug", d_type, true ); + Trace("qcf-qregister-debug") << std::endl; + Assert( d_children.size()==d_children_order.size() ); +} + +void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) { + for( std::map< int, Node >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){ + d_qni_gterm_rep[it->first] = p->getRepresentative( it->second ); + } + for( unsigned i=0; i::iterator itut = p->d_uf_terms.find( f ); + if( itut!=p->d_uf_terms.end() ){ + d_qn.push_back( &itut->second ); + } + } + }else if( d_type==typ_var_eq ){ + bool success = false; + for( unsigned i=0; i<2; i++ ){ + int var = p->d_qinfo[q].getVarNum( d_n[i] ); + if( var!=-1 ){ + int repVar = p->d_qinfo[q].getCurrentRepVar( var ); + Node o = d_n[ i==0 ? 1 : 0 ]; + o = p->d_qinfo[q].getCurrentValue( o ); + int vo = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( o ) ); + int addCons = p->d_qinfo[q].addConstraint( p, repVar, o, vo, d_tgt, false ); + success = addCons!=-1; + //if successful and non-redundant, store that we need to cleanup this + if( addCons==1 ){ + d_qni_bound_cons[repVar] = o; + d_qni_bound[repVar] = vo; + } + break; + } + } + if( success ){ + //store dummy + d_qn.push_back( NULL ); + } + }else if( d_type==typ_valid_lit ){ + //literal + EqRegistry * er = p->getEqRegistry( d_tgt, d_n, false ); + Assert( er ); + d_qn.push_back( &(er->d_qni) ); + }else{ + if( d_children.empty() ){ + //add dummy + d_qn.push_back( NULL ); + }else{ + //reset the first child to d_tgt + d_child_counter = 0; + getChild( d_child_counter )->reset( p, d_tgt, q ); + } + } + Debug("qcf-match") << " Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl; +} + +bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) { + Debug("qcf-match") << " Get next match for : " << d_n << ", type = "; + debugPrintType( "qcf-match", d_type ); + Debug("qcf-match") << ", children = " << d_children.size() << std::endl; + if( d_children.empty() ){ + bool success = doMatching( p, q ); + if( !success ){ + for( std::map< int, Node >::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.find( it->first ); + int vn = itb!=d_qni_bound.end() ? itb->second : -1; + p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true ); + if( vn!=-1 ){ + d_qni_bound.erase( vn ); + } + } + } + d_qni_bound_cons.clear(); + //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->secondd_qinfo[q].getNumVars() ); + p->d_qinfo[q].d_match.erase( it->second ); + } + d_qni_bound.clear(); + } + Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl; + return success; + }else{ + if( d_child_counter!=-1 ){ + bool success = false; + while( !success && d_child_counter>=0 ){ + //transition system based on d_child_counter + 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( d_child_counter<(int)(getNumChildren()-1) ){ + d_child_counter++; + Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", all match " << d_children_order.size() << " " << d_children_order[d_child_counter] << std::endl; + getChild( d_child_counter )->reset( p, d_tgt, q ); + }else{ + success = true; + } + }else{ + d_child_counter--; + } + }else{ + //one child must match + if( !getChild( d_child_counter )->getNextMatch( p, q ) ){ + 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 ); + }else{ + d_child_counter = -1; + } + }else{ + success = true; + } + } + }else if( d_n.getKind()==IFF ){ + //construct match based on both children + if( d_child_counter%2==0 ){ + if( getChild( 0 )->getNextMatch( p, q ) ){ + d_child_counter++; + getChild( 1 )->reset( p, d_child_counter==1, q ); + }else{ + if( d_child_counter==0 ){ + d_child_counter = 2; + getChild( 0 )->reset( p, !d_tgt, q ); + }else{ + d_child_counter = -1; + } + } + } + if( d_child_counter%2==1 ){ + if( getChild( 1 )->getNextMatch( p, q ) ){ + success = true; + }else{ + d_child_counter--; + } + } + }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 ) ){ + d_child_counter++; + getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, q ); + }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 ); + } + } + } + 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 ) ){ + success = true; + }else{ + d_child_counter--; + } + } + } + } + Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl; + return success; + } + } + Debug("qcf-match") << " ...already finished for " << d_n << std::endl; + return false; +} + +bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { + if( !d_qn.empty() ){ + if( d_qn[0]==NULL ){ + d_qn.clear(); + return true; + }else{ + Assert( d_qni_size>0 ); + bool invalidMatch; + do { + invalidMatch = false; + Debug("qcf-match-debug") << " Do matching " << d_qn.size() << " " << d_qni.size() << std::endl; + if( d_qn.size()==d_qni.size()+1 ) { + int index = (int)d_qni.size(); + //initialize + Node 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 + int repVar = p->d_qinfo[q].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() ){ + val = itm->second; + Assert( !val.isNull() ); + Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl; + }else{ + //binding a variable + d_qni_bound[index] = repVar; + std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin(); + 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 ) ){ + Debug("qcf-match-debug") << " Binding variable" << std::endl; + if( d_qn.size()second ); + } + }else{ + Debug("qcf-match") << " Binding variable, currently fail." << std::endl; + invalidMatch = true; + } + }else{ + Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl; + d_qn.pop_back(); + } + } + }else{ + Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl; + Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() ); + Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() ); + val = d_qni_gterm_rep[index]; + Assert( !val.isNull() ); + } + if( !val.isNull() ){ + //constrained by val + std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val ); + if( it!=d_qn[index]->d_children.end() ){ + Debug("qcf-match-debug") << " Match" << std::endl; + d_qni.push_back( it ); + if( d_qn.size()second ); + } + }else{ + Debug("qcf-match-debug") << " Failed to match" << std::endl; + d_qn.pop_back(); + } + } + }else{ + Assert( d_qn.size()==d_qni.size() ); + int index = d_qni.size()-1; + //increment if binding this variable + bool success = false; + std::map< int, int >::iterator itb = d_qni_bound.find( index ); + if( itb!=d_qni_bound.end() ){ + 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 ) ){ + Debug("qcf-match-debug") << " Bind next variable" << std::endl; + if( d_qn.size()second ); + } + }else{ + Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl; + invalidMatch = true; + } + }else{ + Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl; + } + } + //if not incrementing, move to next + if( !success ){ + d_qn.pop_back(); + d_qni.pop_back(); + } + } + if( d_type==typ_var ){ + if( !invalidMatch && d_qni.size()==d_qni_size ){ + //if in the act of binding the variable by this term, bind the variable + std::map< int, Node >::iterator itb = d_qni_bound_cons.begin(); + if( itb!=d_qni_bound_cons.end() ){ + QcfNodeIndex * v_qni = &d_qni[d_qni.size()-1]->second; + Assert( v_qni->d_children.begin()!=v_qni->d_children.end() ); + Node vb = v_qni->d_children.begin()->first; + Assert( !vb.isNull() ); + vb = p->getRepresentative( vb ); + Debug("qcf-match-debug") << " For var, require binding " << itb->first << " to " << vb << ", d_tgt = " << d_tgt << std::endl; + if( !itb->second.isNull() ){ + p->d_qinfo[q].addConstraint( p, itb->first, itb->second, -1, d_tgt, true ); + } + int addCons = p->d_qinfo[q].addConstraint( p, itb->first, vb, -1, d_tgt, false ); + if( addCons==-1 ){ + Debug("qcf-match-debug") << " Failed set for var." << std::endl; + invalidMatch = true; + d_qni_bound_cons[itb->first] = Node::null(); + }else{ + Debug("qcf-match-debug") << " Succeeded set for var." << std::endl; + if( addCons==1 ){ + d_qni_bound_cons[itb->first] = vb; + } + } + } + } + } + }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch ); + } + } + return !d_qn.empty(); +} + +void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) { + if( isTrace ){ + switch( typ ){ + case typ_invalid: Trace(c) << "invalid";break; + case typ_ground: Trace(c) << "ground";break; + case typ_valid_lit: Trace(c) << "valid_lit";break; + case typ_valid: Trace(c) << "valid";break; + case typ_var: Trace(c) << "var";break; + case typ_var_eq: Trace(c) << "var_eq";break; + case typ_top: Trace(c) << "top";break; + } + }else{ + switch( typ ){ + case typ_invalid: Debug(c) << "invalid";break; + case typ_ground: Debug(c) << "ground";break; + case typ_valid_lit: Debug(c) << "valid_lit";break; + case typ_valid: Debug(c) << "valid";break; + case typ_var: Debug(c) << "var";break; + case typ_var_eq: Debug(c) << "var_eq";break; + case typ_top: Debug(c) << "top";break; + } + } +} + + +//-------------------------------------------------- debugging + + +void QuantConflictFind::debugPrint( const char * c ) { + //print the equivalance classes + Trace(c) << "----------EQ classes" << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); + while( !eqcs_i.isFinished() ){ + Node n = (*eqcs_i); + if( !n.getType().isInteger() ){ + Trace(c) << " - " << n << " : {"; + eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() ); + bool pr = false; + while( !eqc_i.isFinished() ){ + Node nn = (*eqc_i); + if( nn.getKind()!=EQUAL && nn!=n ){ + Trace(c) << (pr ? "," : "" ) << " " << nn; + pr = true; + } + ++eqc_i; + } + Trace(c) << (pr ? " " : "" ) << "}" << std::endl; + EqcInfo * eqcn = getEqcInfo( n, false ); + if( eqcn ){ + Trace(c) << " DEQ : {"; + pr = false; + for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){ + if( (*it).second ){ + Trace(c) << (pr ? "," : "" ) << " " << (*it).first; + pr = true; + } + } + Trace(c) << (pr ? " " : "" ) << "}" << std::endl; + } + } + ++eqcs_i; + } + std::map< Node, std::map< Node, bool > > printed; + //print the equality registries + for( unsigned i=0; i<2; i++ ){ + printed.clear(); + Trace(c) << "----------EQR, polarity = " << (i==0) << std::endl; + for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){ + bool prHead = false; + for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + bool print; + if( it->first.getKind()==APPLY_UF && it2->first.getKind()==APPLY_UF && + it->first.getOperator()!=it2->first.getOperator() ){ + print = isLessThan( it->first, it2->first ); + }else{ + print = printed[it->first].find( it2->first )==printed[it->first].end(); + } + if( print ){ + printed[it->first][it2->first] = true; + printed[it2->first][it->first] = true; + if( !prHead ){ + Trace(c) << "- " << it->first << std::endl; + prHead = true; + } + Trace(c) << " " << it2->first << ", terms : " << std::endl; + + /* + Trace(c) << " " << it2->first << " : {"; + bool pr = false; + for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){ + if( (*it3).second ){ + Trace(c) << (pr ? "," : "" ) << " " << (*it3).first; + pr = true; + } + } + Trace(c) << (pr ? " " : "" ) << "}" << std::endl; + */ + //print qni structure + it2->second->debugPrint( c, 3 ); + } + } + } + } +} + +void QuantConflictFind::debugPrintQuant( const char * c, Node q ) { + Trace(c) << "Q" << d_quant_id[q]; +} + +void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) { + if( n.getNumChildren()==0 ){ + Trace(c) << n; + }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){ + Trace(c) << "?x" << d_qinfo[q].d_var_num[n]; + }else{ + Trace(c) << "("; + if( n.getKind()==APPLY_UF ){ + Trace(c) << n.getOperator(); + }else{ + Trace(c) << n.getKind(); + } + for( unsigned i=0; i d_children; + void clear() { d_children.clear(); } + Node addTerm( QuantConflictFind * qcf, Node n, bool doAdd = true, int index = 0 ); + bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 ); + void debugPrint( const char * c, int t ); +}; + +class EqRegistry { + typedef context::CDChunkList NodeList; + typedef context::CDHashMap NodeBoolMap; +public: + EqRegistry( context::Context* c ); + //active + context::CDO< bool > d_active; + //NodeIndex describing pairs that meet the criteria of the EqRegistry + QcfNodeIndex d_qni; + + //qcf nodes that this helps to 1:satisfy -1:falsify 0:both a quantifier conflict node + //std::map< QcfNode *, int > d_qcf; + //has eqc + //bool hasEqc( Node n ) { return d_t_eqc.find( n )!=d_t_eqc.end() && d_t_eqc[n]; } + //void setEqc( Node n, bool val = true ) { d_t_eqc[n] = val; } + void clear() { d_qni.clear(); } + void debugPrint( const char * c, int t ); +}; + +/* +class QcfNode { +public: + QcfNode( context::Context* c ); + QcfNode * d_parent; + std::map< int, QcfNode * > d_child; + Node d_node; + EqRegistry * d_reg[2]; +}; +*/ + +class QuantConflictFind : public QuantifiersModule +{ + friend class QcfNodeIndex; + typedef context::CDChunkList NodeList; + typedef context::CDHashMap NodeBoolMap; +private: + context::Context* d_c; + context::CDO< bool > d_conflict; + //void registerAssertion( Node n ); + void registerQuant( Node q, Node n, bool hasPol, bool pol ); + void flatten( Node q, Node n ); +private: + std::map< TypeNode, Node > d_fv; + Node getFv( TypeNode tn ); + std::map< Node, Node > d_op_node; + int getFunctionId( Node f ); + bool isLessThan( Node a, Node b ); + Node getFunction( Node n, bool isQuant = false ); + int d_fid_count; + std::map< Node, int > d_fid; + Node mkEqNode( Node a, Node b ); +private: //for ground terms + Node d_true; + Node d_false; + std::map< Node, std::map< Node, EqRegistry * > > d_eqr[2]; + EqRegistry * getEqRegistry( bool polarity, Node lit, bool doCreate = true ); + void getEqRegistryApps( Node lit, std::vector< Node >& terms ); + int evaluate( Node n ); +public: //for quantifiers + //match generator + class MatchGen { + private: + //current children information + int d_child_counter; + //children of this object + std::vector< int > d_children_order; + unsigned getNumChildren() { return d_children.size(); } + MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; } + //current matching information + std::vector< QcfNodeIndex * > d_qn; + std::vector< std::map< Node, QcfNodeIndex >::iterator > d_qni; + bool doMatching( QuantConflictFind * p, Node q ); + //for matching : each index is either a variable or a ground term + unsigned d_qni_size; + std::map< int, int > d_qni_var_num; + std::map< int, Node > d_qni_gterm; + std::map< int, Node > d_qni_gterm_rep; + std::map< int, int > d_qni_bound; + std::map< int, Node > d_qni_bound_cons; + public: + //type of the match generator + enum { + typ_invalid, + typ_ground, + typ_var_eq, + typ_valid_lit, + typ_valid, + typ_var, + typ_top, + }; + void debugPrintType( const char * c, short typ, bool isTrace = false ); + public: + MatchGen() : d_type( typ_invalid ){} + MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false ); + bool d_tgt; + Node d_n; + std::vector< MatchGen > d_children; + short d_type; + bool d_type_not; + void reset_round( QuantConflictFind * p ); + void reset( QuantConflictFind * p, bool tgt, Node q ); + bool getNextMatch( QuantConflictFind * p, Node q ); + bool isValid() { return d_type!=typ_invalid; } + }; +private: + //currently asserted quantifiers + NodeList d_qassert; + //info for quantifiers + class QuantInfo { + public: + QuantInfo() : d_mg( NULL ) {} + std::vector< Node > d_vars; + std::map< Node, int > d_var_num; + std::map< EqRegistry *, bool > d_rel_eqr; + std::map< int, std::vector< Node > > d_var_constraint[2]; + int getVarNum( Node v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; } + bool isVar( Node v ) { return d_var_num.find( v )!=d_var_num.end(); } + int getNumVars() { return (int)d_vars.size(); } + Node getVar( int i ) { return d_vars[i]; } + MatchGen * d_mg; + void reset_round( QuantConflictFind * p ); + public: + //current constraints + std::map< int, Node > d_match; + std::map< int, std::map< Node, int > > d_curr_var_deq; + int getCurrentRepVar( int v ); + Node getCurrentValue( Node n ); + bool getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n ); + int addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ); + int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ); + bool setMatch( QuantConflictFind * p, int v, Node n ); + bool isMatchSpurious( QuantConflictFind * p ); + void debugPrintMatch( const char * c ); + }; + std::map< Node, QuantInfo > d_qinfo; +private: //for equivalence classes + eq::EqualityEngine * getEqualityEngine(); + bool areDisequal( Node n1, Node n2 ); + bool areEqual( Node n1, Node n2 ); + Node getRepresentative( Node n ); + Node getTerm( Node n ); + + class EqcInfo { + public: + EqcInfo( context::Context* c ) : d_diseq( c ) {} + NodeBoolMap d_diseq; + bool isDisequal( Node n ) { return d_diseq.find( n )!=d_diseq.end() && d_diseq[n]; } + void setDisequal( Node n, bool val = true ) { d_diseq[n] = val; } + //NodeBoolMap& getRelEqr( int index ) { return index==0 ? d_rel_eqr_e : d_rel_eqr_d; } + }; + std::map< Node, EqcInfo * > d_eqc_info; + EqcInfo * getEqcInfo( Node n, bool doCreate = true ); + // operator -> index(terms) + std::map< Node, QcfNodeIndex > d_uf_terms; + // eqc x operator -> index(terms) + std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms; + // type -> list(eqc) + std::map< TypeNode, std::vector< Node > > d_eqcs; +public: + QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); + + /** register assertions */ + //void registerAssertions( std::vector< Node >& assertions ); + /** register quantifier */ + void registerQuantifier( Node q ); + +public: + /** assert quantifier */ + void assertNode( Node q ); + /** new node */ + void newEqClass( Node n ); + /** merge */ + void merge( Node a, Node b ); + /** assert disequal */ + void assertDisequal( Node a, Node b ); + /** check */ + void check( Theory::Effort level ); + /** needs check */ + bool needsCheck( Theory::Effort level ); +private: + void computeRelevantEqr(); +private: + void debugPrint( const char * c ); + //for debugging + std::vector< Node > d_quants; + std::map< Node, int > d_quant_id; + void debugPrintQuant( const char * c, Node q ); + void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 59995a510..31a95fb8a 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -239,3 +239,17 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } } } + +void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { + newHasPol = hasPol; + newPol = pol; + if( n.getKind()==NOT ){ + newPol = !pol; + }else if( n.getKind()==IFF ){ + newHasPol = false; + }else if( n.getKind()==ITE ){ + if( child==0 ){ + newHasPol = false; + } + } +} \ No newline at end of file diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 86c7bc3a0..711144e7e 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -82,6 +82,8 @@ public: std::map< Node, bool > d_phase_reqs; std::map< Node, bool > d_phase_reqs_equality; std::map< Node, Node > d_phase_reqs_equality_term; + + static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); }; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index ecc3c02bc..3a6785d00 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -229,6 +229,32 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { return RewriteResponse(REWRITE_DONE, in); } +Node QuantifiersRewriter::computeElimSymbols( Node body ) { + if( isLiteral( body ) ){ + return body; + }else{ + bool childrenChanged = false; + std::vector< Node > children; + for( unsigned i=0; imkNode( OR, children ); + }else if( body.getKind()==XOR ){ + return NodeManager::currentNM()->mkNode( IFF, children ); + }else if( childrenChanged ){ + return NodeManager::currentNM()->mkNode( body.getKind(), children ); + }else{ + return body; + } + } +} + Node QuantifiersRewriter::computeNNF( Node body ){ if( body.getKind()==NOT ){ if( body[0].getKind()==NOT ){ @@ -238,10 +264,9 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); - if( body[0].getKind()==OR || body[0].getKind()==IMPLIES || body[0].getKind()==AND ){ + if( body[0].getKind()==OR || body[0].getKind()==AND ){ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - Node nn = body[0].getKind()==IMPLIES && i==0 ? body[0][i] : body[0][i].notNode(); - children.push_back( computeNNF( nn ) ); + children.push_back( computeNNF( body[0][i].notNode() ) ); } k = body[0].getKind()==AND ? OR : AND; }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){ @@ -376,8 +401,7 @@ Node QuantifiersRewriter::computeClause( Node n ){ } }else{ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nc = ( ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i] ); - Node nn = computeClause( nc ); + Node nn = computeClause( n[i] ); addNodeToOrBuilder( nn, t ); } } @@ -391,10 +415,10 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui }else if( !forcePred && isClause( n ) ){ return computeClause( n ); }else{ - Kind k = ( n.getKind()==IMPLIES ? OR : ( n.getKind()==XOR ? IFF : n.getKind() ) ); + Kind k = n.getKind(); NodeBuilder<> t(k); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nc = ( i==0 && ( n.getKind()==IMPLIES || n.getKind()==XOR ) ) ? n[i].notNode() : n[i]; + Node nc = n[i]; Node ncnf = computeCNF( nc, args, defs, k!=OR ); if( k==OR ){ addNodeToOrBuilder( ncnf, t ); @@ -523,7 +547,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b bool childrenChanged = false; std::vector< Node > newChildren; for( int i=0; i<(int)body.getNumChildren(); i++ ){ - bool newPol = ( body.getKind()==NOT || ( body.getKind()==IMPLIES && i==0 ) ) ? !pol : pol; + bool newPol = body.getKind()==NOT ? !pol : pol; Node n = computePrenex( body[i], args, newPol ); newChildren.push_back( n ); if( n!=body[i] ){ @@ -661,7 +685,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ if( f.getNumChildren()==3 ){ ipl = f[2]; } - if( computeOption==COMPUTE_MINISCOPING ){ + if( computeOption==COMPUTE_ELIM_SYMBOLS ){ + n = computeElimSymbols( n ); + }else if( computeOption==COMPUTE_MINISCOPING ){ //return directly return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ @@ -746,11 +772,11 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } return computeMiniscoping( args, t.constructNode(), ipl ); } - }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){ + }else if( body[0].getKind()==OR ){ if( doMiniscopingAnd() ){ NodeBuilder<> t(kind::AND); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - Node trm = ( body[0].getKind()==IMPLIES && i==0 ) ? body[0][i] : ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() ); + Node trm = body[0][i].negate(); t << computeMiniscoping( args, trm, ipl ); } return t.constructNode(); @@ -766,13 +792,13 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo Node retVal = t; return retVal; } - }else if( body.getKind()==OR || body.getKind()==IMPLIES ){ + }else if( body.getKind()==OR ){ if( doMiniscopingNoFreeVar() ){ Node newBody = body; NodeBuilder<> body_split(kind::OR); NodeBuilder<> tb(kind::OR); for( int i=0; i<(int)body.getNumChildren(); i++ ){ - Node trm = ( body.getKind()==IMPLIES && i==0 ) ? ( body[i].getKind()==NOT ? body[i][0] : body[i].notNode() ) : body[i]; + Node trm = body[i]; if( hasArg( args, body[i] ) ){ tb << trm; }else{ @@ -916,7 +942,9 @@ bool QuantifiersRewriter::doMiniscopingAnd(){ } bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){ - if( computeOption==COMPUTE_MINISCOPING ){ + if( computeOption==COMPUTE_ELIM_SYMBOLS ){ + return true; + }else if( computeOption==COMPUTE_MINISCOPING ){ return true; }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return options::aggressiveMiniscopeQuant(); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 40234904f..e97d84701 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -44,6 +44,7 @@ private: static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); static Node computeClause( Node n ); private: + static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); static Node computeNNF( Node body ); @@ -54,7 +55,8 @@ private: static Node computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ - COMPUTE_MINISCOPING = 0, + COMPUTE_ELIM_SYMBOLS = 0, + COMPUTE_MINISCOPING, COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_SIMPLE_ITE_LIFT, diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 39063942d..b13e76afb 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -342,7 +342,7 @@ bool Trigger::isSimpleTrigger( Node n ){ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; - bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol; + bool newHasPol = n.getKind()==IFF ? false : hasPol; bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ @@ -350,9 +350,8 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< }else{ bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ retVal = true; } } @@ -381,9 +380,8 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< } if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ retVal = true; } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5def2a832..2ddc83a4b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -29,6 +29,7 @@ #include "theory/rewriterules/rr_trigger.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/quant_conflict_find.h" #include "theory/uf/options.h" using namespace std; @@ -61,6 +62,12 @@ d_lemmas_produced_c(u){ } //add quantifiers modules + if( options::quantConflictFind() ){ + d_qcf = new quantifiers::QuantConflictFind( this, c); + d_modules.push_back( d_qcf ); + }else{ + d_qcf = NULL; + } if( !options::finiteModelFind() || options::fmfInstEngine() ){ //the instantiation must set incomplete flag unless finite model finding is turned on d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() ); @@ -393,6 +400,10 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ return getInstantiation( f, vars, terms ); } +Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { + return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); +} + bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){ if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){ @@ -497,12 +508,13 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool void QuantifiersEngine::flushLemmas( OutputChannel* out ){ if( !d_lemmas_waiting.empty() ){ + if( !out ){ + out = &getOutputChannel(); + } //take default output channel if none is provided d_hasAddedLemma = true; for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){ - if( out ){ - out->lemma( d_lemmas_waiting[i] ); - } + out->lemma( d_lemmas_waiting[i] ); } d_lemmas_waiting.clear(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 6de13ff3c..ee7e6e6d8 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -52,7 +52,7 @@ public: /* Call during quantifier engine's check */ virtual void check( Theory::Effort e ) = 0; /* Called for new quantifiers */ - virtual void registerQuantifier( Node n ) = 0; + virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) = 0; virtual void propagate( Theory::Effort level ){} virtual Node getNextDecisionRequest() { return TNode::null(); } @@ -66,6 +66,7 @@ namespace quantifiers { class InstantiationEngine; class ModelEngine; class BoundedIntegers; + class QuantConflictFind; class RewriteEngine; }/* CVC4::theory::quantifiers */ @@ -105,6 +106,8 @@ private: quantifiers::ModelEngine* d_model_engine; /** bounded integers utility */ quantifiers::BoundedIntegers * d_bint; + /** Conflict find mechanism for quantifiers */ + quantifiers::QuantConflictFind* d_qcf; /** rewrite rules utility */ quantifiers::RewriteEngine * d_rr_engine; private: @@ -165,6 +168,8 @@ public: EfficientEMatcher* getEfficientEMatcher() { return d_eem; } /** get bounded integers utility */ quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } + /** Conflict find mechanism for quantifiers */ + quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; } public: /** initialize */ void finishInit(); @@ -194,6 +199,8 @@ public: Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** get instantiation */ Node getInstantiation( Node f, InstMatch& m ); + /** get instantiation */ + Node getInstantiation( Node f, std::vector< Node >& terms ); /** exist instantiation ? */ bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ @@ -207,7 +214,7 @@ public: /** has added lemma */ bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** flush lemmas */ - void flushLemmas( OutputChannel* out ); + void flushLemmas( OutputChannel* out = NULL ); /** get number of waiting lemmas */ int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } public: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c598fd01b..e55d6a9c9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -75,12 +75,18 @@ void TheoryEngine::finishInit() { void TheoryEngine::eqNotifyNewClass(TNode t){ d_quantEngine->addTermToDatabase( t ); + if( d_logicInfo.isQuantified() && options::quantConflictFind() ){ + d_quantEngine->getConflictFind()->newEqClass( t ); + } } void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ //TODO: add notification to efficient E-matching - if (d_logicInfo.isQuantified()) { + if( d_logicInfo.isQuantified() ){ d_quantEngine->getEfficientEMatcher()->merge( t1, t2 ); + if( options::quantConflictFind() ){ + d_quantEngine->getConflictFind()->merge( t1, t2 ); + } } } @@ -89,7 +95,11 @@ void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){ } void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ - + if( d_logicInfo.isQuantified() ){ + if( options::quantConflictFind() ){ + d_quantEngine->getConflictFind()->assertDisequal( t1, t2 ); + } + } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 92469aa31..8f292e008 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -39,6 +39,7 @@ #include "util/statistics_registry.h" #include "util/cvc4_assert.h" #include "util/sort_inference.h" +#include "theory/quantifiers/quant_conflict_find.h" #include "theory/uf/equality_engine.h" #include "theory/bv/bv_to_bool.h" #include "theory/atom_requests.h" @@ -778,10 +779,10 @@ private: UnconstrainedSimplifier* d_unconstrainedSimp; /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ - theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; + theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); + void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); Node ppSimpITE(TNode assertion); /** Returns false if an assertion simplified to false. */ bool donePPSimpITE(std::vector& assertions); @@ -790,6 +791,8 @@ public: SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } + theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } + SortInference* getSortInference() { return &d_sortInfer; } private: std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 3ed1ea985..51783c1e3 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -44,8 +44,6 @@ protected: typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; - typedef context::CDChunkList NodeList; - typedef context::CDList BoolList; typedef context::CDHashMap TypeNodeBoolMap; public: /** information for incremental conflict/clique finding for a particular sort */