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-05	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(QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
                                     TermRegistry& tr)
    : QuantifiersModule(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(qs.getEnv()));
  }
}

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