Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus_inst.cpp	Lines:	214	259	82.6 %
Date:	2021-08-16	Branches:	374	1006	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, values, 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);
      values.push_back(value);

      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,
                                  nm->mkNode(kind::SEXPR, values)))
      {
        sendEvalUnfoldLemmas(eval_unfold_lemmas);
      }
    }
    else if (mode == options::SygusInstMode::PRIORITY_EVAL)
    {
      if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
      {
        inst->addInstantiation(q,
                               terms,
                               InferenceId::QUANTIFIERS_INST_SYQI,
                               nm->mkNode(kind::SEXPR, values));
      }
    }
    else
    {
      Assert(mode == options::SygusInstMode::INTERLEAVE);
      inst->addInstantiation(q,
                             terms,
                             InferenceId::QUANTIFIERS_INST_SYQI,
                             nm->mkNode(kind::SEXPR, values));
      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	44	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	88	if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX
55	44	&& options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
56		{
57	44	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	44	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	88	if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN
110	44	&& options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
111		{
112		return;
113		}
114
115	88	Trace("sygus-inst-term") << "Find minimal terms with type " << tn
116	44	<< " in: " << n << std::endl;
117
118	88	Node cur;
119	88	std::vector<TNode> visit;
120
121	44	visit.push_back(n);
122	80119	do
123		{
124	80163	cur = visit.back();
125	80163	visit.pop_back();
126
127	80163	auto it = cache.find(cur);
128	80163	if (it == cache.end())
129		{
130	10656	cache.emplace(cur, std::make_pair(false, false));
131	5328	if (!skip_quant \|\| cur.getKind() != kind::FORALL)
132		{
133	5328	visit.push_back(cur);
134	5328	visit.insert(visit.end(), cur.begin(), cur.end());
135		}
136		}
137		/* up-traversal */
138	74835	else if (!it->second.first)
139		{
140	5328	bool found_min_term = false;
141
142		/* Check if we found a minimal term in one of the children. */
143	25011	for (const Node& c : cur)
144		{
145	23411	found_min_term \|= cache[c].second;
146	23411	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	5328	if (cur.getType() == tn && !expr::hasBoundVar(cur) && !found_min_term)
152		{
153	145	terms.insert(cur);
154	145	found_min_term = true;
155	145	Trace("sygus-inst-term") << " found: " << cur << std::endl;
156		}
157
158	5328	it->second.first = true;
159	5328	it->second.second = found_min_term;
160		}
161	80163	} 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	124	void addSpecialValues(const TypeNode& tn,
172		std::map<TypeNode, std::unordered_set<Node>>& extra_cons)
173		{
174	124	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	124	}
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	408	bool SygusInst::needsCheck(Theory::Effort e)
197		{
198	408	return e >= Theory::EFFORT_LAST_CALL;
199		}
200
201	84	QuantifiersModule::QEffort SygusInst::needsModel(Theory::Effort e)
202		{
203	84	return QEFFORT_STANDARD;
204		}
205
206	84	void SygusInst::reset_round(Theory::Effort e)
207		{
208	84	d_active_quant.clear();
209	84	d_inactive_quant.clear();
210
211	84	FirstOrderModel* model = d_treg.getModel();
212	84	uint32_t nasserted = model->getNumAssertedQuantifiers();
213
214	198	for (uint32_t i = 0; i < nasserted; ++i)
215		{
216	228	Node q = model->getAssertedQuantifier(i);
217
218	114	if (model->isQuantifierActive(q))
219		{
220	90	d_active_quant.insert(q);
221	180	Node lit = getCeLiteral(q);
222
223		bool value;
224	90	if (d_qstate.getValuation().hasSatValue(lit, value))
225		{
226	90	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	84	}
240
241	173	void SygusInst::check(Theory::Effort e, QEffort quant_e)
242		{
243	173	Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;
244
245	173	if (quant_e != QEFFORT_STANDARD) return;
246
247	84	FirstOrderModel* model = d_treg.getModel();
248	84	Instantiate* inst = d_qim.getInstantiate();
249	84	TermDbSygus* db = d_treg.getTermDatabaseSygus();
250	168	SygusExplain syexplain(db);
251	84	NodeManager* nm = NodeManager::currentNM();
252	84	options::SygusInstMode mode = options::sygusInstMode();
253
254	171	for (const Node& q : d_active_quant)
255		{
256	87	const std::vector<Node>& inst_constants = d_inst_constants.at(q);
257	87	const std::vector<Node>& dt_evals = d_var_eval.at(q);
258	87	Assert(inst_constants.size() == dt_evals.size());
259	87	Assert(inst_constants.size() == q[0].getNumChildren());
260
261	174	std::vector<Node> terms, values, eval_unfold_lemmas;
262	765	for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
263		{
264	1356	Node dt_var = inst_constants[i];
265	1356	Node dt_eval = dt_evals[i];
266	1356	Node value = model->getValue(dt_var);
267	1356	Node t = datatypes::utils::sygusToBuiltin(value);
268	678	terms.push_back(t);
269	678	values.push_back(value);
270
271	1356	std::vector<Node> exp;
272	678	syexplain.getExplanationForEquality(dt_var, value, exp);
273	1356	Node lem;
274	678	if (exp.empty())
275		{
276		lem = dt_eval.eqNode(t);
277		}
278		else
279		{
280	2034	lem = nm->mkNode(kind::IMPLIES,
281	1356	exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
282	1356	dt_eval.eqNode(t));
283		}
284	678	eval_unfold_lemmas.push_back(lem);
285		}
286
287	87	if (mode == options::SygusInstMode::PRIORITY_INST)
288		{
289	174	if (!inst->addInstantiation(q,
290		terms,
291		InferenceId::QUANTIFIERS_INST_SYQI,
292	174	nm->mkNode(kind::SEXPR, values)))
293		{
294	48	sendEvalUnfoldLemmas(eval_unfold_lemmas);
295		}
296		}
297		else if (mode == options::SygusInstMode::PRIORITY_EVAL)
298		{
299		if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
300		{
301		inst->addInstantiation(q,
302		terms,
303		InferenceId::QUANTIFIERS_INST_SYQI,
304		nm->mkNode(kind::SEXPR, values));
305		}
306		}
307		else
308		{
309		Assert(mode == options::SygusInstMode::INTERLEAVE);
310		inst->addInstantiation(q,
311		terms,
312		InferenceId::QUANTIFIERS_INST_SYQI,
313		nm->mkNode(kind::SEXPR, values));
314		sendEvalUnfoldLemmas(eval_unfold_lemmas);
315		}
316		}
317		}
318
319	48	bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
320		{
321	48	bool added_lemma = false;
322	435	for (const Node& lem : lemmas)
323		{
324	387	Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
325	387	added_lemma \|=
326	774	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD);
327		}
328	48	return added_lemma;
329		}
330
331	3	bool SygusInst::checkCompleteFor(Node q)
332		{
333	3	return d_inactive_quant.find(q) != d_inactive_quant.end();
334		}
335
336	39	void SygusInst::registerQuantifier(Node q)
337		{
338	39	Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
339
340	39	Trace("sygus-inst") << "Register " << q << std::endl;
341
342	78	std::map<TypeNode, std::unordered_set<Node>> extra_cons;
343	78	std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
344	78	std::map<TypeNode, std::unordered_set<Node>> include_cons;
345	78	std::unordered_set<Node> term_irrelevant;
346
347		/* Collect relevant local ground terms for each variable type. */
348	78	if (options::sygusInstScope() == options::SygusInstScope::IN
349	39	\|\| options::sygusInstScope() == options::SygusInstScope::BOTH)
350		{
351	78	std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms;
352	163	for (const Node& var : q[0])
353		{
354	248	TypeNode tn = var.getType();
355
356		/* Collect relevant ground terms for type tn. */
357	124	if (relevant_terms.find(tn) == relevant_terms.end())
358		{
359	88	std::unordered_set<Node> terms;
360	88	std::unordered_set<TNode> cache_max;
361	88	std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
362
363	44	getMinGroundTerms(q, tn, terms, cache_min);
364	44	getMaxGroundTerms(q, tn, terms, cache_max);
365	44	relevant_terms.emplace(tn, terms);
366		}
367
368		/* Add relevant ground terms to grammar. */
369	124	auto& terms = relevant_terms[tn];
370	586	for (const auto& t : terms)
371		{
372	924	TypeNode ttn = t.getType();
373	462	extra_cons[ttn].insert(t);
374	462	Trace("sygus-inst") << "Adding (local) extra cons: " << t << std::endl;
375		}
376		}
377		}
378
379		/* Collect relevant global ground terms for each variable type. */
380	78	if (options::sygusInstScope() == options::SygusInstScope::OUT
381	39	\|\| options::sygusInstScope() == options::SygusInstScope::BOTH)
382		{
383		for (const Node& var : q[0])
384		{
385		TypeNode tn = var.getType();
386
387		/* Collect relevant ground terms for type tn. */
388		if (d_global_terms.find(tn) == d_global_terms.end())
389		{
390		std::unordered_set<Node> terms;
391		std::unordered_set<TNode> cache_max;
392		std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
393
394		for (const Node& a : d_notified_assertions)
395		{
396		getMinGroundTerms(a, tn, terms, cache_min, true);
397		getMaxGroundTerms(a, tn, terms, cache_max, true);
398		}
399		d_global_terms.insert(tn, terms);
400		}
401
402		/* Add relevant ground terms to grammar. */
403		auto it = d_global_terms.find(tn);
404		if (it != d_global_terms.end())
405		{
406		for (const auto& t : (*it).second)
407		{
408		TypeNode ttn = t.getType();
409		extra_cons[ttn].insert(t);
410		Trace("sygus-inst")
411		<< "Adding (global) extra cons: " << t << std::endl;
412		}
413		}
414		}
415		}
416
417		/* Construct grammar for each bound variable of 'q'. */
418	39	Trace("sygus-inst") << "Process variables of " << q << std::endl;
419	78	std::vector<TypeNode> types;
420	163	for (const Node& var : q[0])
421		{
422	124	addSpecialValues(var.getType(), extra_cons);
423	248	TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
424	248	Node(),
425	248	var.toString(),
426		extra_cons,
427		exclude_cons,
428		include_cons,
429	248	term_irrelevant);
430	124	types.push_back(tn);
431
432	248	Trace("sygus-inst") << "Construct (default) datatype for " << var
433	124	<< std::endl
434	124	<< tn << std::endl;
435		}
436
437	39	registerCeLemma(q, types);
438	39	}
439
440		/* Construct grammars for all bound variables of quantifier 'q'. Currently,
441		* we use the default grammar of the variable's type.
442		*/
443	39	void SygusInst::preRegisterQuantifier(Node q)
444		{
445	39	Trace("sygus-inst") << "preRegister " << q << std::endl;
446	39	addCeLemma(q);
447	39	}
448
449	20	void SygusInst::ppNotifyAssertions(const std::vector<Node>& assertions)
450		{
451	69	for (const Node& a : assertions)
452		{
453	49	d_notified_assertions.insert(a);
454		}
455	20	}
456
457		/*****************************************************************************/
458		/* private methods */
459		/*****************************************************************************/
460
461	129	Node SygusInst::getCeLiteral(Node q)
462		{
463	129	auto it = d_ce_lits.find(q);
464	129	if (it != d_ce_lits.end())
465		{
466	90	return it->second;
467		}
468
469	39	NodeManager* nm = NodeManager::currentNM();
470	39	SkolemManager* sm = nm->getSkolemManager();
471	78	Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType());
472	78	Node lit = d_qstate.getValuation().ensureLiteral(sk);
473	39	d_ce_lits[q] = lit;
474	39	return lit;
475		}
476
477	39	void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
478		{
479	39	Assert(q[0].getNumChildren() == types.size());
480	39	Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
481	39	Assert(d_inst_constants.find(q) == d_inst_constants.end());
482	39	Assert(d_var_eval.find(q) == d_var_eval.end());
483
484	39	Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl;
485
486		/* Generate counterexample lemma for 'q'. */
487	39	NodeManager* nm = NodeManager::currentNM();
488	39	TermDbSygus* db = d_treg.getTermDatabaseSygus();
489
490		/* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
491		* instantiation constant ic_i with type types[i] and wrap each ic_i in
492		* DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
493	78	std::vector<Node> evals;
494	78	std::vector<Node> inst_constants;
495	163	for (size_t i = 0, size = types.size(); i < size; ++i)
496		{
497	248	TypeNode tn = types[i];
498	248	TNode var = q[0][i];
499
500		/* Create the instantiation constant and set attribute accordingly. */
501	248	Node ic = nm->mkInstConstant(tn);
502		InstConstantAttribute ica;
503	124	ic.setAttribute(ica, q);
504	124	Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;
505
506	124	db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
507
508	248	std::vector<Node> args = {ic};
509	248	Node svl = tn.getDType().getSygusVarList();
510	124	if (!svl.isNull())
511		{
512		args.insert(args.end(), svl.begin(), svl.end());
513		}
514	248	Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);
515
516	124	inst_constants.push_back(ic);
517	124	evals.push_back(eval);
518		}
519
520	39	d_inst_constants.emplace(q, inst_constants);
521	39	d_var_eval.emplace(q, evals);
522
523	78	Node lit = getCeLiteral(q);
524	39	d_qim.addPendingPhaseRequirement(lit, true);
525
526		/* The decision strategy for quantified formula 'q' ensures that its
527		* counterexample literal is decided on first. It is user-context dependent.
528		*/
529	39	Assert(d_dstrat.find(q) == d_dstrat.end());
530		DecisionStrategy* ds = new DecisionStrategySingleton(
531	39	"CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
532
533	39	d_dstrat[q].reset(ds);
534	39	d_qim.getDecisionManager()->registerStrategy(
535		DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);
536
537		/* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
538		Node body =
539	78	q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end());
540	78	Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
541	39	lem = Rewriter::rewrite(lem);
542
543	39	d_ce_lemmas.emplace(std::make_pair(q, lem));
544	39	Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl;
545	39	}
546
547	39	void SygusInst::addCeLemma(Node q)
548		{
549	39	Assert(d_ce_lemmas.find(q) != d_ce_lemmas.end());
550
551		/* Already added in previous contexts. */
552	39	if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
553
554	78	Node lem = d_ce_lemmas[q];
555	39	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_CEX);
556	39	d_ce_lemma_added.insert(q);
557	39	Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
558		}
559
560		} // namespace quantifiers
561		} // namespace theory
562	29340	} // namespace cvc5