non-optimal bounds for counterexample-based quantifier instantiation
option cbqiLitDepend --cbqi-lit-dep bool :default false
dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation
-option cbqiInnermost --cbqi-innermost bool :default false
+option cbqiInnermost --cbqi-innermost bool :read-write :default false
only process innermost quantified formulas in counterexample-based quantifier instantiation
+option cbqiNestedQE --cbqi-nested-qe bool :default false
+ process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation
option quantEpr --quant-epr bool :default false
infer whether in effectively propositional fragment, use for cbqi
ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
InternalError(ss.str().c_str());
}
+
+ #if 1
//get the instantiations for all quantified formulas
std::map< Node, std::vector< Node > > insts;
d_theoryEngine->getInstantiations( insts );
ss << " that was not related to the query. Try option --simplification=none.";
InternalError(ss.str().c_str());
}
- }
+ }
+#else
+ Node ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
+#endif
Trace("smt-qe") << "Returned : " << ret_n << std::endl;
ret_n = Rewriter::rewrite( ret_n.negate() );
return ret_n.toExpr();
#include "theory/arith/theory_arith_private.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/theory_engine.h"
#include "theory/bv/theory_bv_utils.h"
int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
if( ires!=0 ){
//disequalities are either strict upper or lower bounds
- unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
+ unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2;
for( unsigned r=0; r<rmax; r++ ){
int uires = ires;
Node uval = val;
}
}
}else{
- bool is_upper = ( r==0 );
+ bool is_upper;
if( options::cbqiModel() ){
// disequality is a disjunction : only consider the bound in the direction of the model
//first check if there is an infinity...
Assert( cmp.isConst() );
is_upper = ( cmp!=d_true );
}
+ }else{
+ is_upper = (r==0);
}
Assert( atom.getKind()==EQUAL && !pol );
if( pvtn.isInteger() ){
unsigned index = uires>0 ? 0 : 1;
mbp_bounds[index].push_back( uval );
mbp_coeff[index].push_back( veq_c );
+ Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
for( unsigned t=0; t<2; t++ ){
mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
}
//[5] 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() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
+
+#ifdef CVC4_ASSERTIONS
+ if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){
+ Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
+ Assert( false );
+ }
+#endif
Node mv = getModelValue( pv );
Node pv_coeff_m;
Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
}
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 );
+ //only if no nested quantifiers
+ if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){
+ 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 );
+ 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 CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
- Assert( d_vars.empty() );
+ //Assert( d_vars.empty() );
+ d_vars.clear();
d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
//determine variable order: must do Reals before Ints
//remove ITEs
IteSkolemMap iteSkolemMap;
d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
- Assert( d_aux_vars.empty() );
+ //Assert( d_aux_vars.empty() );
+ d_aux_vars.clear();
+ d_aux_eq.clear();
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 );
if( options::cbqiAll() ){
// when not pure LIA/LRA, we must check whether the lhs contains pv
if( TermDb::containsTerm( val, pv ) ){
+ Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl;
return 0;
}
}
}
vts_coeff_inf = vts_coeff[0];
vts_coeff_delta = vts_coeff[1];
+ Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl;
+ }else{
+ Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl;
}
return ires;
}
}
}
}else{
- insts.push_back( qe->getInstantiation( q, terms, true ) );
+ if( hasInstLemma() ){
+ insts.push_back( getInstLemma() );
+ }else{
+ insts.push_back( qe->getInstantiation( q, terms, true ) );
+ }
}
}else{
for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
if( terms.size()==q[0].getNumChildren() ){
if( useActive ){
if( hasInstLemma() ){
- Node lem;
+ Node lem = getInstLemma();
if( std::find( active.begin(), active.end(), lem )!=active.end() ){
insts.push_back( lem );
}
}
}else{
- insts.push_back( qe->getInstantiation( q, terms, true ) );
+ if( hasInstLemma() ){
+ insts.push_back( getInstLemma() );
+ }else{
+ insts.push_back( qe->getInstantiation( q, terms, true ) );
+ }
}
}else{
for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/theory_engine.h"
using namespace std;
#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
- : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() )
+ : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ),
+d_elim_quants( qe->getSatContext() ),
+d_nested_qe_waitlist_size( qe->getUserContext() ),
+d_nested_qe_waitlist_proc( qe->getUserContext() )
//, d_added_inst( qe->getUserContext() )
{
+ d_qid_count = 0;
}
InstStrategyCbqi::~InstStrategyCbqi() throw(){}
return QuantifiersEngine::QEFFORT_NONE;
}
+bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
+ if( !hasAddedCbqiLemma( q ) ){
+ d_added_cbqi_lemma.insert( q );
+ Trace("cbqi-debug") << "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-lemma") << "Counterexample lemma : " << lem << std::endl;
+ registerCounterexampleLemma( q, lem );
+
+ //totality lemmas for EPR
+ QuantEPR * qepr = d_quantEngine->getQuantEPR();
+ if( qepr!=NULL ){
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ TypeNode tn = q[0][i].getType();
+ if( tn.isSort() ){
+ if( qepr->isEPR( tn ) ){
+ //add totality lemma
+ std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
+ if( itc!=qepr->d_consts.end() ){
+ Assert( !itc->second.empty() );
+ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
+ std::vector< Node > disj;
+ for( unsigned j=0; j<itc->second.size(); j++ ){
+ disj.push_back( ic.eqNode( itc->second[j] ) );
+ }
+ Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
+ Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
+ d_quantEngine->getOutputChannel().lemma( tlem );
+ }else{
+ Assert( false );
+ }
+ }else{
+ Assert( !options::cbqiAll() );
+ }
+ }
+ }
+ }
+
+ //compute dependencies between quantified formulas
+ if( options::cbqiLitDepend() || options::cbqiInnermost() ){
+ std::vector< Node > ics;
+ TermDb::computeVarContains( q, ics );
+ d_parent_quant[q].clear();
+ d_children_quant[q].clear();
+ std::vector< Node > dep;
+ for( unsigned i=0; i<ics.size(); i++ ){
+ Node qi = ics[i].getAttribute(InstConstantAttribute());
+ if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
+ d_parent_quant[q].push_back( qi );
+ d_children_quant[qi].push_back( q );
+ Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
+ dep.push_back( qi );
+ dep.push_back( qicel );
+ }
+ }
+ if( !dep.empty() ){
+ Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
+ Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
+ d_quantEngine->getOutputChannel().lemma( dep_lemma );
+ }
+ }
+
+ //must register all sub-quantifiers of counterexample lemma, register their lemmas
+ std::vector< Node > quants;
+ TermDb::computeQuantContains( lem, quants );
+ for( unsigned i=0; i<quants.size(); i++ ){
+ if( doCbqi( quants[i] ) ){
+ registerCbqiLemma( quants[i] );
+ }
+ if( options::cbqiNestedQE() ){
+ //record these as counterexample quantifiers
+ QAttributes qa;
+ TermDb::computeQuantAttributes( quants[i], qa );
+ if( qa.d_qid_num!=-1 ){
+ d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
+ d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
+ Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
+ }
+ }
+ }
+ }
+ return true;
+ }else{
+ return false;
+ }
+}
+
void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
d_cbqi_set_quant_inactive = false;
d_incomplete_check = false;
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( doCbqi( q ) ){
- if( !hasAddedCbqiLemma( q ) ){
- d_added_cbqi_lemma.insert( q );
- 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 );
-
- //totality lemmas for EPR
- QuantEPR * qepr = d_quantEngine->getQuantEPR();
- if( qepr!=NULL ){
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- TypeNode tn = q[0][i].getType();
- if( tn.isSort() ){
- if( qepr->isEPR( tn ) ){
- //add totality lemma
- std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
- if( itc!=qepr->d_consts.end() ){
- Assert( !itc->second.empty() );
- Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
- std::vector< Node > disj;
- for( unsigned j=0; j<itc->second.size(); j++ ){
- disj.push_back( ic.eqNode( itc->second[j] ) );
- }
- Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
- Trace("cbqi") << "EPR totality lemma : " << tlem << std::endl;
- d_quantEngine->getOutputChannel().lemma( tlem );
- }else{
- Assert( false );
- }
- }else{
- Assert( !options::cbqiAll() );
- }
- }
- }
- }
-
- //compute dependencies between quantified formulas
- if( options::cbqiLitDepend() || options::cbqiInnermost() ){
- std::vector< Node > ics;
- TermDb::computeVarContains( q, ics );
- d_parent_quant[q].clear();
- d_children_quant[q].clear();
- std::vector< Node > dep;
- for( unsigned i=0; i<ics.size(); i++ ){
- Node qi = ics[i].getAttribute(InstConstantAttribute());
- if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
- d_parent_quant[q].push_back( qi );
- d_children_quant[qi].push_back( q );
- Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
- dep.push_back( qi );
- dep.push_back( qicel );
- }
- }
- if( !dep.empty() ){
- Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
- Trace("cbqi") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
- d_quantEngine->getOutputChannel().lemma( dep_lemma );
- }
- }
- }
+ if( registerCbqiLemma( q ) ){
+ Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl;
//set inactive the quantified formulas whose CE literals are asserted false
}else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
d_active_quant[q] = true;
if( d_quantEngine->getValuation().isDecision( cel ) ){
Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
}else{
+ Trace("cbqi") << "Inactive : " << q << std::endl;
d_quantEngine->getModel()->setQuantifierActive( q, false );
d_cbqi_set_quant_inactive = true;
d_active_quant.erase( q );
+ d_elim_quants.insert( q );
+ Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
+ //process from waitlist
+ while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
+ int index = d_nested_qe_waitlist_proc[q];
+ Assert( index>=0 );
+ Assert( index<(int)d_nested_qe_waitlist[q].size() );
+ Node nq = d_nested_qe_waitlist[q][index];
+ Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
+ Node dqelem = nq.iffNode( nqeqn );
+ Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
+ d_quantEngine->getOutputChannel().lemma( dqelem );
+ d_nested_qe_waitlist_proc[q] = index + 1;
+ }
}
}
}else{
// if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
Node q = it->first;
- process( q, e, ee );
- if( d_quantEngine->inConflict() ){
- break;
+ Trace("cbqi") << "CBQI : Process " << q << " at effort " << ee << std::endl;
+ if( d_nested_qe.find( q )==d_nested_qe.end() ){
+ process( q, e, ee );
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
+ }else{
+ Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
+ Assert( false );
}
}
if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
}
}
+Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( it==visited.end() ){
+ Node ret = n;
+ if( n.getKind()==FORALL ){
+ QAttributes qa;
+ TermDb::computeQuantAttributes( n, qa );
+ if( qa.d_qid_num==-1 ){
+ std::vector< Node > rc;
+ rc.push_back( n[0] );
+ rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
+ Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+ QuantIdNumAttribute ida;
+ avar.setAttribute(ida,d_qid_count);
+ d_qid_count++;
+ std::vector< Node > iplc;
+ iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+ if( n.getNumChildren()==3 ){
+ for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+ iplc.push_back( n[2][i] );
+ }
+ }
+ rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+ ret = NodeManager::currentNM()->mkNode( FORALL, rc );
+ }
+ }else if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = getIdMarkedQuantNode( n[i], visited );
+ childChanged = childChanged || nc!=n[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ visited[n] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+}
+
void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
if( !options::cbqiAll() && !options::cbqiSplx() ){
//take full ownership of the quantified formula
d_quantEngine->setOwner( q, this );
+
+ //mark all nested quantifiers with id
+ if( options::cbqiNestedQE() ){
+ std::map< Node, Node > visited;
+ Node mq = getIdMarkedQuantNode( q[1], visited );
+ if( mq!=q[1] ){
+ //do not do cbqi
+ d_do_cbqi[q] = false;
+ //instead do reduction
+ std::vector< Node > qqc;
+ qqc.push_back( q[0] );
+ qqc.push_back( mq );
+ if( q.getNumChildren()==3 ){
+ qqc.push_back( q[2] );
+ }
+ Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
+ Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
+ Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+ d_quantEngine->getOutputChannel().lemma( mlem );
+ }
+ }
}
}
}
}
+Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
+ // there is a nested quantified formula (forall y. nq[y,x]) such that
+ // q is (forall y. nq[y,t]) for ground terms t,
+ // ceq is (forall y. nq[y,e]) for CE variables e.
+ // we call this function when we know (exists e. ceq[e,k]) is equivalent to quantifier-free formula C[k].
+ // in this case, q is equivalent to the quantifier-free formula C[t].
+ if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
+ d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
+ Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
+ Trace("cbqi-nqe") << " " << ceq << std::endl;
+ Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl;
+ //should not contain quantifiers
+ Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
+ }
+ Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() );
+ //replace inst constants with instantiation
+ Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(),
+ d_quantEngine->getTermDatabase()->d_inst_constants[q].end(),
+ inst_terms.begin(), inst_terms.end() );
+ if( doVts ){
+ //do virtual term substitution
+ ret = Rewriter::rewrite( ret );
+ ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret );
+ }
+ Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
+ Trace("cbqi-nqe") << " " << n << std::endl;
+ Trace("cbqi-nqe") << " " << ret << std::endl;
+ return ret;
+}
+
+Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) {
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( visited.find( n )==visited.end() ){
+ Node ret = n;
+ if( n.getKind()==FORALL ){
+ QAttributes qa;
+ TermDb::computeQuantAttributes( n, qa );
+ if( qa.d_qid_num!=-1 ){
+ //if it has an id, check whether we have done quantifier elimination for this id
+ std::map< int, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
+ if( it!=d_id_to_ce_quant.end() ){
+ Node ceq = it->second;
+ bool doNestedQe = d_elim_quants.contains( ceq );
+ if( doNestedQe ){
+ ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
+ }else{
+ Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
+ Node nr = Rewriter::rewrite( n );
+ Trace("cbqi-nqe") << " " << ceq << std::endl;
+ Trace("cbqi-nqe") << " " << nr << std::endl;
+ int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
+ d_nested_qe_waitlist_size[ceq] = wlsize;
+ if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
+ d_nested_qe_waitlist[ceq][wlsize] = nr;
+ }else{
+ d_nested_qe_waitlist[ceq].push_back( nr );
+ }
+ d_nested_qe_info[nr].d_q = q;
+ d_nested_qe_info[nr].d_inst_terms.clear();
+ d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
+ d_nested_qe_info[nr].d_doVts = doVts;
+ }
+ }
+ }
+ }else if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
+ childChanged = childChanged || nc!=n[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ visited[n] = ret;
+ return ret;
+ }else{
+ return n;
+ }
+}
+
+Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
+ std::map< Node, Node > visited;
+ return doNestedQERec( q, lem, visited, inst_terms, doVts );
+}
+
void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
d_quantEngine->addLemma( lem, false );
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;
- if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
- ret = true;
- }else{
+ bool ret = true;
+ if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
//if has an instantiation pattern, don't do it
if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
- ret = false;
- }else{
+ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+ if( q[2][i].getKind()==INST_PATTERN ){
+ ret = false;
+ }
+ }
+ }
+ if( ret ){
if( options::cbqiAll() ){
ret = true;
}else{
}else if( ncbqiv==0 ){
std::map< Node, bool > visited;
ret = !hasNonCbqiOperator( q[1], visited );
+ }else{
+ ret = false;
}
}
}
}
- Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl;
+ Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
d_do_cbqi[q] = ret;
return ret;
}else{
}
}
-Node InstStrategyCbqi::getNextDecisionRequest(){
- // all counterexample literals that are not asserted
- for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
+ if( proc.find( q )==proc.end() ){
+ proc[q] = true;
+ //first check children
+ std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q );
+ if( itc!=d_children_quant.end() ){
+ for( unsigned j=0; j<itc->second.size(); j++ ){
+ Node d = getNextDecisionRequestProc( itc->second[j], proc );
+ if( !d.isNull() ){
+ return d;
+ }
+ }
+ }
+ //then check self
if( hasAddedCbqiLemma( q ) ){
Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
bool value;
Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
return cel;
}
+ }
+ }
+ return Node::null();
+}
+
+Node InstStrategyCbqi::getNextDecisionRequest(){
+ std::map< Node, bool > proc;
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ Node d = getNextDecisionRequestProc( q, proc );
+ if( !d.isNull() ){
+ return d;
}
}
return Node::null();
//d_added_inst.insert( d_curr_quant );
return true;
}else{
+ //this should never happen for monotonic selection strategies
+ Trace("cbqi-warn") << "Existing instantiation" << std::endl;
+ Assert( !options::cbqiNestedQE() || options::cbqiAll() );
return false;
}
}
void InstStrategyCegqi::presolve() {
if( options::cbqiPreRegInst() ){
for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
+ Trace("cbqi-presolve") << "Presolve " << it->first << std::endl;
it->second->presolve( it->first );
}
}
}
+
class InstStrategyCbqi : public QuantifiersModule {
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
protected:
bool d_cbqi_set_quant_inactive;
bool d_incomplete_check;
/** whether we have added cbqi lemma */
NodeSet d_added_cbqi_lemma;
+ /** whether we have added cbqi lemma */
+ NodeSet d_elim_quants;
/** parent guards */
std::map< Node, std::vector< Node > > d_parent_quant;
std::map< Node, std::vector< Node > > d_children_quant;
/** whether to do cbqi for this quantified formula */
std::map< Node, bool > d_do_cbqi;
/** register ce lemma */
+ bool registerCbqiLemma( Node q );
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 */
int hasNonCbqiVariable( Node q );
bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+ /** get next decision request with dependency checking */
+ Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );
/** process functions */
virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
virtual void process( Node q, Theory::Effort effort, int e ) = 0;
+protected:
+ //for identification
+ uint64_t d_qid_count;
+ //nested qe map
+ std::map< Node, Node > d_nested_qe;
+ //mark ids on quantifiers
+ Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
+ // id to ce quant
+ std::map< int, Node > d_id_to_ce_quant;
+ std::map< Node, int > d_ce_quant_to_id;
+ //do nested quantifier elimination recursive
+ Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
+ Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
+ //elimination information (for delayed elimination)
+ class NestedQEInfo {
+ public:
+ NestedQEInfo(){}
+ ~NestedQEInfo(){}
+ Node d_q;
+ std::vector< Node > d_inst_terms;
+ bool d_doVts;
+ };
+ std::map< Node, NestedQEInfo > d_nested_qe_info;
+ NodeIntMap d_nested_qe_waitlist_size;
+ NodeIntMap d_nested_qe_waitlist_proc;
+ std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
+public:
+ //do nested quantifier elimination
+ Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
public:
InstStrategyCbqi( QuantifiersEngine * qe );
~InstStrategyCbqi() throw();
void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) {
std::map< Node, bool > visited;
- computeVarContains2( n, varContains, visited );
+ computeVarContains2( n, INST_CONSTANT, varContains, visited );
}
-void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
+void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) {
+ std::map< Node, bool > visited;
+ computeVarContains2( n, FORALL, quantContains, visited );
+}
+
+
+void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( n.getKind()==INST_CONSTANT ){
+ if( n.getKind()==k ){
if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){
varContains.push_back( n );
}
}else{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- computeVarContains2( n[i], varContains, visited );
+ computeVarContains2( n[i], k, varContains, visited );
}
}
}
qa.d_quant_elim_partial = true;
//don't set owner, should happen naturally
}
+ if( avar.hasAttribute(QuantIdNumAttribute()) ){
+ qa.d_qid_num = avar.getAttribute(QuantIdNumAttribute());
+ Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num << " : " << q << std::endl;
+ }
if( avar.getKind()==REWRITE_RULE ){
Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
Assert( i==0 );
}
}
+int TermDb::getQAttrQuantIdNum( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return -1;
+ }else{
+ return it->second.d_qid_num;
+ }
+}
+
TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
struct QuantElimPartialAttributeId {};
typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
+/** Attribute for id number */
+struct QuantIdNumAttributeId {};
+typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
+
+
class QuantifiersEngine;
namespace inst{
class QAttributes{
public:
QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
- d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
+ d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false), d_qid_num(-1){}
~QAttributes(){}
bool d_hasPattern;
Node d_rr;
bool d_quant_elim;
bool d_quant_elim_partial;
Node d_ipl;
+ int d_qid_num;
bool isRewriteRule() { return !d_rr.isNull(); }
bool isFunDef() { return !d_fundef_f.isNull(); }
};
/** map from universal quantifiers to the list of variables */
std::map< Node, std::vector< Node > > d_vars;
std::map< Node, std::map< Node, unsigned > > d_var_num;
- /** map from universal quantifiers to the list of instantiation constants */
- std::map< Node, std::vector< Node > > d_inst_constants;
/** map from universal quantifiers to their inst constant body */
std::map< Node, Node > d_inst_const_body;
/** map from universal quantifiers to their counterexample literals */
/** make instantiation constants for */
void makeInstantiationConstantsFor( Node q );
public:
+ /** map from universal quantifiers to the list of instantiation constants */
+ std::map< Node, std::vector< Node > > d_inst_constants;
/** get variable number */
unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
/** get the i^th instantiation constant of q */
//for triggers
private:
/** helper function for compute var contains */
- static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
+ static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
/** triggers for each operator */
std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
/** helper for is instance of */
static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
/** get var contains for node n */
static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+ /** compute quant contains */
+ static void computeQuantContains( Node n, std::vector< Node >& quantContains );
/** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
static int isInstanceOf( Node n1, Node n2 );
/** filter all nodes that have instances */
bool isQAttrQuantElim( Node q );
/** is quant elim partial */
bool isQAttrQuantElimPartial( Node q );
+ /** get quant id num */
+ int getQAttrQuantIdNum( Node q );
/** compute quantifier attributes */
static void computeQuantAttributes( Node q, QAttributes& qa );
};/* class TermDb */
d_rel_dom = NULL;
d_builder = NULL;
- d_trackInstLemmas = options::proof() && options::trackInstLemmas();
+ d_trackInstLemmas = options::cbqiNestedQE() || ( options::proof() && options::trackInstLemmas() );
d_total_inst_count_debug = 0;
//allow theory combination to go first, once initially
}
bool QuantifiersEngine::reduceQuantifier( Node q ) {
+ //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
BoolMap::const_iterator it = d_quants_red.find( q );
if( it==d_quants_red.end() ){
Node lem;
//register the quantifier, assert it to each module
if( registerQuantifier( f ) ){
d_model->assertQuantifier( f );
- for( int i=0; i<(int)d_modules.size(); i++ ){
+ for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->assertNode( f );
}
addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
Assert( d_term_db->d_vars[q].size()==terms.size() );
Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution
Node orig_body = body;
+ if( options::cbqiNestedQE() && d_i_cbqi ){
+ body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
+ }
body = quantifiers::QuantifiersRewriter::preprocess( body, true );
Trace("inst-debug") << "...preprocess to " << body << std::endl;
}
}
+void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
+ if( options::incrementalSolving() ){
+ std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
+ if( it!=d_c_inst_match_trie.end() ){
+ std::vector< Node > active_lemmas;
+ it->second->getInstantiations( insts, it->first, this, false, active_lemmas );
+ }
+ }else{
+ std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.find( q );
+ if( it!=d_inst_match_trie.end() ){
+ std::vector< Node > active_lemmas;
+ it->second.getInstantiations( insts, it->first, this, false, active_lemmas );
+ }
+ }
+}
+
+Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
+ std::vector< Node > insts;
+ getInstantiations( q, insts );
+ if( insts.empty() ){
+ return NodeManager::currentNM()->mkConst(true);
+ }else{
+ Node ret;
+ if( insts.size()==1 ){
+ ret = insts[0];
+ }else{
+ ret = NodeManager::currentNM()->mkNode( kind::AND, insts );
+ }
+ //have to remove q, TODO: avoid this in a better way
+ TNode tq = q;
+ TNode tt = d_term_db->d_true;
+ ret = ret.substitute( tq, tt );
+ return ret;
+ }
+}
+
QuantifiersEngine::Statistics::Statistics()
: d_time("theory::QuantifiersEngine::time"),
d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
class QuantifiersEngine {
friend class quantifiers::InstantiationEngine;
+ friend class quantifiers::InstStrategyCbqi;
friend class quantifiers::InstStrategyCegqi;
friend class quantifiers::ModelEngine;
friend class quantifiers::RewriteEngine;
/** print solution for synthesis conjectures */
void printSynthSolution( std::ostream& out );
/** get instantiations */
+ void getInstantiations( Node q, std::vector< Node >& insts );
void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+ /** get instantiated conjunction */
+ Node getInstantiatedConjunction( Node q );
/** get unsat core lemmas */
bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
}
}
+Node TheoryEngine::getInstantiatedConjunction( Node q ) {
+ if( d_quantEngine ){
+ return d_quantEngine->getInstantiatedConjunction( q );
+ }else{
+ Assert( false );
+ return Node::null();
+ }
+}
+
static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
* Get instantiations
*/
void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+
+ /**
+ * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q.
+ * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q
+ */
+ Node getInstantiatedConjunction( Node q );
/**
* Forwards an entailment check according to the given theoryOfMode.
projects / cvc5.git / commitdiff