Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp	Lines:	262	280	93.6 %
Date:	2021-09-18	Branches:	465	972	47.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Implementation of counterexample-guided quantifier instantiation strategies.
 */
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;
using namespace cvc5::context;

namespace cvc5 {
namespace theory {
namespace quantifiers {

InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
    : InstantiationRewriter(), d_parent(p)
{
}

TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
                                                  std::vector<Node>& terms,
                                                  Node inst,
                                                  bool doVts)
{
  return d_parent->rewriteInstantiation(q, terms, inst, doVts);
}

InstStrategyCegqi::InstStrategyCegqi(Env& env,
                                     QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
                                     TermRegistry& tr)
    : QuantifiersModule(env, qs, qim, qr, tr),
      d_irew(new InstRewriterCegqi(this)),
      d_cbqi_set_quant_inactive(false),
      d_incomplete_check(false),
      d_added_cbqi_lemma(userContext()),
      d_vtsCache(new VtsTermCache(qim)),
      d_bv_invert(nullptr),
      d_small_const_multiplier(
          NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))),
      d_small_const(d_small_const_multiplier)
{
  d_check_vts_lemma_lc = false;
  if (options::cegqiBv())
  {
    // if doing instantiation for BV, need the inverter class
    d_bv_invert.reset(new BvInverter);
  }
  if (options::cegqiNestedQE())
  {
    d_nestedQe.reset(new NestedQe(d_env));
  }
}

InstStrategyCegqi::~InstStrategyCegqi() {}

bool InstStrategyCegqi::needsCheck(Theory::Effort e)
{
  return e>=Theory::EFFORT_LAST_CALL;
}

QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
{
  size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers();
  for (size_t i = 0; i < nquant; i++)
  {
    Node q = d_treg.getModel()->getAssertedQuantifier(i);
    if (doCbqi(q))
    {
      return QEFFORT_STANDARD;
    }
  }
  return QEFFORT_NONE;
}

bool InstStrategyCegqi::registerCbqiLemma(Node q)
{
  if( !hasAddedCbqiLemma( q ) ){
    NodeManager* nm = NodeManager::currentNM();
    d_added_cbqi_lemma.insert( q );
    Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
    //add cbqi lemma
    //get the counterexample literal
    Node ceLit = getCounterexampleLiteral(q);
    Node ceBody = d_qreg.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_qim.addPendingPhaseRequirement(ceLit, true);
      Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
      //add counterexample lemma
      lem = Rewriter::rewrite( lem );
      Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
      registerCounterexampleLemma( q, lem );

      //compute dependencies between quantified formulas
      std::vector<Node> ics;
      TermUtil::computeInstConstContains(q, ics);
      d_parent_quant[q].clear();
      d_children_quant[q].clear();
      std::vector<Node> dep;
      for (const Node& ic : ics)
      {
        Node qi = ic.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);
          // may not have added the CEX lemma, but the literal is created by
          // the following call regardless. One rare case where this can happen
          // is if both sygus-inst and CEGQI are being run in parallel, and
          // a parent quantified formula is not handled by CEGQI, but a child
          // is.
          Node qicel = getCounterexampleLiteral(qi);
          dep.push_back(qi);
          dep.push_back(qicel);
        }
      }
      if (!dep.empty())
      {
        // This lemma states that if the child is active, then the parent must
        // be asserted, in particular G => Q where G is the CEX literal for the
        // child and Q is the parent.
        Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
        Trace("cegqi-lemma")
            << "Counterexample dependency lemma : " << dep_lemma << std::endl;
        d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP);
      }

      //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] );
        }
      }
    }
    // 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(
          d_env, "CexLiteral", ceLit, d_qstate.getValuation()));
      dlds = d_dstrat[q].get();
    }
    else
    {
      dlds = itds->second.get();
    }
    // it is appended to the list of strategies
    d_qim.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
  FirstOrderModel* fm = d_treg.getModel();
  size_t nquant = fm->getNumAssertedQuantifiers();
  for (size_t i = 0; i < nquant; i++)
  {
    Node q = fm->getAssertedQuantifier(i);
    //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
    if( doCbqi( q ) ){
      if (fm->isQuantifierActive(q))
      {
        d_active_quant[q] = true;
        Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
        Node cel = getCounterexampleLiteral(q);
        bool value;
        if (d_qstate.getValuation().hasSatValue(cel, value))
        {
          Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
          if( !value ){
            if (d_qstate.getValuation().isDecision(cel))
            {
              Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
            }else{
              Trace("cegqi") << "Inactive : " << q << std::endl;
              fm->setQuantifierActive(q, false);
              d_cbqi_set_quant_inactive = true;
              d_active_quant.erase( q );
            }
          }
        }else{
          Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
        }
      }
    }
  }

  //refinement: only consider innermost active quantified formulas
  if( options::cegqiInnermost() ){
    if( !d_children_quant.empty() && !d_active_quant.empty() ){
      Trace("cegqi-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("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
              ninner.push_back( it->first );
              break;
            }
          }
        }
      }
      Trace("cegqi-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("cegqi-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_qstate.isInConflict());
    double clSet = 0;
    if( Trace.isOn("cegqi-engine") ){
      clSet = double(clock())/double(CLOCKS_PER_SEC);
      Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
    }
    size_t lastWaiting = d_qim.numPendingLemmas();
    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("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
        process(q, e, ee);
        if (d_qstate.isInConflict())
        {
          break;
        }
      }
      if (d_qstate.isInConflict() || d_qim.numPendingLemmas() > lastWaiting)
      {
        break;
      }
    }
    if( Trace.isOn("cegqi-engine") ){
      if (d_qim.numPendingLemmas() > lastWaiting)
      {
        Trace("cegqi-engine")
            << "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting)
            << std::endl;
      }
      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
      Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
    }
  }
}

bool InstStrategyCegqi::checkComplete(IncompleteId& incId)
{
  if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
    incId = IncompleteId::QUANTIFIERS_CEGQI;
    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;
  }
}

void InstStrategyCegqi::checkOwnership(Node q)
{
  if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
  {
    if (d_do_cbqi[q] == CEG_HANDLED)
    {
      //take full ownership of the quantified formula
      d_qreg.setOwner(q, this);
    }
  }
}

void InstStrategyCegqi::preRegisterQuantifier(Node q)
{
  if (doCbqi(q))
  {
    if (processNestedQe(q, true))
    {
      // will process using nested quantifier elimination
      return;
    }
    // register the cbqi lemma
    if( registerCbqiLemma( q ) ){
      Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
    }
  }
}
TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
                                                  std::vector<Node>& terms,
                                                  Node inst,
                                                  bool doVts)
{
  Node prevInst = inst;
  if (doVts)
  {
    // do virtual term substitution
    inst = Rewriter::rewrite(inst);
    Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
    inst = d_vtsCache->rewriteVtsSymbols(inst);
    Trace("quant-vts-debug") << "...got " << inst << std::endl;
  }
  if (prevInst != inst)
  {
    // not proof producing yet
    return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
  }
  return TrustNode::null();
}

InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
{
  return d_irew.get();
}

void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
{
  // must register with the instantiator
  // must explicitly remove ITEs so that we record dependencies
  std::vector<Node> ce_vars;
  for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
       i++)
  {
    ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
  }
  // send the lemma
  d_qim.lemma(lem, InferenceId::QUANTIFIERS_CEGQI_CEX);
  // get the preprocessed form of the lemma we just sent
  std::vector<Node> skolems;
  std::vector<Node> skAsserts;
  Node ppLem =
      d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
  std::vector<Node> lemp{ppLem};
  lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
  ppLem = NodeManager::currentNM()->mkAnd(lemp);
  Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
                       << std::endl;
  std::vector<Node> auxLems;
  CegInstantiator* cinst = getInstantiator(q);
  cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
  for (size_t i = 0, size = auxLems.size(); i < size; i++)
  {
    Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
                         << std::endl;
    d_qim.addPendingLemma(auxLems[i], InferenceId::QUANTIFIERS_CEGQI_CEX_AUX);
  }
}

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);
    Trace("cegqi-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 we are doing nested quantifier elimination, check if q was already
  // processed.
  if (processNestedQe(q, false))
  {
    // don't need to process this, since it has been reduced
    return;
  }
  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_multiplier);
      d_small_const = Rewriter::rewrite( d_small_const );
      //heuristic for now, until we know how to do nested quantification
      Node delta = d_vtsCache->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_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
      }
      std::vector< Node > inf;
      d_vtsCache->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_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
      }
    }
  }
}

Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
{
  std::map<Node, Node>::iterator it = d_ce_lit.find(q);
  if (it != d_ce_lit.end())
  {
    return it->second;
  }
  NodeManager * nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node g = sm->mkDummySkolem("g", nm->booleanType());
  // ensure that it is a SAT literal
  Node ceLit = d_qstate.getValuation().ensureLiteral(g);
  d_ce_lit[q] = ceLit;
  return ceLit;
}

bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
  Assert(!d_curr_quant.isNull());
  // check if we need virtual term substitution (if used delta or infinity)
  bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
  Instantiate* inst = d_qim.getInstantiate();
  //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
  if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
  {
    d_cbqi_set_quant_inactive = true;
    d_incomplete_check = true;
    inst->recordInstantiation(d_curr_quant, subs, usedVts);
    return true;
  }
  else if (inst->addInstantiation(d_curr_quant,
                                  subs,
                                  InferenceId::QUANTIFIERS_INST_CEGQI,
                                  Node::null(),
                                  false,
                                  usedVts))
  {
    return true;
  }
  // this should never happen for monotonic selection strategies
  Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
  return false;
}

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(q, d_qstate, d_treg, this));
    return d_cinst[q].get();
  }
  return it->second.get();
}

VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
{
  return d_vtsCache.get();
}

BvInverter* InstStrategyCegqi::getBvInverter() const
{
  return d_bv_invert.get();
}

bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
{
  if (d_nestedQe != nullptr)
  {
    if (isPreregister)
    {
      // If at preregister, we are done if we have nested quantification.
      // We will process nested quantification.
      return NestedQe::hasNestedQuantification(q);
    }
    // if not a preregister, we process, which may trigger quantifier
    // elimination in subsolvers.
    std::vector<Node> lems;
    if (d_nestedQe->process(q, lems))
    {
      // add lemmas to process
      for (const Node& lem : lems)
      {
        d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_CEGQI_NESTED_QE);
      }
      // don't need to process this, since it has been reduced
      return true;
    }
  }
  return false;
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of counterexample-guided quantifier instantiation strategies.
14		*/
15		#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
16
17		#include "expr/node_algorithm.h"
18		#include "expr/skolem_manager.h"
19		#include "options/quantifiers_options.h"
20		#include "theory/quantifiers/first_order_model.h"
21		#include "theory/quantifiers/instantiate.h"
22		#include "theory/quantifiers/quantifiers_attributes.h"
23		#include "theory/quantifiers/quantifiers_rewriter.h"
24		#include "theory/quantifiers/term_database.h"
25		#include "theory/quantifiers/term_registry.h"
26		#include "theory/quantifiers/term_util.h"
27		#include "theory/rewriter.h"
28
29		using namespace std;
30		using namespace cvc5::kind;
31		using namespace cvc5::context;
32
33		namespace cvc5 {
34		namespace theory {
35		namespace quantifiers {
36
37	6723	InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
38	6723	: InstantiationRewriter(), d_parent(p)
39		{
40	6723	}
41
42	140409	TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
43		std::vector<Node>& terms,
44		Node inst,
45		bool doVts)
46		{
47	140409	return d_parent->rewriteInstantiation(q, terms, inst, doVts);
48		}
49
50	6723	InstStrategyCegqi::InstStrategyCegqi(Env& env,
51		QuantifiersState& qs,
52		QuantifiersInferenceManager& qim,
53		QuantifiersRegistry& qr,
54	6723	TermRegistry& tr)
55		: QuantifiersModule(env, qs, qim, qr, tr),
56	6723	d_irew(new InstRewriterCegqi(this)),
57		d_cbqi_set_quant_inactive(false),
58		d_incomplete_check(false),
59	6723	d_added_cbqi_lemma(userContext()),
60	6723	d_vtsCache(new VtsTermCache(qim)),
61		d_bv_invert(nullptr),
62		d_small_const_multiplier(
63	13446	NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))),
64	40338	d_small_const(d_small_const_multiplier)
65		{
66	6723	d_check_vts_lemma_lc = false;
67	6723	if (options::cegqiBv())
68		{
69		// if doing instantiation for BV, need the inverter class
70	5117	d_bv_invert.reset(new BvInverter);
71		}
72	6723	if (options::cegqiNestedQE())
73		{
74	30	d_nestedQe.reset(new NestedQe(d_env));
75		}
76	6723	}
77
78	13440	InstStrategyCegqi::~InstStrategyCegqi() {}
79
80	75750	bool InstStrategyCegqi::needsCheck(Theory::Effort e)
81		{
82	75750	return e>=Theory::EFFORT_LAST_CALL;
83		}
84
85	11249	QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
86		{
87	11249	size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers();
88	47270	for (size_t i = 0; i < nquant; i++)
89		{
90	76281	Node q = d_treg.getModel()->getAssertedQuantifier(i);
91	40260	if (doCbqi(q))
92		{
93	4239	return QEFFORT_STANDARD;
94		}
95		}
96	7010	return QEFFORT_NONE;
97		}
98
99	1785	bool InstStrategyCegqi::registerCbqiLemma(Node q)
100		{
101	1785	if( !hasAddedCbqiLemma( q ) ){
102	1625	NodeManager* nm = NodeManager::currentNM();
103	1625	d_added_cbqi_lemma.insert( q );
104	1625	Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
105		//add cbqi lemma
106		//get the counterexample literal
107	3250	Node ceLit = getCounterexampleLiteral(q);
108	3250	Node ceBody = d_qreg.getInstConstantBody(q);
109	1625	if( !ceBody.isNull() ){
110		//add counterexample lemma
111	3250	Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
112		//require any decision on cel to be phase=true
113	1625	d_qim.addPendingPhaseRequirement(ceLit, true);
114	1625	Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
115		//add counterexample lemma
116	1625	lem = Rewriter::rewrite( lem );
117	1625	Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
118	1626	registerCounterexampleLemma( q, lem );
119
120		//compute dependencies between quantified formulas
121	3248	std::vector<Node> ics;
122	1624	TermUtil::computeInstConstContains(q, ics);
123	1624	d_parent_quant[q].clear();
124	1624	d_children_quant[q].clear();
125	3248	std::vector<Node> dep;
126	2066	for (const Node& ic : ics)
127		{
128	884	Node qi = ic.getAttribute(InstConstantAttribute());
129	1326	if (std::find(d_parent_quant[q].begin(), d_parent_quant[q].end(), qi)
130	1326	== d_parent_quant[q].end())
131		{
132	272	d_parent_quant[q].push_back(qi);
133	272	d_children_quant[qi].push_back(q);
134		// may not have added the CEX lemma, but the literal is created by
135		// the following call regardless. One rare case where this can happen
136		// is if both sygus-inst and CEGQI are being run in parallel, and
137		// a parent quantified formula is not handled by CEGQI, but a child
138		// is.
139	544	Node qicel = getCounterexampleLiteral(qi);
140	272	dep.push_back(qi);
141	272	dep.push_back(qicel);
142		}
143		}
144	1624	if (!dep.empty())
145		{
146		// This lemma states that if the child is active, then the parent must
147		// be asserted, in particular G => Q where G is the CEX literal for the
148		// child and Q is the parent.
149	376	Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
150	376	Trace("cegqi-lemma")
151	188	<< "Counterexample dependency lemma : " << dep_lemma << std::endl;
152	188	d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP);
153		}
154
155		//must register all sub-quantifiers of counterexample lemma, register their lemmas
156	3248	std::vector< Node > quants;
157	1624	TermUtil::computeQuantContains( lem, quants );
158	1788	for( unsigned i=0; i<quants.size(); i++ ){
159	164	if( doCbqi( quants[i] ) ){
160	160	registerCbqiLemma( quants[i] );
161		}
162		}
163		}
164		// The decision strategy for this quantified formula ensures that its
165		// counterexample literal is decided on first. It is user-context dependent.
166		std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds =
167	1624	d_dstrat.find(q);
168	1624	DecisionStrategy* dlds = nullptr;
169	1624	if (itds == d_dstrat.end())
170		{
171	4872	d_dstrat[q].reset(new DecisionStrategySingleton(
172	3248	d_env, "CexLiteral", ceLit, d_qstate.getValuation()));
173	1624	dlds = d_dstrat[q].get();
174		}
175		else
176		{
177		dlds = itds->second.get();
178		}
179		// it is appended to the list of strategies
180	1624	d_qim.getDecisionManager()->registerStrategy(
181		DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
182	1624	return true;
183		}else{
184	160	return false;
185		}
186		}
187
188	27260	void InstStrategyCegqi::reset_round(Theory::Effort effort)
189		{
190	27260	d_cbqi_set_quant_inactive = false;
191	27260	d_incomplete_check = false;
192	27260	d_active_quant.clear();
193		//check if any cbqi lemma has not been added yet
194	27260	FirstOrderModel* fm = d_treg.getModel();
195	27260	size_t nquant = fm->getNumAssertedQuantifiers();
196	260223	for (size_t i = 0; i < nquant; i++)
197		{
198	465926	Node q = fm->getAssertedQuantifier(i);
199		//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
200	232963	if( doCbqi( q ) ){
201	9077	if (fm->isQuantifierActive(q))
202		{
203	9077	d_active_quant[q] = true;
204	9077	Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
205	18154	Node cel = getCounterexampleLiteral(q);
206		bool value;
207	9077	if (d_qstate.getValuation().hasSatValue(cel, value))
208		{
209	9053	Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
210	9053	if( !value ){
211	1439	if (d_qstate.getValuation().isDecision(cel))
212		{
213		Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
214		}else{
215	1439	Trace("cegqi") << "Inactive : " << q << std::endl;
216	1439	fm->setQuantifierActive(q, false);
217	1439	d_cbqi_set_quant_inactive = true;
218	1439	d_active_quant.erase( q );
219		}
220		}
221		}else{
222	24	Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
223		}
224		}
225		}
226		}
227
228		//refinement: only consider innermost active quantified formulas
229	27260	if( options::cegqiInnermost() ){
230	27260	if( !d_children_quant.empty() && !d_active_quant.empty() ){
231	6449	Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
232	12898	std::vector< Node > ninner;
233	14067	for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
234	7618	std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
235	7618	if( itc!=d_children_quant.end() ){
236	7876	for( unsigned j=0; j<itc->second.size(); j++ ){
237	368	if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
238	106	Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
239	106	ninner.push_back( it->first );
240	106	break;
241		}
242		}
243		}
244		}
245	6449	Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
246	6555	for( unsigned i=0; i<ninner.size(); i++ ){
247	106	Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
248	106	d_active_quant.erase( ninner[i] );
249		}
250	6449	Assert(!d_active_quant.empty());
251	6449	Trace("cegqi-debug") << "...done removing." << std::endl;
252		}
253		}
254	27260	d_check_vts_lemma_lc = false;
255	27260	}
256
257	30972	void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
258		{
259	30972	if (quant_e == QEFFORT_STANDARD)
260		{
261	11219	Assert(!d_qstate.isInConflict());
262	11219	double clSet = 0;
263	11219	if( Trace.isOn("cegqi-engine") ){
264		clSet = double(clock())/double(CLOCKS_PER_SEC);
265		Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
266		}
267	11219	size_t lastWaiting = d_qim.numPendingLemmas();
268	25685	for( int ee=0; ee<=1; ee++ ){
269		//for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
270		// Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
271		// if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
272	23371	for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
273	9838	Node q = it->first;
274	4919	Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
275	4919	process(q, e, ee);
276	4919	if (d_qstate.isInConflict())
277		{
278		break;
279		}
280		}
281	18452	if (d_qstate.isInConflict() \|\| d_qim.numPendingLemmas() > lastWaiting)
282		{
283	3986	break;
284		}
285		}
286	11219	if( Trace.isOn("cegqi-engine") ){
287		if (d_qim.numPendingLemmas() > lastWaiting)
288		{
289		Trace("cegqi-engine")
290		<< "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting)
291		<< std::endl;
292		}
293		double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
294		Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
295		}
296		}
297	30972	}
298
299	2587	bool InstStrategyCegqi::checkComplete(IncompleteId& incId)
300		{
301	2587	if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) \|\| d_incomplete_check ){
302	63	incId = IncompleteId::QUANTIFIERS_CEGQI;
303	63	return false;
304		}else{
305	2524	return true;
306		}
307		}
308
309	1455	bool InstStrategyCegqi::checkCompleteFor(Node q)
310		{
311	1455	std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
312	1455	if( it!=d_do_cbqi.end() ){
313	1455	return it->second != CEG_UNHANDLED;
314		}else{
315		return false;
316		}
317		}
318
319	23409	void InstStrategyCegqi::checkOwnership(Node q)
320		{
321	23409	if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
322		{
323	1643	if (d_do_cbqi[q] == CEG_HANDLED)
324		{
325		//take full ownership of the quantified formula
326	1626	d_qreg.setOwner(q, this);
327		}
328		}
329	23409	}
330
331	23442	void InstStrategyCegqi::preRegisterQuantifier(Node q)
332		{
333	23442	if (doCbqi(q))
334		{
335	1643	if (processNestedQe(q, true))
336		{
337		// will process using nested quantifier elimination
338	18	return;
339		}
340		// register the cbqi lemma
341	1626	if( registerCbqiLemma( q ) ){
342	1464	Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
343		}
344		}
345		}
346	140409	TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
347		std::vector<Node>& terms,
348		Node inst,
349		bool doVts)
350		{
351	280818	Node prevInst = inst;
352	140409	if (doVts)
353		{
354		// do virtual term substitution
355	79	inst = Rewriter::rewrite(inst);
356	79	Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
357	79	inst = d_vtsCache->rewriteVtsSymbols(inst);
358	79	Trace("quant-vts-debug") << "...got " << inst << std::endl;
359		}
360	140409	if (prevInst != inst)
361		{
362		// not proof producing yet
363	79	return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
364		}
365	140330	return TrustNode::null();
366		}
367
368	6723	InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
369		{
370	6723	return d_irew.get();
371		}
372
373	1625	void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
374		{
375		// must register with the instantiator
376		// must explicitly remove ITEs so that we record dependencies
377	3250	std::vector<Node> ce_vars;
378	4834	for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
379		i++)
380		{
381	3209	ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
382		}
383		// send the lemma
384	1626	d_qim.lemma(lem, InferenceId::QUANTIFIERS_CEGQI_CEX);
385		// get the preprocessed form of the lemma we just sent
386	3248	std::vector<Node> skolems;
387	3248	std::vector<Node> skAsserts;
388		Node ppLem =
389	3248	d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
390	3248	std::vector<Node> lemp{ppLem};
391	1624	lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
392	1624	ppLem = NodeManager::currentNM()->mkAnd(lemp);
393	3248	Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
394	1624	<< std::endl;
395	3248	std::vector<Node> auxLems;
396	1624	CegInstantiator* cinst = getInstantiator(q);
397	1624	cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
398	1727	for (size_t i = 0, size = auxLems.size(); i < size; i++)
399		{
400	206	Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
401	103	<< std::endl;
402	103	d_qim.addPendingLemma(auxLems[i], InferenceId::QUANTIFIERS_CEGQI_CEX_AUX);
403		}
404	1624	}
405
406	320238	bool InstStrategyCegqi::doCbqi(Node q)
407		{
408	320238	std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
409	320238	if( it==d_do_cbqi.end() ){
410	23409	CegHandledStatus ret = CegInstantiator::isCbqiQuant(q);
411	23409	Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
412	23409	d_do_cbqi[q] = ret;
413	23409	return ret != CEG_UNHANDLED;
414		}
415	296829	return it->second != CEG_UNHANDLED;
416		}
417
418	4919	void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
419		// If we are doing nested quantifier elimination, check if q was already
420		// processed.
421	4919	if (processNestedQe(q, false))
422		{
423		// don't need to process this, since it has been reduced
424	26	return;
425		}
426	4893	if( e==0 ){
427	4592	CegInstantiator * cinst = getInstantiator( q );
428	4592	Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
429	4592	d_curr_quant = q;
430	4592	if( !cinst->check() ){
431	300	d_incomplete_check = true;
432	300	d_check_vts_lemma_lc = true;
433		}
434	4592	d_curr_quant = Node::null();
435	301	}else if( e==1 ){
436		//minimize the free delta heuristically on demand
437	301	if( d_check_vts_lemma_lc ){
438	87	Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
439	87	d_check_vts_lemma_lc = false;
440	174	d_small_const = NodeManager::currentNM()->mkNode(
441	87	MULT, d_small_const, d_small_const_multiplier);
442	87	d_small_const = Rewriter::rewrite( d_small_const );
443		//heuristic for now, until we know how to do nested quantification
444	174	Node delta = d_vtsCache->getVtsDelta(true, false);
445	87	if( !delta.isNull() ){
446		Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
447		Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
448		d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
449		}
450	174	std::vector< Node > inf;
451	87	d_vtsCache->getVtsTerms(inf, true, false, false);
452	87	for( unsigned i=0; i<inf.size(); i++ ){
453		Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
454		Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
455		d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
456		}
457		}
458		}
459		}
460
461	10974	Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
462		{
463	10974	std::map<Node, Node>::iterator it = d_ce_lit.find(q);
464	10974	if (it != d_ce_lit.end())
465		{
466	9335	return it->second;
467		}
468	1639	NodeManager * nm = NodeManager::currentNM();
469	1639	SkolemManager* sm = nm->getSkolemManager();
470	3278	Node g = sm->mkDummySkolem("g", nm->booleanType());
471		// ensure that it is a SAT literal
472	3278	Node ceLit = d_qstate.getValuation().ensureLiteral(g);
473	1639	d_ce_lit[q] = ceLit;
474	1639	return ceLit;
475		}
476
477	9895	bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
478	9895	Assert(!d_curr_quant.isNull());
479		// check if we need virtual term substitution (if used delta or infinity)
480	9895	bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
481	9895	Instantiate* inst = d_qim.getInstantiate();
482		//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
483	9895	if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
484		{
485	1	d_cbqi_set_quant_inactive = true;
486	1	d_incomplete_check = true;
487	1	inst->recordInstantiation(d_curr_quant, subs, usedVts);
488	1	return true;
489		}
490	29682	else if (inst->addInstantiation(d_curr_quant,
491		subs,
492		InferenceId::QUANTIFIERS_INST_CEGQI,
493	19788	Node::null(),
494		false,
495		usedVts))
496		{
497	4291	return true;
498		}
499		// this should never happen for monotonic selection strategies
500	5603	Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
501	5603	return false;
502		}
503
504	6216	CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
505		std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
506	6216	d_cinst.find(q);
507	6216	if( it==d_cinst.end() ){
508	1624	d_cinst[q].reset(new CegInstantiator(q, d_qstate, d_treg, this));
509	1624	return d_cinst[q].get();
510		}
511	4592	return it->second.get();
512		}
513
514	1729	VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
515		{
516	1729	return d_vtsCache.get();
517		}
518
519	1110	BvInverter* InstStrategyCegqi::getBvInverter() const
520		{
521	1110	return d_bv_invert.get();
522		}
523
524	6562	bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
525		{
526	6562	if (d_nestedQe != nullptr)
527		{
528	96	if (isPreregister)
529		{
530		// If at preregister, we are done if we have nested quantification.
531		// We will process nested quantification.
532	42	return NestedQe::hasNestedQuantification(q);
533		}
534		// if not a preregister, we process, which may trigger quantifier
535		// elimination in subsolvers.
536	82	std::vector<Node> lems;
537	54	if (d_nestedQe->process(q, lems))
538		{
539		// add lemmas to process
540	40	for (const Node& lem : lems)
541		{
542	14	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_CEGQI_NESTED_QE);
543		}
544		// don't need to process this, since it has been reduced
545	26	return true;
546		}
547		}
548	6494	return false;
549		}
550
551		} // namespace quantifiers
552		} // namespace theory
553	29574	} // namespace cvc5