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 \
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 );
}
}
options::ceGuidedInst.set( true );
}
if( options::ceGuidedInst() ){
+ //counterexample-guided instantiation for sygus
if( !options::cegqiSingleInv.wasSetByUser() ){
options::cegqiSingleInv.set( true );
}
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 );
+ }
+ }
}
}
--- /dev/null
+/********************* */
+/*! \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 );
+ }
+}
--- /dev/null
+/********************* */
+/*! \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
#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;
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) );
}
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 ){
}
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;
+ }
}
}
}
}
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: ";
}
-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 );
+ }
}
}
}
}
}
+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 ){
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/arith/arithvar.h"
+#include "theory/quantifiers/ceg_instantiator.h"
#include "util/statistics_registry.h"
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 */
class InstStrategyCegqi;
-class CegqiOutputInstStrategy : public CegqiOutput
-{
+class CegqiOutputInstStrategy : public CegqiOutput {
public:
CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
InstStrategyCegqi * d_out;
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;
/** 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() {}
//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;
}
}
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;
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 ){
++(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) ){
}
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++ ){
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 ){
}
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;
}
}
}
class InstStrategyUserPatterns;
class InstStrategyAutoGenTriggers;
class InstStrategyFreeVariable;
+class InstStrategyCbqi;
class InstStrategySimplex;
class InstStrategyCegqi;
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
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 */
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();
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;
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
+ 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\
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") {
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++ ){
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 );
}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 );
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;
+ }
}
}
}
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
}
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;
}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{
-; COMMAND-LINE: -mi --tlimit-per 1000
-; EXPECT: unknown
+; COMMAND-LINE: -mi
+; EXPECT: sat
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(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)
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
+% EXPECT: sat
-; COMMAND-LINE: --cbqi2
+; COMMAND-LINE: --dt-rewrite-error-sel
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
projects / cvc5.git / commitdiff