theory/quantifiers/cegqi/ceg_dt_instantiator.h \
theory/quantifiers/cegqi/ceg_epr_instantiator.cpp \
theory/quantifiers/cegqi/ceg_epr_instantiator.h \
- theory/quantifiers/cegqi/inst_strategy_cbqi.cpp \
- theory/quantifiers/cegqi/inst_strategy_cbqi.h \
+ theory/quantifiers/cegqi/inst_strategy_cegqi.cpp \
+ theory/quantifiers/cegqi/inst_strategy_cegqi.h \
theory/quantifiers/conjecture_generator.cpp \
theory/quantifiers/conjecture_generator.h \
theory/quantifiers/dynamic_rewrite.cpp \
+++ /dev/null
-/********************* */
-/*! \file inst_strategy_cbqi.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of counterexample-guided quantifier instantiation strategies
- **/
-#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
-
-#include "expr/node_algorithm.h"
-#include "options/quantifiers_options.h"
-#include "smt/term_formula_removal.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_epr.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-bool CegqiOutputInstStrategy::doAddInstantiation(std::vector<Node>& subs)
-{
- return d_out->doAddInstantiation(subs);
-}
-
-bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n)
-{
- return d_out->isEligibleForInstantiation(n);
-}
-
-bool CegqiOutputInstStrategy::addLemma(Node lem)
-{
- return d_out->addLemma(lem);
-}
-
-InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
- : QuantifiersModule(qe),
- d_cbqi_set_quant_inactive(false),
- d_incomplete_check(false),
- d_added_cbqi_lemma(qe->getUserContext()),
- d_elim_quants(qe->getSatContext()),
- d_out(new CegqiOutputInstStrategy(this)),
- d_nested_qe_waitlist_size(qe->getUserContext()),
- d_nested_qe_waitlist_proc(qe->getUserContext())
-//, d_added_inst( qe->getUserContext() )
-{
- d_qid_count = 0;
- d_small_const =
- NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
- d_check_vts_lemma_lc = false;
-}
-
-InstStrategyCegqi::~InstStrategyCegqi() {}
-
-bool InstStrategyCegqi::needsCheck(Theory::Effort e)
-{
- return e>=Theory::EFFORT_LAST_CALL;
-}
-
-QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
-{
- for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
- if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
- return QEFFORT_STANDARD;
- }
- }
- return QEFFORT_NONE;
-}
-
-bool InstStrategyCegqi::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->getTermUtil()->getCounterexampleLiteral( q );
- Node ceBody = d_quantEngine->getTermUtil()->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->getTermUtil()->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;
- TermUtil::computeInstConstContains(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 );
- Assert( hasAddedCbqiLemma( qi ) );
- Node qicel = d_quantEngine->getTermUtil()->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;
- TermUtil::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;
- QuantAttributes::computeQuantAttributes( quants[i], qa );
- if( !qa.d_qid_num.isNull() ){
- 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;
- }
- }
- }
- }
- // The decision strategy for this quantified formula ensures that its
- // counterexample literal is decided on first. It is user-context dependent.
- std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds =
- d_dstrat.find(q);
- DecisionStrategy* dlds = nullptr;
- if (itds == d_dstrat.end())
- {
- d_dstrat[q].reset(
- new DecisionStrategySingleton("CexLiteral",
- ceLit,
- d_quantEngine->getSatContext(),
- d_quantEngine->getValuation()));
- dlds = d_dstrat[q].get();
- }
- else
- {
- dlds = itds->second.get();
- }
- // it is appended to the list of strategies
- d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy(
- DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
- return true;
- }else{
- return false;
- }
-}
-
-void InstStrategyCegqi::reset_round(Theory::Effort effort)
-{
- d_cbqi_set_quant_inactive = false;
- d_incomplete_check = false;
- d_active_quant.clear();
- //check if any cbqi lemma has not been added yet
- for( unsigned 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( doCbqi( q ) ){
- Assert( hasAddedCbqiLemma( q ) );
- if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
- d_active_quant[q] = true;
- Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
- Node cel = d_quantEngine->getTermUtil()->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") << "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.eqNode( 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{
- Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
- }
- }
- }
- }
-
- //refinement: only consider innermost active quantified formulas
- if( options::cbqiInnermost() ){
- if( !d_children_quant.empty() && !d_active_quant.empty() ){
- Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
- std::vector< Node > ninner;
- for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
- std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
- if( itc!=d_children_quant.end() ){
- for( unsigned j=0; j<itc->second.size(); j++ ){
- if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
- Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
- ninner.push_back( it->first );
- break;
- }
- }
- }
- }
- Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
- for( unsigned i=0; i<ninner.size(); i++ ){
- Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() );
- d_active_quant.erase( ninner[i] );
- }
- Assert( !d_active_quant.empty() );
- Trace("cbqi-debug") << "...done removing." << std::endl;
- }
- }
- d_check_vts_lemma_lc = false;
-}
-
-void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
-{
- if (quant_e == QEFFORT_STANDARD)
- {
- Assert( !d_quantEngine->inConflict() );
- double clSet = 0;
- if( Trace.isOn("cbqi-engine") ){
- clSet = double(clock())/double(CLOCKS_PER_SEC);
- Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
- }
- unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
- for( int ee=0; ee<=1; ee++ ){
- //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
- // 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;
- Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " 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 ){
- break;
- }
- }
- if( Trace.isOn("cbqi-engine") ){
- if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
- Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
- }
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
- }
- }
-}
-
-bool InstStrategyCegqi::checkComplete()
-{
- if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
- return false;
- }else{
- return true;
- }
-}
-
-bool InstStrategyCegqi::checkCompleteFor(Node q)
-{
- std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
- if( it!=d_do_cbqi.end() ){
- return it->second != CEG_UNHANDLED;
- }else{
- return false;
- }
-}
-
-Node InstStrategyCegqi::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;
- QuantAttributes::computeQuantAttributes( n, qa );
- if( qa.d_qid_num.isNull() ){
- 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 InstStrategyCegqi::checkOwnership(Node q)
-{
- if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
- if (d_do_cbqi[q] == CEG_HANDLED)
- {
- //take full ownership of the quantified formula
- d_quantEngine->setOwner( q, this );
- }
- }
-}
-
-void InstStrategyCegqi::preRegisterQuantifier(Node q)
-{
- // mark all nested quantifiers with id
- if (options::cbqiNestedQE())
- {
- if( d_quantEngine->getOwner(q)==this )
- {
- std::map<Node, Node> visited;
- Node mq = getIdMarkedQuantNode(q[1], visited);
- if (mq != q[1])
- {
- // do not do cbqi, we are reducing this quantified formula to a marked
- // one
- d_do_cbqi[q] = CEG_UNHANDLED;
- // 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->addLemma(mlem);
- }
- }
- }
- if( doCbqi( q ) ){
- // get the instantiator
- if (options::cbqiPreRegInst())
- {
- getInstantiator(q);
- }
- // register the cbqi lemma
- if( registerCbqiLemma( q ) ){
- Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
- }
- }
-}
-
-Node InstStrategyCegqi::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 (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
- // 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->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() );
- //replace inst constants with instantiation
- Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
- d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
- inst_terms.begin(), inst_terms.end() );
- if( doVts ){
- //do virtual term substitution
- ret = Rewriter::rewrite( ret );
- ret = d_quantEngine->getTermUtil()->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 InstStrategyCegqi::doNestedQERec(Node q,
- Node n,
- std::map<Node, Node>& visited,
- std::vector<Node>& inst_terms,
- bool doVts)
-{
- if( visited.find( n )==visited.end() ){
- Node ret = n;
- if( n.getKind()==FORALL ){
- QAttributes qa;
- QuantAttributes::computeQuantAttributes( n, qa );
- if( !qa.d_qid_num.isNull() ){
- //if it has an id, check whether we have done quantifier elimination for this id
- std::map< Node, 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;
- //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
- Assert( !options::cbqiInnermost() );
- }
- }
- }
- }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 InstStrategyCegqi::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 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;
- TermUtil* tutil = d_quantEngine->getTermUtil();
- for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics;
- i++)
- {
- ce_vars.push_back(tutil->getInstantiationConstant(q, i));
- }
- std::vector<Node> lems;
- lems.push_back(lem);
- CegInstantiator* cinst = getInstantiator(q);
- cinst->registerCounterexampleLemma(lems, ce_vars);
- for (unsigned i = 0, size = lems.size(); i < size; i++)
- {
- Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
- << std::endl;
- d_quantEngine->addLemma(lems[i], false);
- }
-}
-
-bool InstStrategyCegqi::doCbqi(Node q)
-{
- std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
- if( it==d_do_cbqi.end() ){
- CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
- Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
- d_do_cbqi[q] = ret;
- return ret != CEG_UNHANDLED;
- }
- return it->second != CEG_UNHANDLED;
-}
-
-void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
- if( e==0 ){
- CegInstantiator * cinst = getInstantiator( q );
- Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
- d_curr_quant = q;
- if( !cinst->check() ){
- d_incomplete_check = true;
- d_check_vts_lemma_lc = true;
- }
- d_curr_quant = Node::null();
- }else if( e==1 ){
- //minimize the free delta heuristically on demand
- if( d_check_vts_lemma_lc ){
- Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
- 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->getTermUtil()->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->getTermUtil()->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 );
- }
- }
- }
-}
-
-bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
- Assert( !d_curr_quant.isNull() );
- //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
- if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
- d_cbqi_set_quant_inactive = true;
- d_incomplete_check = true;
- d_quantEngine->getInstantiate()->recordInstantiation(
- d_curr_quant, subs, false, false);
- return true;
- }else{
- //check if we need virtual term substitution (if used delta or infinity)
- bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
- if (d_quantEngine->getInstantiate()->addInstantiation(
- d_curr_quant, subs, false, false, used_vts))
- {
- ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
- //d_added_inst.insert( d_curr_quant );
- return true;
- }else{
- //this should never happen for monotonic selection strategies
- Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
- return false;
- }
- }
-}
-
-bool InstStrategyCegqi::addLemma( Node lem ) {
- return d_quantEngine->addLemma( lem );
-}
-
-bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
- if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
- if( n.getAttribute(VirtualTermSkolemAttribute()) ){
- // virtual terms are allowed
- return true;
- }else{
- TypeNode tn = n.getType();
- if( tn.isSort() ){
- QuantEPR * qepr = d_quantEngine->getQuantEPR();
- if( qepr!=NULL ){
- //legal if in the finite set of constants of type tn
- if( qepr->isEPRConstant( tn, n ) ){
- return true;
- }
- }
- }
- //only legal if current quantified formula contains n
- return expr::hasSubterm(d_curr_quant, n);
- }
- }else{
- return true;
- }
-}
-
-CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
- std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
- d_cinst.find(q);
- if( it==d_cinst.end() ){
- d_cinst[q].reset(
- new CegInstantiator(d_quantEngine, d_out.get(), true, true));
- return d_cinst[q].get();
- }
- return it->second.get();
-}
-
-void InstStrategyCegqi::presolve() {
- if (!options::cbqiPreRegInst())
- {
- return;
- }
- for (std::pair<const Node, std::unique_ptr<CegInstantiator>>& ci : d_cinst)
- {
- Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl;
- ci.second->presolve(ci.first);
- }
-}
-
+++ /dev/null
-/********************* */
-/*! \file inst_strategy_cbqi.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. 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__INST_STRATEGY_CBQI_H
-#define __CVC4__INST_STRATEGY_CBQI_H
-
-#include "theory/decision_manager.h"
-#include "theory/quantifiers/cegqi/ceg_instantiator.h"
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstStrategyCegqi;
-
-/**
- * An output channel class, used by instantiator objects below. The methods
- * of this class call the corresponding functions of InstStrategyCegqi below.
- */
-class CegqiOutputInstStrategy : public CegqiOutput
-{
- public:
- CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {}
- /** The module whose functions we call. */
- InstStrategyCegqi* d_out;
- /** add instantiation */
- bool doAddInstantiation(std::vector<Node>& subs) override;
- /** is eligible for instantiation */
- bool isEligibleForInstantiation(Node n) override;
- /** add lemma */
- bool addLemma(Node lem) override;
-};
-
-/**
- * Counterexample-guided quantifier instantiation module.
- *
- * This class manages counterexample-guided instantiation strategies for all
- * asserted quantified formulas.
- */
-class InstStrategyCegqi : public QuantifiersModule
-{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
-
- public:
- InstStrategyCegqi(QuantifiersEngine* qe);
- ~InstStrategyCegqi();
-
- /** whether to do counterexample-guided instantiation for quantifier q */
- bool doCbqi(Node q);
- /** needs check at effort */
- bool needsCheck(Theory::Effort e) override;
- /** needs model at effort */
- QEffort needsModel(Theory::Effort e) override;
- /** reset round */
- void reset_round(Theory::Effort e) override;
- /** check */
- void check(Theory::Effort e, QEffort quant_e) override;
- /** check complete */
- bool checkComplete() override;
- /** check complete for quantified formula */
- bool checkCompleteFor(Node q) override;
- /** check ownership */
- void checkOwnership(Node q) override;
- /** identify */
- std::string identify() const override { return std::string("Cegqi"); }
- /** get instantiator for quantifier */
- CegInstantiator* getInstantiator(Node q);
- /** pre-register quantifier */
- void preRegisterQuantifier(Node q) override;
- // presolve
- void presolve() override;
- /** Do nested quantifier elimination. */
- Node doNestedQE(Node q, std::vector<Node>& inst_terms, Node lem, bool doVts);
-
- //------------------- interface for CegqiOutputInstStrategy
- /** Instantiate the current quantified formula forall x. Q with x -> subs. */
- bool doAddInstantiation(std::vector<Node>& subs);
- /**
- * Are we allowed to instantiate the current quantified formula with n? This
- * includes restrictions such as if n is a variable, it must occur free in
- * the current quantified formula.
- */
- bool isEligibleForInstantiation(Node n);
- /** Add lemma lem via the output channel of this class. */
- bool addLemma(Node lem);
- //------------------- end interface for CegqiOutputInstStrategy
-
- protected:
- /** set quantified formula inactive
- *
- * This flag is set to true during a full effort check if at least one
- * quantified formula is set "inactive", that is, its negation is
- * unsatisfiable in the current context.
- */
- bool d_cbqi_set_quant_inactive;
- /** incomplete check
- *
- * This is set to true during a full effort check if this strategy could
- * not find an instantiation for at least one asserted quantified formula.
- */
- 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;
- std::map< Node, bool > d_active_quant;
- /** Whether cegqi handles each quantified formula. */
- std::map<Node, CegHandledStatus> d_do_cbqi;
- /**
- * An output channel used by instantiators for communicating with this
- * class.
- */
- std::unique_ptr<CegqiOutputInstStrategy> d_out;
- /**
- * The instantiator for each quantified formula q registered to this class.
- * This object is responsible for finding instantiatons for q.
- */
- std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
- /**
- * The decision strategy for each quantified formula q registered to this
- * class.
- */
- std::map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
- /** the current quantified formula we are processing */
- Node d_curr_quant;
- //---------------------- for vts delta minimization
- /**
- * Whether we will use vts delta minimization. If this flag is true, we
- * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c
- * is a small (< 1) constant. This heuristic is used in strategies where
- * vts delta cannot be fully eliminated from assertions (for example, when
- * using nested quantifiers and a non-innermost instantiation strategy).
- * The same strategy applies for vts infinity, which we add lemmas of the
- * form inf > (1/c)^1, inf > (1/c)^2, ....
- */
- bool d_check_vts_lemma_lc;
- /** a small constant, used as a coefficient above */
- Node d_small_const;
- //---------------------- end for vts delta minimization
- /** register ce lemma */
- bool registerCbqiLemma( Node q );
- /** register counterexample lemma
- *
- * This is called when we have constructed lem, the negation of the body of
- * quantified formula q, skolemized with the instantiation constants of q.
- * This function is used for setting up the proper information in the
- * instantiator for q.
- */
- 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(); }
- /** process functions */
- void process(Node q, Theory::Effort effort, int e);
-
- //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< Node, Node > d_id_to_ce_quant;
- std::map< Node, Node > 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() : d_doVts(false){}
- ~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;
-
-};
-
-
-}
-}
-}
-
-#endif
--- /dev/null
+/********************* */
+/*! \file inst_strategy_cegqi.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of counterexample-guided quantifier instantiation strategies
+ **/
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+
+#include "expr/node_algorithm.h"
+#include "options/quantifiers_options.h"
+#include "smt/term_formula_removal.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/theory_arith_private.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_epr.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+bool CegqiOutputInstStrategy::doAddInstantiation(std::vector<Node>& subs)
+{
+ return d_out->doAddInstantiation(subs);
+}
+
+bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n)
+{
+ return d_out->isEligibleForInstantiation(n);
+}
+
+bool CegqiOutputInstStrategy::addLemma(Node lem)
+{
+ return d_out->addLemma(lem);
+}
+
+InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
+ : QuantifiersModule(qe),
+ d_cbqi_set_quant_inactive(false),
+ d_incomplete_check(false),
+ d_added_cbqi_lemma(qe->getUserContext()),
+ d_elim_quants(qe->getSatContext()),
+ d_out(new CegqiOutputInstStrategy(this)),
+ d_nested_qe_waitlist_size(qe->getUserContext()),
+ d_nested_qe_waitlist_proc(qe->getUserContext())
+//, d_added_inst( qe->getUserContext() )
+{
+ d_qid_count = 0;
+ d_small_const =
+ NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
+ d_check_vts_lemma_lc = false;
+}
+
+InstStrategyCegqi::~InstStrategyCegqi() {}
+
+bool InstStrategyCegqi::needsCheck(Theory::Effort e)
+{
+ return e>=Theory::EFFORT_LAST_CALL;
+}
+
+QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
+{
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ return QEFFORT_STANDARD;
+ }
+ }
+ return QEFFORT_NONE;
+}
+
+bool InstStrategyCegqi::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->getTermUtil()->getCounterexampleLiteral( q );
+ Node ceBody = d_quantEngine->getTermUtil()->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->getTermUtil()->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;
+ TermUtil::computeInstConstContains(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 );
+ Assert( hasAddedCbqiLemma( qi ) );
+ Node qicel = d_quantEngine->getTermUtil()->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;
+ TermUtil::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;
+ QuantAttributes::computeQuantAttributes( quants[i], qa );
+ if( !qa.d_qid_num.isNull() ){
+ 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;
+ }
+ }
+ }
+ }
+ // The decision strategy for this quantified formula ensures that its
+ // counterexample literal is decided on first. It is user-context dependent.
+ std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds =
+ d_dstrat.find(q);
+ DecisionStrategy* dlds = nullptr;
+ if (itds == d_dstrat.end())
+ {
+ d_dstrat[q].reset(
+ new DecisionStrategySingleton("CexLiteral",
+ ceLit,
+ d_quantEngine->getSatContext(),
+ d_quantEngine->getValuation()));
+ dlds = d_dstrat[q].get();
+ }
+ else
+ {
+ dlds = itds->second.get();
+ }
+ // it is appended to the list of strategies
+ d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy(
+ DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
+ return true;
+ }else{
+ return false;
+ }
+}
+
+void InstStrategyCegqi::reset_round(Theory::Effort effort)
+{
+ d_cbqi_set_quant_inactive = false;
+ d_incomplete_check = false;
+ d_active_quant.clear();
+ //check if any cbqi lemma has not been added yet
+ for( unsigned 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( doCbqi( q ) ){
+ Assert( hasAddedCbqiLemma( q ) );
+ if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ d_active_quant[q] = true;
+ Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
+ Node cel = d_quantEngine->getTermUtil()->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") << "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.eqNode( 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{
+ Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
+ }
+ }
+ }
+ }
+
+ //refinement: only consider innermost active quantified formulas
+ if( options::cbqiInnermost() ){
+ if( !d_children_quant.empty() && !d_active_quant.empty() ){
+ Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
+ std::vector< Node > ninner;
+ for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
+ std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
+ if( itc!=d_children_quant.end() ){
+ for( unsigned j=0; j<itc->second.size(); j++ ){
+ if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
+ Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
+ ninner.push_back( it->first );
+ break;
+ }
+ }
+ }
+ }
+ Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
+ for( unsigned i=0; i<ninner.size(); i++ ){
+ Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() );
+ d_active_quant.erase( ninner[i] );
+ }
+ Assert( !d_active_quant.empty() );
+ Trace("cbqi-debug") << "...done removing." << std::endl;
+ }
+ }
+ d_check_vts_lemma_lc = false;
+}
+
+void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
+{
+ if (quant_e == QEFFORT_STANDARD)
+ {
+ Assert( !d_quantEngine->inConflict() );
+ double clSet = 0;
+ if( Trace.isOn("cbqi-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
+ }
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ for( int ee=0; ee<=1; ee++ ){
+ //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ // 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;
+ Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " 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 ){
+ break;
+ }
+ }
+ if( Trace.isOn("cbqi-engine") ){
+ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+ Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ }
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
+ }
+ }
+}
+
+bool InstStrategyCegqi::checkComplete()
+{
+ if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
+ return false;
+ }else{
+ return true;
+ }
+}
+
+bool InstStrategyCegqi::checkCompleteFor(Node q)
+{
+ std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
+ if( it!=d_do_cbqi.end() ){
+ return it->second != CEG_UNHANDLED;
+ }else{
+ return false;
+ }
+}
+
+Node InstStrategyCegqi::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;
+ QuantAttributes::computeQuantAttributes( n, qa );
+ if( qa.d_qid_num.isNull() ){
+ 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 InstStrategyCegqi::checkOwnership(Node q)
+{
+ if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
+ if (d_do_cbqi[q] == CEG_HANDLED)
+ {
+ //take full ownership of the quantified formula
+ d_quantEngine->setOwner( q, this );
+ }
+ }
+}
+
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
+{
+ // mark all nested quantifiers with id
+ if (options::cbqiNestedQE())
+ {
+ if( d_quantEngine->getOwner(q)==this )
+ {
+ std::map<Node, Node> visited;
+ Node mq = getIdMarkedQuantNode(q[1], visited);
+ if (mq != q[1])
+ {
+ // do not do cbqi, we are reducing this quantified formula to a marked
+ // one
+ d_do_cbqi[q] = CEG_UNHANDLED;
+ // 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->addLemma(mlem);
+ }
+ }
+ }
+ if( doCbqi( q ) ){
+ // get the instantiator
+ if (options::cbqiPreRegInst())
+ {
+ getInstantiator(q);
+ }
+ // register the cbqi lemma
+ if( registerCbqiLemma( q ) ){
+ Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+ }
+ }
+}
+
+Node InstStrategyCegqi::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 (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
+ // 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->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() );
+ //replace inst constants with instantiation
+ Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
+ d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
+ inst_terms.begin(), inst_terms.end() );
+ if( doVts ){
+ //do virtual term substitution
+ ret = Rewriter::rewrite( ret );
+ ret = d_quantEngine->getTermUtil()->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 InstStrategyCegqi::doNestedQERec(Node q,
+ Node n,
+ std::map<Node, Node>& visited,
+ std::vector<Node>& inst_terms,
+ bool doVts)
+{
+ if( visited.find( n )==visited.end() ){
+ Node ret = n;
+ if( n.getKind()==FORALL ){
+ QAttributes qa;
+ QuantAttributes::computeQuantAttributes( n, qa );
+ if( !qa.d_qid_num.isNull() ){
+ //if it has an id, check whether we have done quantifier elimination for this id
+ std::map< Node, 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;
+ //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
+ Assert( !options::cbqiInnermost() );
+ }
+ }
+ }
+ }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 InstStrategyCegqi::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 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;
+ TermUtil* tutil = d_quantEngine->getTermUtil();
+ for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics;
+ i++)
+ {
+ ce_vars.push_back(tutil->getInstantiationConstant(q, i));
+ }
+ std::vector<Node> lems;
+ lems.push_back(lem);
+ CegInstantiator* cinst = getInstantiator(q);
+ cinst->registerCounterexampleLemma(lems, ce_vars);
+ for (unsigned i = 0, size = lems.size(); i < size; i++)
+ {
+ Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
+ << std::endl;
+ d_quantEngine->addLemma(lems[i], false);
+ }
+}
+
+bool InstStrategyCegqi::doCbqi(Node q)
+{
+ std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
+ if( it==d_do_cbqi.end() ){
+ CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
+ Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
+ d_do_cbqi[q] = ret;
+ return ret != CEG_UNHANDLED;
+ }
+ return it->second != CEG_UNHANDLED;
+}
+
+void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
+ if( e==0 ){
+ CegInstantiator * cinst = getInstantiator( q );
+ Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
+ d_curr_quant = q;
+ if( !cinst->check() ){
+ d_incomplete_check = true;
+ d_check_vts_lemma_lc = true;
+ }
+ d_curr_quant = Node::null();
+ }else if( e==1 ){
+ //minimize the free delta heuristically on demand
+ if( d_check_vts_lemma_lc ){
+ Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
+ 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->getTermUtil()->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->getTermUtil()->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 );
+ }
+ }
+ }
+}
+
+bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
+ Assert( !d_curr_quant.isNull() );
+ //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
+ if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
+ d_cbqi_set_quant_inactive = true;
+ d_incomplete_check = true;
+ d_quantEngine->getInstantiate()->recordInstantiation(
+ d_curr_quant, subs, false, false);
+ return true;
+ }else{
+ //check if we need virtual term substitution (if used delta or infinity)
+ bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
+ if (d_quantEngine->getInstantiate()->addInstantiation(
+ d_curr_quant, subs, false, false, used_vts))
+ {
+ ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
+ //d_added_inst.insert( d_curr_quant );
+ return true;
+ }else{
+ //this should never happen for monotonic selection strategies
+ Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
+ return false;
+ }
+ }
+}
+
+bool InstStrategyCegqi::addLemma( Node lem ) {
+ return d_quantEngine->addLemma( lem );
+}
+
+bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
+ if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
+ if( n.getAttribute(VirtualTermSkolemAttribute()) ){
+ // virtual terms are allowed
+ return true;
+ }else{
+ TypeNode tn = n.getType();
+ if( tn.isSort() ){
+ QuantEPR * qepr = d_quantEngine->getQuantEPR();
+ if( qepr!=NULL ){
+ //legal if in the finite set of constants of type tn
+ if( qepr->isEPRConstant( tn, n ) ){
+ return true;
+ }
+ }
+ }
+ //only legal if current quantified formula contains n
+ return expr::hasSubterm(d_curr_quant, n);
+ }
+ }else{
+ return true;
+ }
+}
+
+CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
+ std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
+ d_cinst.find(q);
+ if( it==d_cinst.end() ){
+ d_cinst[q].reset(
+ new CegInstantiator(d_quantEngine, d_out.get(), true, true));
+ return d_cinst[q].get();
+ }
+ return it->second.get();
+}
+
+void InstStrategyCegqi::presolve() {
+ if (!options::cbqiPreRegInst())
+ {
+ return;
+ }
+ for (std::pair<const Node, std::unique_ptr<CegInstantiator>>& ci : d_cinst)
+ {
+ Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl;
+ ci.second->presolve(ci.first);
+ }
+}
+
--- /dev/null
+/********************* */
+/*! \file inst_strategy_cegqi.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. 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__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+
+#include "theory/decision_manager.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class InstStrategyCegqi;
+
+/**
+ * An output channel class, used by instantiator objects below. The methods
+ * of this class call the corresponding functions of InstStrategyCegqi below.
+ */
+class CegqiOutputInstStrategy : public CegqiOutput
+{
+ public:
+ CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {}
+ /** The module whose functions we call. */
+ InstStrategyCegqi* d_out;
+ /** add instantiation */
+ bool doAddInstantiation(std::vector<Node>& subs) override;
+ /** is eligible for instantiation */
+ bool isEligibleForInstantiation(Node n) override;
+ /** add lemma */
+ bool addLemma(Node lem) override;
+};
+
+/**
+ * Counterexample-guided quantifier instantiation module.
+ *
+ * This class manages counterexample-guided instantiation strategies for all
+ * asserted quantified formulas.
+ */
+class InstStrategyCegqi : public QuantifiersModule
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
+
+ public:
+ InstStrategyCegqi(QuantifiersEngine* qe);
+ ~InstStrategyCegqi();
+
+ /** whether to do counterexample-guided instantiation for quantifier q */
+ bool doCbqi(Node q);
+ /** needs check at effort */
+ bool needsCheck(Theory::Effort e) override;
+ /** needs model at effort */
+ QEffort needsModel(Theory::Effort e) override;
+ /** reset round */
+ void reset_round(Theory::Effort e) override;
+ /** check */
+ void check(Theory::Effort e, QEffort quant_e) override;
+ /** check complete */
+ bool checkComplete() override;
+ /** check complete for quantified formula */
+ bool checkCompleteFor(Node q) override;
+ /** check ownership */
+ void checkOwnership(Node q) override;
+ /** identify */
+ std::string identify() const override { return std::string("Cegqi"); }
+ /** get instantiator for quantifier */
+ CegInstantiator* getInstantiator(Node q);
+ /** pre-register quantifier */
+ void preRegisterQuantifier(Node q) override;
+ // presolve
+ void presolve() override;
+ /** Do nested quantifier elimination. */
+ Node doNestedQE(Node q, std::vector<Node>& inst_terms, Node lem, bool doVts);
+
+ //------------------- interface for CegqiOutputInstStrategy
+ /** Instantiate the current quantified formula forall x. Q with x -> subs. */
+ bool doAddInstantiation(std::vector<Node>& subs);
+ /**
+ * Are we allowed to instantiate the current quantified formula with n? This
+ * includes restrictions such as if n is a variable, it must occur free in
+ * the current quantified formula.
+ */
+ bool isEligibleForInstantiation(Node n);
+ /** Add lemma lem via the output channel of this class. */
+ bool addLemma(Node lem);
+ //------------------- end interface for CegqiOutputInstStrategy
+
+ protected:
+ /** set quantified formula inactive
+ *
+ * This flag is set to true during a full effort check if at least one
+ * quantified formula is set "inactive", that is, its negation is
+ * unsatisfiable in the current context.
+ */
+ bool d_cbqi_set_quant_inactive;
+ /** incomplete check
+ *
+ * This is set to true during a full effort check if this strategy could
+ * not find an instantiation for at least one asserted quantified formula.
+ */
+ 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;
+ std::map< Node, bool > d_active_quant;
+ /** Whether cegqi handles each quantified formula. */
+ std::map<Node, CegHandledStatus> d_do_cbqi;
+ /**
+ * An output channel used by instantiators for communicating with this
+ * class.
+ */
+ std::unique_ptr<CegqiOutputInstStrategy> d_out;
+ /**
+ * The instantiator for each quantified formula q registered to this class.
+ * This object is responsible for finding instantiatons for q.
+ */
+ std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
+ /**
+ * The decision strategy for each quantified formula q registered to this
+ * class.
+ */
+ std::map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
+ /** the current quantified formula we are processing */
+ Node d_curr_quant;
+ //---------------------- for vts delta minimization
+ /**
+ * Whether we will use vts delta minimization. If this flag is true, we
+ * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c
+ * is a small (< 1) constant. This heuristic is used in strategies where
+ * vts delta cannot be fully eliminated from assertions (for example, when
+ * using nested quantifiers and a non-innermost instantiation strategy).
+ * The same strategy applies for vts infinity, which we add lemmas of the
+ * form inf > (1/c)^1, inf > (1/c)^2, ....
+ */
+ bool d_check_vts_lemma_lc;
+ /** a small constant, used as a coefficient above */
+ Node d_small_const;
+ //---------------------- end for vts delta minimization
+ /** register ce lemma */
+ bool registerCbqiLemma( Node q );
+ /** register counterexample lemma
+ *
+ * This is called when we have constructed lem, the negation of the body of
+ * quantified formula q, skolemized with the instantiation constants of q.
+ * This function is used for setting up the proper information in the
+ * instantiator for q.
+ */
+ 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(); }
+ /** process functions */
+ void process(Node q, Theory::Effort effort, int e);
+
+ //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< Node, Node > d_id_to_ce_quant;
+ std::map< Node, Node > 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() : d_doVts(false){}
+ ~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;
+
+};
+
+
+}
+}
+}
+
+#endif
#include "options/quantifiers_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/term_database.h"
#include "context/cdlist.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
#include "theory/quantifiers/inst_match_trie.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/single_inv_partition.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/alpha_equivalence.h"
#include "theory/quantifiers/anti_skolem.h"
#include "theory/quantifiers/bv_inverter.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/conjecture_generator.h"
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
#include "theory/quantifiers/ematching/instantiation_engine.h"
projects / cvc5.git / commitdiff