Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_eval_unfold.cpp	Lines:	180	185	97.3 %
Date:	2021-05-22	Branches:	392	934	42.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of sygus_eval_unfold.
 */

#include "theory/quantifiers/sygus/sygus_eval_unfold.h"

#include "expr/dtype_cons.h"
#include "expr/sygus_datatype.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;
using namespace cvc5::context;

namespace cvc5 {
namespace theory {
namespace quantifiers {

SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}

void SygusEvalUnfold::registerEvalTerm(Node n)
{
  Assert(options::sygusEvalUnfold());
  // is this a sygus evaluation function application?
  if (n.getKind() != DT_SYGUS_EVAL)
  {
    return;
  }
  if (d_eval_processed.find(n) != d_eval_processed.end())
  {
    return;
  }
  Trace("sygus-eval-unfold")
      << "SygusEvalUnfold: register eval term : " << n << std::endl;
  d_eval_processed.insert(n);
  TypeNode tn = n[0].getType();
  // since n[0] is an evaluation head, we know tn is a sygus datatype
  Assert(tn.isDatatype());
  const DType& dt = tn.getDType();
  Assert(dt.isSygus());
  if (n[0].getKind() == APPLY_CONSTRUCTOR)
  {
    // constructors should be unfolded and reduced already
    Assert(false);
    return;
  }
  // register this evaluation term with its head
  d_evals[n[0]].push_back(n);
  Node var_list = dt.getSygusVarList();
  d_eval_args[n[0]].push_back(std::vector<Node>());
  for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
  {
    d_eval_args[n[0]].back().push_back(n[j]);
  }
  Node a = TermDbSygus::getAnchor(n[0]);
  d_subterms[a].insert(n[0]);
}

void SygusEvalUnfold::registerModelValue(Node a,
                                         Node v,
                                         std::vector<Node>& terms,
                                         std::vector<Node>& vals,
                                         std::vector<Node>& exps)
{
  std::map<Node, std::unordered_set<Node> >::iterator its = d_subterms.find(a);
  if (its == d_subterms.end())
  {
    return;
  }
  NodeManager* nm = NodeManager::currentNM();
  SygusExplain* sy_exp = d_tds->getExplain();
  Trace("sygus-eval-unfold")
      << "SygusEvalUnfold: " << a << ", has " << its->second.size()
      << " registered subterms." << std::endl;
  for (const Node& n : its->second)
  {
    Trace("sygus-eval-unfold-debug") << "...process : " << n << std::endl;
    std::map<Node, std::vector<std::vector<Node> > >::iterator it =
        d_eval_args.find(n);
    if (it != d_eval_args.end() && !it->second.empty())
    {
      TNode at = a;
      TNode vt = v;
      Node vn = n.substitute(at, vt);
      vn = Rewriter::rewrite(vn);
      unsigned start = d_node_mv_args_proc[n][vn];
      // get explanation in terms of testers
      std::vector<Node> antec_exp;
      sy_exp->getExplanationForEquality(n, vn, antec_exp);
      Node antec =
          antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
      // Node antec = n.eqNode( vn );
      TypeNode tn = n.getType();
      // Check if the sygus type has any symbolic constructors. This will
      // impact how the unfolding is computed below.
      SygusTypeInfo& sti = d_tds->getTypeInfo(tn);
      bool hasSymCons = sti.hasSubtermSymbolicCons();
      // n occurs as an evaluation head, thus it has sygus datatype type
      Assert(tn.isDatatype());
      const DType& dt = tn.getDType();
      Assert(dt.isSygus());
      Trace("sygus-eval-unfold")
          << "SygusEvalUnfold: Register model value : " << vn << " for " << n
          << std::endl;
      unsigned curr_size = it->second.size();
      Trace("sygus-eval-unfold")
          << "...it has " << curr_size << " evaluations, already processed "
          << start << "." << std::endl;
      Node bTerm = d_tds->sygusToBuiltin(vn, tn);
      Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
      std::vector<Node> vars;
      Node var_list = dt.getSygusVarList();
      for (const Node& var : var_list)
      {
        vars.push_back(var);
      }
      // evaluation children
      std::vector<Node> eval_children;
      eval_children.push_back(n);
      // for each evaluation
      for (unsigned i = start; i < curr_size; i++)
      {
        Node res;
        Node expn;
        // should we unfold?
        bool do_unfold = false;
        if (options::sygusEvalUnfoldBool())
        {
          Node bTermUse = bTerm;
          if (bTerm.getKind() == APPLY_UF)
          {
            // if the builtin term is non-beta-reduced application of lambda,
            // we look at the body of the lambda.
            Node bTermOp = bTerm.getOperator();
            if (bTermOp.getKind() == LAMBDA)
            {
              bTermUse = bTermOp[0];
            }
          }
          if (bTermUse.getKind() == ITE || bTermUse.getType().isBoolean())
          {
            do_unfold = true;
          }
        }
        if (do_unfold || hasSymCons)
        {
          // note that this is replicated for different values
          std::map<Node, Node> vtm;
          std::vector<Node> exp;
          vtm[n] = vn;
          eval_children.insert(
              eval_children.end(), it->second[i].begin(), it->second[i].end());
          Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
          eval_children.resize(1);
          // If we explicitly asked to unfold, we use single step, otherwise
          // we use multi step.
          res = unfold(eval_fun, vtm, exp, true, !do_unfold);
          Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl;
          expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
        }
        else
        {
          EvalSygusInvarianceTest esit;
          eval_children.insert(
              eval_children.end(), it->second[i].begin(), it->second[i].end());
          Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
          eval_children[0] = vn;
          Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
          res = d_tds->evaluateWithUnfolding(eval_fun);
          Trace("sygus-eval-unfold")
              << "Evaluate with unfolding returns " << res << std::endl;
          esit.init(conj, n, res);
          eval_children.resize(1);
          eval_children[0] = n;

          // evaluate with minimal explanation
          std::vector<Node> mexp;
          sy_exp->getExplanationFor(n, vn, mexp, esit);
          Assert(!mexp.empty());
          expn = mexp.size() == 1 ? mexp[0] : nm->mkNode(AND, mexp);
        }
        Assert(!res.isNull());
        terms.push_back(d_evals[n][i]);
        vals.push_back(res);
        exps.push_back(expn);
        Trace("sygus-eval-unfold")
            << "Conclude : " << d_evals[n][i] << " == " << res << std::endl;
        Trace("sygus-eval-unfold") << "   from " << expn << std::endl;
      }
      d_node_mv_args_proc[n][vn] = curr_size;
    }
  }
}

Node SygusEvalUnfold::unfold(Node en,
                             std::map<Node, Node>& vtm,
                             std::vector<Node>& exp,
                             bool track_exp,
                             bool doRec)
{
  if (en.getKind() != DT_SYGUS_EVAL)
  {
    Assert(en.isConst());
    return en;
  }
  Trace("sygus-eval-unfold-debug")
      << "Unfold : " << en << ", track exp is " << track_exp << ", doRec is "
      << doRec << std::endl;
  Node ev = en[0];
  if (track_exp)
  {
    std::map<Node, Node>::iterator itv = vtm.find(en[0]);
    Assert(itv != vtm.end());
    if (itv != vtm.end())
    {
      ev = itv->second;
    }
    Assert(en[0].getType() == ev.getType());
    Assert(ev.isConst());
  }
  Trace("sygus-eval-unfold-debug")
      << "Unfold model value is : " << ev << std::endl;
  AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR);
  std::vector<Node> args;
  for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
  {
    args.push_back(en[i]);
  }

  TypeNode headType = en[0].getType();
  NodeManager* nm = NodeManager::currentNM();
  const DType& dt = headType.getDType();
  unsigned i = datatypes::utils::indexOf(ev.getOperator());
  if (track_exp)
  {
    // explanation
    Node ee = nm->mkNode(APPLY_TESTER, dt[i].getTester(), en[0]);
    if (std::find(exp.begin(), exp.end(), ee) == exp.end())
    {
      exp.push_back(ee);
    }
  }
  // if we are a symbolic constructor, unfolding returns the subterm itself
  Node sop = dt[i].getSygusOp();
  if (sop.getAttribute(SygusAnyConstAttribute()))
  {
    Trace("sygus-eval-unfold-debug")
        << "...it is an any-constant constructor" << std::endl;
    Assert(dt[i].getNumArgs() == 1);
    // If the argument to evaluate is itself concrete, then we use its
    // argument; otherwise we return its selector.
    if (en[0].getKind() == APPLY_CONSTRUCTOR)
    {
      Trace("sygus-eval-unfold-debug")
          << "...return (from constructor) " << en[0][0] << std::endl;
      return en[0][0];
    }
    else
    {
      Node ret = nm->mkNode(
          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
      Trace("sygus-eval-unfold-debug")
          << "...return (from constructor) " << ret << std::endl;
      return ret;
    }
  }

  Assert(!dt.isParametric());
  std::map<int, Node> pre;
  for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
  {
    std::vector<Node> cc;
    Node s;
    // get the j^th subfield of en
    if (en[0].getKind() == APPLY_CONSTRUCTOR)
    {
      // if it is a concrete constructor application, as an optimization,
      // just return the argument
      s = en[0][j];
    }
    else
    {
      s = nm->mkNode(
          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
    }
    cc.push_back(s);
    if (track_exp)
    {
      // update vtm map
      vtm[s] = ev[j];
    }
    cc.insert(cc.end(), args.begin(), args.end());
    Node argj = nm->mkNode(DT_SYGUS_EVAL, cc);
    if (doRec)
    {
      Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl;
      // evaluate recursively
      argj = unfold(argj, vtm, exp, track_exp, doRec);
    }
    pre[j] = argj;
  }
  Node ret = d_tds->mkGeneric(dt, i, pre);
  // apply the appropriate substitution to ret
  ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
  Trace("sygus-eval-unfold-debug")
      << "Applied sygus args : " << ret << std::endl;
  // rewrite
  ret = Rewriter::rewrite(ret);
  Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl;
  return ret;
}

Node SygusEvalUnfold::unfold(Node en)
{
  std::map<Node, Node> vtm;
  std::vector<Node> exp;
  return unfold(en, vtm, exp, false, false);
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of sygus_eval_unfold.
14		*/
15
16		#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
17
18		#include "expr/dtype_cons.h"
19		#include "expr/sygus_datatype.h"
20		#include "options/quantifiers_options.h"
21		#include "theory/datatypes/sygus_datatype_utils.h"
22		#include "theory/quantifiers/sygus/term_database_sygus.h"
23		#include "theory/rewriter.h"
24
25		using namespace std;
26		using namespace cvc5::kind;
27		using namespace cvc5::context;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33	1529	SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
34
35	175022	void SygusEvalUnfold::registerEvalTerm(Node n)
36		{
37	175022	Assert(options::sygusEvalUnfold());
38		// is this a sygus evaluation function application?
39	175022	if (n.getKind() != DT_SYGUS_EVAL)
40		{
41	345483	return;
42		}
43	3331	if (d_eval_processed.find(n) != d_eval_processed.end())
44		{
45	2101	return;
46		}
47	2460	Trace("sygus-eval-unfold")
48	1230	<< "SygusEvalUnfold: register eval term : " << n << std::endl;
49	1230	d_eval_processed.insert(n);
50	2460	TypeNode tn = n[0].getType();
51		// since n[0] is an evaluation head, we know tn is a sygus datatype
52	1230	Assert(tn.isDatatype());
53	1230	const DType& dt = tn.getDType();
54	1230	Assert(dt.isSygus());
55	1230	if (n[0].getKind() == APPLY_CONSTRUCTOR)
56		{
57		// constructors should be unfolded and reduced already
58		Assert(false);
59		return;
60		}
61		// register this evaluation term with its head
62	1230	d_evals[n[0]].push_back(n);
63	2460	Node var_list = dt.getSygusVarList();
64	1230	d_eval_args[n[0]].push_back(std::vector<Node>());
65	4281	for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
66		{
67	3051	d_eval_args[n[0]].back().push_back(n[j]);
68		}
69	2460	Node a = TermDbSygus::getAnchor(n[0]);
70	1230	d_subterms[a].insert(n[0]);
71		}
72
73	6209	void SygusEvalUnfold::registerModelValue(Node a,
74		Node v,
75		std::vector<Node>& terms,
76		std::vector<Node>& vals,
77		std::vector<Node>& exps)
78		{
79	6209	std::map<Node, std::unordered_set<Node> >::iterator its = d_subterms.find(a);
80	6209	if (its == d_subterms.end())
81		{
82	2241	return;
83		}
84	3968	NodeManager* nm = NodeManager::currentNM();
85	3968	SygusExplain* sy_exp = d_tds->getExplain();
86	7936	Trace("sygus-eval-unfold")
87	7936	<< "SygusEvalUnfold: " << a << ", has " << its->second.size()
88	3968	<< " registered subterms." << std::endl;
89	12084	for (const Node& n : its->second)
90		{
91	8116	Trace("sygus-eval-unfold-debug") << "...process : " << n << std::endl;
92		std::map<Node, std::vector<std::vector<Node> > >::iterator it =
93	8116	d_eval_args.find(n);
94	8116	if (it != d_eval_args.end() && !it->second.empty())
95		{
96	16232	TNode at = a;
97	16232	TNode vt = v;
98	16232	Node vn = n.substitute(at, vt);
99	8116	vn = Rewriter::rewrite(vn);
100	8116	unsigned start = d_node_mv_args_proc[n][vn];
101		// get explanation in terms of testers
102	16232	std::vector<Node> antec_exp;
103	8116	sy_exp->getExplanationForEquality(n, vn, antec_exp);
104		Node antec =
105	16232	antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
106		// Node antec = n.eqNode( vn );
107	16232	TypeNode tn = n.getType();
108		// Check if the sygus type has any symbolic constructors. This will
109		// impact how the unfolding is computed below.
110	8116	SygusTypeInfo& sti = d_tds->getTypeInfo(tn);
111	8116	bool hasSymCons = sti.hasSubtermSymbolicCons();
112		// n occurs as an evaluation head, thus it has sygus datatype type
113	8116	Assert(tn.isDatatype());
114	8116	const DType& dt = tn.getDType();
115	8116	Assert(dt.isSygus());
116	16232	Trace("sygus-eval-unfold")
117	8116	<< "SygusEvalUnfold: Register model value : " << vn << " for " << n
118	8116	<< std::endl;
119	8116	unsigned curr_size = it->second.size();
120	16232	Trace("sygus-eval-unfold")
121	8116	<< "...it has " << curr_size << " evaluations, already processed "
122	8116	<< start << "." << std::endl;
123	16232	Node bTerm = d_tds->sygusToBuiltin(vn, tn);
124	8116	Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
125	16232	std::vector<Node> vars;
126	16232	Node var_list = dt.getSygusVarList();
127	34650	for (const Node& var : var_list)
128		{
129	26534	vars.push_back(var);
130		}
131		// evaluation children
132	16232	std::vector<Node> eval_children;
133	8116	eval_children.push_back(n);
134		// for each evaluation
135	19019	for (unsigned i = start; i < curr_size; i++)
136		{
137	21806	Node res;
138	21806	Node expn;
139		// should we unfold?
140	10903	bool do_unfold = false;
141	21806	if (options::sygusEvalUnfoldBool())
142		{
143	21806	Node bTermUse = bTerm;
144	10903	if (bTerm.getKind() == APPLY_UF)
145		{
146		// if the builtin term is non-beta-reduced application of lambda,
147		// we look at the body of the lambda.
148	8	Node bTermOp = bTerm.getOperator();
149	4	if (bTermOp.getKind() == LAMBDA)
150		{
151		bTermUse = bTermOp[0];
152		}
153		}
154	10903	if (bTermUse.getKind() == ITE \|\| bTermUse.getType().isBoolean())
155		{
156	2997	do_unfold = true;
157		}
158		}
159	10903	if (do_unfold \|\| hasSymCons)
160		{
161		// note that this is replicated for different values
162	6998	std::map<Node, Node> vtm;
163	6998	std::vector<Node> exp;
164	3499	vtm[n] = vn;
165	3499	eval_children.insert(
166	6998	eval_children.end(), it->second[i].begin(), it->second[i].end());
167	6998	Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
168	3499	eval_children.resize(1);
169		// If we explicitly asked to unfold, we use single step, otherwise
170		// we use multi step.
171	3499	res = unfold(eval_fun, vtm, exp, true, !do_unfold);
172	3499	Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl;
173	6998	expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
174		}
175		else
176		{
177	14808	EvalSygusInvarianceTest esit;
178	7404	eval_children.insert(
179	14808	eval_children.end(), it->second[i].begin(), it->second[i].end());
180	14808	Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
181	7404	eval_children[0] = vn;
182	14808	Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
183	7404	res = d_tds->evaluateWithUnfolding(eval_fun);
184	14808	Trace("sygus-eval-unfold")
185	7404	<< "Evaluate with unfolding returns " << res << std::endl;
186	7404	esit.init(conj, n, res);
187	7404	eval_children.resize(1);
188	7404	eval_children[0] = n;
189
190		// evaluate with minimal explanation
191	14808	std::vector<Node> mexp;
192	7404	sy_exp->getExplanationFor(n, vn, mexp, esit);
193	7404	Assert(!mexp.empty());
194	7404	expn = mexp.size() == 1 ? mexp[0] : nm->mkNode(AND, mexp);
195		}
196	10903	Assert(!res.isNull());
197	10903	terms.push_back(d_evals[n][i]);
198	10903	vals.push_back(res);
199	10903	exps.push_back(expn);
200	21806	Trace("sygus-eval-unfold")
201	10903	<< "Conclude : " << d_evals[n][i] << " == " << res << std::endl;
202	10903	Trace("sygus-eval-unfold") << " from " << expn << std::endl;
203		}
204	8116	d_node_mv_args_proc[n][vn] = curr_size;
205		}
206		}
207		}
208
209	52306	Node SygusEvalUnfold::unfold(Node en,
210		std::map<Node, Node>& vtm,
211		std::vector<Node>& exp,
212		bool track_exp,
213		bool doRec)
214		{
215	52306	if (en.getKind() != DT_SYGUS_EVAL)
216		{
217		Assert(en.isConst());
218		return en;
219		}
220	104612	Trace("sygus-eval-unfold-debug")
221	52306	<< "Unfold : " << en << ", track exp is " << track_exp << ", doRec is "
222	52306	<< doRec << std::endl;
223	104612	Node ev = en[0];
224	52306	if (track_exp)
225		{
226	4746	std::map<Node, Node>::iterator itv = vtm.find(en[0]);
227	4746	Assert(itv != vtm.end());
228	4746	if (itv != vtm.end())
229		{
230	4746	ev = itv->second;
231		}
232	4746	Assert(en[0].getType() == ev.getType());
233	4746	Assert(ev.isConst());
234		}
235	104612	Trace("sygus-eval-unfold-debug")
236	52306	<< "Unfold model value is : " << ev << std::endl;
237	52306	AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR);
238	104612	std::vector<Node> args;
239	167897	for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
240		{
241	115591	args.push_back(en[i]);
242		}
243
244	104612	TypeNode headType = en[0].getType();
245	52306	NodeManager* nm = NodeManager::currentNM();
246	52306	const DType& dt = headType.getDType();
247	52306	unsigned i = datatypes::utils::indexOf(ev.getOperator());
248	52306	if (track_exp)
249		{
250		// explanation
251	9492	Node ee = nm->mkNode(APPLY_TESTER, dt[i].getTester(), en[0]);
252	4746	if (std::find(exp.begin(), exp.end(), ee) == exp.end())
253		{
254	4746	exp.push_back(ee);
255		}
256		}
257		// if we are a symbolic constructor, unfolding returns the subterm itself
258	104612	Node sop = dt[i].getSygusOp();
259	52306	if (sop.getAttribute(SygusAnyConstAttribute()))
260		{
261	1010	Trace("sygus-eval-unfold-debug")
262	505	<< "...it is an any-constant constructor" << std::endl;
263	505	Assert(dt[i].getNumArgs() == 1);
264		// If the argument to evaluate is itself concrete, then we use its
265		// argument; otherwise we return its selector.
266	505	if (en[0].getKind() == APPLY_CONSTRUCTOR)
267		{
268	2	Trace("sygus-eval-unfold-debug")
269	1	<< "...return (from constructor) " << en[0][0] << std::endl;
270	1	return en[0][0];
271		}
272		else
273		{
274		Node ret = nm->mkNode(
275	1008	APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
276	1008	Trace("sygus-eval-unfold-debug")
277	504	<< "...return (from constructor) " << ret << std::endl;
278	504	return ret;
279		}
280		}
281
282	51801	Assert(!dt.isParametric());
283	103602	std::map<int, Node> pre;
284	155324	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
285		{
286	207046	std::vector<Node> cc;
287	207046	Node s;
288		// get the j^th subfield of en
289	103523	if (en[0].getKind() == APPLY_CONSTRUCTOR)
290		{
291		// if it is a concrete constructor application, as an optimization,
292		// just return the argument
293	96226	s = en[0][j];
294		}
295		else
296		{
297	21891	s = nm->mkNode(
298	14594	APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
299		}
300	103523	cc.push_back(s);
301	103523	if (track_exp)
302		{
303		// update vtm map
304	7297	vtm[s] = ev[j];
305		}
306	103523	cc.insert(cc.end(), args.begin(), args.end());
307	207046	Node argj = nm->mkNode(DT_SYGUS_EVAL, cc);
308	103523	if (doRec)
309		{
310	1247	Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl;
311		// evaluate recursively
312	1247	argj = unfold(argj, vtm, exp, track_exp, doRec);
313		}
314	103523	pre[j] = argj;
315		}
316	103602	Node ret = d_tds->mkGeneric(dt, i, pre);
317		// apply the appropriate substitution to ret
318	51801	ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
319	103602	Trace("sygus-eval-unfold-debug")
320	51801	<< "Applied sygus args : " << ret << std::endl;
321		// rewrite
322	51801	ret = Rewriter::rewrite(ret);
323	51801	Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl;
324	51801	return ret;
325		}
326
327	47560	Node SygusEvalUnfold::unfold(Node en)
328		{
329	95120	std::map<Node, Node> vtm;
330	95120	std::vector<Node> exp;
331	95120	return unfold(en, vtm, exp, false, false);
332		}
333
334		} // namespace quantifiers
335		} // namespace theory
336	39097	} // namespace cvc5