Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp	Lines:	263	281	93.6 %
Date:	2021-09-10	Branches:	466	974	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(qs.getUserContext()),
      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("CexLiteral",
                                                      ceLit,
                                                      d_qstate.getSatContext(),
                                                      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	6708	InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
38	6708	: InstantiationRewriter(), d_parent(p)
39		{
40	6708	}
41
42	135752	TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
43		std::vector<Node>& terms,
44		Node inst,
45		bool doVts)
46		{
47	135752	return d_parent->rewriteInstantiation(q, terms, inst, doVts);
48		}
49
50	6708	InstStrategyCegqi::InstStrategyCegqi(Env& env,
51		QuantifiersState& qs,
52		QuantifiersInferenceManager& qim,
53		QuantifiersRegistry& qr,
54	6708	TermRegistry& tr)
55		: QuantifiersModule(env, qs, qim, qr, tr),
56	6708	d_irew(new InstRewriterCegqi(this)),
57		d_cbqi_set_quant_inactive(false),
58		d_incomplete_check(false),
59	6708	d_added_cbqi_lemma(qs.getUserContext()),
60	6708	d_vtsCache(new VtsTermCache(qim)),
61		d_bv_invert(nullptr),
62		d_small_const_multiplier(
63	13416	NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))),
64	40248	d_small_const(d_small_const_multiplier)
65		{
66	6708	d_check_vts_lemma_lc = false;
67	6708	if (options::cegqiBv())
68		{
69		// if doing instantiation for BV, need the inverter class
70	5107	d_bv_invert.reset(new BvInverter);
71		}
72	6708	if (options::cegqiNestedQE())
73		{
74	30	d_nestedQe.reset(new NestedQe(d_env));
75		}
76	6708	}
77
78	13410	InstStrategyCegqi::~InstStrategyCegqi() {}
79
80	75707	bool InstStrategyCegqi::needsCheck(Theory::Effort e)
81		{
82	75707	return e>=Theory::EFFORT_LAST_CALL;
83		}
84
85	11247	QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
86		{
87	11247	size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers();
88	47261	for (size_t i = 0; i < nquant; i++)
89		{
90	76272	Node q = d_treg.getModel()->getAssertedQuantifier(i);
91	40258	if (doCbqi(q))
92		{
93	4244	return QEFFORT_STANDARD;
94		}
95		}
96	7003	return QEFFORT_NONE;
97		}
98
99	1784	bool InstStrategyCegqi::registerCbqiLemma(Node q)
100		{
101	1784	if( !hasAddedCbqiLemma( q ) ){
102	1624	NodeManager* nm = NodeManager::currentNM();
103	1624	d_added_cbqi_lemma.insert( q );
104	1624	Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
105		//add cbqi lemma
106		//get the counterexample literal
107	3248	Node ceLit = getCounterexampleLiteral(q);
108	3248	Node ceBody = d_qreg.getInstConstantBody(q);
109	1624	if( !ceBody.isNull() ){
110		//add counterexample lemma
111	3248	Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
112		//require any decision on cel to be phase=true
113	1624	d_qim.addPendingPhaseRequirement(ceLit, true);
114	1624	Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
115		//add counterexample lemma
116	1624	lem = Rewriter::rewrite( lem );
117	1624	Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
118	1625	registerCounterexampleLemma( q, lem );
119
120		//compute dependencies between quantified formulas
121	3246	std::vector<Node> ics;
122	1623	TermUtil::computeInstConstContains(q, ics);
123	1623	d_parent_quant[q].clear();
124	1623	d_children_quant[q].clear();
125	3246	std::vector<Node> dep;
126	2065	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	1623	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	3246	std::vector< Node > quants;
157	1623	TermUtil::computeQuantContains( lem, quants );
158	1787	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	1623	d_dstrat.find(q);
168	1623	DecisionStrategy* dlds = nullptr;
169	1623	if (itds == d_dstrat.end())
170		{
171	4869	d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
172		ceLit,
173	1623	d_qstate.getSatContext(),
174	3246	d_qstate.getValuation()));
175	1623	dlds = d_dstrat[q].get();
176		}
177		else
178		{
179		dlds = itds->second.get();
180		}
181		// it is appended to the list of strategies
182	1623	d_qim.getDecisionManager()->registerStrategy(
183		DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
184	1623	return true;
185		}else{
186	160	return false;
187		}
188		}
189
190	27237	void InstStrategyCegqi::reset_round(Theory::Effort effort)
191		{
192	27237	d_cbqi_set_quant_inactive = false;
193	27237	d_incomplete_check = false;
194	27237	d_active_quant.clear();
195		//check if any cbqi lemma has not been added yet
196	27237	FirstOrderModel* fm = d_treg.getModel();
197	27237	size_t nquant = fm->getNumAssertedQuantifiers();
198	260112	for (size_t i = 0; i < nquant; i++)
199		{
200	465750	Node q = fm->getAssertedQuantifier(i);
201		//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
202	232875	if( doCbqi( q ) ){
203	9068	if (fm->isQuantifierActive(q))
204		{
205	9068	d_active_quant[q] = true;
206	9068	Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
207	18136	Node cel = getCounterexampleLiteral(q);
208		bool value;
209	9068	if (d_qstate.getValuation().hasSatValue(cel, value))
210		{
211	9044	Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
212	9044	if( !value ){
213	1415	if (d_qstate.getValuation().isDecision(cel))
214		{
215		Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
216		}else{
217	1415	Trace("cegqi") << "Inactive : " << q << std::endl;
218	1415	fm->setQuantifierActive(q, false);
219	1415	d_cbqi_set_quant_inactive = true;
220	1415	d_active_quant.erase( q );
221		}
222		}
223		}else{
224	24	Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
225		}
226		}
227		}
228		}
229
230		//refinement: only consider innermost active quantified formulas
231	27237	if( options::cegqiInnermost() ){
232	27237	if( !d_children_quant.empty() && !d_active_quant.empty() ){
233	6464	Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
234	12928	std::vector< Node > ninner;
235	14097	for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
236	7633	std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
237	7633	if( itc!=d_children_quant.end() ){
238	7891	for( unsigned j=0; j<itc->second.size(); j++ ){
239	368	if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
240	106	Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
241	106	ninner.push_back( it->first );
242	106	break;
243		}
244		}
245		}
246		}
247	6464	Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
248	6570	for( unsigned i=0; i<ninner.size(); i++ ){
249	106	Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
250	106	d_active_quant.erase( ninner[i] );
251		}
252	6464	Assert(!d_active_quant.empty());
253	6464	Trace("cegqi-debug") << "...done removing." << std::endl;
254		}
255		}
256	27237	d_check_vts_lemma_lc = false;
257	27237	}
258
259	30956	void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
260		{
261	30956	if (quant_e == QEFFORT_STANDARD)
262		{
263	11217	Assert(!d_qstate.isInConflict());
264	11217	double clSet = 0;
265	11217	if( Trace.isOn("cegqi-engine") ){
266		clSet = double(clock())/double(CLOCKS_PER_SEC);
267		Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
268		}
269	11217	size_t lastWaiting = d_qim.numPendingLemmas();
270	25669	for( int ee=0; ee<=1; ee++ ){
271		//for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
272		// Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
273		// if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
274	23367	for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
275	9848	Node q = it->first;
276	4924	Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
277	4924	process(q, e, ee);
278	4924	if (d_qstate.isInConflict())
279		{
280		break;
281		}
282		}
283	18443	if (d_qstate.isInConflict() \|\| d_qim.numPendingLemmas() > lastWaiting)
284		{
285	3991	break;
286		}
287		}
288	11217	if( Trace.isOn("cegqi-engine") ){
289		if (d_qim.numPendingLemmas() > lastWaiting)
290		{
291		Trace("cegqi-engine")
292		<< "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting)
293		<< std::endl;
294		}
295		double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
296		Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
297		}
298		}
299	30956	}
300
301	2582	bool InstStrategyCegqi::checkComplete(IncompleteId& incId)
302		{
303	2582	if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) \|\| d_incomplete_check ){
304	63	incId = IncompleteId::QUANTIFIERS_CEGQI;
305	63	return false;
306		}else{
307	2519	return true;
308		}
309		}
310
311	1451	bool InstStrategyCegqi::checkCompleteFor(Node q)
312		{
313	1451	std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
314	1451	if( it!=d_do_cbqi.end() ){
315	1451	return it->second != CEG_UNHANDLED;
316		}else{
317		return false;
318		}
319		}
320
321	23406	void InstStrategyCegqi::checkOwnership(Node q)
322		{
323	23406	if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
324		{
325	1642	if (d_do_cbqi[q] == CEG_HANDLED)
326		{
327		//take full ownership of the quantified formula
328	1625	d_qreg.setOwner(q, this);
329		}
330		}
331	23406	}
332
333	23439	void InstStrategyCegqi::preRegisterQuantifier(Node q)
334		{
335	23439	if (doCbqi(q))
336		{
337	1642	if (processNestedQe(q, true))
338		{
339		// will process using nested quantifier elimination
340	18	return;
341		}
342		// register the cbqi lemma
343	1625	if( registerCbqiLemma( q ) ){
344	1463	Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
345		}
346		}
347		}
348	135752	TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
349		std::vector<Node>& terms,
350		Node inst,
351		bool doVts)
352		{
353	271504	Node prevInst = inst;
354	135752	if (doVts)
355		{
356		// do virtual term substitution
357	79	inst = Rewriter::rewrite(inst);
358	79	Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
359	79	inst = d_vtsCache->rewriteVtsSymbols(inst);
360	79	Trace("quant-vts-debug") << "...got " << inst << std::endl;
361		}
362	135752	if (prevInst != inst)
363		{
364		// not proof producing yet
365	79	return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
366		}
367	135673	return TrustNode::null();
368		}
369
370	6708	InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
371		{
372	6708	return d_irew.get();
373		}
374
375	1624	void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
376		{
377		// must register with the instantiator
378		// must explicitly remove ITEs so that we record dependencies
379	3248	std::vector<Node> ce_vars;
380	4791	for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
381		i++)
382		{
383	3167	ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
384		}
385		// send the lemma
386	1625	d_qim.lemma(lem, InferenceId::QUANTIFIERS_CEGQI_CEX);
387		// get the preprocessed form of the lemma we just sent
388	3246	std::vector<Node> skolems;
389	3246	std::vector<Node> skAsserts;
390		Node ppLem =
391	3246	d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
392	3246	std::vector<Node> lemp{ppLem};
393	1623	lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
394	1623	ppLem = NodeManager::currentNM()->mkAnd(lemp);
395	3246	Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
396	1623	<< std::endl;
397	3246	std::vector<Node> auxLems;
398	1623	CegInstantiator* cinst = getInstantiator(q);
399	1623	cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
400	1726	for (size_t i = 0, size = auxLems.size(); i < size; i++)
401		{
402	206	Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
403	103	<< std::endl;
404	103	d_qim.addPendingLemma(auxLems[i], InferenceId::QUANTIFIERS_CEGQI_CEX_AUX);
405		}
406	1623	}
407
408	320142	bool InstStrategyCegqi::doCbqi(Node q)
409		{
410	320142	std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
411	320142	if( it==d_do_cbqi.end() ){
412	23406	CegHandledStatus ret = CegInstantiator::isCbqiQuant(q);
413	23406	Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
414	23406	d_do_cbqi[q] = ret;
415	23406	return ret != CEG_UNHANDLED;
416		}
417	296736	return it->second != CEG_UNHANDLED;
418		}
419
420	4924	void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
421		// If we are doing nested quantifier elimination, check if q was already
422		// processed.
423	4924	if (processNestedQe(q, false))
424		{
425		// don't need to process this, since it has been reduced
426	26	return;
427		}
428	4898	if( e==0 ){
429	4597	CegInstantiator * cinst = getInstantiator( q );
430	4597	Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
431	4597	d_curr_quant = q;
432	4597	if( !cinst->check() ){
433	300	d_incomplete_check = true;
434	300	d_check_vts_lemma_lc = true;
435		}
436	4597	d_curr_quant = Node::null();
437	301	}else if( e==1 ){
438		//minimize the free delta heuristically on demand
439	301	if( d_check_vts_lemma_lc ){
440	87	Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
441	87	d_check_vts_lemma_lc = false;
442	174	d_small_const = NodeManager::currentNM()->mkNode(
443	87	MULT, d_small_const, d_small_const_multiplier);
444	87	d_small_const = Rewriter::rewrite( d_small_const );
445		//heuristic for now, until we know how to do nested quantification
446	174	Node delta = d_vtsCache->getVtsDelta(true, false);
447	87	if( !delta.isNull() ){
448		Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
449		Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
450		d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
451		}
452	174	std::vector< Node > inf;
453	87	d_vtsCache->getVtsTerms(inf, true, false, false);
454	87	for( unsigned i=0; i<inf.size(); i++ ){
455		Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
456		Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
457		d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
458		}
459		}
460		}
461		}
462
463	10964	Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
464		{
465	10964	std::map<Node, Node>::iterator it = d_ce_lit.find(q);
466	10964	if (it != d_ce_lit.end())
467		{
468	9326	return it->second;
469		}
470	1638	NodeManager * nm = NodeManager::currentNM();
471	1638	SkolemManager* sm = nm->getSkolemManager();
472	3276	Node g = sm->mkDummySkolem("g", nm->booleanType());
473		// ensure that it is a SAT literal
474	3276	Node ceLit = d_qstate.getValuation().ensureLiteral(g);
475	1638	d_ce_lit[q] = ceLit;
476	1638	return ceLit;
477		}
478
479	9900	bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
480	9900	Assert(!d_curr_quant.isNull());
481		// check if we need virtual term substitution (if used delta or infinity)
482	9900	bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
483	9900	Instantiate* inst = d_qim.getInstantiate();
484		//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
485	9900	if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
486		{
487	1	d_cbqi_set_quant_inactive = true;
488	1	d_incomplete_check = true;
489	1	inst->recordInstantiation(d_curr_quant, subs, usedVts);
490	1	return true;
491		}
492	29697	else if (inst->addInstantiation(d_curr_quant,
493		subs,
494		InferenceId::QUANTIFIERS_INST_CEGQI,
495	19798	Node::null(),
496		false,
497		usedVts))
498		{
499	4296	return true;
500		}
501		// this should never happen for monotonic selection strategies
502	5603	Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
503	5603	return false;
504		}
505
506	6220	CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
507		std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
508	6220	d_cinst.find(q);
509	6220	if( it==d_cinst.end() ){
510	1623	d_cinst[q].reset(new CegInstantiator(q, d_qstate, d_treg, this));
511	1623	return d_cinst[q].get();
512		}
513	4597	return it->second.get();
514		}
515
516	1687	VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
517		{
518	1687	return d_vtsCache.get();
519		}
520
521	1110	BvInverter* InstStrategyCegqi::getBvInverter() const
522		{
523	1110	return d_bv_invert.get();
524		}
525
526	6566	bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
527		{
528	6566	if (d_nestedQe != nullptr)
529		{
530	96	if (isPreregister)
531		{
532		// If at preregister, we are done if we have nested quantification.
533		// We will process nested quantification.
534	42	return NestedQe::hasNestedQuantification(q);
535		}
536		// if not a preregister, we process, which may trigger quantifier
537		// elimination in subsolvers.
538	82	std::vector<Node> lems;
539	54	if (d_nestedQe->process(q, lems))
540		{
541		// add lemmas to process
542	40	for (const Node& lem : lems)
543		{
544	14	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_CEGQI_NESTED_QE);
545		}
546		// don't need to process this, since it has been reduced
547	26	return true;
548		}
549		}
550	6498	return false;
551		}
552
553		} // namespace quantifiers
554		} // namespace theory
555	29502	} // namespace cvc5