diff options
-rw-r--r-- | src/Makefile.am | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 54 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 1402 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 135 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 1661 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 132 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 186 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 20 | ||||
-rw-r--r-- | test/regress/regress0/bug519.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/bug291.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/bug291.smt2.expect | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 | 2 |
18 files changed, 1903 insertions, 1744 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 90a4d6f5b..95ca44e63 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -337,9 +337,11 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_engine.h \ - theory/quantifiers/fun_def_engine.cpp \ - theory/quantifiers/quant_equality_engine.h \ - theory/quantifiers/quant_equality_engine.cpp \ + theory/quantifiers/fun_def_engine.cpp \ + theory/quantifiers/quant_equality_engine.h \ + theory/quantifiers/quant_equality_engine.cpp \ + theory/quantifiers/ceg_instantiator.h \ + theory/quantifiers/ceg_instantiator.cpp \ theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a4f18e57b..2784bb006 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1381,10 +1381,9 @@ void SmtEngine::setDefaults() { if( !options::eMatching.wasSetByUser() ){ options::eMatching.set( options::fmfInstEngine() ); } - if( ! options::instWhenMode.wasSetByUser()){ - //instantiate only on last call + if( !options::instWhenMode.wasSetByUser() ){ + //instantiate only on last call FIXME: remove? if( options::eMatching() ){ - Trace("smt") << "setting inst when mode to LAST_CALL" << endl; options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } @@ -1406,6 +1405,7 @@ void SmtEngine::setDefaults() { options::ceGuidedInst.set( true ); } if( options::ceGuidedInst() ){ + //counterexample-guided instantiation for sygus if( !options::cegqiSingleInv.wasSetByUser() ){ options::cegqiSingleInv.set( true ); } @@ -1440,29 +1440,37 @@ void SmtEngine::setDefaults() { if( !options::cbqiPreRegInst.wasSetByUser()) { options::cbqiPreRegInst.set( true ); } - } - - //cbqi options - // enable if pure arithmetic quantifiers - if( d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) ){ - if( !options::cbqi.wasSetByUser() && !options::cbqi2.wasSetByUser() ){ - options::cbqi2.set( true ); + }else{ + //counterexample-guided instantiation for non-sygus + // enable if any quantifiers with arithmetic or datatypes + if( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ){ + if( !options::cbqi.wasSetByUser() ){ + options::cbqi.set( true ); + } } - } - if( options::cbqi2() ){ - options::cbqi.set( true ); - } - if( options::cbqi2() ){ - if( !options::rewriteDivk.wasSetByUser()) { - options::rewriteDivk.set( true ); + if( options::cbqiSplx() ){ + //implies more general option + options::cbqi.set( true ); } - } - if( options::cbqi() ){ - if( !options::quantConflictFind.wasSetByUser() ){ - options::quantConflictFind.set( false ); + if( options::cbqi() ){ + //must rewrite divk + if( !options::rewriteDivk.wasSetByUser()) { + options::rewriteDivk.set( true ); + } } - if( !options::instNoEntail.wasSetByUser() ){ - options::instNoEntail.set( false ); + if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){ + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + if( !options::instNoEntail.wasSetByUser() ){ + options::instNoEntail.set( false ); + } + if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){ + //only instantiation should happen at last call when model is avaiable + if( !options::instWhenMode.wasSetByUser() ){ + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + } + } } } diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp new file mode 100644 index 000000000..90639d68c --- /dev/null +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -0,0 +1,1402 @@ +/********************* */ +/*! \file ceg_instantiator.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-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of counterexample-guided quantifier instantiation + **/ + +#include "theory/quantifiers/ceg_instantiator.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" +#include "util/ite_removal.h" + +//#define MBP_STRICT_ASSERTIONS + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) : +d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){ + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + d_true = NodeManager::currentNM()->mkConst( true ); + d_is_nested_quant = false; +} + +void CegInstantiator::computeProgVars( Node n ){ + if( d_prog_var.find( n )==d_prog_var.end() ){ + d_prog_var[n].clear(); + if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ + d_prog_var[n][n] = true; + }else if( !d_out->isEligibleForInstantiation( n ) ){ + d_inelig[n] = true; + return; + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + computeProgVars( n[i] ); + if( d_inelig.find( n[i] )!=d_inelig.end() ){ + d_inelig[n] = true; + return; + } + 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; + } + //selectors applied to program variables are also variables + if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){ + d_prog_var[n][n] = true; + } + } + } +} + +bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ + if( i==d_vars.size() ){ + //solved for all variables, now construct instantiation + if( !sf.d_has_coeff.empty() ){ + if( options::cbqiSymLia() ){ + //use symbolic solved forms + SolvedForm csf; + csf.copy( ssf ); + return addInstantiationCoeff( csf, vars, btyp, 0, cons ); + }else{ + return addInstantiationCoeff( sf, vars, btyp, 0, cons ); + } + }else{ + return addInstantiation( sf.d_subs, vars, cons ); + } + }else{ + std::map< Node, std::map< Node, bool > > subs_proc; + //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; + bool is_cv = false; + Node pv; + if( curr_var.empty() ){ + pv = d_vars[i]; + }else{ + pv = curr_var.back(); + is_cv = true; + } + TypeNode pvtn = pv.getType(); + Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl; + Node pv_value; + if( options::cbqiModel() ){ + pv_value = getModelValue( pv ); + Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; + } + Node pvr = pv; + if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){ + pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv ); + } + + //if in effort=2, we must choose at least one model value + if( (i+1)<d_vars.size() || effort!=2 ){ + + //[1] easy case : pv is in the equivalence class as another term not containing pv + Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl; + std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr ); + if( it_eqc!=d_curr_eqc.end() ){ + Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl; + for( unsigned k=0; k<it_eqc->second.size(); k++ ){ + Node n = it_eqc->second[k]; + if( n!=pv ){ + Trace("cbqi-inst-debug") << "...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 + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) + bool proc = false; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, sf, vars, pv_coeff, false ); + if( !ns.isNull() ){ + computeProgVars( ns ); + //substituted version must be new and cannot contain pv + proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); + } + }else{ + ns = n; + proc = true; + } + if( proc ){ + //try the substitution + subs_proc[ns][pv_coeff] = true; + if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + }else{ + Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl; + } + + //[2] : we can solve an equality for pv + if( pvtn.isInteger() || pvtn.isReal() ){ + ///iterate over equivalence classes to find cases where we can solve for the variable + TypeNode pvtnb = pvtn.getBaseType(); + Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl; + for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ + Node r = d_curr_type_eqc[pvtnb][k]; + std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + Assert( it_reqc!=d_curr_eqc.end() ); + for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ + Node n = it_reqc->second[kk]; + Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; + //compute the variables in n + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, sf, vars, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; + } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; + 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("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; + Node eq_lhs = lhs[j]; + Node eq_rhs = ns; + //make the same coefficient + if( pv_coeff!=lhs_coeff[j] ){ + if( !pv_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff[j].isNull() ){ + Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + //cannot contain infinity? + //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){ + Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; + } + Node veq; + if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ + Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl; + Node veq_c; + if( veq[0]!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + Node val = veq[1]; + if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ + subs_proc[val][veq_c] = true; + if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); + }else{ + Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; + } + }else{ + Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; + } + } + } + }else if( pvtn.isDatatype() ){ + Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; + //look in equivalence class for a constructor + if( it_eqc!=d_curr_eqc.end() ){ + for( unsigned k=0; k<it_eqc->second.size(); k++ ){ + Node n = it_eqc->second[k]; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + Trace("cbqi-inst-debug") << "... " << i << "...try based on constructor term " << n << std::endl; + cons[pv] = n.getOperator(); + const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype(); + unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); + if( is_cv ){ + curr_var.pop_back(); + } + //now must solve for selectors applied to pv + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); + } + if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + }else{ + //cleanup + cons.erase( pv ); + Assert( curr_var.size()>=dt[cindex].getNumArgs() ); + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + curr_var.pop_back(); + } + if( is_cv ){ + curr_var.push_back( pv ); + } + break; + } + } + } + }else{ + Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl; + } + } + + //[3] directly look at assertions + Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl; + Node vts_sym[2]; + vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); + vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); + std::vector< Node > mbp_bounds[2]; + std::vector< Node > mbp_coeff[2]; + std::vector< Node > mbp_vts_coeff[2][2]; + std::vector< Node > mbp_lit[2]; + unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() ); + Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl; + std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid ); + if( ita!=d_curr_asserts.end() ){ + for (unsigned j = 0; j<ita->second.size(); j++) { + Node lit = ita->second[j]; + Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + if( tid==THEORY_ARITH ){ + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ + Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() ); + 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_lhs )==d_inelig.end() ){ + //apply substitution to LHS of atom + if( !d_prog_var[atom_lhs].empty() ){ + Node atom_lhs_coeff; + atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff ); + if( !atom_lhs.isNull() ){ + computeProgVars( atom_lhs ); + if( !atom_lhs_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + } + } + } + //if it contains pv, not infinity + 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 ); + //cannot contain infinity? + //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){ + Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + } + //get the coefficient of infinity and remove it from msum + Node vts_coeff[2]; + for( unsigned t=0; t<2; t++ ){ + if( !vts_sym[t].isNull() ){ + std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] ); + if( itminf!=msum.end() ){ + vts_coeff[t] = itminf->second; + if( vts_coeff[t].isNull() ){ + vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + } + //negate if coefficient on variable is positive + std::map< Node, Node >::iterator itv = msum.find( pv ); + if( itv!=msum.end() ){ + //multiply by the coefficient we will isolate for + if( itv->second.isNull() ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + }else{ + if( !pvtn.isInteger() ){ + vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); + vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); + }else if( itv->second.getConst<Rational>().sgn()==1 ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + } + } + } + Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase( vts_sym[t] ); + } + } + } + + Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; + Node vatom; + //isolate pv in the inequality + int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); + if( ires!=0 ){ + Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl; + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + Node veq_c; + if( pvm!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + + //disequalities are either strict upper or lower bounds + unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + int uires = ires; + Node uval = val; + if( atom.getKind()==GEQ ){ + //push negation downwards + if( !pol ){ + uires = -ires; + if( pvtn.isInteger() ){ + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( pvtn.isReal() ); + //now is strict inequality + uires = uires*2; + } + } + }else{ + bool is_upper = ( r==0 ); + if( options::cbqiModel() ){ + // disequality is a disjunction : only consider the bound in the direction of the model + //first check if there is an infinity... + if( !vts_coeff[0].isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl; + Assert( vts_coeff[0].isConst() ); + is_upper = ( vts_coeff[0].getConst<Rational>().sgn()==1 ); + }else{ + Node rhs_value = getModelValue( val ); + Node lhs_value = pv_value; + if( !veq_c.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Assert( lhs_value!=rhs_value ); + Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); + cmp = Rewriter::rewrite( cmp ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=d_true ); + } + } + Assert( atom.getKind()==EQUAL && !pol ); + if( pvtn.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( pvtn.isReal() ); + uires = is_upper ? -2 : 2; + } + } + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + if( !veq_c.isNull() ){ + Trace("cbqi-bound-inf") << veq_c << " * "; + } + Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + //take into account delta + if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff[1].isNull() ){ + vts_coeff[1] = delta_coeff; + }else{ + vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff ); + vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] ); + } + }else{ + Node delta = d_qe->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + mbp_bounds[index].push_back( uval ); + mbp_coeff[index].push_back( veq_c ); + for( unsigned t=0; t<2; t++ ){ + mbp_vts_coeff[index][t].push_back( vts_coeff[t] ); + } + mbp_lit[index].push_back( lit ); + }else{ + //try this bound + if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ + subs_proc[uval][veq_c] = true; + if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + } + } + } + } + } + } + } + } + if( options::cbqiModel() ){ + if( pvtn.isInteger() || pvtn.isReal() ){ + bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); + bool upper_first = false; + if( options::cbqiMinBounds() ){ + upper_first = mbp_bounds[1].size()<mbp_bounds[0].size(); + } + unsigned best_used[2]; + std::vector< Node > t_values[3]; + //try optimal bounds + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + if( mbp_bounds[rr].empty() ){ + if( use_inf ){ + Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; + //no bounds, we do +- infinity + Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); + //TODO : rho value for infinity? + if( rr==0 ){ + val = NodeManager::currentNM()->mkNode( UMINUS, val ); + val = Rewriter::rewrite( val ); + } + if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + }else{ + Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; + int best = -1; + Node best_bound_value[3]; + for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ + Node value[3]; + if( Trace.isOn("cbqi-bound") ){ + Assert( !mbp_bounds[rr][j].isNull() ); + Trace("cbqi-bound") << " " << j << ": " << mbp_bounds[rr][j]; + if( !mbp_vts_coeff[rr][0][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][0][j] << " * INF)"; + } + if( !mbp_vts_coeff[rr][1][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][1][j] << " * DELTA)"; + } + if( !mbp_coeff[rr][j].isNull() ){ + Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")"; + } + Trace("cbqi-bound") << ", value = "; + } + t_values[rr].push_back( Node::null() ); + //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts + bool new_best = true; + for( unsigned t=0; t<3; t++ ){ + //get the value + if( t==0 ){ + value[0] = mbp_vts_coeff[rr][0][j]; + if( !value[0].isNull() ){ + Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; + }else{ + value[0] = d_zero; + } + }else if( t==1 ){ + Node t_value = getModelValue( mbp_bounds[rr][j] ); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cbqi-bound") << value[1]; + }else{ + value[2] = mbp_vts_coeff[rr][1][j]; + if( !value[2].isNull() ){ + Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; + }else{ + value[2] = d_zero; + } + } + //multiply by coefficient + if( value[t]!=d_zero && !mbp_coeff[rr][j].isNull() ){ + Assert( mbp_coeff[rr][j].isConst() ); + value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); + value[t] = Rewriter::rewrite( value[t] ); + } + //check if new best + if( best!=-1 ){ + Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); + if( value[t]!=best_bound_value[t] ){ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound!=d_true ){ + new_best = false; + break; + } + } + } + } + Trace("cbqi-bound") << std::endl; + if( new_best ){ + for( unsigned t=0; t<3; t++ ){ + best_bound_value[t] = value[t]; + } + best = j; + } + } + if( best!=-1 ){ + Trace("cbqi-bound") << "...best bound is " << best << " : "; + if( best_bound_value[0]!=d_zero ){ + Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cbqi-bound") << best_bound_value[1]; + if( best_bound_value[2]!=d_zero ){ + Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cbqi-bound") << std::endl; + best_used[rr] = (unsigned)best; + Node val = mbp_bounds[rr][best]; + val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, + mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] ); + if( !val.isNull() ){ + if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ + subs_proc[val][mbp_coeff[rr][best]] = true; + if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + } + //if not using infinity, use model value of zero + if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ + Node val = d_zero; + Node c; //null (one) coefficient + val = getModelBasedProjectionValue( val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] ); + if( !val.isNull() ){ + if( subs_proc[val].find( c )==subs_proc[val].end() ){ + subs_proc[val][c] = true; + if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } +#ifdef MBP_STRICT_ASSERTIONS + Assert( false ); +#endif + //try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ + if( j!=best_used[rr] ){ + Node val = getModelBasedProjectionValue( mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta, + mbp_vts_coeff[rr][0][j], vts_sym[0], mbp_vts_coeff[rr][1][j], vts_sym[1] ); + if( !val.isNull() ){ + if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){ + subs_proc[val][mbp_coeff[rr][j]] = true; + if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + } + } + } + } + + //[4] resort to using value in model + // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype + if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){ + Node mv = getModelValue( pv ); + Node pv_coeff_m; + Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; + int new_effort = pvtn.isBoolean() ? effort : 1; +#ifdef MBP_STRICT_ASSERTIONS + //we only resort to values in the case of booleans + Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); +#endif + if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ + return true; + } + } + Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; + return false; + } +} + + +bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { + if( Trace.isOn("cbqi-inst") ){ + for( unsigned j=0; j<sf.d_subs.size(); j++ ){ + Trace("cbqi-inst") << " "; + } + Trace("cbqi-inst") << sf.d_subs.size() << ": "; + if( !pv_coeff.isNull() ){ + Trace("cbqi-inst") << pv_coeff << " * "; + } + Trace("cbqi-inst") << pv << " -> " << n << std::endl; + } + //must ensure variables have been computed for n + computeProgVars( n ); + + //substitute into previous substitutions, when applicable + std::vector< Node > a_subs; + a_subs.push_back( n ); + std::vector< Node > a_var; + a_var.push_back( pv ); + std::vector< Node > a_coeff; + std::vector< Node > a_has_coeff; + if( !pv_coeff.isNull() ){ + 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; + std::map< int, Node > prev_sym_subs; + std::vector< Node > new_has_coeff; + for( unsigned j=0; j<sf.d_subs.size(); j++ ){ + Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); + if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ + prev_subs[j] = sf.d_subs[j]; + TNode tv = pv; + TNode ts = n; + Node a_pv_coeff; + Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true ); + if( !new_subs.isNull() ){ + sf.d_subs[j] = new_subs; + if( !a_pv_coeff.isNull() ){ + prev_coeff[j] = sf.d_coeff[j]; + if( sf.d_coeff[j].isNull() ){ + Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() ); + //now has coefficient + new_has_coeff.push_back( vars[j] ); + sf.d_has_coeff.push_back( vars[j] ); + sf.d_coeff[j] = a_pv_coeff; + }else{ + sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); + } + } + if( sf.d_subs[j]!=prev_subs[j] ){ + computeProgVars( sf.d_subs[j] ); + } + }else{ + Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; + success = false; + break; + } + } + if( options::cbqiSymLia() && pv_coeff.isNull() ){ + //apply simple substitutions also to sym_subs + prev_sym_subs[j] = ssf.d_subs[j]; + ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() ); + ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] ); + } + } + if( success ){ + vars.push_back( pv ); + btyp.push_back( bt ); + sf.push_back( pv, n, pv_coeff ); + ssf.push_back( pv, n, pv_coeff ); + Node new_theta = theta; + if( !pv_coeff.isNull() ){ + if( new_theta.isNull() ){ + new_theta = pv_coeff; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff ); + new_theta = Rewriter::rewrite( new_theta ); + } + } + bool is_cv = false; + if( !curr_var.empty() ){ + Assert( curr_var.back()==pv ); + curr_var.pop_back(); + is_cv = true; + } + success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); + if( !success ){ + if( is_cv ){ + curr_var.push_back( pv ); + } + sf.pop_back( pv, n, pv_coeff ); + ssf.pop_back( pv, n, pv_coeff ); + vars.pop_back(); + btyp.pop_back(); + } + } + if( success ){ + return true; + }else{ + //revert substitution information + for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ + sf.d_subs[it->first] = it->second; + } + for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ + sf.d_coeff[it->first] = it->second; + } + for( unsigned i=0; i<new_has_coeff.size(); i++ ){ + sf.d_has_coeff.pop_back(); + } + for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){ + ssf.d_subs[it->first] = it->second; + } + return false; + } +} + +bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, + unsigned j, std::map< Node, Node >& cons ) { + + + if( j==sf.d_has_coeff.size() ){ + return addInstantiation( sf.d_subs, vars, cons ); + }else{ + Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() ); + unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin(); + Node prev = sf.d_subs[index]; + Assert( !sf.d_coeff[index].isNull() ); + Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl; + Assert( vars[index].getType().isInteger() ); + //must ensure that divisibility constraints are met + //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] ); + Node eq_rhs = sf.d_subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Node veq; + if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ + Node veq_c; + if( veq[0]!=vars[index] ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==vars[index] ); + } + } + sf.d_subs[index] = veq[1]; + if( !veq_c.isNull() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); + Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; + //intger division rounding up if from a lower bound + if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_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 ) + ); + } + } + Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl; + if( options::cbqiSymLia() ){ + //must apply substitution to previous subs + std::vector< Node > curr_var; + std::vector< Node > curr_subs; + curr_var.push_back( vars[index] ); + curr_subs.push_back( sf.d_subs[index] ); + for( unsigned k=0; k<index; k++ ){ + Node prevs = sf.d_subs[k]; + sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() ); + if( prevs!=sf.d_subs[k] ){ + Trace("cbqi-inst-debug2") << " rewrite " << vars[k] << " -> " << prevs << " to "; + sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] ); + Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl; + } + } + } + if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ + return true; + } + } + } + sf.d_subs[index] = prev; + Trace("cbqi-inst-debug") << "...failed." << std::endl; + return false; + } +} + +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { + if( vars.size()>d_vars.size() ){ + Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; + std::map< Node, Node > subs_map; + for( unsigned i=0; i<subs.size(); i++ ){ + subs_map[vars[i]] = subs[i]; + } + subs.clear(); + for( unsigned i=0; i<d_vars.size(); i++ ){ + Node n = constructInstantiation( d_vars[i], subs_map, cons ); + Trace("cbqi-inst-debug") << " " << d_vars[i] << " -> " << n << std::endl; + subs.push_back( n ); + } + } + bool ret = d_out->addInstantiation( subs ); +#ifdef MBP_STRICT_ASSERTIONS + Assert( ret ); +#endif + return ret; +} + +Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ) { + std::map< Node, Node >::iterator it = subs_map.find( n ); + if( it!=subs_map.end() ){ + return it->second; + }else{ + it = cons.find( n ); + Assert( it!=cons.end() ); + std::vector< Node > children; + children.push_back( it->second ); + const Datatype& dt = Datatype::datatypeOf( it->second.toExpr() ); + unsigned cindex = Datatype::indexOf( it->second.toExpr() ); + for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){ + Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), n ); + Node nc = constructInstantiation( nn, subs_map, cons ); + children.push_back( nc ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + } +} + +Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) { + Assert( d_prog_var.find( n )!=d_prog_var.end() ); + Assert( n==Rewriter::rewrite( n ) ); + bool req_coeff = false; + if( !has_coeff.empty() ){ + for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ + if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){ + req_coeff = true; + break; + } + } + } + if( !req_coeff ){ + Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( n!=nret ){ + nret = Rewriter::rewrite( nret ); + } + //result is nret + return nret; + }else{ + if( try_coeff ){ + //must convert to monomial representation + std::map< Node, Node > msum; + if( QuantArith::getMonomialSum( n, msum ) ){ + std::map< Node, Node > msum_coeff; + std::map< Node, Node > msum_term; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + //check if in substitution + std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); + if( its!=vars.end() ){ + int index = its-vars.begin(); + if( coeff[index].isNull() ){ + //apply substitution + msum_term[it->first] = subs[index]; + }else{ + //apply substitution, multiply to ensure no divisibility conflict + msum_term[it->first] = subs[index]; + //relative coefficient + msum_coeff[it->first] = coeff[index]; + if( pv_coeff.isNull() ){ + pv_coeff = coeff[index]; + }else{ + pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); + } + } + }else{ + msum_term[it->first] = it->first; + } + } + //make sum with normalized coefficient + Assert( !pv_coeff.isNull() ); + pv_coeff = Rewriter::rewrite( pv_coeff ); + Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; + std::vector< Node > children; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Node c_coeff; + if( !msum_coeff[it->first].isNull() ){ + c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) ); + }else{ + c_coeff = pv_coeff; + } + if( !it->second.isNull() ){ + c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); + } + Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + children.push_back( c ); + Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; + } + Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); + nret = Rewriter::rewrite( nret ); + //result is ( nret / pv_coeff ) + return nret; + }else{ + Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; + } + } + // failed to apply the substitution + return Node::null(); + } +} + +Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) { + Node val = t; + Trace("cbqi-bound2") << "Value : " << val << std::endl; + //add rho value + //get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if( !c.isNull() ){ + ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); + ceValue = Rewriter::rewrite( ceValue ); + if( new_theta.isNull() ){ + new_theta = c; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); + new_theta = Rewriter::rewrite( new_theta ); + } + Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; + } + if( !new_theta.isNull() ){ + Node rho; + if( isLower ){ + rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); + }else{ + rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); + } + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; + rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << rho << std::endl; + Kind rk = isLower ? PLUS : MINUS; + val = NodeManager::currentNM()->mkNode( rk, val, rho ); + val = Rewriter::rewrite( val ); + Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; + } + if( !inf_coeff.isNull() ){ + Assert( !vts_inf.isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) ); + val = Rewriter::rewrite( val ); + } + if( !delta_coeff.isNull() ){ + //create delta here if necessary + if( vts_delta.isNull() ){ + vts_delta = d_qe->getTermDatabase()->getVtsDelta(); + } + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) ); + val = Rewriter::rewrite( val ); + } + return val; +} + +bool CegInstantiator::check() { + if( d_qe->getTheoryEngine()->needCheck() ){ + Trace("cegqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; + return false; + } + processAssertions(); + for( unsigned r=0; r<2; r++ ){ + SolvedForm sf; + SolvedForm ssf; + std::vector< Node > vars; + std::vector< int > btyp; + Node theta; + std::map< Node, Node > cons; + std::vector< Node > curr_var; + //try to add an instantiation + if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + return true; + } + } + Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; +} + +void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { + if( n.getKind()==FORALL || n.getKind()==EXISTS ){ + //do nothing + }else{ + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); + if( it!=teq.end() ){ + Node nn = n[ i==0 ? 1 : 0 ]; + if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ + it->second.push_back( nn ); + Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; + } + } + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectPresolveEqTerms( n[i], teq ); + } + } +} + +void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, + std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { + if( conj.size()<1000 ){ + if( terms.size()==f[0].getNumChildren() ){ + Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + conj.push_back( c ); + }else{ + unsigned i = terms.size(); + Node v = f[0][i]; + terms.push_back( Node::null() ); + for( unsigned j=0; j<teq[v].size(); j++ ){ + terms[i] = teq[v][j]; + getPresolveEqConjuncts( vars, terms, teq, f, conj ); + } + terms.pop_back(); + } + } +} + +void CegInstantiator::presolve( Node q ) { + Trace("cbqi-presolve") << "CBQI presolve " << q << std::endl; + //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing + std::vector< Node > vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + vars.push_back( q[0][i] ); + teq[q[0][i]].clear(); + } + collectPresolveEqTerms( q[1], teq ); + std::vector< Node > terms; + std::vector< Node > conj; + getPresolveEqConjuncts( vars, terms, teq, q, conj ); + + if( !conj.empty() ){ + Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); + lem = NodeManager::currentNM()->mkNode( OR, g, lem ); + Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + d_qe->getOutputChannel().lemma( lem, false, true ); + } +} + +void collectTheoryIds( TypeNode tn, std::map< TypeNode, bool >& visited, std::vector< TheoryId >& tids ){ + std::map< TypeNode, bool >::iterator itt = visited.find( tn ); + if( itt==visited.end() ){ + visited[tn] = true; + TheoryId tid = Theory::theoryOf( tn ); + if( std::find( tids.begin(), tids.end(), tid )==tids.end() ){ + tids.push_back( tid ); + } + if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ + collectTheoryIds( TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ), visited, tids ); + } + } + } + } +} + +void CegInstantiator::processAssertions() { + Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl; + d_curr_asserts.clear(); + d_curr_eqc.clear(); + d_curr_type_eqc.clear(); + + eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); + //to eliminate identified illegal terms + std::map< Node, Node > aux_subs; + + //for each variable + std::vector< TheoryId > tids; + for( unsigned i=0; i<d_vars.size(); i++ ){ + Node pv = d_vars[i]; + TypeNode pvtn = pv.getType(); + //collect relevant theories + std::map< TypeNode, bool > visited; + collectTheoryIds( pvtn, visited, tids ); + //collect information about eqc + if( ee->hasTerm( pv ) ){ + Node pvr = ee->getRepresentative( pv ); + if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){ + Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl; + eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); + while( !eqc_i.isFinished() ){ + d_curr_eqc[pvr].push_back( *eqc_i ); + ++eqc_i; + } + } + } + } + //collect assertions for relevant theories + for( unsigned i=0; i<tids.size(); i++ ){ + TheoryId tid = tids[i]; + Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); + if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ + Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl; + d_curr_asserts[tid].clear(); + //collect all assertions from theory + for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { + Node lit = (*it).assertion; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ + d_curr_asserts[tid].push_back( lit ); + Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + }else{ + Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; + } + if( lit.getKind()==EQUAL ){ + std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit ); + if( itae!=d_aux_eq.end() ){ + for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){ + aux_subs[ itae2->first ] = itae2->second; + Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; + } + } + } + } + } + } + //collect equivalence classes that correspond to relevant theories + Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node r = *eqcs_i; + TypeNode rtn = r.getType(); + TheoryId tid = Theory::theoryOf( rtn ); + //if we care about the theory of this eqc + if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){ + if( rtn.isInteger() || rtn.isReal() ){ + rtn = rtn.getBaseType(); + } + Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl; + d_curr_type_eqc[rtn].push_back( r ); + if( d_curr_eqc.find( r )==d_curr_eqc.end() ){ + Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl; + Trace("cbqi-proc-debug") << " "; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Trace("cbqi-proc-debug") << *eqc_i << " "; + d_curr_eqc[r].push_back( *eqc_i ); + ++eqc_i; + } + Trace("cbqi-proc-debug") << std::endl; + } + } + ++eqcs_i; + } + //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula) + std::vector< Node > subs_lhs; + std::vector< Node > subs_rhs; + for( unsigned i=0; i<d_aux_vars.size(); i++ ){ + Node r = d_aux_vars[i]; + std::map< Node, Node >::iterator it = aux_subs.find( r ); + if( it!=aux_subs.end() ){ + addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); + }else{ + Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; +#ifdef MBP_STRICT_ASSERTIONS + Assert( false ); +#endif + } + } + + //apply substitutions to everything, if necessary + if( !subs_lhs.empty() ){ + Trace("cbqi-proc") << "Applying substitution : " << std::endl; + for( unsigned i=0; i<subs_lhs.size(); i++ ){ + Trace("cbqi-proc") << " " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl; + } + for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + Node lit = it->second[i]; + lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + lit = Rewriter::rewrite( lit ); + it->second[i] = lit; + } + } + for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + n = Rewriter::rewrite( n ); + it->second[i] = n; + } + } + } + + //remove unecessary assertions + for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ + std::vector< Node > akeep; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + //compute the variables in assertion + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + //must contain at least one variable + if( !d_prog_var[n].empty() ){ + Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; + akeep.push_back( n ); + }else{ + Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl; + } + }else{ + Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl; + } + } + it->second.clear(); + it->second.insert( it->second.end(), akeep.begin(), akeep.end() ); + } + + //remove duplicate terms from eqc + for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ + std::vector< Node > new_eqc; + for( unsigned i=0; i<it->second.size(); i++ ){ + if( std::find( new_eqc.begin(), new_eqc.end(), it->second[i] )==new_eqc.end() ){ + new_eqc.push_back( it->second[i] ); + } + } + it->second.clear(); + it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() ); + } +} + +void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) { + r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + + std::vector< Node > cl; + cl.push_back( l ); + std::vector< Node > cr; + cr.push_back( r ); + for( unsigned i=0; i<subs_lhs.size(); i++ ){ + Node nr = subs_rhs[i].substitute( cl.begin(), cl.end(), cr.begin(), cr.end() ); + nr = Rewriter::rewrite( nr ); + subs_rhs[i] = nr; + } + + subs_lhs.push_back( l ); + subs_rhs.push_back( r ); +} + +Node CegInstantiator::getModelValue( Node n ) { + return d_qe->getModel()->getValue( n ); +} + +void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { + if( n.getKind()==FORALL ){ + d_is_nested_quant = true; + }else{ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( TermDb::isBoolConnective( n.getKind() ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectCeAtoms( n[i], visited ); + } + }else{ + if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ + d_ce_atoms.push_back( n ); + } + } + } + } +} + +void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { + Assert( d_vars.empty() ); + d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); + IteSkolemMap iteSkolemMap; + d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); + Assert( d_aux_vars.empty() ); + for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { + Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; + d_aux_vars.push_back( i->first ); + } + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; + Node rlem = lems[i]; + rlem = Rewriter::rewrite( rlem ); + Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; + //record the literals that imply auxiliary variables to be equal to terms + if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ + if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){ + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){ + Node v = lems[i][1][0]; + for( unsigned r=1; r<=2; r++ ){ + d_aux_eq[rlem[r]][v] = lems[i][r][1]; + Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; + } + } + } + } + lems[i] = rlem; + } + //collect atoms from all lemmas: we will only do bounds coming from original body + d_is_nested_quant = false; + std::map< Node, bool > visited; + for( unsigned i=0; i<lems.size(); i++ ){ + collectCeAtoms( lems[i], visited ); + } +} diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h new file mode 100644 index 000000000..7dd6ef12b --- /dev/null +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -0,0 +1,135 @@ +/********************* */ +/*! \file ceg_instantiator.h + ** \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-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CEG_INSTANTIATOR_H +#define __CVC4__CEG_INSTANTIATOR_H + +#include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +namespace arith { + class TheoryArith; +} + +namespace quantifiers { + +class CegqiOutput { +public: + virtual ~CegqiOutput() {} + virtual bool addInstantiation( std::vector< Node >& subs ) = 0; + virtual bool isEligibleForInstantiation( Node n ) = 0; + virtual bool addLemma( Node lem ) = 0; +}; + +class CegInstantiator { +private: + QuantifiersEngine * d_qe; + CegqiOutput * d_out; + //constants + Node d_zero; + Node d_one; + Node d_true; + bool d_use_vts_delta; + bool d_use_vts_inf; + //program variable contains cache + std::map< Node, std::map< Node, bool > > d_prog_var; + std::map< Node, bool > d_inelig; + //current assertions + std::map< TheoryId, std::vector< Node > > d_curr_asserts; + std::map< Node, std::vector< Node > > d_curr_eqc; + std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; + //auxiliary variables + std::vector< Node > d_aux_vars; + //literals to equalities for aux vars + std::map< Node, std::map< Node, Node > > d_aux_eq; + //the CE variables + std::vector< Node > d_vars; + //atoms of the CE lemma + bool d_is_nested_quant; + std::vector< Node > d_ce_atoms; +private: + //collect atoms + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); + //for adding instantiations during check + void computeProgVars( Node n ); + //solved form, involves substitution with coefficients + class SolvedForm { + public: + std::vector< Node > d_subs; + std::vector< Node > d_coeff; + std::vector< Node > d_has_coeff; + void copy( SolvedForm& sf ){ + d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); + d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); + d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); + } + void push_back( Node pv, Node n, Node pv_coeff ){ + d_subs.push_back( n ); + d_coeff.push_back( pv_coeff ); + if( !pv_coeff.isNull() ){ + d_has_coeff.push_back( pv ); + } + } + void pop_back( Node pv, Node n, Node pv_coeff ){ + d_subs.pop_back(); + d_coeff.pop_back(); + if( !pv_coeff.isNull() ){ + d_has_coeff.pop_back(); + } + } + }; + // effort=0 : do not use model value, 1: use model value, 2: one must use model value + bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ); + bool addInstantiationCoeff( SolvedForm& sf, + std::vector< Node >& vars, std::vector< int >& btyp, + unsigned j, std::map< Node, Node >& cons ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); + Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); + Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); + } + Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); + Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); + void processAssertions(); + void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); + //get model value + Node getModelValue( Node n ); +public: + CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); + //check : add instantiations based on valuation of d_vars + bool check(); + //presolve for quantified formula + void presolve( Node q ); + //register the counterexample lemma (stored in lems), modify vector + void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 1f4d398be..39e7abd3b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/trigger.h" #include "util/ite_removal.h" using namespace std; @@ -31,1377 +32,145 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA -//#define MBP_STRICT_ASSERTIONS - -CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) : -d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){ - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - d_true = NodeManager::currentNM()->mkConst( true ); - d_is_nested_quant = false; -} - -void CegInstantiator::computeProgVars( Node n ){ - if( d_prog_var.find( n )==d_prog_var.end() ){ - d_prog_var[n].clear(); - if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ - d_prog_var[n][n] = true; - }else if( !d_out->isEligibleForInstantiation( n ) ){ - d_inelig[n] = true; - return; - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - computeProgVars( n[i] ); - if( d_inelig.find( n[i] )!=d_inelig.end() ){ - d_inelig[n] = true; - return; - } - 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; - } - //selectors applied to program variables are also variables - if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){ - d_prog_var[n][n] = true; - } - } - } -} - -bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ - if( i==d_vars.size() ){ - //solved for all variables, now construct instantiation - if( !sf.d_has_coeff.empty() ){ - if( options::cbqiSymLia() ){ - //use symbolic solved forms - SolvedForm csf; - csf.copy( ssf ); - return addInstantiationCoeff( csf, vars, btyp, 0, cons ); - }else{ - return addInstantiationCoeff( sf, vars, btyp, 0, cons ); - } - }else{ - return addInstantiation( sf.d_subs, vars, cons ); - } - }else{ - std::map< Node, std::map< Node, bool > > subs_proc; - //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; - bool is_cv = false; - Node pv; - if( curr_var.empty() ){ - pv = d_vars[i]; - }else{ - pv = curr_var.back(); - is_cv = true; - } - TypeNode pvtn = pv.getType(); - Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl; - Node pv_value; - if( options::cbqiModel() ){ - pv_value = d_qe->getModel()->getValue( pv ); - Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; - } - Node pvr = pv; - if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){ - pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv ); - } - - //if in effort=2, we must choose at least one model value - if( (i+1)<d_vars.size() || effort!=2 ){ - - //[1] easy case : pv is in the equivalence class as another term not containing pv - Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl; - std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr ); - if( it_eqc!=d_curr_eqc.end() ){ - Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl; - for( unsigned k=0; k<it_eqc->second.size(); k++ ){ - Node n = it_eqc->second[k]; - if( n!=pv ){ - Trace("cbqi-inst-debug") << "...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 - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) - bool proc = false; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, sf, vars, pv_coeff, false ); - if( !ns.isNull() ){ - computeProgVars( ns ); - //substituted version must be new and cannot contain pv - proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); - } - }else{ - ns = n; - proc = true; - } - if( proc ){ - //try the substitution - subs_proc[ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } +InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : InstStrategy( qe ){ + +} + +void InstStrategyCbqi::processResetInstantiationRound( Theory::Effort effort ) { + d_cbqi_set_quant_inactive = false; + //check if any cbqi lemma has not been added yet + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine + if( d_quantEngine->hasOwnership( q, d_quantEngine->getInstantiationEngine() ) && doCbqi( q ) ){ + if( !hasAddedCbqiLemma( q ) ){ + d_added_cbqi_lemma[q] = true; + Trace("cbqi") << "Do cbqi for " << q << std::endl; + //add cbqi lemma + //get the counterexample literal + Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); + //require any decision on cel to be phase=true + d_quantEngine->addRequirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + lem = Rewriter::rewrite( lem ); + Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; + registerCounterexampleLemma( q, lem ); } - }else{ - Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl; - } - - //[2] : we can solve an equality for pv - if( pvtn.isInteger() || pvtn.isReal() ){ - ///iterate over equivalence classes to find cases where we can solve for the variable - TypeNode pvtnb = pvtn.getBaseType(); - Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl; - for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ - Node r = d_curr_type_eqc[pvtnb][k]; - std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); - std::vector< Node > lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - Assert( it_reqc!=d_curr_eqc.end() ); - for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ - Node n = it_reqc->second[kk]; - Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; - //compute the variables in n - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, sf, vars, pv_coeff ); - if( !ns.isNull() ){ - computeProgVars( ns ); - } - }else{ - ns = n; - } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; - 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("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; - Node eq_lhs = lhs[j]; - Node eq_rhs = ns; - //make the same coefficient - if( pv_coeff!=lhs_coeff[j] ){ - if( !pv_coeff.isNull() ){ - Trace("cbqi-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; - eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - //cannot contain infinity? - //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){ - Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; - } - Node veq; - if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ - Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl; - Node veq_c; - if( veq[0]!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - Node val = veq[1]; - if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ - subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - lhs.push_back( ns ); - lhs_v.push_back( hasVar ); - lhs_coeff.push_back( pv_coeff ); - }else{ - Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; - } + //set inactive the quantified formulas whose CE literals are asserted false + }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + bool value; + if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; + if( !value ){ + if( d_quantEngine->getValuation().isDecision( cel ) ){ + Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ - Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; - } - } - } - }else if( pvtn.isDatatype() ){ - Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; - //look in equivalence class for a constructor - if( it_eqc!=d_curr_eqc.end() ){ - for( unsigned k=0; k<it_eqc->second.size(); k++ ){ - Node n = it_eqc->second[k]; - if( n.getKind()==APPLY_CONSTRUCTOR ){ - Trace("cbqi-inst-debug") << "... " << i << "...try based on constructor term " << n << std::endl; - cons[pv] = n.getOperator(); - const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype(); - unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); - if( is_cv ){ - curr_var.pop_back(); - } - //now must solve for selectors applied to pv - for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ - curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); - } - if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - }else{ - //cleanup - cons.erase( pv ); - Assert( curr_var.size()>=dt[cindex].getNumArgs() ); - for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ - curr_var.pop_back(); - } - if( is_cv ){ - curr_var.push_back( pv ); - } - break; - } + d_quantEngine->getModel()->setQuantifierActive( q, false ); + d_cbqi_set_quant_inactive = true; } } }else{ - Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl; - } - } - - //[3] directly look at assertions - Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl; - Node vts_sym[2]; - vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); - vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); - std::vector< Node > mbp_bounds[2]; - std::vector< Node > mbp_coeff[2]; - std::vector< Node > mbp_vts_coeff[2][2]; - std::vector< Node > mbp_lit[2]; - unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; - for( unsigned r=0; r<rmax; r++ ){ - TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() ); - Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl; - std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid ); - if( ita!=d_curr_asserts.end() ){ - for (unsigned j = 0; j<ita->second.size(); j++) { - Node lit = ita->second[j]; - Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( tid==THEORY_ARITH ){ - //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ - Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() ); - 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_lhs )==d_inelig.end() ){ - //apply substitution to LHS of atom - if( !d_prog_var[atom_lhs].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff ); - if( !atom_lhs.isNull() ){ - computeProgVars( atom_lhs ); - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); - } - } - } - //if it contains pv, not infinity - 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 ); - //cannot contain infinity? - //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){ - Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - } - //get the coefficient of infinity and remove it from msum - Node vts_coeff[2]; - for( unsigned t=0; t<2; t++ ){ - if( !vts_sym[t].isNull() ){ - std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] ); - if( itminf!=msum.end() ){ - vts_coeff[t] = itminf->second; - if( vts_coeff[t].isNull() ){ - vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - } - //negate if coefficient on variable is positive - std::map< Node, Node >::iterator itv = msum.find( pv ); - if( itv!=msum.end() ){ - //multiply by the coefficient we will isolate for - if( itv->second.isNull() ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - }else{ - if( !pvtn.isInteger() ){ - vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); - vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); - }else if( itv->second.getConst<Rational>().sgn()==1 ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - } - } - } - Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; - msum.erase( vts_sym[t] ); - } - } - } - - Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; - Node vatom; - //isolate pv in the inequality - int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); - if( ires!=0 ){ - Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl; - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - Node veq_c; - if( pvm!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - - //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; - for( unsigned r=0; r<rmax; r++ ){ - int uires = ires; - Node uval = val; - if( atom.getKind()==GEQ ){ - //push negation downwards - if( !pol ){ - uires = -ires; - if( pvtn.isInteger() ){ - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper = ( r==0 ); - if( options::cbqiModel() ){ - // disequality is a disjunction : only consider the bound in the direction of the model - //first check if there is an infinity... - if( !vts_coeff[0].isNull() ){ - //coefficient or val won't make a difference, just compare with zero - Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl; - Assert( vts_coeff[0].isConst() ); - is_upper = ( vts_coeff[0].getConst<Rational>().sgn()==1 ); - }else{ - Node rhs_value = d_qe->getModel()->getValue( val ); - Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); - lhs_value = Rewriter::rewrite( lhs_value ); - } - Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; - Assert( lhs_value!=rhs_value ); - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - is_upper = ( cmp!=d_true ); - } - } - Assert( atom.getKind()==EQUAL && !pol ); - if( pvtn.isInteger() ){ - uires = is_upper ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - uires = is_upper ? -2 : 2; - } - } - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - if( !veq_c.isNull() ){ - Trace("cbqi-bound-inf") << veq_c << " * "; - } - Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; - //take into account delta - if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); - if( vts_coeff[1].isNull() ){ - vts_coeff[1] = delta_coeff; - }else{ - vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff ); - vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] ); - } - }else{ - Node delta = d_qe->getTermDatabase()->getVtsDelta(); - uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); - uval = Rewriter::rewrite( uval ); - } - } - if( options::cbqiModel() ){ - //just store bounds, will choose based on tighest bound - unsigned index = uires>0 ? 0 : 1; - mbp_bounds[index].push_back( uval ); - mbp_coeff[index].push_back( veq_c ); - for( unsigned t=0; t<2; t++ ){ - mbp_vts_coeff[index][t].push_back( vts_coeff[t] ); - } - mbp_lit[index].push_back( lit ); - }else{ - //try this bound - if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ - subs_proc[uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - } - } - } - } - } - } - } - if( options::cbqiModel() ){ - if( pvtn.isInteger() || pvtn.isReal() ){ - bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); - bool upper_first = false; - if( options::cbqiMinBounds() ){ - upper_first = mbp_bounds[1].size()<mbp_bounds[0].size(); - } - unsigned best_used[2]; - std::vector< Node > t_values[3]; - //try optimal bounds - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - if( mbp_bounds[rr].empty() ){ - if( use_inf ){ - Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; - //no bounds, we do +- infinity - Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); - //TODO : rho value for infinity? - if( rr==0 ){ - val = NodeManager::currentNM()->mkNode( UMINUS, val ); - val = Rewriter::rewrite( val ); - } - if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - }else{ - Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; - int best = -1; - Node best_bound_value[3]; - for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ - Node value[3]; - if( Trace.isOn("cbqi-bound") ){ - Assert( !mbp_bounds[rr][j].isNull() ); - Trace("cbqi-bound") << " " << j << ": " << mbp_bounds[rr][j]; - if( !mbp_vts_coeff[rr][0][j].isNull() ){ - Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][0][j] << " * INF)"; - } - if( !mbp_vts_coeff[rr][1][j].isNull() ){ - Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][1][j] << " * DELTA)"; - } - if( !mbp_coeff[rr][j].isNull() ){ - Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")"; - } - Trace("cbqi-bound") << ", value = "; - } - t_values[rr].push_back( Node::null() ); - //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts - bool new_best = true; - for( unsigned t=0; t<3; t++ ){ - //get the value - if( t==0 ){ - value[0] = mbp_vts_coeff[rr][0][j]; - if( !value[0].isNull() ){ - Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; - }else{ - value[0] = d_zero; - } - }else if( t==1 ){ - Node t_value = d_qe->getModel()->getValue( mbp_bounds[rr][j] ); - t_values[rr][j] = t_value; - value[1] = t_value; - Trace("cbqi-bound") << value[1]; - }else{ - value[2] = mbp_vts_coeff[rr][1][j]; - if( !value[2].isNull() ){ - Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; - }else{ - value[2] = d_zero; - } - } - //multiply by coefficient - if( value[t]!=d_zero && !mbp_coeff[rr][j].isNull() ){ - Assert( mbp_coeff[rr][j].isConst() ); - value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); - value[t] = Rewriter::rewrite( value[t] ); - } - //check if new best - if( best!=-1 ){ - Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); - if( value[t]!=best_bound_value[t] ){ - Kind k = rr==0 ? GEQ : LEQ; - Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); - cmp_bound = Rewriter::rewrite( cmp_bound ); - if( cmp_bound!=d_true ){ - new_best = false; - break; - } - } - } - } - Trace("cbqi-bound") << std::endl; - if( new_best ){ - for( unsigned t=0; t<3; t++ ){ - best_bound_value[t] = value[t]; - } - best = j; - } - } - if( best!=-1 ){ - Trace("cbqi-bound") << "...best bound is " << best << " : "; - if( best_bound_value[0]!=d_zero ){ - Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; - } - Trace("cbqi-bound") << best_bound_value[1]; - if( best_bound_value[2]!=d_zero ){ - Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; - } - Trace("cbqi-bound") << std::endl; - best_used[rr] = (unsigned)best; - Node val = mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, - mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] ); - if( !val.isNull() ){ - if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ - subs_proc[val][mbp_coeff[rr][best]] = true; - if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - //if not using infinity, use model value of zero - if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ - Node val = d_zero; - Node c; //null (one) coefficient - val = getModelBasedProjectionValue( val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] ); - if( !val.isNull() ){ - if( subs_proc[val].find( c )==subs_proc[val].end() ){ - subs_proc[val][c] = true; - if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } -#ifdef MBP_STRICT_ASSERTIONS - Assert( false ); -#endif - //try non-optimal bounds (heuristic, may help when nested quantification) ? - Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ - if( j!=best_used[rr] ){ - Node val = getModelBasedProjectionValue( mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta, - mbp_vts_coeff[rr][0][j], vts_sym[0], mbp_vts_coeff[rr][1][j], vts_sym[1] ); - if( !val.isNull() ){ - if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){ - subs_proc[val][mbp_coeff[rr][j]] = true; - if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - } - } - } - - //[4] resort to using value in model - // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){ - Node mv = d_qe->getModel()->getValue( pv ); - Node pv_coeff_m; - Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; - int new_effort = pvtn.isBoolean() ? effort : 1; -#ifdef MBP_STRICT_ASSERTIONS - //we only resort to values in the case of booleans - Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); -#endif - if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ - return true; - } - } - Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; - return false; - } -} - - -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { - if( Trace.isOn("cbqi-inst") ){ - for( unsigned j=0; j<sf.d_subs.size(); j++ ){ - Trace("cbqi-inst") << " "; - } - Trace("cbqi-inst") << sf.d_subs.size() << ": "; - if( !pv_coeff.isNull() ){ - Trace("cbqi-inst") << pv_coeff << " * "; - } - Trace("cbqi-inst") << pv << " -> " << n << std::endl; - } - //must ensure variables have been computed for n - computeProgVars( n ); - - //substitute into previous substitutions, when applicable - std::vector< Node > a_subs; - a_subs.push_back( n ); - std::vector< Node > a_var; - a_var.push_back( pv ); - std::vector< Node > a_coeff; - std::vector< Node > a_has_coeff; - if( !pv_coeff.isNull() ){ - 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; - std::map< int, Node > prev_sym_subs; - std::vector< Node > new_has_coeff; - for( unsigned j=0; j<sf.d_subs.size(); j++ ){ - Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); - if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ - prev_subs[j] = sf.d_subs[j]; - TNode tv = pv; - TNode ts = n; - Node a_pv_coeff; - Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true ); - if( !new_subs.isNull() ){ - sf.d_subs[j] = new_subs; - if( !a_pv_coeff.isNull() ){ - prev_coeff[j] = sf.d_coeff[j]; - if( sf.d_coeff[j].isNull() ){ - Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() ); - //now has coefficient - new_has_coeff.push_back( vars[j] ); - sf.d_has_coeff.push_back( vars[j] ); - sf.d_coeff[j] = a_pv_coeff; - }else{ - sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); - } + Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; } - if( sf.d_subs[j]!=prev_subs[j] ){ - computeProgVars( sf.d_subs[j] ); - } - }else{ - Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; - success = false; - break; - } - } - if( options::cbqiSymLia() && pv_coeff.isNull() ){ - //apply simple substitutions also to sym_subs - prev_sym_subs[j] = ssf.d_subs[j]; - ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() ); - ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] ); - } - } - if( success ){ - vars.push_back( pv ); - btyp.push_back( bt ); - sf.push_back( pv, n, pv_coeff ); - ssf.push_back( pv, n, pv_coeff ); - Node new_theta = theta; - if( !pv_coeff.isNull() ){ - if( new_theta.isNull() ){ - new_theta = pv_coeff; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff ); - new_theta = Rewriter::rewrite( new_theta ); - } - } - bool is_cv = false; - if( !curr_var.empty() ){ - Assert( curr_var.back()==pv ); - curr_var.pop_back(); - is_cv = true; - } - success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); - if( !success ){ - if( is_cv ){ - curr_var.push_back( pv ); } - sf.pop_back( pv, n, pv_coeff ); - ssf.pop_back( pv, n, pv_coeff ); - vars.pop_back(); - btyp.pop_back(); } } - if( success ){ - return true; - }else{ - //revert substitution information - for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ - sf.d_subs[it->first] = it->second; - } - for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ - sf.d_coeff[it->first] = it->second; - } - for( unsigned i=0; i<new_has_coeff.size(); i++ ){ - sf.d_has_coeff.pop_back(); - } - for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){ - ssf.d_subs[it->first] = it->second; - } - return false; - } } -bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, - unsigned j, std::map< Node, Node >& cons ) { - - - if( j==sf.d_has_coeff.size() ){ - return addInstantiation( sf.d_subs, vars, cons ); - }else{ - Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() ); - unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin(); - Node prev = sf.d_subs[index]; - Assert( !sf.d_coeff[index].isNull() ); - Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl; - Assert( vars[index].getType().isInteger() ); - //must ensure that divisibility constraints are met - //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] ); - Node eq_rhs = sf.d_subs[index]; - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - Node veq; - if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ - Node veq_c; - if( veq[0]!=vars[index] ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==vars[index] ); - } - } - sf.d_subs[index] = veq[1]; - if( !veq_c.isNull() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); - Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; - //intger division rounding up if from a lower bound - if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_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 ) - ); - } - } - Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl; - if( options::cbqiSymLia() ){ - //must apply substitution to previous subs - std::vector< Node > curr_var; - std::vector< Node > curr_subs; - curr_var.push_back( vars[index] ); - curr_subs.push_back( sf.d_subs[index] ); - for( unsigned k=0; k<index; k++ ){ - Node prevs = sf.d_subs[k]; - sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() ); - if( prevs!=sf.d_subs[k] ){ - Trace("cbqi-inst-debug2") << " rewrite " << vars[k] << " -> " << prevs << " to "; - sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] ); - Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl; - } - } - } - if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ - return true; - } - } - } - sf.d_subs[index] = prev; - Trace("cbqi-inst-debug") << "...failed." << std::endl; - return false; - } +void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ + Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem, false ); } -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { - if( vars.size()>d_vars.size() ){ - Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; - std::map< Node, Node > subs_map; - for( unsigned i=0; i<subs.size(); i++ ){ - subs_map[vars[i]] = subs[i]; - } - subs.clear(); - for( unsigned i=0; i<d_vars.size(); i++ ){ - Node n = constructInstantiation( d_vars[i], subs_map, cons ); - Trace("cbqi-inst-debug") << " " << d_vars[i] << " -> " << n << std::endl; - subs.push_back( n ); - } - } - bool ret = d_out->addInstantiation( subs ); -#ifdef MBP_STRICT_ASSERTIONS - Assert( ret ); -#endif - return ret; -} - -Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ) { - std::map< Node, Node >::iterator it = subs_map.find( n ); - if( it!=subs_map.end() ){ - return it->second; - }else{ - it = cons.find( n ); - Assert( it!=cons.end() ); - std::vector< Node > children; - children.push_back( it->second ); - const Datatype& dt = Datatype::datatypeOf( it->second.toExpr() ); - unsigned cindex = Datatype::indexOf( it->second.toExpr() ); - for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){ - Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), n ); - Node nc = constructInstantiation( nn, subs_map, cons ); - children.push_back( nc ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - } -} - -Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, - std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) { - Assert( d_prog_var.find( n )!=d_prog_var.end() ); - Assert( n==Rewriter::rewrite( n ) ); - bool req_coeff = false; - if( !has_coeff.empty() ){ - for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ - if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){ - req_coeff = true; - break; - } - } - } - if( !req_coeff ){ - Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - if( n!=nret ){ - nret = Rewriter::rewrite( nret ); - } - //result is nret - return nret; - }else{ - if( try_coeff ){ - //must convert to monomial representation - std::map< Node, Node > msum; - if( QuantArith::getMonomialSum( n, msum ) ){ - std::map< Node, Node > msum_coeff; - std::map< Node, Node > msum_term; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - //check if in substitution - std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); - if( its!=vars.end() ){ - int index = its-vars.begin(); - if( coeff[index].isNull() ){ - //apply substitution - msum_term[it->first] = subs[index]; - }else{ - //apply substitution, multiply to ensure no divisibility conflict - msum_term[it->first] = subs[index]; - //relative coefficient - msum_coeff[it->first] = coeff[index]; - if( pv_coeff.isNull() ){ - pv_coeff = coeff[index]; - }else{ - pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); - } - } - }else{ - msum_term[it->first] = it->first; - } - } - //make sum with normalized coefficient - Assert( !pv_coeff.isNull() ); - pv_coeff = Rewriter::rewrite( pv_coeff ); - Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; - std::vector< Node > children; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Node c_coeff; - if( !msum_coeff[it->first].isNull() ){ - c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) ); - }else{ - c_coeff = pv_coeff; - } - if( !it->second.isNull() ){ - c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); - } - Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); - children.push_back( c ); - Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; - } - Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); - nret = Rewriter::rewrite( nret ); - //result is ( nret / pv_coeff ) - return nret; +bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr( n ) ){ + if( !inst::Trigger::isCbqiKind( n.getKind() ) ){ + Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; + return true; + }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){ + Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl; + return true; }else{ - Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; - } - } - // failed to apply the substitution - return Node::null(); - } -} - -Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, - Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) { - Node val = t; - Trace("cbqi-bound2") << "Value : " << val << std::endl; - //add rho value - //get the value of c*e - Node ceValue = me; - Node new_theta = theta; - if( !c.isNull() ){ - ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); - ceValue = Rewriter::rewrite( ceValue ); - if( new_theta.isNull() ){ - new_theta = c; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); - new_theta = Rewriter::rewrite( new_theta ); - } - Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; - Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; - } - if( !new_theta.isNull() ){ - Node rho; - if( isLower ){ - rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); - }else{ - rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); - } - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; - Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; - rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : MINUS; - val = NodeManager::currentNM()->mkNode( rk, val, rho ); - val = Rewriter::rewrite( val ); - Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; - } - if( !inf_coeff.isNull() ){ - Assert( !vts_inf.isNull() ); - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) ); - val = Rewriter::rewrite( val ); - } - if( !delta_coeff.isNull() ){ - //create delta here if necessary - if( vts_delta.isNull() ){ - vts_delta = d_qe->getTermDatabase()->getVtsDelta(); - } - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) ); - val = Rewriter::rewrite( val ); - } - return val; -} - -bool CegInstantiator::check() { - if( d_qe->getTheoryEngine()->needCheck() ){ - Trace("cegqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; - return false; - } - processAssertions(); - for( unsigned r=0; r<2; r++ ){ - SolvedForm sf; - SolvedForm ssf; - std::vector< Node > vars; - std::vector< int > btyp; - Node theta; - std::map< Node, Node > cons; - std::vector< Node > curr_var; - //try to add an instantiation - if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ - return true; - } - } - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; - return false; -} - -void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { - if( n.getKind()==FORALL || n.getKind()==EXISTS ){ - //do nothing - }else{ - if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); - if( it!=teq.end() ){ - Node nn = n[ i==0 ? 1 : 0 ]; - if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ - it->second.push_back( nn ); - Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( hasNonCbqiOperator( n[i], visited ) ){ + return true; } } } } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectPresolveEqTerms( n[i], teq ); - } - } -} - -void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, - std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { - if( conj.size()<1000 ){ - if( terms.size()==f[0].getNumChildren() ){ - Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - conj.push_back( c ); - }else{ - unsigned i = terms.size(); - Node v = f[0][i]; - terms.push_back( Node::null() ); - for( unsigned j=0; j<teq[v].size(); j++ ){ - terms[i] = teq[v][j]; - getPresolveEqConjuncts( vars, terms, teq, f, conj ); - } - terms.pop_back(); - } } + return false; } - -void CegInstantiator::presolve( Node q ) { - Trace("cbqi-presolve") << "CBQI presolve " << q << std::endl; - //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing - std::vector< Node > vars; - std::map< Node, std::vector< Node > > teq; +bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - vars.push_back( q[0][i] ); - teq[q[0][i]].clear(); - } - collectPresolveEqTerms( q[1], teq ); - std::vector< Node > terms; - std::vector< Node > conj; - getPresolveEqConjuncts( vars, terms, teq, q, conj ); - - if( !conj.empty() ){ - Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); - lem = NodeManager::currentNM()->mkNode( OR, g, lem ); - Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma( lem, false, true ); - } -} - -void collectTheoryIds( TypeNode tn, std::map< TypeNode, bool >& visited, std::vector< TheoryId >& tids ){ - std::map< TypeNode, bool >::iterator itt = visited.find( tn ); - if( itt==visited.end() ){ - visited[tn] = true; - TheoryId tid = Theory::theoryOf( tn ); - if( std::find( tids.begin(), tids.end(), tid )==tids.end() ){ - tids.push_back( tid ); - } - if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - collectTheoryIds( TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ), visited, tids ); + TypeNode tn = q[0][i].getType(); + if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){ + if( options::cbqiSplx() ){ + return true; + }else{ + //datatypes supported in new implementation + if( !tn.isDatatype() ){ + return true; } } } } + return false; } -void CegInstantiator::processAssertions() { - Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl; - d_curr_asserts.clear(); - d_curr_eqc.clear(); - d_curr_type_eqc.clear(); - - eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - //to eliminate identified illegal terms - std::map< Node, Node > aux_subs; - - //for each variable - std::vector< TheoryId > tids; - for( unsigned i=0; i<d_vars.size(); i++ ){ - Node pv = d_vars[i]; - TypeNode pvtn = pv.getType(); - //collect relevant theories - std::map< TypeNode, bool > visited; - collectTheoryIds( pvtn, visited, tids ); - //collect information about eqc - if( ee->hasTerm( pv ) ){ - Node pvr = ee->getRepresentative( pv ); - if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){ - Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl; - eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); - while( !eqc_i.isFinished() ){ - d_curr_eqc[pvr].push_back( *eqc_i ); - ++eqc_i; - } - } - } - } - //collect assertions for relevant theories - for( unsigned i=0; i<tids.size(); i++ ){ - TheoryId tid = tids[i]; - Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); - if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ - Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl; - d_curr_asserts[tid].clear(); - //collect all assertions from theory - for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { - Node lit = (*it).assertion; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ - d_curr_asserts[tid].push_back( lit ); - Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; - }else{ - Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; - } - if( lit.getKind()==EQUAL ){ - std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit ); - if( itae!=d_aux_eq.end() ){ - for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){ - aux_subs[ itae2->first ] = itae2->second; - Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; - } - } - } - } - } - } - //collect equivalence classes that correspond to relevant theories - Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - Node r = *eqcs_i; - TypeNode rtn = r.getType(); - TheoryId tid = Theory::theoryOf( rtn ); - //if we care about the theory of this eqc - if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){ - if( rtn.isInteger() || rtn.isReal() ){ - rtn = rtn.getBaseType(); - } - Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl; - d_curr_type_eqc[rtn].push_back( r ); - if( d_curr_eqc.find( r )==d_curr_eqc.end() ){ - Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl; - Trace("cbqi-proc-debug") << " "; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - Trace("cbqi-proc-debug") << *eqc_i << " "; - d_curr_eqc[r].push_back( *eqc_i ); - ++eqc_i; - } - Trace("cbqi-proc-debug") << std::endl; - } - } - ++eqcs_i; - } - //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula) - std::vector< Node > subs_lhs; - std::vector< Node > subs_rhs; - for( unsigned i=0; i<d_aux_vars.size(); i++ ){ - Node r = d_aux_vars[i]; - std::map< Node, Node >::iterator it = aux_subs.find( r ); - if( it!=aux_subs.end() ){ - addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); +bool InstStrategyCbqi::doCbqi( Node q ){ + std::map< Node, bool >::iterator it = d_do_cbqi.find( q ); + if( it==d_do_cbqi.end() ){ + bool ret = false; + Assert( options::cbqi() ); + if( options::cbqiAll() ){ + ret = true; }else{ - Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; -#ifdef MBP_STRICT_ASSERTIONS - Assert( false ); -#endif - } - } - - //apply substitutions to everything, if necessary - if( !subs_lhs.empty() ){ - Trace("cbqi-proc") << "Applying substitution : " << std::endl; - for( unsigned i=0; i<subs_lhs.size(); i++ ){ - Trace("cbqi-proc") << " " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl; - } - for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ - for( unsigned i=0; i<it->second.size(); i++ ){ - Node lit = it->second[i]; - lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - lit = Rewriter::rewrite( lit ); - it->second[i] = lit; - } - } - for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ - for( unsigned i=0; i<it->second.size(); i++ ){ - Node n = it->second[i]; - n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - n = Rewriter::rewrite( n ); - it->second[i] = n; - } - } - } - - //remove unecessary assertions - for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ - std::vector< Node > akeep; - for( unsigned i=0; i<it->second.size(); i++ ){ - Node n = it->second[i]; - //compute the variables in assertion - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - //must contain at least one variable - if( !d_prog_var[n].empty() ){ - Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; - akeep.push_back( n ); - }else{ - Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl; - } - }else{ - Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl; - } - } - it->second.clear(); - it->second.insert( it->second.end(), akeep.begin(), akeep.end() ); + //if quantifier has a non-arithmetic variable, then do not use cbqi + //if quantifier has an APPLY_UF term, then do not use cbqi + Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + std::map< Node, bool > visited; + ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited ); + } + d_do_cbqi[q] = ret; + return ret; + }else{ + return it->second; } +} - //remove duplicate terms from eqc - for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ - std::vector< Node > new_eqc; - for( unsigned i=0; i<it->second.size(); i++ ){ - if( std::find( new_eqc.begin(), new_eqc.end(), it->second[i] )==new_eqc.end() ){ - new_eqc.push_back( it->second[i] ); +Node InstStrategyCbqi::getNextDecisionRequest(){ + // all counterexample literals that are not asserted + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( hasAddedCbqiLemma( q ) ){ + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl; + return cel; } } - it->second.clear(); - it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() ); } + return Node::null(); } -void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) { - r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - std::vector< Node > cl; - cl.push_back( l ); - std::vector< Node > cr; - cr.push_back( r ); - for( unsigned i=0; i<subs_lhs.size(); i++ ){ - Node nr = subs_rhs[i].substitute( cl.begin(), cl.end(), cr.begin(), cr.end() ); - nr = Rewriter::rewrite( nr ); - subs_rhs[i] = nr; - } - subs_lhs.push_back( l ); - subs_rhs.push_back( r ); -} - -void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { - if( n.getKind()==FORALL ){ - d_is_nested_quant = true; - }else{ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( TermDb::isBoolConnective( n.getKind() ) ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectCeAtoms( n[i], visited ); - } - }else{ - if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ - d_ce_atoms.push_back( n ); - } - } - } - } -} - -void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { - Assert( d_vars.empty() ); - d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); - IteSkolemMap iteSkolemMap; - d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); - Assert( d_aux_vars.empty() ); - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; - d_aux_vars.push_back( i->first ); - } - for( unsigned i=0; i<lems.size(); i++ ){ - Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; - Node rlem = lems[i]; - rlem = Rewriter::rewrite( rlem ); - Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; - //record the literals that imply auxiliary variables to be equal to terms - if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ - if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){ - if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){ - Node v = lems[i][1][0]; - for( unsigned r=1; r<=2; r++ ){ - d_aux_eq[rlem[r]][v] = lems[i][r][1]; - Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; - } - } - } - } - lems[i] = rlem; - } - //collect atoms from lem[0]: we will only do bounds coming from original body - d_is_nested_quant = false; - std::map< Node, bool > visited; - collectCeAtoms( lems[0], visited ); -} //old implementation -InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : - InstStrategy( ie ), d_th( th ), d_counter( 0 ){ +InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategyCbqi( ie ), d_th( th ), d_counter( 0 ){ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); } @@ -1465,6 +234,7 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort Debug("quant-arith-debug") << std::endl; debugPrint( "quant-arith-debug" ); d_counter++; + InstStrategyCbqi::processResetInstantiationRound( effort ); } void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){ @@ -1494,89 +264,91 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder< } int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ - if( e<1 ){ - return STATUS_UNFINISHED; - }else if( e==1 ){ - if( d_quantActive.find( f )!=d_quantActive.end() ){ - //the point instantiation - InstMatch m_point( f ); - bool m_point_valid = true; - int lem = 0; - //scan over all instantiation rows - for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ - Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); - Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; - for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ - ArithVar x = d_instRows[ic][j]; - if( !d_ceTableaux[ic][x].empty() ){ - if( Debug.isOn("quant-arith-simplex") ){ - Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl; - Debug("quant-arith-simplex") << " "; - for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){ - if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } - Debug("quant-arith-simplex") << it->first << " * " << it->second; - } - Debug("quant-arith-simplex") << " = "; - Node v = getTableauxValue( x, false ); - Debug("quant-arith-simplex") << v << std::endl; - Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl; - Debug("quant-arith-simplex") << " ce-term : "; - for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){ - if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } - Debug("quant-arith-simplex") << it->first << " * " << it->second; - } - Debug("quant-arith-simplex") << std::endl; - } - //instantiation row will be A*e + B*t = beta, - // where e is a vector of terms , and t is vector of ground terms. - // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant - // We will construct the term ( beta - B*t)/coeff to use for e_i. - InstMatch m( f ); - for( unsigned k=0; k<f[0].getNumChildren(); k++ ){ - if( f[0][k].getType().isInteger() ){ - m.setValue( k, d_zero ); + if( doCbqi( f ) ){ + if( e<1 ){ + return STATUS_UNFINISHED; + }else if( e==1 ){ + if( d_quantActive.find( f )!=d_quantActive.end() ){ + //the point instantiation + InstMatch m_point( f ); + bool m_point_valid = true; + int lem = 0; + //scan over all instantiation rows + for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); + Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; + for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ + ArithVar x = d_instRows[ic][j]; + if( !d_ceTableaux[ic][x].empty() ){ + if( Debug.isOn("quant-arith-simplex") ){ + Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl; + Debug("quant-arith-simplex") << " "; + for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){ + if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } + Debug("quant-arith-simplex") << it->first << " * " << it->second; + } + Debug("quant-arith-simplex") << " = "; + Node v = getTableauxValue( x, false ); + Debug("quant-arith-simplex") << v << std::endl; + Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl; + Debug("quant-arith-simplex") << " ce-term : "; + for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){ + if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } + Debug("quant-arith-simplex") << it->first << " * " << it->second; + } + Debug("quant-arith-simplex") << std::endl; } - } - //By default, choose the first instantiation constant to be e_i. - Node var = d_ceTableaux[ic][x].begin()->first; - //if it is integer, we need to find variable with coefficent +/- 1 - if( var.getType().isInteger() ){ - std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); - while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ - ++it; - if( it==d_ceTableaux[ic][x].end() ){ - var = Node::null(); - }else{ - var = it->first; + //instantiation row will be A*e + B*t = beta, + // where e is a vector of terms , and t is vector of ground terms. + // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant + // We will construct the term ( beta - B*t)/coeff to use for e_i. + InstMatch m( f ); + for( unsigned k=0; k<f[0].getNumChildren(); k++ ){ + if( f[0][k].getType().isInteger() ){ + m.setValue( k, d_zero ); } } - //Otherwise, try one that divides all ground term coefficients? - // Might be futile, if rewrite ensures gcd of coeffs is 1. - } - if( !var.isNull() ){ - //add to point instantiation if applicable - if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){ - Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl; - Node v = getTableauxValue( x, false ); - if( !var.getType().isInteger() || v.getType().isInteger() ){ - m_point.setValue( i, v ); - }else{ - m_point_valid = false; + //By default, choose the first instantiation constant to be e_i. + Node var = d_ceTableaux[ic][x].begin()->first; + //if it is integer, we need to find variable with coefficent +/- 1 + if( var.getType().isInteger() ){ + std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); + while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ + ++it; + if( it==d_ceTableaux[ic][x].end() ){ + var = Node::null(); + }else{ + var = it->first; + } } + //Otherwise, try one that divides all ground term coefficients? + // Might be futile, if rewrite ensures gcd of coeffs is 1. } - Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; - if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){ - lem++; + if( !var.isNull() ){ + //add to point instantiation if applicable + if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){ + Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl; + Node v = getTableauxValue( x, false ); + if( !var.getType().isInteger() || v.getType().isInteger() ){ + m_point.setValue( i, v ); + }else{ + m_point_valid = false; + } + } + Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; + if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){ + lem++; + } + }else{ + Debug("quant-arith-simplex") << "Could not find var." << std::endl; } - }else{ - Debug("quant-arith-simplex") << "Could not find var." << std::endl; } } } - } - if( lem==0 && m_point_valid ){ - if( d_quantEngine->addInstantiation( f, m_point ) ){ - Debug("quant-arith-simplex") << "...added point instantiation." << std::endl; + if( lem==0 && m_point_valid ){ + if( d_quantEngine->addInstantiation( f, m_point ) ){ + Debug("quant-arith-simplex") << "...added point instantiation." << std::endl; + } } } } @@ -1623,7 +395,7 @@ void InstStrategySimplex::debugPrint( const char* c ){ } Debug(c) << std::endl; - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug(c) << f << std::endl; Debug(c) << " Inst constants: "; @@ -1733,44 +505,48 @@ bool CegqiOutputInstStrategy::addLemma( Node lem ) { } -InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) { +InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) { d_out = new CegqiOutputInstStrategy( this ); d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); } void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { d_check_vts_lemma_lc = true; + InstStrategyCbqi::processResetInstantiationRound( effort ); } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { - if( e<1 ){ - return STATUS_UNFINISHED; - }else if( e==1 ){ - CegInstantiator * cinst = getInstantiator( f ); - Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; - d_curr_quant = f; - bool addedLemma = cinst->check(); - d_curr_quant = Node::null(); - return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; - }else if( e==2 ){ - //minimize the free delta heuristically on demand - if( d_check_vts_lemma_lc ){ - d_check_vts_lemma_lc = false; - d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); - d_small_const = Rewriter::rewrite( d_small_const ); - //heuristic for now, until we know how to do nested quantification - Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); - if( !delta.isNull() ){ - Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; - Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); - d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); - } - std::vector< Node > inf; - d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false ); - for( unsigned i=0; i<inf.size(); i++ ){ - Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; - Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); - d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); + //can only be called at last call, since it is model-based + if( doCbqi( f ) && effort==Theory::EFFORT_LAST_CALL ){ + if( e<1 ){ + return STATUS_UNFINISHED; + }else if( e==1 ){ + CegInstantiator * cinst = getInstantiator( f ); + Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; + d_curr_quant = f; + bool addedLemma = cinst->check(); + d_curr_quant = Node::null(); + return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; + }else if( e==2 ){ + //minimize the free delta heuristically on demand + if( d_check_vts_lemma_lc ){ + d_check_vts_lemma_lc = false; + d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); + d_small_const = Rewriter::rewrite( d_small_const ); + //heuristic for now, until we know how to do nested quantification + Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); + if( !delta.isNull() ){ + Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } + std::vector< Node > inf; + d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false ); + for( unsigned i=0; i<inf.size(); i++ ){ + Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; + Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); + d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); + } } } } @@ -1815,6 +591,23 @@ void InstStrategyCegqi::registerQuantifier( Node q ) { } } +void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { + //must register with the instantiator + //must explicitly remove ITEs so that we record dependencies + std::vector< Node > ce_vars; + for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){ + ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) ); + } + std::vector< Node > lems; + lems.push_back( lem ); + CegInstantiator * cinst = getInstantiator( q ); + cinst->registerCounterexampleLemma( lems, ce_vars ); + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl; + d_quantEngine->addLemma( lems[i], false ); + } +} + void InstStrategyCegqi::presolve() { if( options::cbqiPreRegInst() ){ for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 9fe938f16..adbb2a5e4 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -20,6 +20,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/arith/arithvar.h" +#include "theory/quantifiers/ceg_instantiator.h" #include "util/statistics_registry.h" @@ -32,106 +33,36 @@ namespace arith { namespace quantifiers { -class CegqiOutput -{ +class InstStrategyCbqi : public InstStrategy { +protected: + bool d_cbqi_set_quant_inactive; + /** whether we have added cbqi lemma */ + std::map< Node, bool > d_added_cbqi_lemma; + /** whether to do cbqi for this quantified formula */ + std::map< Node, bool > d_do_cbqi; + /** register ce lemma */ + virtual void registerCounterexampleLemma( Node q, Node lem ); + /** has added cbqi lemma */ + bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } + /** helper functions */ + bool hasNonCbqiVariable( Node q ); + bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); public: - virtual ~CegqiOutput() {} - virtual bool addInstantiation( std::vector< Node >& subs ) = 0; - virtual bool isEligibleForInstantiation( Node n ) = 0; - virtual bool addLemma( Node lem ) = 0; + InstStrategyCbqi( QuantifiersEngine * qe ); + ~InstStrategyCbqi() throw() {} + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + /** get next decision request */ + Node getNextDecisionRequest(); + //set quant inactive + bool setQuantifierInactive() { return d_cbqi_set_quant_inactive; } + /** whether to do CBQI for quantifier q */ + bool doCbqi( Node q ); }; -class CegInstantiator -{ -private: - QuantifiersEngine * d_qe; - CegqiOutput * d_out; - //constants - Node d_zero; - Node d_one; - Node d_true; - bool d_use_vts_delta; - bool d_use_vts_inf; - //program variable contains cache - std::map< Node, std::map< Node, bool > > d_prog_var; - std::map< Node, bool > d_inelig; - //current assertions - std::map< TheoryId, std::vector< Node > > d_curr_asserts; - std::map< Node, std::vector< Node > > d_curr_eqc; - std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; - //auxiliary variables - std::vector< Node > d_aux_vars; - //literals to equalities for aux vars - std::map< Node, std::map< Node, Node > > d_aux_eq; - //the CE variables - std::vector< Node > d_vars; - //atoms of the CE lemma - bool d_is_nested_quant; - std::vector< Node > d_ce_atoms; -private: - //collect atoms - void collectCeAtoms( Node n, std::map< Node, bool >& visited ); - //for adding instantiations during check - void computeProgVars( Node n ); - //solved form, involves substitution with coefficients - class SolvedForm { - public: - std::vector< Node > d_subs; - std::vector< Node > d_coeff; - std::vector< Node > d_has_coeff; - void copy( SolvedForm& sf ){ - d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); - d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); - d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); - } - void push_back( Node pv, Node n, Node pv_coeff ){ - d_subs.push_back( n ); - d_coeff.push_back( pv_coeff ); - if( !pv_coeff.isNull() ){ - d_has_coeff.push_back( pv ); - } - } - void pop_back( Node pv, Node n, Node pv_coeff ){ - d_subs.pop_back(); - d_coeff.pop_back(); - if( !pv_coeff.isNull() ){ - d_has_coeff.pop_back(); - } - } - }; - // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool addInstantiationCoeff( SolvedForm& sf, - std::vector< Node >& vars, std::vector< int >& btyp, - unsigned j, std::map< Node, Node >& cons ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); - Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); - Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); - } - Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, - std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); - Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, - Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); - void processAssertions(); - void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); -public: - CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); - //check : add instantiations based on valuation of d_vars - bool check(); - //presolve for quantified formula - void presolve( Node q ); - //register the counterexample lemma (stored in lems), modify vector - void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); -}; -class InstStrategySimplex : public InstStrategy{ -private: +class InstStrategySimplex : public InstStrategyCbqi { +protected: /** reference to theory arithmetic */ arith::TheoryArith* d_th; /** quantifiers we should process */ @@ -177,8 +108,7 @@ public: class InstStrategyCegqi; -class CegqiOutputInstStrategy : public CegqiOutput -{ +class CegqiOutputInstStrategy : public CegqiOutput { public: CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} InstStrategyCegqi * d_out; @@ -187,8 +117,8 @@ public: bool addLemma( Node lem ); }; -class InstStrategyCegqi : public InstStrategy { -private: +class InstStrategyCegqi : public InstStrategyCbqi { +protected: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_small_const; @@ -197,6 +127,8 @@ private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); + /** register ce lemma */ + void registerCounterexampleLemma( Node q, Node lem ); public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() throw() {} diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 8f1ef42d8..b32f27d8f 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -59,13 +59,17 @@ void InstantiationEngine::finishInit(){ //counterexample-based quantifier instantiation if( options::cbqi() ){ - if( !options::cbqi2() ){ + if( options::cbqiSplx() ){ d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); d_instStrategies.push_back( d_i_splx ); + d_i_cbqi = d_i_splx; }else{ d_i_cegqi = new InstStrategyCegqi( d_quantEngine ); d_instStrategies.push_back( d_i_cegqi ); + d_i_cbqi = d_i_cegqi; } + }else{ + d_i_cbqi = NULL; } } @@ -77,63 +81,6 @@ void InstantiationEngine::presolve() { bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size(); - //if counterexample-based quantifier instantiation is active - if( options::cbqi() ){ - //check if any cbqi lemma has not been added yet - bool addedLemma = false; - for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ - d_added_cbqi_lemma[f] = true; - Trace("cbqi") << "Do cbqi for " << f << std::endl; - //add cbqi lemma - //get the counterexample literal - Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); - if( !ceBody.isNull() ){ - //add counterexample lemma - Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); - //require any decision on cel to be phase=true - d_quantEngine->addRequirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - lem = Rewriter::rewrite( lem ); - Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - - if( d_i_cegqi ){ - //must register with the instantiator - //must explicitly remove ITEs so that we record dependencies - std::vector< Node > ce_vars; - for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ - ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) ); - } - std::vector< Node > lems; - lems.push_back( lem ); - CegInstantiator * cinst = d_i_cegqi->getInstantiator( f ); - cinst->registerCounterexampleLemma( lems, ce_vars ); - for( unsigned i=0; i<lems.size(); i++ ){ - Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl; - d_quantEngine->addLemma( lems[i], false ); - } - }else{ - Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->addLemma( lem, false ); - } - addedLemma = true; - } - } - } - if( addedLemma ){ - return true; - } - } - //if not, proceed to instantiation round - //reset the instantiation strategies - for( unsigned i=0; i<d_instStrategies.size(); ++i ){ - InstStrategy* is = d_instStrategies[i]; - is->processResetInstantiationRound( effort ); - } - //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; @@ -181,41 +128,27 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ return d_quantEngine->getInstWhenNeedsCheck( e ); } -unsigned InstantiationEngine::needsModel( Theory::Effort e ) { +unsigned InstantiationEngine::needsModel( Theory::Effort e ){ if( options::cbqiModel() && options::cbqi() ){ - return QuantifiersEngine::QEFFORT_STANDARD; - }else{ - return QuantifiersEngine::QEFFORT_NONE; - } -} - -void InstantiationEngine::reset_round( Theory::Effort e ) { - d_cbqi_set_quant_inactive = false; - if( options::cbqi() ){ - //set inactive the quantified formulas whose CE literals are asserted false + Assert( d_i_cbqi!=NULL ); + //needs model if there is at least one cbqi quantified formula that is active for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine - if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) && hasAddedCbqiLemma( q ) ){ - Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); - bool value; - if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; - if( !value ){ - if( d_quantEngine->getValuation().isDecision( cel ) ){ - Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; - }else{ - d_quantEngine->getModel()->setQuantifierActive( q, false ); - d_cbqi_set_quant_inactive = true; - } - } - }else{ - Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; - } + if( d_quantEngine->hasOwnership( q, this ) && d_i_cbqi->doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + return QuantifiersEngine::QEFFORT_STANDARD; } } } + return QuantifiersEngine::QEFFORT_NONE; +} + +void InstantiationEngine::reset_round( Theory::Effort e ){ + //if not, proceed to instantiation round + //reset the instantiation strategies + for( unsigned i=0; i<d_instStrategies.size(); ++i ){ + InstStrategy* is = d_instStrategies[i]; + is->processResetInstantiationRound( e ); + } } void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ @@ -228,7 +161,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ ++(d_statistics.d_instantiation_rounds); bool quantActive = false; d_quants.clear(); - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ if( !options::cbqi() || !TermDb::hasInstConstAttr(q) ){ @@ -253,7 +186,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } bool InstantiationEngine::checkComplete() { - if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){ + if( !options::cbqiSat() && ( d_i_cbqi && d_i_cbqi->setQuantifierInactive() ) ){ return false; }else{ for( unsigned i=0; i<d_quants.size(); i++ ){ @@ -271,12 +204,14 @@ void InstantiationEngine::registerQuantifier( Node f ){ d_instStrategies[i]->registerQuantifier( f ); } //Notice() << "do cbqi " << f << " ? " << std::endl; + /* if( options::cbqi() ){ Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); if( !doCbqi( f ) ){ d_quantEngine->addTermToDatabase( ceBody, true ); } } + */ //take into account user patterns if( f.getNumChildren()==3 ){ @@ -295,83 +230,20 @@ void InstantiationEngine::registerQuantifier( Node f ){ } void InstantiationEngine::assertNode( Node f ){ - ////if we are doing cbqi and have not added the lemma yet, do so - //if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ - // addCbqiLemma( f ); - //} -} -bool InstantiationEngine::hasApplyUf( Node n ){ - if( n.getKind()==APPLY_UF ){ - return true; - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( hasApplyUf( n[i] ) ){ - return true; - } - } - return false; - } -} -bool InstantiationEngine::hasNonCbqiVariable( Node q ){ - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); - if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){ - if( options::cbqi2() ){ - //datatypes supported in new implementation - if( !tn.isDatatype() ){ - return true; - } - }else{ - return true; - } - } - } - return false; -} - -bool InstantiationEngine::doCbqi( Node q ){ - if( options::cbqi.wasSetByUser() || options::cbqi2.wasSetByUser() ){ - return options::cbqi(); - }else if( options::cbqi() ){ - //if quantifier has a non-arithmetic variable, then do not use cbqi - //if quantifier has an APPLY_UF term, then do not use cbqi - return !hasNonCbqiVariable( q ) && !hasApplyUf( q[1] ); - }else{ - return false; - } } bool InstantiationEngine::isIncomplete( Node q ) { return true; - //TODO : ensure completeness for local theory extensions - //if( d_i_lte ){ - //return !d_i_lte->isLocalTheoryExt( f ); } - - - - - - - - - - - Node InstantiationEngine::getNextDecisionRequest(){ - //propagate as decision all counterexample literals that are not asserted if( options::cbqi() ){ - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( hasAddedCbqiLemma( f ) ){ - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - bool value; - if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Debug("cbqi-prop-as-dec") << "CBQI: get next decision " << cel << std::endl; - return cel; - } + for( unsigned i=0; i<d_instStrategies.size(); ++i ){ + InstStrategy* is = d_instStrategies[i]; + Node lit = is->getNextDecisionRequest(); + if( !lit.isNull() ){ + return lit; } } } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 3b7a5f4f8..e545ff43d 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -27,6 +27,7 @@ namespace quantifiers { class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; class InstStrategyFreeVariable; +class InstStrategyCbqi; class InstStrategySimplex; class InstStrategyCegqi; @@ -53,6 +54,8 @@ public: virtual std::string identify() const { return std::string("Unknown"); } /** register quantifier */ virtual void registerQuantifier( Node q ) {} + /** get next decision request */ + virtual Node getNextDecisionRequest() { return Node::null(); } };/* class InstStrategy */ class InstantiationEngine : public QuantifiersModule @@ -66,6 +69,7 @@ private: InstStrategyUserPatterns* d_isup; /** auto gen triggers; only kept for destructor cleanup */ InstStrategyAutoGenTriggers* d_i_ag; + InstStrategyCbqi * d_i_cbqi; /** simplex (cbqi) */ InstStrategySimplex * d_i_splx; /** generic cegqi */ @@ -74,25 +78,11 @@ private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** current processing quantified formulas */ std::vector< Node > d_quants; - /** whether we have added cbqi lemma */ - std::map< Node, bool > d_added_cbqi_lemma; private: - /** has added cbqi lemma */ - bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } - /** helper functions */ - bool hasNonCbqiVariable( Node q ); - bool hasApplyUf( Node n ); - /** whether to do CBQI for quantifier q */ - bool doCbqi( Node q ); /** is the engine incomplete for this quantifier */ bool isIncomplete( Node q ); - /** cbqi set inactive */ - bool d_cbqi_set_quant_inactive; -private: /** do instantiation round */ bool doInstantiationRound( Theory::Effort effort ); - /** register literals of n, f is the quantifier it belongs to */ - //void registerLiterals( Node n, Node f ); public: InstantiationEngine( QuantifiersEngine* qe ); ~InstantiationEngine(); diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 9502fd362..01d3f0c22 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -35,6 +35,8 @@ typedef enum { INST_WHEN_FULL_DELAY, /** Apply instantiation round at full effort half the time, and last call always */ INST_WHEN_FULL_LAST_CALL, + /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */ + INST_WHEN_FULL_DELAY_LAST_CALL, /** Apply instantiation round at last call only */ INST_WHEN_LAST_CALL, } InstWhenMode; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 9e8d02d30..a60f5af78 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -229,16 +229,18 @@ option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::Sygus template mode for sygus invariant synthesis # approach applied to general quantified formulas +option cbqiSplx --cbqi-splx bool :read-write :default false + turns on old implementation of counterexample-based quantifier instantiation option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation -option cbqi2 --cbqi2 bool :read-write :default false - turns on new implementation of counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default true turns on recursive counterexample-based quantifier instantiation option cbqiSat --cbqi-sat bool :read-write :default true answer sat when quantifiers are asserted with counterexample-based quantifier instantiation option cbqiModel --cbqi-model bool :read-write :default true guide instantiations by model values for counterexample-based quantifier instantiation +option cbqiAll --cbqi-all bool :default false + apply counterexample-based instantiation to all quantified formulas option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false use integer infinity for vts in counterexample-based quantifier instantiation option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index f27b98a3d..02a1a6cf2 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -40,6 +40,10 @@ full-delay \n\ + Run instantiation round at full effort, before theory combination, after\n\ all other theories have finished.\n\ \n\ +full-delay-last-call \n\ ++ Alternate running instantiation rounds at full effort after all other\n\ + theories have finished, and last call. \n\ +\n\ last-call\n\ + Run instantiation at last call effort, after theory combination and\n\ and theories report sat.\n\ @@ -235,6 +239,8 @@ inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, return INST_WHEN_FULL_DELAY; } else if(optarg == "full-last-call") { return INST_WHEN_FULL_LAST_CALL; + } else if(optarg == "full-delay-last-call") { + return INST_WHEN_FULL_DELAY_LAST_CALL; } else if(optarg == "last-call") { return INST_WHEN_LAST_CALL; } else if(optarg == "help") { diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 0085177cc..5706c789e 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -312,12 +312,18 @@ bool Trigger::isAtomicTrigger( Node n ){ return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || ( k!=APPLY_UF && isAtomicTriggerKind( k ) ); } + bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON; } +bool Trigger::isCbqiKind( Kind k ) { + return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT || + k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER; +} + bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index f601a02ab..bd4c19dba 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -108,6 +108,7 @@ public: static bool isUsableTrigger( Node n, Node f ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); + static bool isCbqiKind( Kind k ); static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 622ef5a52..28a4d4c6b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -137,7 +137,7 @@ d_presolve_cache_wic(u){ }else{ d_inst_engine = NULL; } - if( options::finiteModelFind() ){ + if( options::finiteModelFind() ){ if( options::fmfBoundInt() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); d_modules.push_back( d_bint ); @@ -336,8 +336,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_modules[i]->needsCheck( e ) ){ qm.push_back( d_modules[i] ); needsCheck = true; - unsigned me = d_modules[i]->needsModel( e ); - needsModelE = me<needsModelE ? me : needsModelE; + //can only request model at last call since theory combination can find inconsistencies + if( e>=Theory::EFFORT_LAST_CALL ){ + unsigned me = d_modules[i]->needsModel( e ); + needsModelE = me<needsModelE ? me : needsModelE; + } } } } @@ -402,6 +405,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_modules[i]->reset_round( e ); } Trace("quant-engine-debug") << "Done resetting all modules." << std::endl; + //reset may have added lemmas + flushLemmas(); + if( d_hasAddedLemma ){ + return; + } if( e==Theory::EFFORT_LAST_CALL ){ //if effort is last call, try to minimize model first @@ -702,7 +710,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); } - if( options::cbqi() && !options::cbqi2() ){ + if( options::cbqiSplx() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; @@ -987,7 +995,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){ + performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2 index 406cb0c1b..72ec634a8 100644 --- a/test/regress/regress0/bug519.smt2 +++ b/test/regress/regress0/bug519.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: -mi --tlimit-per 1000 -; EXPECT: unknown +; COMMAND-LINE: -mi +; EXPECT: sat ; EXPECT: unsat (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2 index b39e415a8..dbc230599 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2 +++ b/test/regress/regress0/quantifiers/bug291.smt2 @@ -10,5 +10,4 @@ (declare-fun store2 (Int) Int) (assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A))))) (check-sat) -(get-info :reason-unknown) (exit) diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect index 2bd8349de..7856f23b4 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2.expect +++ b/test/regress/regress0/quantifiers/bug291.smt2.expect @@ -1,2 +1 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) +% EXPECT: sat diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index e8d53669c..bd7ca19cd 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi2 +; COMMAND-LINE: --dt-rewrite-error-sel ; EXPECT: unsat (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) |