diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 22 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 221 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 24 | ||||
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 89 | ||||
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 59 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/options | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 32 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 31 |
11 files changed, 344 insertions, 151 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7844cede5..cb18b8464 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -866,7 +866,7 @@ SmtEngine::~SmtEngine() throw() { PROOF(delete d_proofManager;); PROOF(d_proofManager = NULL;); - + delete d_stats; d_stats = NULL; delete d_statisticsRegistry; @@ -1342,12 +1342,15 @@ void SmtEngine::setDefaults() { if( !options::preSkolemQuant.wasSetByUser() ){ options::preSkolemQuant.set( true ); } + if( !options::preSkolemQuantNested.wasSetByUser() ){ + options::preSkolemQuantNested.set( true ); + } if( !options::fmfOneInstPerRound.wasSetByUser() ){ options::fmfOneInstPerRound.set( true ); } } } - + //apply counterexample guided instantiation options if( options::cegqiSingleInv() ){ options::ceGuidedInst.set( true ); @@ -1376,10 +1379,17 @@ void SmtEngine::setDefaults() { } } - //implied options... + //cbqi options if( options::recurseCbqi() || options::cbqi2() ){ options::cbqi.set( true ); } + if( options::cbqi() ){ + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + } + + //implied options... if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } @@ -3430,10 +3440,10 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl; // Give it to proof manager - PROOF( + PROOF( if( inInput ){ // n is an input assertion - ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); + ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); }else{ // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); @@ -3634,7 +3644,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 0fef2aa42..7d1c06b8e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -31,11 +31,13 @@ using namespace CVC4::theory::quantifiers; using namespace std; namespace CVC4 { - + CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){ - -} - + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + d_true = NodeManager::currentNM()->mkConst( true ); +} + void CegInstantiator::computeProgVars( Node n ){ if( d_prog_var.find( n )==d_prog_var.end() ){ d_prog_var[n].clear(); @@ -51,14 +53,20 @@ void CegInstantiator::computeProgVars( Node n ){ d_inelig[n] = true; return; } + if( d_has_delta.find( n[i] )!=d_has_delta.end() ){ + d_has_delta[n] = true; + } for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ d_prog_var[n][it->first] = true; } } + if( n==d_n_delta ){ + d_has_delta[n] = true; + } } } -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ @@ -69,7 +77,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; Node pv = d_vars[i]; TypeNode pvtn = pv.getType(); - + if( (i+1)<d_vars.size() || effort!=2 ){ //[1] easy case : pv is in the equivalence class as another term not containing pv if( ee->hasTerm( pv ) ){ @@ -78,7 +86,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< while( !eqc_i.isFinished() ){ Node n = *eqc_i; if( n!=pv ){ - Trace("cegqi-si-inst-debug") << i << "...try based on equal term " << n << std::endl; + Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl; //compute d_subs_fv, which program variables are contained in n computeProgVars( n ); //must be an eligible term @@ -97,6 +105,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< ns = n; proc = true; } + if( d_has_delta.find( ns )!=d_has_delta.end() ){ + //also must set delta to zero + ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero ); + ns = Rewriter::rewrite( ns ); + computeProgVars( ns ); + } if( proc ){ //try the substitution subs_proc[0][ns][pv_coeff] = true; @@ -109,7 +123,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< ++eqc_i; } } - + //[2] : we can solve an equality for pv ///iterate over equivalence classes to find cases where we can solve for the variable if( pvtn.isInteger() || pvtn.isReal() ){ @@ -142,7 +156,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< for( unsigned j=0; j<lhs.size(); j++ ){ //if this term or the another has pv in it, try to solve for it if( hasVar || lhs_v[j] ){ - Trace("cegqi-si-inst-debug") << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; + Trace("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; Node eq_lhs = lhs[j]; Node eq_rhs = ns; //make the same coefficient @@ -163,6 +177,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( !d_n_delta.isNull() ){ + msum.erase( d_n_delta ); + } if( Trace.isOn("cegqi-si-inst-debug") ){ Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); @@ -199,7 +216,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< ++eqcs_i; } } - + //[3] directly look at assertions TheoryId tid = Theory::theoryOf( pv ); Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); @@ -211,34 +228,42 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< bool pol = lit.getKind()!=NOT; if( tid==THEORY_ARITH ){ if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ - Assert( atom[1].isConst() ); - computeProgVars( atom[0] ); + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = d_zero; + } + + computeProgVars( atom_lhs ); //must be an eligible term - if( d_inelig.find( atom[0] )==d_inelig.end() ){ + if( d_inelig.find( atom_lhs )==d_inelig.end() ){ //apply substitution to LHS of atom - Node atom_lhs; - Node atom_rhs; - if( !d_prog_var[atom[0]].empty() ){ + if( !d_prog_var[atom_lhs].empty() ){ Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom[0], subs, vars, coeff, has_coeff, atom_lhs_coeff ); + atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff ); if( !atom_lhs.isNull() ){ computeProgVars( atom_lhs ); - atom_rhs = atom[1]; if( !atom_lhs_coeff.isNull() ){ atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); } } - }else{ - atom_lhs = atom[0]; - atom_rhs = atom[1]; } //if it contains pv if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - Trace("cegqi-si-inst-debug") << "From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( !d_n_delta.isNull() ){ + msum.erase( d_n_delta ); + } if( Trace.isOn("cegqi-si-inst-debug") ){ Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); @@ -295,6 +320,8 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ return true; } + }else{ + Trace("cegqi-si-inst-debug") << "...already processed." << std::endl; } } } @@ -306,12 +333,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } } - - //[4] resort to using value in model + + //[4] resort to using value in model if( effort>0 ){ Node mv = d_qe->getModel()->getValue( pv ); Node pv_coeff_m; - Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl; + Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl; return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 ); }else{ return false; @@ -320,9 +347,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, +bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, unsigned effort ) { + unsigned i, unsigned effort ) { //must ensure variables have been computed for n computeProgVars( n ); //substitute into previous substitutions, when applicable @@ -336,7 +363,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s a_coeff.push_back( pv_coeff ); a_has_coeff.push_back( pv ); } - + bool success = true; std::map< int, Node > prev_subs; std::map< int, Node > prev_coeff; @@ -413,7 +440,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s } } -bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, +bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) { if( j==has_coeff.size() ){ return addInstantiation( subs, vars, subs_typ ); @@ -446,13 +473,12 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec if( !veq_c.isNull() ){ subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); if( subs_typ[index]>=1 && subs_typ[index]<=2 ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ), - NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + d_zero ), + d_zero, d_one ) ); } } @@ -463,10 +489,10 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec //equalities are both upper and lower bounds /* if( subs_typ[index]==0 && !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), NodeManager::currentNM()->mkConst( Rational( 0 ) ), NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) @@ -503,7 +529,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< prev[i] = subs[i]; if( d_n_delta.isNull() ){ d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, d_zero ); d_qe->getOutputChannel().lemma( delta_lem ); } subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); @@ -521,7 +547,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } -Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, +Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) { Assert( d_prog_var.find( n )!=d_prog_var.end() ); Assert( n==Rewriter::rewrite( n ) ); @@ -603,7 +629,77 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: } } +//check if delta has a lower bound L +// if so, add lemma L>0 => L>d +void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { + if( !d_n_delta.isNull() ){ + Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); + if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned j = 0; it != it_end; ++ it, ++j) { + Node lit = (*it).assertion; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = d_zero; + } + computeProgVars( atom_lhs ); + //must be an eligible term with delta + if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){ + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + Node vatom; + //isolate delta in the inequality + int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true ); + if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){ + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + if( pvm!=d_n_delta ){ + Node veq_c; + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==d_n_delta ); + val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) ); + val = Rewriter::rewrite( val ); + }else{ + val = Node::null(); + } + } + if( !val.isNull() ){ + Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero ); + lem1 = Rewriter::rewrite( lem1 ); + if( !lem1.isConst() || lem1==d_true ){ + Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta ); + Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 ); + lems.push_back( lem ); + Trace("cegqi-delta") << "...lemma : " << lem << std::endl; + } + } + }else{ + Trace("cegqi-delta") << "...wrong polarity." << std::endl; + } + } + } + } + } + } + } +} + void CegInstantiator::check() { + for( unsigned r=0; r<2; r++ ){ std::vector< Node > subs; std::vector< Node > vars; @@ -617,18 +713,21 @@ void CegInstantiator::check() { } Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; } - - + + bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { return d_out->addInstantiation( subs, subs_typ ); } - + bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) { return d_out->isEligibleForInstantiation( n ); -} - - - +} + +bool CegqiOutputSingleInv::addLemma( Node n ) { + return d_out->addLemma( n ); +} + + CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){ d_sol = NULL; d_c_inst_match_trie = NULL; @@ -651,12 +750,12 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; - + //initialize the instantiator for this CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); d_cinst = new CegInstantiator( d_qe, cosi ); d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - + return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); }else{ return Node::null(); @@ -1056,14 +1155,24 @@ bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) { return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end(); } +bool CegConjectureSingleInv::addLemma( Node n ) { + d_curr_lemmas.push_back( n ); + return true; +} + void CegConjectureSingleInv::check( std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { Assert( d_cinst!=NULL ); d_curr_lemmas.clear(); - //call check for instantiator - d_cinst->check(); - //add lemmas - lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); + //check if there are delta lemmas + d_cinst->getDeltaLemmas( d_curr_lemmas ); + //if not, do ce-guided instantiation + if( d_curr_lemmas.empty() ){ + //call check for instantiator + d_cinst->check(); + //add lemmas + lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); + } } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 9e65b0c24..b5ebe3d7c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -33,38 +33,47 @@ class CegqiOutput public: virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0; virtual bool isEligibleForInstantiation( Node n ) = 0; + virtual bool addLemma( Node lem ) = 0; }; class CegInstantiator { private: + Node d_zero; + Node d_one; + Node d_true; QuantifiersEngine * d_qe; CegqiOutput * d_out; //program variable contains cache std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; + std::map< Node, bool > d_has_delta; private: - Node d_n_delta; //for adding instantiations during check void computeProgVars( Node n ); // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned i, unsigned effort ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned i, unsigned effort ); - bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, + bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ); bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ); - Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); + Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ); //the CE variables std::vector< Node > d_vars; + //delta + Node d_n_delta; + //check : add instantiations based on valuation of d_vars void check(); + // get delta lemmas : on-demand force minimality of d_n_delta + void getDeltaLemmas( std::vector< Node >& lems ); }; @@ -77,6 +86,7 @@ public: CegConjectureSingleInv * d_out; bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); bool isEligibleForInstantiation( Node n ); + bool addLemma( Node lem ); }; @@ -129,6 +139,8 @@ private: bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); //is eligible for instantiation bool isEligibleForInstantiation( Node n ); + // add lemma + bool addLemma( Node lem ); public: CegConjectureSingleInv( CegConjecture * p ); // original conjecture diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index cb772a31f..0bc365ec7 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -38,19 +38,19 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Node n = assertions[i][1][0]; Assert( n.getKind()==APPLY_UF ); Node f = n.getOperator(); - + //check if already defined, if so, throw error if( d_sorts.find( f )!=d_sorts.end() ){ Message() << "Cannot define function " << f << " more than once." << std::endl; exit( 0 ); } - + //create a sort S that represents the inputs of the function std::stringstream ss; ss << "I_" << f; TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() ); d_sorts[f] = iType; - + //create functions f1...fn mapping from this sort to concrete elements for( unsigned j=0; j<n.getNumChildren(); j++ ){ TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); @@ -58,7 +58,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { ss << f << "_arg_" << j; d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); } - + //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] std::vector< Node > children; Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType ); @@ -70,7 +70,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) ); } Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - + Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); @@ -81,8 +81,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } //second pass : rewrite assertions for( unsigned i=0; i<assertions.size(); i++ ){ - bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end(); + int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0; std::vector< Node > constraints; + Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; Node n = simplify( assertions[i], true, true, constraints, is_fd ); Assert( constraints.empty() ); if( n!=assertions[i] ){ @@ -95,7 +96,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } } -Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def ) { +Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) { Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl; if( n.getKind()==FORALL ){ Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def ); @@ -104,51 +105,51 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co }else{ return n; } - }else if( n.getType().isBoolean() && n.getKind()!=APPLY_UF ){ - std::vector< Node > children; - bool childChanged = false; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node c = n[i]; - //do not process LHS of definition - if( !is_fun_def || i!=0 ){ - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); - //get child constraints - std::vector< Node > cconstraints; - c = simplify( n[i], newPol, newHasPol, cconstraints ); - constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); + }else{ + Node nn = n; + bool isBool = n.getType().isBoolean(); + if( isBool && n.getKind()!=APPLY_UF && is_fun_def!=2 ){ + std::vector< Node > children; + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node c = n[i]; + //do not process LHS of definition + if( is_fun_def!=1 || i!=0 ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); + //get child constraints + std::vector< Node > cconstraints; + c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 ); + constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); + } + children.push_back( c ); + childChanged = c!=n[i] || childChanged; } - children.push_back( c ); - childChanged = c!=n[i] || childChanged; - } - if( !constraints.empty() || childChanged ){ - std::vector< Node > c; if( childChanged ){ - c.push_back( NodeManager::currentNM()->mkNode( n.getKind(), children ) ); - }else{ - c.push_back( n ); + nn = n; } - if( hasPol ){ - //conjoin with current - for( unsigned i=0; i<constraints.size(); i++ ){ - if( pol ){ - c.push_back( constraints[i] ); - }else{ - c.push_back( constraints[i].negate() ); - } + }else{ + //simplify term + simplifyTerm( n, constraints ); + } + if( !constraints.empty() && isBool && hasPol ){ + std::vector< Node > c; + c.push_back( nn ); + //conjoin with current + for( unsigned i=0; i<constraints.size(); i++ ){ + if( pol ){ + c.push_back( constraints[i] ); + }else{ + c.push_back( constraints[i].negate() ); } - constraints.clear(); - }else{ - //must add at higher level } + constraints.clear(); return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c ); + }else{ + return nn; } - }else{ - //simplify term - simplifyTerm( n, constraints ); } - return n; } void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) { diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 40364eeb7..63aa1bf94 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -36,7 +36,7 @@ private: //defined functions to injections input -> argument elements std::map< Node, std::vector< Node > > d_input_arg_inj; //simplify - Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false ); + Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 ); //simplify term void simplifyTerm( Node n, std::vector< Node >& constraints ); public: diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 6de6e1d03..f97c4040b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -357,13 +357,17 @@ bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { return d_out->isEligibleForInstantiation( n ); } +bool CegqiOutputInstStrategy::addLemma( Node lem ) { + return d_out->addLemma( lem ); +} + InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) { d_out = new CegqiOutputInstStrategy( this ); } void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { - + d_check_delta_lemma = true; } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { @@ -374,6 +378,12 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f ); if( it==d_cinst.end() ){ cinst = new CegInstantiator( d_quantEngine, d_out ); + if( d_n_delta.isNull() ){ + d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + d_quantEngine->getOutputChannel().lemma( delta_lem ); + } + cinst->d_n_delta = d_n_delta; for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) ); } @@ -381,24 +391,59 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { }else{ cinst = it->second; } + if( d_check_delta_lemma ){ + Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl; + d_check_delta_lemma = false; + std::vector< Node > dlemmas; + cinst->getDeltaLemmas( dlemmas ); + Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl; + if( !dlemmas.empty() ){ + bool addedLemma = false; + for( unsigned i=0; i<dlemmas.size(); i++ ){ + if( addLemma( dlemmas[i] ) ){ + addedLemma = true; + } + } + if( addedLemma ){ + return STATUS_UNKNOWN; + } + } + } + Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; cinst->check(); d_curr_quant = Node::null(); - - return STATUS_UNKNOWN; - }else{ - // To fix warning - Unreachable(); } + return STATUS_UNKNOWN; } bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { Assert( !d_curr_quant.isNull() ); + /* + std::stringstream siss; + if( Trace.isOn("inst-cegqi") || Trace.isOn("inst-cegqi-debug") ){ + for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){ + Node v = d_single_inv_map_to_prog[d_single_inv[0][j]]; + siss << " * " << v; + siss << " (" << d_single_inv_sk[j] << ")"; + siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl; + } + } + */ return d_quantEngine->addInstantiation( d_curr_quant, subs, false ); } +bool InstStrategyCegqi::addLemma( Node lem ) { + return d_quantEngine->addLemma( lem ); +} + bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { - return true; + if( n.getKind()==INST_CONSTANT ){ + //only legal if current quantified formula contains n + return TermDb::containsTerm( d_curr_quant, n ); + }else{ + return true; + } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index e139d0b6f..9435fc97c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -92,13 +92,16 @@ public: InstStrategyCegqi * d_out; bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); bool isEligibleForInstantiation( Node n ); + bool addLemma( Node lem ); }; class InstStrategyCegqi : public InstStrategy { private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; + Node d_n_delta; Node d_curr_quant; + bool d_check_delta_lemma; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); @@ -108,6 +111,7 @@ public: bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); bool isEligibleForInstantiation( Node n ); + bool addLemma( Node lem ); /** identify */ std::string identify() const { return std::string("Cegqi"); } }; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 9c3035c85..cb01fd373 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -143,9 +143,9 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //check each instantiation strategy for( size_t i=0; i<d_instStrategies.size(); ++i ){ InstStrategy* is = d_instStrategies[i]; - Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; + Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; int quantStatus = is->process( f, effort, e_use ); - Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl; + Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ finished = false; } @@ -185,11 +185,14 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Debug("quantifiers") << "Process " << n << "..." << std::endl; //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( !d_quantEngine->hasOwnership( n, this ) ){ d_quant_active[n] = false; + Debug("quantifiers") << " Quantifier has owner." << std::endl; }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){ d_quant_active[n] = false; + Debug("quantifiers") << " Quantifier is not active (from model)." << std::endl; //it is not active if we have found the skolemized negation is unsat }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 62790432d..a529e37d0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -44,6 +44,10 @@ option clauseSplit --clause-split bool :default false # forall x. P( x ) => f( S( x ) ) = x option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas +option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true + apply skolemization to nested quantified formulass +option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true + apply skolemization to quantified formulas aggressively # Whether to perform agressive miniscoping option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index a78fa8d7b..991043157 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -285,7 +285,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); - + if( body[0].getKind()==OR || body[0].getKind()==AND ){ k = body[0].getKind()==AND ? OR : AND; for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ @@ -1210,7 +1210,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return nn.negate(); }else if( n.getKind()==kind::FORALL ){ if( polarity ){ - if( options::preSkolemQuant() ){ + if( options::preSkolemQuant() && ( options::preSkolemQuantNested() || fvs.empty() ) ){ vector< Node > children; children.push_back( n[0] ); //add children to current scope @@ -1245,20 +1245,22 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v if( containsQuantifiers( n ) ){ if( n.getType().isBoolean() ){ if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + if( options::preSkolemQuantAgg() ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + } + return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ vector< Node > children; for( int i=0; i<(int)n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 888cdbce0..ba75af873 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -417,7 +417,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ Trace("quant") << " : " << f << std::endl; ++(d_statistics.d_num_quant); Assert( f.getKind()==FORALL ); - + //check whether we should apply a reduction bool reduced = false; if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ @@ -567,7 +567,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << std::endl; Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); } - if( options::cbqi() ){ + if( options::cbqi() && !options::cbqi2() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; @@ -589,7 +589,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } setInstantiationLevelAttr( body, f[1], maxInstLevel+1 ); } - Trace("inst-debug") << "*** Lemma is " << lem << std::endl; ++(d_statistics.d_instantiations); return true; }else{ @@ -673,13 +672,17 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std Trace("partial-inst") << "Partial instantiation : " << f << std::endl; Trace("partial-inst") << " : " << body << std::endl; }else{ - //do optimized version - Node icb = d_term_db->getInstConstantBody( f ); - body = getSubstitute( icb, terms ); - if( Debug.isOn("check-inst") ){ - Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( body!=body2 ){ - Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + if( options::cbqi() ){ + body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + }else{ + //do optimized version + Node icb = d_term_db->getInstConstantBody( f ); + body = getSubstitute( icb, terms ); + if( Debug.isOn("check-inst") ){ + Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( body!=body2 ){ + Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + } } } } @@ -722,16 +725,16 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ - Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; lem = Rewriter::rewrite(lem); + Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl; if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); - Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; + Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl; return true; }else{ - Debug("inst-engine-debug") << "Duplicate." << std::endl; + Trace("inst-add-debug2") << "Duplicate." << std::endl; return false; } }else{ @@ -943,7 +946,7 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { out << "Internal error : module for synth solution not found." << std::endl; } } - + QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), |