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-11-07	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"
#include "util/rational.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, const 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().quantifiers.cegqiBv)
  {
    // if doing instantiation for BV, need the inverter class
    d_bv_invert.reset(new BvInverter);
  }
  if (options().quantifiers.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 = 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().quantifiers.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().quantifiers.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, const std::vector<Node>& terms, Node inst, bool doVts)
{
  Node prevInst = inst;
  if (doVts)
  {
    // do virtual term substitution
    inst = 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 = 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(d_env, 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		#include "util/rational.h"
29
30		using namespace std;
31		using namespace cvc5::kind;
32		using namespace cvc5::context;
33
34		namespace cvc5 {
35		namespace theory {
36		namespace quantifiers {
37
38	12031	InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
39	12031	: InstantiationRewriter(), d_parent(p)
40		{
41	12031	}
42
43	52236	TrustNode InstRewriterCegqi::rewriteInstantiation(
44		Node q, const std::vector<Node>& terms, Node inst, bool doVts)
45		{
46	52236	return d_parent->rewriteInstantiation(q, terms, inst, doVts);
47		}
48
49	12031	InstStrategyCegqi::InstStrategyCegqi(Env& env,
50		QuantifiersState& qs,
51		QuantifiersInferenceManager& qim,
52		QuantifiersRegistry& qr,
53	12031	TermRegistry& tr)
54		: QuantifiersModule(env, qs, qim, qr, tr),
55	12031	d_irew(new InstRewriterCegqi(this)),
56		d_cbqi_set_quant_inactive(false),
57		d_incomplete_check(false),
58	12031	d_added_cbqi_lemma(userContext()),
59	12031	d_vtsCache(new VtsTermCache(qim)),
60		d_bv_invert(nullptr),
61		d_small_const_multiplier(
62	24062	NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))),
63	72186	d_small_const(d_small_const_multiplier)
64		{
65	12031	d_check_vts_lemma_lc = false;
66	12031	if (options().quantifiers.cegqiBv)
67		{
68		// if doing instantiation for BV, need the inverter class
69	9396	d_bv_invert.reset(new BvInverter);
70		}
71	12031	if (options().quantifiers.cegqiNestedQE)
72		{
73	30	d_nestedQe.reset(new NestedQe(d_env));
74		}
75	12031	}
76
77	24052	InstStrategyCegqi::~InstStrategyCegqi() {}
78
79	90476	bool InstStrategyCegqi::needsCheck(Theory::Effort e)
80		{
81	90476	return e>=Theory::EFFORT_LAST_CALL;
82		}
83
84	17656	QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
85		{
86	17656	size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers();
87	59831	for (size_t i = 0; i < nquant; i++)
88		{
89	88691	Node q = d_treg.getModel()->getAssertedQuantifier(i);
90	46516	if (doCbqi(q))
91		{
92	4341	return QEFFORT_STANDARD;
93		}
94		}
95	13315	return QEFFORT_NONE;
96		}
97
98	2103	bool InstStrategyCegqi::registerCbqiLemma(Node q)
99		{
100	2103	if( !hasAddedCbqiLemma( q ) ){
101	1933	NodeManager* nm = NodeManager::currentNM();
102	1933	d_added_cbqi_lemma.insert( q );
103	1933	Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
104		//add cbqi lemma
105		//get the counterexample literal
106	3866	Node ceLit = getCounterexampleLiteral(q);
107	3866	Node ceBody = d_qreg.getInstConstantBody(q);
108	1933	if( !ceBody.isNull() ){
109		//add counterexample lemma
110	3866	Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
111		//require any decision on cel to be phase=true
112	1933	d_qim.addPendingPhaseRequirement(ceLit, true);
113	1933	Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
114		//add counterexample lemma
115	1933	lem = rewrite(lem);
116	1933	Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
117	1934	registerCounterexampleLemma( q, lem );
118
119		//compute dependencies between quantified formulas
120	3864	std::vector<Node> ics;
121	1932	TermUtil::computeInstConstContains(q, ics);
122	1932	d_parent_quant[q].clear();
123	1932	d_children_quant[q].clear();
124	3864	std::vector<Node> dep;
125	2382	for (const Node& ic : ics)
126		{
127	900	Node qi = ic.getAttribute(InstConstantAttribute());
128	1350	if (std::find(d_parent_quant[q].begin(), d_parent_quant[q].end(), qi)
129	1350	== d_parent_quant[q].end())
130		{
131	280	d_parent_quant[q].push_back(qi);
132	280	d_children_quant[qi].push_back(q);
133		// may not have added the CEX lemma, but the literal is created by
134		// the following call regardless. One rare case where this can happen
135		// is if both sygus-inst and CEGQI are being run in parallel, and
136		// a parent quantified formula is not handled by CEGQI, but a child
137		// is.
138	560	Node qicel = getCounterexampleLiteral(qi);
139	280	dep.push_back(qi);
140	280	dep.push_back(qicel);
141		}
142		}
143	1932	if (!dep.empty())
144		{
145		// This lemma states that if the child is active, then the parent must
146		// be asserted, in particular G => Q where G is the CEX literal for the
147		// child and Q is the parent.
148	392	Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
149	392	Trace("cegqi-lemma")
150	196	<< "Counterexample dependency lemma : " << dep_lemma << std::endl;
151	196	d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP);
152		}
153
154		//must register all sub-quantifiers of counterexample lemma, register their lemmas
155	3864	std::vector< Node > quants;
156	1932	TermUtil::computeQuantContains( lem, quants );
157	2106	for( unsigned i=0; i<quants.size(); i++ ){
158	174	if( doCbqi( quants[i] ) ){
159	170	registerCbqiLemma( quants[i] );
160		}
161		}
162		}
163		// The decision strategy for this quantified formula ensures that its
164		// counterexample literal is decided on first. It is user-context dependent.
165		std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds =
166	1932	d_dstrat.find(q);
167	1932	DecisionStrategy* dlds = nullptr;
168	1932	if (itds == d_dstrat.end())
169		{
170	5796	d_dstrat[q].reset(new DecisionStrategySingleton(
171	3864	d_env, "CexLiteral", ceLit, d_qstate.getValuation()));
172	1932	dlds = d_dstrat[q].get();
173		}
174		else
175		{
176		dlds = itds->second.get();
177		}
178		// it is appended to the list of strategies
179	1932	d_qim.getDecisionManager()->registerStrategy(
180		DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
181	1932	return true;
182		}else{
183	170	return false;
184		}
185		}
186
187	34062	void InstStrategyCegqi::reset_round(Theory::Effort effort)
188		{
189	34062	d_cbqi_set_quant_inactive = false;
190	34062	d_incomplete_check = false;
191	34062	d_active_quant.clear();
192		//check if any cbqi lemma has not been added yet
193	34062	FirstOrderModel* fm = d_treg.getModel();
194	34062	size_t nquant = fm->getNumAssertedQuantifiers();
195	273776	for (size_t i = 0; i < nquant; i++)
196		{
197	479428	Node q = fm->getAssertedQuantifier(i);
198		//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
199	239714	if( doCbqi( q ) ){
200	9545	if (fm->isQuantifierActive(q))
201		{
202	9545	d_active_quant[q] = true;
203	9545	Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
204	19090	Node cel = getCounterexampleLiteral(q);
205		bool value;
206	9545	if (d_qstate.getValuation().hasSatValue(cel, value))
207		{
208	9521	Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
209	9521	if( !value ){
210	1456	if (d_qstate.getValuation().isDecision(cel))
211		{
212		Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
213		}else{
214	1456	Trace("cegqi") << "Inactive : " << q << std::endl;
215	1456	fm->setQuantifierActive(q, false);
216	1456	d_cbqi_set_quant_inactive = true;
217	1456	d_active_quant.erase( q );
218		}
219		}
220		}else{
221	24	Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
222		}
223		}
224		}
225		}
226
227		//refinement: only consider innermost active quantified formulas
228	34062	if (options().quantifiers.cegqiInnermost)
229		{
230	34062	if( !d_children_quant.empty() && !d_active_quant.empty() ){
231	6747	Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
232	13494	std::vector< Node > ninner;
233	14816	for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
234	8069	std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
235	8069	if( itc!=d_children_quant.end() ){
236	8371	for( unsigned j=0; j<itc->second.size(); j++ ){
237	492	if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
238	186	Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
239	186	ninner.push_back( it->first );
240	186	break;
241		}
242		}
243		}
244		}
245	6747	Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
246	6933	for( unsigned i=0; i<ninner.size(); i++ ){
247	186	Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
248	186	d_active_quant.erase( ninner[i] );
249		}
250	6747	Assert(!d_active_quant.empty());
251	6747	Trace("cegqi-debug") << "...done removing." << std::endl;
252		}
253		}
254	34062	d_check_vts_lemma_lc = false;
255	34062	}
256
257	52765	void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
258		{
259	52765	if (quant_e == QEFFORT_STANDARD)
260		{
261	17596	Assert(!d_qstate.isInConflict());
262	17596	double clSet = 0;
263	17596	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	17596	size_t lastWaiting = d_qim.numPendingLemmas();
268	44582	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	36172	for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
273	10166	Node q = it->first;
274	5083	Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
275	5083	process(q, e, ee);
276	5083	if (d_qstate.isInConflict())
277		{
278		break;
279		}
280		}
281	31089	if (d_qstate.isInConflict() \|\| d_qim.numPendingLemmas() > lastWaiting)
282		{
283	4103	break;
284		}
285		}
286	17596	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	52765	}
298
299	5481	bool InstStrategyCegqi::checkComplete(IncompleteId& incId)
300		{
301	10962	if ((!options().quantifiers.cegqiSat && d_cbqi_set_quant_inactive)
302	10962	\|\| d_incomplete_check)
303		{
304	64	incId = IncompleteId::QUANTIFIERS_CEGQI;
305	64	return false;
306		}
307		else
308		{
309	5417	return true;
310		}
311		}
312
313	1516	bool InstStrategyCegqi::checkCompleteFor(Node q)
314		{
315	1516	std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
316	1516	if( it!=d_do_cbqi.end() ){
317	1516	return it->second != CEG_UNHANDLED;
318		}else{
319		return false;
320		}
321		}
322
323	24331	void InstStrategyCegqi::checkOwnership(Node q)
324		{
325	24331	if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
326		{
327	1951	if (d_do_cbqi[q] == CEG_HANDLED)
328		{
329		//take full ownership of the quantified formula
330	1934	d_qreg.setOwner(q, this);
331		}
332		}
333	24331	}
334
335	24369	void InstStrategyCegqi::preRegisterQuantifier(Node q)
336		{
337	24369	if (doCbqi(q))
338		{
339	1951	if (processNestedQe(q, true))
340		{
341		// will process using nested quantifier elimination
342	18	return;
343		}
344		// register the cbqi lemma
345	1934	if( registerCbqiLemma( q ) ){
346	1762	Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
347		}
348		}
349		}
350	52236	TrustNode InstStrategyCegqi::rewriteInstantiation(
351		Node q, const std::vector<Node>& terms, Node inst, bool doVts)
352		{
353	104472	Node prevInst = inst;
354	52236	if (doVts)
355		{
356		// do virtual term substitution
357	77	inst = rewrite(inst);
358	77	Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
359	77	inst = d_vtsCache->rewriteVtsSymbols(inst);
360	77	Trace("quant-vts-debug") << "...got " << inst << std::endl;
361		}
362	52236	if (prevInst != inst)
363		{
364		// not proof producing yet
365	77	return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
366		}
367	52159	return TrustNode::null();
368		}
369
370	12031	InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
371		{
372	12031	return d_irew.get();
373		}
374
375	1933	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	3866	std::vector<Node> ce_vars;
380	5905	for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
381		i++)
382		{
383	3972	ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
384		}
385		// send the lemma
386	1934	d_qim.lemma(lem, InferenceId::QUANTIFIERS_CEGQI_CEX);
387		// get the preprocessed form of the lemma we just sent
388	3864	std::vector<Node> skolems;
389	3864	std::vector<Node> skAsserts;
390		Node ppLem =
391	3864	d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
392	3864	std::vector<Node> lemp{ppLem};
393	1932	lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
394	1932	ppLem = NodeManager::currentNM()->mkAnd(lemp);
395	3864	Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
396	1932	<< std::endl;
397	3864	std::vector<Node> auxLems;
398	1932	CegInstantiator* cinst = getInstantiator(q);
399	1932	cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
400	2071	for (size_t i = 0, size = auxLems.size(); i < size; i++)
401		{
402	278	Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
403	139	<< std::endl;
404	139	d_qim.addPendingLemma(auxLems[i], InferenceId::QUANTIFIERS_CEGQI_CEX_AUX);
405		}
406	1932	}
407
408	335104	bool InstStrategyCegqi::doCbqi(Node q)
409		{
410	335104	std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
411	335104	if( it==d_do_cbqi.end() ){
412	24331	CegHandledStatus ret = CegInstantiator::isCbqiQuant(q);
413	24331	Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
414	24331	d_do_cbqi[q] = ret;
415	24331	return ret != CEG_UNHANDLED;
416		}
417	310773	return it->second != CEG_UNHANDLED;
418		}
419
420	5083	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	5083	if (processNestedQe(q, false))
424		{
425		// don't need to process this, since it has been reduced
426	26	return;
427		}
428	5057	if( e==0 ){
429	4760	CegInstantiator * cinst = getInstantiator( q );
430	4760	Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
431	4760	d_curr_quant = q;
432	4760	if( !cinst->check() ){
433	300	d_incomplete_check = true;
434	300	d_check_vts_lemma_lc = true;
435		}
436	4760	d_curr_quant = Node::null();
437	297	}else if( e==1 ){
438		//minimize the free delta heuristically on demand
439	297	if( d_check_vts_lemma_lc ){
440	83	Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
441	83	d_check_vts_lemma_lc = false;
442	166	d_small_const = NodeManager::currentNM()->mkNode(
443	83	MULT, d_small_const, d_small_const_multiplier);
444	83	d_small_const = rewrite(d_small_const);
445		//heuristic for now, until we know how to do nested quantification
446	166	Node delta = d_vtsCache->getVtsDelta(true, false);
447	83	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	166	std::vector< Node > inf;
453	83	d_vtsCache->getVtsTerms(inf, true, false, false);
454	83	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	11758	Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
464		{
465	11758	std::map<Node, Node>::iterator it = d_ce_lit.find(q);
466	11758	if (it != d_ce_lit.end())
467		{
468	9811	return it->second;
469		}
470	1947	NodeManager * nm = NodeManager::currentNM();
471	1947	SkolemManager* sm = nm->getSkolemManager();
472	3894	Node g = sm->mkDummySkolem("g", nm->booleanType());
473		// ensure that it is a SAT literal
474	3894	Node ceLit = d_qstate.getValuation().ensureLiteral(g);
475	1947	d_ce_lit[q] = ceLit;
476	1947	return ceLit;
477		}
478
479	5952	bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
480	5952	Assert(!d_curr_quant.isNull());
481		// check if we need virtual term substitution (if used delta or infinity)
482	5952	bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
483	5952	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	5952	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	17853	else if (inst->addInstantiation(d_curr_quant,
493		subs,
494		InferenceId::QUANTIFIERS_INST_CEGQI,
495	11902	Node::null(),
496		false,
497		usedVts))
498		{
499	4459	return true;
500		}
501		// this should never happen for monotonic selection strategies
502	1492	Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
503	1492	return false;
504		}
505
506	6692	CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
507		std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
508	6692	d_cinst.find(q);
509	6692	if( it==d_cinst.end() ){
510	1932	d_cinst[q].reset(new CegInstantiator(d_env, q, d_qstate, d_treg, this));
511	1932	return d_cinst[q].get();
512		}
513	4760	return it->second.get();
514		}
515
516	2021	VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
517		{
518	2021	return d_vtsCache.get();
519		}
520
521	1224	BvInverter* InstStrategyCegqi::getBvInverter() const
522		{
523	1224	return d_bv_invert.get();
524		}
525
526	7034	bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
527		{
528	7034	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	6966	return false;
551		}
552
553		} // namespace quantifiers
554		} // namespace theory
555	31137	} // namespace cvc5