Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus_inst.cpp	Lines:	214	259	82.6 %
Date:	2021-09-13	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(Env& env,
                     QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
                     QuantifiersRegistry& qr,
                     TermRegistry& tr)
    : QuantifiersModule(env, qs, qim, qr, tr),
      d_ce_lemma_added(userContext()),
      d_global_terms(userContext()),
      d_notified_assertions(userContext())
{
}

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