Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus_inst.cpp	Lines:	212	255	83.1 %
Date:	2021-05-22	Branches:	379	1020	37.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Andrew Reynolds, 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.
 * ****************************************************************************
 *
 * SyGuS instantiator class.
 */

#include "theory/quantifiers/sygus_inst.h"

#include <sstream>
#include <unordered_set>

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/sygus/sygus_enumerator.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

namespace {

/**
 * Collect maximal ground terms with type tn in node n.
 *
 * @param n: Node to traverse.
 * @param tn: Collects only terms with type tn.
 * @param terms: Collected terms.
 * @param cache: Caches visited nodes.
 * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
 */
void getMaxGroundTerms(TNode n,
                       TypeNode tn,
                       std::unordered_set<Node>& terms,
                       std::unordered_set<TNode>& cache,
                       bool skip_quant = false)
{
  if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX
      && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
  {
    return;
  }

  Trace("sygus-inst-term") << "Find maximal terms with type " << tn
                           << " in: " << n << std::endl;

  Node cur;
  std::vector<TNode> visit;

  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();

    if (cache.find(cur) != cache.end())
    {
      continue;
    }
    cache.insert(cur);

    if (expr::hasBoundVar(cur) || cur.getType() != tn)
    {
      if (!skip_quant || cur.getKind() != kind::FORALL)
      {
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    else
    {
      terms.insert(cur);
      Trace("sygus-inst-term") << "  found: " << cur << std::endl;
    }
  } while (!visit.empty());
}

/*
 * Collect minimal ground terms with type tn in node n.
 *
 * @param n: Node to traverse.
 * @param tn: Collects only terms with type tn.
 * @param terms: Collected terms.
 * @param cache: Caches visited nodes and flags indicating whether a minimal
 *               term was already found in a subterm.
 * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
 */
void getMinGroundTerms(TNode n,
                       TypeNode tn,
                       std::unordered_set<Node>& terms,
                       std::unordered_map<TNode, std::pair<bool, bool>>& cache,
                       bool skip_quant = false)
{
  if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN
      && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
  {
    return;
  }

  Trace("sygus-inst-term") << "Find minimal terms with type " << tn
                           << " in: " << n << std::endl;

  Node cur;
  std::vector<TNode> visit;

  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();

    auto it = cache.find(cur);
    if (it == cache.end())
    {
      cache.emplace(cur, std::make_pair(false, false));
      if (!skip_quant || cur.getKind() != kind::FORALL)
      {
        visit.push_back(cur);
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    /* up-traversal */
    else if (!it->second.first)
    {
      bool found_min_term = false;

      /* Check if we found a minimal term in one of the children. */
      for (const Node& c : cur)
      {
        found_min_term |= cache[c].second;
        if (found_min_term) break;
      }

      /* If we haven't found a minimal term yet, add this term if it has the
       * right type. */
      if (cur.getType() == tn && !expr::hasBoundVar(cur) && !found_min_term)
      {
        terms.insert(cur);
        found_min_term = true;
        Trace("sygus-inst-term") << "  found: " << cur << std::endl;
      }

      it->second.first = true;
      it->second.second = found_min_term;
    }
  } while (!visit.empty());
}

/*
 * Add special values for a given type.
 *
 * @param tn: The type node.
 * @param extra_cons: A map of TypeNode to constants, which are added in
 *                    addition to the default grammar.
 */
void addSpecialValues(const TypeNode& tn,
                      std::map<TypeNode, std::unordered_set<Node>>& extra_cons)
{
  if (tn.isBitVector())
  {
    uint32_t size = tn.getBitVectorSize();
    extra_cons[tn].insert(bv::utils::mkOnes(size));
    extra_cons[tn].insert(bv::utils::mkMinSigned(size));
    extra_cons[tn].insert(bv::utils::mkMaxSigned(size));
  }
}

}  // namespace

SygusInst::SygusInst(QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
                     QuantifiersRegistry& qr,
                     TermRegistry& tr)
    : QuantifiersModule(qs, qim, qr, tr),
      d_ce_lemma_added(qs.getUserContext()),
      d_global_terms(qs.getUserContext()),
      d_notified_assertions(qs.getUserContext())
{
}

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

QuantifiersModule::QEffort SygusInst::needsModel(Theory::Effort e)
{
  return QEFFORT_STANDARD;
}

void SygusInst::reset_round(Theory::Effort e)
{
  d_active_quant.clear();
  d_inactive_quant.clear();

  FirstOrderModel* model = d_treg.getModel();
  uint32_t nasserted = model->getNumAssertedQuantifiers();

  for (uint32_t i = 0; i < nasserted; ++i)
  {
    Node q = model->getAssertedQuantifier(i);

    if (model->isQuantifierActive(q))
    {
      d_active_quant.insert(q);
      Node lit = getCeLiteral(q);

      bool value;
      if (d_qstate.getValuation().hasSatValue(lit, value))
      {
        if (!value)
        {
          if (!d_qstate.getValuation().isDecision(lit))
          {
            model->setQuantifierActive(q, false);
            d_active_quant.erase(q);
            d_inactive_quant.insert(q);
            Trace("sygus-inst") << "Set inactive: " << q << std::endl;
          }
        }
      }
    }
  }
}

void SygusInst::check(Theory::Effort e, QEffort quant_e)
{
  Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;

  if (quant_e != QEFFORT_STANDARD) return;

  FirstOrderModel* model = d_treg.getModel();
  Instantiate* inst = d_qim.getInstantiate();
  TermDbSygus* db = d_treg.getTermDatabaseSygus();
  SygusExplain syexplain(db);
  NodeManager* nm = NodeManager::currentNM();
  options::SygusInstMode mode = options::sygusInstMode();

  for (const Node& q : d_active_quant)
  {
    const std::vector<Node>& inst_constants = d_inst_constants.at(q);
    const std::vector<Node>& dt_evals = d_var_eval.at(q);
    Assert(inst_constants.size() == dt_evals.size());
    Assert(inst_constants.size() == q[0].getNumChildren());

    std::vector<Node> terms, eval_unfold_lemmas;
    for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
    {
      Node dt_var = inst_constants[i];
      Node dt_eval = dt_evals[i];
      Node value = model->getValue(dt_var);
      Node t = datatypes::utils::sygusToBuiltin(value);
      terms.push_back(t);

      std::vector<Node> exp;
      syexplain.getExplanationForEquality(dt_var, value, exp);
      Node lem;
      if (exp.empty())
      {
        lem = dt_eval.eqNode(t);
      }
      else
      {
        lem = nm->mkNode(kind::IMPLIES,
                         exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
                         dt_eval.eqNode(t));
      }
      eval_unfold_lemmas.push_back(lem);
    }

    if (mode == options::SygusInstMode::PRIORITY_INST)
    {
      if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI))
      {
        sendEvalUnfoldLemmas(eval_unfold_lemmas);
      }
    }
    else if (mode == options::SygusInstMode::PRIORITY_EVAL)
    {
      if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
      {
        inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
      }
    }
    else
    {
      Assert(mode == options::SygusInstMode::INTERLEAVE);
      inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
      sendEvalUnfoldLemmas(eval_unfold_lemmas);
    }
  }
}

bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
{
  bool added_lemma = false;
  for (const Node& lem : lemmas)
  {
    Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
    added_lemma |=
        d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD);
  }
  return added_lemma;
}

bool SygusInst::checkCompleteFor(Node q)
{
  return d_inactive_quant.find(q) != d_inactive_quant.end();
}

void SygusInst::registerQuantifier(Node q)
{
  Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());

  Trace("sygus-inst") << "Register " << q << std::endl;

  std::map<TypeNode, std::unordered_set<Node>> extra_cons;
  std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
  std::map<TypeNode, std::unordered_set<Node>> include_cons;
  std::unordered_set<Node> term_irrelevant;

  /* Collect relevant local ground terms for each variable type. */
  if (options::sygusInstScope() == options::SygusInstScope::IN
      || options::sygusInstScope() == options::SygusInstScope::BOTH)
  {
    std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms;
    for (const Node& var : q[0])
    {
      TypeNode tn = var.getType();

      /* Collect relevant ground terms for type tn. */
      if (relevant_terms.find(tn) == relevant_terms.end())
      {
        std::unordered_set<Node> terms;
        std::unordered_set<TNode> cache_max;
        std::unordered_map<TNode, std::pair<bool, bool>> cache_min;

        getMinGroundTerms(q, tn, terms, cache_min);
        getMaxGroundTerms(q, tn, terms, cache_max);
        relevant_terms.emplace(tn, terms);
      }

      /* Add relevant ground terms to grammar. */
      auto& terms = relevant_terms[tn];
      for (const auto& t : terms)
      {
        TypeNode ttn = t.getType();
        extra_cons[ttn].insert(t);
        Trace("sygus-inst") << "Adding (local) extra cons: " << t << std::endl;
      }
    }
  }

  /* Collect relevant global ground terms for each variable type. */
  if (options::sygusInstScope() == options::SygusInstScope::OUT
      || options::sygusInstScope() == options::SygusInstScope::BOTH)
  {
    for (const Node& var : q[0])
    {
      TypeNode tn = var.getType();

      /* Collect relevant ground terms for type tn. */
      if (d_global_terms.find(tn) == d_global_terms.end())
      {
        std::unordered_set<Node> terms;
        std::unordered_set<TNode> cache_max;
        std::unordered_map<TNode, std::pair<bool, bool>> cache_min;

        for (const Node& a : d_notified_assertions)
        {
          getMinGroundTerms(a, tn, terms, cache_min, true);
          getMaxGroundTerms(a, tn, terms, cache_max, true);
        }
        d_global_terms.insert(tn, terms);
      }

      /* Add relevant ground terms to grammar. */
      auto it = d_global_terms.find(tn);
      if (it != d_global_terms.end())
      {
        for (const auto& t : (*it).second)
        {
          TypeNode ttn = t.getType();
          extra_cons[ttn].insert(t);
          Trace("sygus-inst")
              << "Adding (global) extra cons: " << t << std::endl;
        }
      }
    }
  }

  /* Construct grammar for each bound variable of 'q'. */
  Trace("sygus-inst") << "Process variables of " << q << std::endl;
  std::vector<TypeNode> types;
  for (const Node& var : q[0])
  {
    addSpecialValues(var.getType(), extra_cons);
    TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
                                                            Node(),
                                                            var.toString(),
                                                            extra_cons,
                                                            exclude_cons,
                                                            include_cons,
                                                            term_irrelevant);
    types.push_back(tn);

    Trace("sygus-inst") << "Construct (default) datatype for " << var
                        << std::endl
                        << tn << std::endl;
  }

  registerCeLemma(q, types);
}

/* Construct grammars for all bound variables of quantifier 'q'. Currently,
 * we use the default grammar of the variable's type.
 */
void SygusInst::preRegisterQuantifier(Node q)
{
  Trace("sygus-inst") << "preRegister " << q << std::endl;
  addCeLemma(q);
}

void SygusInst::ppNotifyAssertions(const std::vector<Node>& assertions)
{
  for (const Node& a : assertions)
  {
    d_notified_assertions.insert(a);
  }
}

/*****************************************************************************/
/* private methods                                                           */
/*****************************************************************************/

Node SygusInst::getCeLiteral(Node q)
{
  auto it = d_ce_lits.find(q);
  if (it != d_ce_lits.end())
  {
    return it->second;
  }

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType());
  Node lit = d_qstate.getValuation().ensureLiteral(sk);
  d_ce_lits[q] = lit;
  return lit;
}

void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
{
  Assert(q[0].getNumChildren() == types.size());
  Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
  Assert(d_inst_constants.find(q) == d_inst_constants.end());
  Assert(d_var_eval.find(q) == d_var_eval.end());

  Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl;

  /* Generate counterexample lemma for 'q'. */
  NodeManager* nm = NodeManager::currentNM();
  TermDbSygus* db = d_treg.getTermDatabaseSygus();

  /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
   * instantiation constant ic_i with type types[i] and wrap each ic_i in
   * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
  std::vector<Node> evals;
  std::vector<Node> inst_constants;
  for (size_t i = 0, size = types.size(); i < size; ++i)
  {
    TypeNode tn = types[i];
    TNode var = q[0][i];

    /* Create the instantiation constant and set attribute accordingly. */
    Node ic = nm->mkInstConstant(tn);
    InstConstantAttribute ica;
    ic.setAttribute(ica, q);
    Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;

    db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);

    std::vector<Node> args = {ic};
    Node svl = tn.getDType().getSygusVarList();
    if (!svl.isNull())
    {
      args.insert(args.end(), svl.begin(), svl.end());
    }
    Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);

    inst_constants.push_back(ic);
    evals.push_back(eval);
  }

  d_inst_constants.emplace(q, inst_constants);
  d_var_eval.emplace(q, evals);

  Node lit = getCeLiteral(q);
  d_qim.addPendingPhaseRequirement(lit, true);

  /* The decision strategy for quantified formula 'q' ensures that its
   * counterexample literal is decided on first. It is user-context dependent.
   */
  Assert(d_dstrat.find(q) == d_dstrat.end());
  DecisionStrategy* ds = new DecisionStrategySingleton(
      "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());

  d_dstrat[q].reset(ds);
  d_qim.getDecisionManager()->registerStrategy(
      DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);

  /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
  Node body =
      q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end());
  Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
  lem = Rewriter::rewrite(lem);

  d_ce_lemmas.emplace(std::make_pair(q, lem));
  Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl;
}

void SygusInst::addCeLemma(Node q)
{
  Assert(d_ce_lemmas.find(q) != d_ce_lemmas.end());

  /* Already added in previous contexts. */
  if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;

  Node lem = d_ce_lemmas[q];
  d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_CEX);
  d_ce_lemma_added.insert(q);
  Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Andrew Reynolds, 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		* SyGuS instantiator class.
14		*/
15
16		#include "theory/quantifiers/sygus_inst.h"
17
18		#include <sstream>
19		#include <unordered_set>
20
21		#include "expr/node_algorithm.h"
22		#include "expr/skolem_manager.h"
23		#include "options/quantifiers_options.h"
24		#include "theory/bv/theory_bv_utils.h"
25		#include "theory/datatypes/sygus_datatype_utils.h"
26		#include "theory/quantifiers/first_order_model.h"
27		#include "theory/quantifiers/sygus/sygus_enumerator.h"
28		#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
29		#include "theory/quantifiers/sygus/synth_engine.h"
30		#include "theory/quantifiers/term_util.h"
31		#include "theory/rewriter.h"
32
33		namespace cvc5 {
34		namespace theory {
35		namespace quantifiers {
36
37		namespace {
38
39		/**
40		* Collect maximal ground terms with type tn in node n.
41		*
42		* @param n: Node to traverse.
43		* @param tn: Collects only terms with type tn.
44		* @param terms: Collected terms.
45		* @param cache: Caches visited nodes.
46		* @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
47		*/
48	45	void getMaxGroundTerms(TNode n,
49		TypeNode tn,
50		std::unordered_set<Node>& terms,
51		std::unordered_set<TNode>& cache,
52		bool skip_quant = false)
53		{
54	225	if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX
55	45	&& options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
56		{
57	45	return;
58		}
59
60		Trace("sygus-inst-term") << "Find maximal terms with type " << tn
61		<< " in: " << n << std::endl;
62
63		Node cur;
64		std::vector<TNode> visit;
65
66		visit.push_back(n);
67		do
68		{
69		cur = visit.back();
70		visit.pop_back();
71
72		if (cache.find(cur) != cache.end())
73		{
74		continue;
75		}
76		cache.insert(cur);
77
78		if (expr::hasBoundVar(cur) \|\| cur.getType() != tn)
79		{
80		if (!skip_quant \|\| cur.getKind() != kind::FORALL)
81		{
82		visit.insert(visit.end(), cur.begin(), cur.end());
83		}
84		}
85		else
86		{
87		terms.insert(cur);
88		Trace("sygus-inst-term") << " found: " << cur << std::endl;
89		}
90		} while (!visit.empty());
91		}
92
93		/*
94		* Collect minimal ground terms with type tn in node n.
95		*
96		* @param n: Node to traverse.
97		* @param tn: Collects only terms with type tn.
98		* @param terms: Collected terms.
99		* @param cache: Caches visited nodes and flags indicating whether a minimal
100		* term was already found in a subterm.
101		* @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
102		*/
103	45	void getMinGroundTerms(TNode n,
104		TypeNode tn,
105		std::unordered_set<Node>& terms,
106		std::unordered_map<TNode, std::pair<bool, bool>>& cache,
107		bool skip_quant = false)
108		{
109	90	if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN
110	45	&& options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
111		{
112		return;
113		}
114
115	90	Trace("sygus-inst-term") << "Find minimal terms with type " << tn
116	45	<< " in: " << n << std::endl;
117
118	90	Node cur;
119	90	std::vector<TNode> visit;
120
121	45	visit.push_back(n);
122	80138	do
123		{
124	80183	cur = visit.back();
125	80183	visit.pop_back();
126
127	80183	auto it = cache.find(cur);
128	80183	if (it == cache.end())
129		{
130	10674	cache.emplace(cur, std::make_pair(false, false));
131	5337	if (!skip_quant \|\| cur.getKind() != kind::FORALL)
132		{
133	5337	visit.push_back(cur);
134	5337	visit.insert(visit.end(), cur.begin(), cur.end());
135		}
136		}
137		/* up-traversal */
138	74846	else if (!it->second.first)
139		{
140	5337	bool found_min_term = false;
141
142		/* Check if we found a minimal term in one of the children. */
143	25034	for (const Node& c : cur)
144		{
145	23430	found_min_term \|= cache[c].second;
146	23430	if (found_min_term) break;
147		}
148
149		/* If we haven't found a minimal term yet, add this term if it has the
150		* right type. */
151	5337	if (cur.getType() == tn && !expr::hasBoundVar(cur) && !found_min_term)
152		{
153	147	terms.insert(cur);
154	147	found_min_term = true;
155	147	Trace("sygus-inst-term") << " found: " << cur << std::endl;
156		}
157
158	5337	it->second.first = true;
159	5337	it->second.second = found_min_term;
160		}
161	80183	} while (!visit.empty());
162		}
163
164		/*
165		* Add special values for a given type.
166		*
167		* @param tn: The type node.
168		* @param extra_cons: A map of TypeNode to constants, which are added in
169		* addition to the default grammar.
170		*/
171	125	void addSpecialValues(const TypeNode& tn,
172		std::map<TypeNode, std::unordered_set<Node>>& extra_cons)
173		{
174	125	if (tn.isBitVector())
175		{
176	6	uint32_t size = tn.getBitVectorSize();
177	6	extra_cons[tn].insert(bv::utils::mkOnes(size));
178	6	extra_cons[tn].insert(bv::utils::mkMinSigned(size));
179	6	extra_cons[tn].insert(bv::utils::mkMaxSigned(size));
180		}
181	125	}
182
183		} // namespace
184
185	20	SygusInst::SygusInst(QuantifiersState& qs,
186		QuantifiersInferenceManager& qim,
187		QuantifiersRegistry& qr,
188	20	TermRegistry& tr)
189		: QuantifiersModule(qs, qim, qr, tr),
190	20	d_ce_lemma_added(qs.getUserContext()),
191	20	d_global_terms(qs.getUserContext()),
192	60	d_notified_assertions(qs.getUserContext())
193		{
194	20	}
195
196	429	bool SygusInst::needsCheck(Theory::Effort e)
197		{
198	429	return e >= Theory::EFFORT_LAST_CALL;
199		}
200
201	87	QuantifiersModule::QEffort SygusInst::needsModel(Theory::Effort e)
202		{
203	87	return QEFFORT_STANDARD;
204		}
205
206	87	void SygusInst::reset_round(Theory::Effort e)
207		{
208	87	d_active_quant.clear();
209	87	d_inactive_quant.clear();
210
211	87	FirstOrderModel* model = d_treg.getModel();
212	87	uint32_t nasserted = model->getNumAssertedQuantifiers();
213
214	207	for (uint32_t i = 0; i < nasserted; ++i)
215		{
216	240	Node q = model->getAssertedQuantifier(i);
217
218	120	if (model->isQuantifierActive(q))
219		{
220	91	d_active_quant.insert(q);
221	182	Node lit = getCeLiteral(q);
222
223		bool value;
224	91	if (d_qstate.getValuation().hasSatValue(lit, value))
225		{
226	91	if (!value)
227		{
228	3	if (!d_qstate.getValuation().isDecision(lit))
229		{
230	3	model->setQuantifierActive(q, false);
231	3	d_active_quant.erase(q);
232	3	d_inactive_quant.insert(q);
233	3	Trace("sygus-inst") << "Set inactive: " << q << std::endl;
234		}
235		}
236		}
237		}
238		}
239	87	}
240
241	181	void SygusInst::check(Theory::Effort e, QEffort quant_e)
242		{
243	181	Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;
244
245	181	if (quant_e != QEFFORT_STANDARD) return;
246
247	87	FirstOrderModel* model = d_treg.getModel();
248	87	Instantiate* inst = d_qim.getInstantiate();
249	87	TermDbSygus* db = d_treg.getTermDatabaseSygus();
250	174	SygusExplain syexplain(db);
251	87	NodeManager* nm = NodeManager::currentNM();
252	174	options::SygusInstMode mode = options::sygusInstMode();
253
254	175	for (const Node& q : d_active_quant)
255		{
256	88	const std::vector<Node>& inst_constants = d_inst_constants.at(q);
257	88	const std::vector<Node>& dt_evals = d_var_eval.at(q);
258	88	Assert(inst_constants.size() == dt_evals.size());
259	88	Assert(inst_constants.size() == q[0].getNumChildren());
260
261	176	std::vector<Node> terms, eval_unfold_lemmas;
262	767	for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
263		{
264	1358	Node dt_var = inst_constants[i];
265	1358	Node dt_eval = dt_evals[i];
266	1358	Node value = model->getValue(dt_var);
267	1358	Node t = datatypes::utils::sygusToBuiltin(value);
268	679	terms.push_back(t);
269
270	1358	std::vector<Node> exp;
271	679	syexplain.getExplanationForEquality(dt_var, value, exp);
272	1358	Node lem;
273	679	if (exp.empty())
274		{
275		lem = dt_eval.eqNode(t);
276		}
277		else
278		{
279	2037	lem = nm->mkNode(kind::IMPLIES,
280	1358	exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
281	1358	dt_eval.eqNode(t));
282		}
283	679	eval_unfold_lemmas.push_back(lem);
284		}
285
286	88	if (mode == options::SygusInstMode::PRIORITY_INST)
287		{
288	88	if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI))
289		{
290	50	sendEvalUnfoldLemmas(eval_unfold_lemmas);
291		}
292		}
293		else if (mode == options::SygusInstMode::PRIORITY_EVAL)
294		{
295		if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
296		{
297		inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
298		}
299		}
300		else
301		{
302		Assert(mode == options::SygusInstMode::INTERLEAVE);
303		inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
304		sendEvalUnfoldLemmas(eval_unfold_lemmas);
305		}
306		}
307		}
308
309	50	bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
310		{
311	50	bool added_lemma = false;
312	489	for (const Node& lem : lemmas)
313		{
314	439	Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
315	439	added_lemma \|=
316	878	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD);
317		}
318	50	return added_lemma;
319		}
320
321	3	bool SygusInst::checkCompleteFor(Node q)
322		{
323	3	return d_inactive_quant.find(q) != d_inactive_quant.end();
324		}
325
326	40	void SygusInst::registerQuantifier(Node q)
327		{
328	40	Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
329
330	40	Trace("sygus-inst") << "Register " << q << std::endl;
331
332	80	std::map<TypeNode, std::unordered_set<Node>> extra_cons;
333	80	std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
334	80	std::map<TypeNode, std::unordered_set<Node>> include_cons;
335	80	std::unordered_set<Node> term_irrelevant;
336
337		/* Collect relevant local ground terms for each variable type. */
338	200	if (options::sygusInstScope() == options::SygusInstScope::IN
339	40	\|\| options::sygusInstScope() == options::SygusInstScope::BOTH)
340		{
341	80	std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms;
342	165	for (const Node& var : q[0])
343		{
344	250	TypeNode tn = var.getType();
345
346		/* Collect relevant ground terms for type tn. */
347	125	if (relevant_terms.find(tn) == relevant_terms.end())
348		{
349	90	std::unordered_set<Node> terms;
350	90	std::unordered_set<TNode> cache_max;
351	90	std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
352
353	45	getMinGroundTerms(q, tn, terms, cache_min);
354	45	getMaxGroundTerms(q, tn, terms, cache_max);
355	45	relevant_terms.emplace(tn, terms);
356		}
357
358		/* Add relevant ground terms to grammar. */
359	125	auto& terms = relevant_terms[tn];
360	589	for (const auto& t : terms)
361		{
362	928	TypeNode ttn = t.getType();
363	464	extra_cons[ttn].insert(t);
364	464	Trace("sygus-inst") << "Adding (local) extra cons: " << t << std::endl;
365		}
366		}
367		}
368
369		/* Collect relevant global ground terms for each variable type. */
370	80	if (options::sygusInstScope() == options::SygusInstScope::OUT
371	40	\|\| options::sygusInstScope() == options::SygusInstScope::BOTH)
372		{
373		for (const Node& var : q[0])
374		{
375		TypeNode tn = var.getType();
376
377		/* Collect relevant ground terms for type tn. */
378		if (d_global_terms.find(tn) == d_global_terms.end())
379		{
380		std::unordered_set<Node> terms;
381		std::unordered_set<TNode> cache_max;
382		std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
383
384		for (const Node& a : d_notified_assertions)
385		{
386		getMinGroundTerms(a, tn, terms, cache_min, true);
387		getMaxGroundTerms(a, tn, terms, cache_max, true);
388		}
389		d_global_terms.insert(tn, terms);
390		}
391
392		/* Add relevant ground terms to grammar. */
393		auto it = d_global_terms.find(tn);
394		if (it != d_global_terms.end())
395		{
396		for (const auto& t : (*it).second)
397		{
398		TypeNode ttn = t.getType();
399		extra_cons[ttn].insert(t);
400		Trace("sygus-inst")
401		<< "Adding (global) extra cons: " << t << std::endl;
402		}
403		}
404		}
405		}
406
407		/* Construct grammar for each bound variable of 'q'. */
408	40	Trace("sygus-inst") << "Process variables of " << q << std::endl;
409	80	std::vector<TypeNode> types;
410	165	for (const Node& var : q[0])
411		{
412	125	addSpecialValues(var.getType(), extra_cons);
413	250	TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
414	250	Node(),
415	250	var.toString(),
416		extra_cons,
417		exclude_cons,
418		include_cons,
419	250	term_irrelevant);
420	125	types.push_back(tn);
421
422	250	Trace("sygus-inst") << "Construct (default) datatype for " << var
423	125	<< std::endl
424	125	<< tn << std::endl;
425		}
426
427	40	registerCeLemma(q, types);
428	40	}
429
430		/* Construct grammars for all bound variables of quantifier 'q'. Currently,
431		* we use the default grammar of the variable's type.
432		*/
433	40	void SygusInst::preRegisterQuantifier(Node q)
434		{
435	40	Trace("sygus-inst") << "preRegister " << q << std::endl;
436	40	addCeLemma(q);
437	40	}
438
439	20	void SygusInst::ppNotifyAssertions(const std::vector<Node>& assertions)
440		{
441	69	for (const Node& a : assertions)
442		{
443	49	d_notified_assertions.insert(a);
444		}
445	20	}
446
447		/*****************************************************************************/
448		/* private methods */
449		/*****************************************************************************/
450
451	131	Node SygusInst::getCeLiteral(Node q)
452		{
453	131	auto it = d_ce_lits.find(q);
454	131	if (it != d_ce_lits.end())
455		{
456	91	return it->second;
457		}
458
459	40	NodeManager* nm = NodeManager::currentNM();
460	40	SkolemManager* sm = nm->getSkolemManager();
461	80	Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType());
462	80	Node lit = d_qstate.getValuation().ensureLiteral(sk);
463	40	d_ce_lits[q] = lit;
464	40	return lit;
465		}
466
467	40	void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
468		{
469	40	Assert(q[0].getNumChildren() == types.size());
470	40	Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
471	40	Assert(d_inst_constants.find(q) == d_inst_constants.end());
472	40	Assert(d_var_eval.find(q) == d_var_eval.end());
473
474	40	Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl;
475
476		/* Generate counterexample lemma for 'q'. */
477	40	NodeManager* nm = NodeManager::currentNM();
478	40	TermDbSygus* db = d_treg.getTermDatabaseSygus();
479
480		/* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
481		* instantiation constant ic_i with type types[i] and wrap each ic_i in
482		* DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
483	80	std::vector<Node> evals;
484	80	std::vector<Node> inst_constants;
485	165	for (size_t i = 0, size = types.size(); i < size; ++i)
486		{
487	250	TypeNode tn = types[i];
488	250	TNode var = q[0][i];
489
490		/* Create the instantiation constant and set attribute accordingly. */
491	250	Node ic = nm->mkInstConstant(tn);
492		InstConstantAttribute ica;
493	125	ic.setAttribute(ica, q);
494	125	Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;
495
496	125	db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
497
498	250	std::vector<Node> args = {ic};
499	250	Node svl = tn.getDType().getSygusVarList();
500	125	if (!svl.isNull())
501		{
502		args.insert(args.end(), svl.begin(), svl.end());
503		}
504	250	Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);
505
506	125	inst_constants.push_back(ic);
507	125	evals.push_back(eval);
508		}
509
510	40	d_inst_constants.emplace(q, inst_constants);
511	40	d_var_eval.emplace(q, evals);
512
513	80	Node lit = getCeLiteral(q);
514	40	d_qim.addPendingPhaseRequirement(lit, true);
515
516		/* The decision strategy for quantified formula 'q' ensures that its
517		* counterexample literal is decided on first. It is user-context dependent.
518		*/
519	40	Assert(d_dstrat.find(q) == d_dstrat.end());
520		DecisionStrategy* ds = new DecisionStrategySingleton(
521	40	"CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
522
523	40	d_dstrat[q].reset(ds);
524	40	d_qim.getDecisionManager()->registerStrategy(
525		DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);
526
527		/* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
528		Node body =
529	80	q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end());
530	80	Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
531	40	lem = Rewriter::rewrite(lem);
532
533	40	d_ce_lemmas.emplace(std::make_pair(q, lem));
534	40	Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl;
535	40	}
536
537	40	void SygusInst::addCeLemma(Node q)
538		{
539	40	Assert(d_ce_lemmas.find(q) != d_ce_lemmas.end());
540
541		/* Already added in previous contexts. */
542	40	if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
543
544	80	Node lem = d_ce_lemmas[q];
545	40	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_CEX);
546	40	d_ce_lemma_added.insert(q);
547	40	Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
548		}
549
550		} // namespace quantifiers
551		} // namespace theory
552	28194	} // namespace cvc5