Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_explain.cpp	Lines:	157	164	95.7 %
Date:	2021-11-07	Branches:	294	786	37.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   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.
 * ****************************************************************************
 *
 * Implementation of techniques for sygus explanations.
 */

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

#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "smt/logic_exception.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/sygus_invariance.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"

using namespace cvc5::kind;
using namespace std;

namespace cvc5 {
namespace theory {
namespace quantifiers {

void TermRecBuild::addTerm(Node n)
{
  d_term.push_back(n);
  std::vector<Node> currc;
  d_kind.push_back(n.getKind());
  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
  {
    currc.push_back(n.getOperator());
    d_has_op.push_back(true);
  }
  else
  {
    d_has_op.push_back(false);
  }
  for (unsigned i = 0; i < n.getNumChildren(); i++)
  {
    currc.push_back(n[i]);
  }
  d_children.push_back(currc);
}

void TermRecBuild::init(Node n)
{
  Assert(d_term.empty());
  addTerm(n);
}

void TermRecBuild::push(unsigned p)
{
  Assert(!d_term.empty());
  unsigned curr = d_term.size() - 1;
  Assert(d_pos.size() == curr);
  Assert(d_pos.size() + 1 == d_children.size());
  Assert(p < d_term[curr].getNumChildren());
  addTerm(d_term[curr][p]);
  d_pos.push_back(p);
}

void TermRecBuild::pop()
{
  Assert(!d_pos.empty());
  d_pos.pop_back();
  d_kind.pop_back();
  d_has_op.pop_back();
  d_children.pop_back();
  d_term.pop_back();
}

void TermRecBuild::replaceChild(unsigned i, Node r)
{
  Assert(!d_term.empty());
  unsigned curr = d_term.size() - 1;
  unsigned o = d_has_op[curr] ? 1 : 0;
  d_children[curr][i + o] = r;
}

Node TermRecBuild::getChild(unsigned i)
{
  unsigned curr = d_term.size() - 1;
  unsigned o = d_has_op[curr] ? 1 : 0;
  return d_children[curr][i + o];
}

Node TermRecBuild::build(unsigned d)
{
  Assert(d_pos.size() + 1 == d_term.size());
  Assert(d < d_term.size());
  int p = d < d_pos.size() ? d_pos[d] : -2;
  std::vector<Node> children;
  unsigned o = d_has_op[d] ? 1 : 0;
  for (unsigned i = 0; i < d_children[d].size(); i++)
  {
    Node nc;
    if (p + o == i)
    {
      nc = build(d + 1);
    }
    else
    {
      nc = d_children[d][i];
    }
    children.push_back(nc);
  }
  return NodeManager::currentNM()->mkNode(d_kind[d], children);
}

void SygusExplain::getExplanationForEquality(Node n,
                                             Node vn,
                                             std::vector<Node>& exp)
{
  std::map<unsigned, bool> cexc;
  getExplanationForEquality(n, vn, exp, cexc);
}

void SygusExplain::getExplanationForEquality(Node n,
                                             Node vn,
                                             std::vector<Node>& exp,
                                             std::map<unsigned, bool>& cexc)
{
  // since builtin types occur in grammar, types are comparable but not
  // necessarily equal
  Assert(n.getType().isComparableTo(n.getType()));
  if (n == vn)
  {
    return;
  }
  TypeNode tn = n.getType();
  if (!tn.isDatatype())
  {
    // sygus datatype fields that are not sygus datatypes are treated as
    // abstractions only, hence we disregard this field
    return;
  }
  Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
  const DType& dt = tn.getDType();
  int i = datatypes::utils::indexOf(vn.getOperator());
  Node tst = datatypes::utils::mkTester(n, i, dt);
  exp.push_back(tst);
  for (unsigned j = 0; j < vn.getNumChildren(); j++)
  {
    if (cexc.find(j) == cexc.end())
    {
      Node sel = NodeManager::currentNM()->mkNode(
          kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
      getExplanationForEquality(sel, vn[j], exp);
    }
  }
}

Node SygusExplain::getExplanationForEquality(Node n, Node vn)
{
  std::map<unsigned, bool> cexc;
  return getExplanationForEquality(n, vn, cexc);
}

Node SygusExplain::getExplanationForEquality(Node n,
                                             Node vn,
                                             std::map<unsigned, bool>& cexc)
{
  std::vector<Node> exp;
  getExplanationForEquality(n, vn, exp, cexc);
  Assert(!exp.empty());
  return exp.size() == 1 ? exp[0]
                         : NodeManager::currentNM()->mkNode(kind::AND, exp);
}

// we have ( n = vn => eval( n ) = bvr ) ^ vn != vnr , returns exp such that exp
// => ( eval( n ) = bvr ^ vn != vnr )
void SygusExplain::getExplanationFor(TermRecBuild& trb,
                                     Node n,
                                     Node vn,
                                     std::vector<Node>& exp,
                                     std::map<TypeNode, int>& var_count,
                                     SygusInvarianceTest& et,
                                     Node vnr,
                                     Node& vnr_exp,
                                     int& sz)
{
  Assert(vnr.isNull() || vn != vnr);
  Assert(n.getType().isComparableTo(vn.getType()));
  TypeNode ntn = n.getType();
  if (!ntn.isDatatype())
  {
    // SyGuS datatype fields that are not sygus datatypes are treated as
    // abstractions only, hence we disregard this field. It is important
    // that users of this method pay special attention to any constants,
    // otherwise the explanation n.eqNode(vn) is necessary here. For example,
    // any lemma schema that blocks the current value of an enumerator should
    // not make any assumptions about the value of the arguments of its any
    // constant constructors, since their explanation is not included here.
    return;
  }
  Assert(vn.getKind() == APPLY_CONSTRUCTOR);
  Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR);
  std::map<unsigned, bool> cexc;
  // for each child,
  // check whether replacing that child by a fresh variable
  // also satisfies the invariance test.
  for (unsigned i = 0; i < vn.getNumChildren(); i++)
  {
    TypeNode xtn = vn[i].getType();
    Node x = d_tdb->getFreeVarInc(xtn, var_count);
    trb.replaceChild(i, x);
    Node nvn = trb.build();
    Assert(nvn.getKind() == kind::APPLY_CONSTRUCTOR);
    if (et.is_invariant(d_tdb, nvn, x))
    {
      cexc[i] = true;
      // we are tracking term size if positive
      if (sz >= 0)
      {
        int s = datatypes::utils::getSygusTermSize(vn[i]);
        sz = sz - s;
      }
    }
    else
    {
      // revert
      trb.replaceChild(i, vn[i]);
    }
  }
  const DType& dt = ntn.getDType();
  int cindex = datatypes::utils::indexOf(vn.getOperator());
  Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
  Node tst = datatypes::utils::mkTester(n, cindex, dt);
  exp.push_back(tst);
  // if the operator of vn is different than vnr, then disunification obligation
  // is met
  if (!vnr.isNull())
  {
    if (vnr.getOperator() != vn.getOperator())
    {
      vnr = Node::null();
      vnr_exp = NodeManager::currentNM()->mkConst(true);
    }
  }
  for (unsigned i = 0; i < vn.getNumChildren(); i++)
  {
    Node sel = NodeManager::currentNM()->mkNode(
        kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
    Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
    if (cexc.find(i) == cexc.end())
    {
      trb.push(i);
      Node vnr_exp_c;
      getExplanationFor(
          trb, sel, vn[i], exp, var_count, et, vnr_c, vnr_exp_c, sz);
      trb.pop();
      if (!vnr_c.isNull())
      {
        Assert(!vnr_exp_c.isNull());
        if (vnr_exp_c.isConst() || vnr_exp.isNull())
        {
          // recursively satisfied the disunification obligation
          if (vnr_exp_c.isConst())
          {
            // was successful, don't consider further
            vnr = Node::null();
          }
          vnr_exp = vnr_exp_c;
        }
      }
    }
    else
    {
      // if excluded, we may need to add the explanation for this
      if (vnr_exp.isNull() && !vnr_c.isNull())
      {
        vnr_exp = getExplanationForEquality(sel, vnr[i]);
      }
    }
  }
}

void SygusExplain::getExplanationFor(Node n,
                                     Node vn,
                                     std::vector<Node>& exp,
                                     SygusInvarianceTest& et,
                                     Node vnr,
                                     unsigned& sz)
{
  std::map<TypeNode, int> var_count;
  return getExplanationFor(n, vn, exp, et, vnr, var_count, sz);
}

void SygusExplain::getExplanationFor(Node n,
                                     Node vn,
                                     std::vector<Node>& exp,
                                     SygusInvarianceTest& et,
                                     Node vnr,
                                     std::map<TypeNode, int>& var_count,
                                     unsigned& sz)
{
  // naive :
  // return getExplanationForEquality( n, vn, exp );

  // set up the recursion object;
  TermRecBuild trb;
  trb.init(vn);
  Node vnr_exp;
  int sz_use = sz;
  getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz_use);
  Assert(sz_use >= 0);
  sz = sz_use;
  Assert(vnr.isNull() || !vnr_exp.isNull());
  if (!vnr_exp.isNull() && !vnr_exp.isConst())
  {
    exp.push_back(vnr_exp.negate());
  }
}

void SygusExplain::getExplanationFor(Node n,
                                     Node vn,
                                     std::vector<Node>& exp,
                                     SygusInvarianceTest& et,
                                     bool strict)
{
  std::map<TypeNode, int> var_count;
  getExplanationFor(n, vn, exp, et, var_count, strict);
}

void SygusExplain::getExplanationFor(Node n,
                                     Node vn,
                                     std::vector<Node>& exp,
                                     SygusInvarianceTest& et,
                                     std::map<TypeNode, int>& var_count,
                                     bool strict)
{
  if (!strict)
  {
    // check if it is invariant over the entire node
    TypeNode vtn = vn.getType();
    Node x = d_tdb->getFreeVarInc(vtn, var_count);
    if (et.is_invariant(d_tdb, x, x))
    {
      return;
    }
    var_count[vtn]--;
  }
  int sz = -1;
  TermRecBuild trb;
  trb.init(vn);
  Node vnr;
  Node vnr_exp;
  getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz);
}

}  // 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, 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 techniques for sygus explanations.
14		*/
15
16		#include "theory/quantifiers/sygus/sygus_explain.h"
17
18		#include "expr/dtype.h"
19		#include "expr/dtype_cons.h"
20		#include "smt/logic_exception.h"
21		#include "theory/datatypes/sygus_datatype_utils.h"
22		#include "theory/datatypes/theory_datatypes_utils.h"
23		#include "theory/quantifiers/sygus/sygus_invariance.h"
24		#include "theory/quantifiers/sygus/term_database_sygus.h"
25
26		using namespace cvc5::kind;
27		using namespace std;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33	156439	void TermRecBuild::addTerm(Node n)
34		{
35	156439	d_term.push_back(n);
36	312878	std::vector<Node> currc;
37	156439	d_kind.push_back(n.getKind());
38	156439	if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
39		{
40	156357	currc.push_back(n.getOperator());
41	156357	d_has_op.push_back(true);
42		}
43		else
44		{
45	82	d_has_op.push_back(false);
46		}
47	282742	for (unsigned i = 0; i < n.getNumChildren(); i++)
48		{
49	126303	currc.push_back(n[i]);
50		}
51	156439	d_children.push_back(currc);
52	156439	}
53
54	35026	void TermRecBuild::init(Node n)
55		{
56	35026	Assert(d_term.empty());
57	35026	addTerm(n);
58	35026	}
59
60	121413	void TermRecBuild::push(unsigned p)
61		{
62	121413	Assert(!d_term.empty());
63	121413	unsigned curr = d_term.size() - 1;
64	121413	Assert(d_pos.size() == curr);
65	121413	Assert(d_pos.size() + 1 == d_children.size());
66	121413	Assert(p < d_term[curr].getNumChildren());
67	121413	addTerm(d_term[curr][p]);
68	121413	d_pos.push_back(p);
69	121413	}
70
71	121413	void TermRecBuild::pop()
72		{
73	121413	Assert(!d_pos.empty());
74	121413	d_pos.pop_back();
75	121413	d_kind.pop_back();
76	121413	d_has_op.pop_back();
77	121413	d_children.pop_back();
78	121413	d_term.pop_back();
79	121413	}
80
81	247646	void TermRecBuild::replaceChild(unsigned i, Node r)
82		{
83	247646	Assert(!d_term.empty());
84	247646	unsigned curr = d_term.size() - 1;
85	247646	unsigned o = d_has_op[curr] ? 1 : 0;
86	247646	d_children[curr][i + o] = r;
87	247646	}
88
89		Node TermRecBuild::getChild(unsigned i)
90		{
91		unsigned curr = d_term.size() - 1;
92		unsigned o = d_has_op[curr] ? 1 : 0;
93		return d_children[curr][i + o];
94		}
95
96	213023	Node TermRecBuild::build(unsigned d)
97		{
98	213023	Assert(d_pos.size() + 1 == d_term.size());
99	213023	Assert(d < d_term.size());
100	213023	int p = d < d_pos.size() ? d_pos[d] : -2;
101	426046	std::vector<Node> children;
102	213023	unsigned o = d_has_op[d] ? 1 : 0;
103	851621	for (unsigned i = 0; i < d_children[d].size(); i++)
104		{
105	1277196	Node nc;
106	638598	if (p + o == i)
107		{
108	86790	nc = build(d + 1);
109		}
110		else
111		{
112	551808	nc = d_children[d][i];
113		}
114	638598	children.push_back(nc);
115		}
116	426046	return NodeManager::currentNM()->mkNode(d_kind[d], children);
117		}
118
119	63617	void SygusExplain::getExplanationForEquality(Node n,
120		Node vn,
121		std::vector<Node>& exp)
122		{
123	127234	std::map<unsigned, bool> cexc;
124	63617	getExplanationForEquality(n, vn, exp, cexc);
125	63617	}
126
127	63942	void SygusExplain::getExplanationForEquality(Node n,
128		Node vn,
129		std::vector<Node>& exp,
130		std::map<unsigned, bool>& cexc)
131		{
132		// since builtin types occur in grammar, types are comparable but not
133		// necessarily equal
134	63942	Assert(n.getType().isComparableTo(n.getType()));
135	63942	if (n == vn)
136		{
137	711	return;
138		}
139	127173	TypeNode tn = n.getType();
140	63942	if (!tn.isDatatype())
141		{
142		// sygus datatype fields that are not sygus datatypes are treated as
143		// abstractions only, hence we disregard this field
144	711	return;
145		}
146	63231	Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
147	63231	const DType& dt = tn.getDType();
148	63231	int i = datatypes::utils::indexOf(vn.getOperator());
149	126462	Node tst = datatypes::utils::mkTester(n, i, dt);
150	63231	exp.push_back(tst);
151	107204	for (unsigned j = 0; j < vn.getNumChildren(); j++)
152		{
153	43973	if (cexc.find(j) == cexc.end())
154		{
155		Node sel = NodeManager::currentNM()->mkNode(
156	87946	kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
157	43973	getExplanationForEquality(sel, vn[j], exp);
158		}
159		}
160		}
161
162	325	Node SygusExplain::getExplanationForEquality(Node n, Node vn)
163		{
164	650	std::map<unsigned, bool> cexc;
165	650	return getExplanationForEquality(n, vn, cexc);
166		}
167
168	325	Node SygusExplain::getExplanationForEquality(Node n,
169		Node vn,
170		std::map<unsigned, bool>& cexc)
171		{
172	650	std::vector<Node> exp;
173	325	getExplanationForEquality(n, vn, exp, cexc);
174	325	Assert(!exp.empty());
175	444	return exp.size() == 1 ? exp[0]
176	769	: NodeManager::currentNM()->mkNode(kind::AND, exp);
177		}
178
179		// we have ( n = vn => eval( n ) = bvr ) ^ vn != vnr , returns exp such that exp
180		// => ( eval( n ) = bvr ^ vn != vnr )
181	156439	void SygusExplain::getExplanationFor(TermRecBuild& trb,
182		Node n,
183		Node vn,
184		std::vector<Node>& exp,
185		std::map<TypeNode, int>& var_count,
186		SygusInvarianceTest& et,
187		Node vnr,
188		Node& vnr_exp,
189		int& sz)
190		{
191	156439	Assert(vnr.isNull() \|\| vn != vnr);
192	156439	Assert(n.getType().isComparableTo(vn.getType()));
193	312726	TypeNode ntn = n.getType();
194	156439	if (!ntn.isDatatype())
195		{
196		// SyGuS datatype fields that are not sygus datatypes are treated as
197		// abstractions only, hence we disregard this field. It is important
198		// that users of this method pay special attention to any constants,
199		// otherwise the explanation n.eqNode(vn) is necessary here. For example,
200		// any lemma schema that blocks the current value of an enumerator should
201		// not make any assumptions about the value of the arguments of its any
202		// constant constructors, since their explanation is not included here.
203	152	return;
204		}
205	156287	Assert(vn.getKind() == APPLY_CONSTRUCTOR);
206	156287	Assert(vnr.isNull() \|\| vnr.getKind() == APPLY_CONSTRUCTOR);
207	312574	std::map<unsigned, bool> cexc;
208		// for each child,
209		// check whether replacing that child by a fresh variable
210		// also satisfies the invariance test.
211	282520	for (unsigned i = 0; i < vn.getNumChildren(); i++)
212		{
213	252466	TypeNode xtn = vn[i].getType();
214	252466	Node x = d_tdb->getFreeVarInc(xtn, var_count);
215	126233	trb.replaceChild(i, x);
216	252466	Node nvn = trb.build();
217	126233	Assert(nvn.getKind() == kind::APPLY_CONSTRUCTOR);
218	126233	if (et.is_invariant(d_tdb, nvn, x))
219		{
220	4820	cexc[i] = true;
221		// we are tracking term size if positive
222	4820	if (sz >= 0)
223		{
224	400	int s = datatypes::utils::getSygusTermSize(vn[i]);
225	400	sz = sz - s;
226		}
227		}
228		else
229		{
230		// revert
231	121413	trb.replaceChild(i, vn[i]);
232		}
233		}
234	156287	const DType& dt = ntn.getDType();
235	156287	int cindex = datatypes::utils::indexOf(vn.getOperator());
236	156287	Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
237	312574	Node tst = datatypes::utils::mkTester(n, cindex, dt);
238	156287	exp.push_back(tst);
239		// if the operator of vn is different than vnr, then disunification obligation
240		// is met
241	156287	if (!vnr.isNull())
242		{
243	7902	if (vnr.getOperator() != vn.getOperator())
244		{
245	4448	vnr = Node::null();
246	4448	vnr_exp = NodeManager::currentNM()->mkConst(true);
247		}
248		}
249	282520	for (unsigned i = 0; i < vn.getNumChildren(); i++)
250		{
251		Node sel = NodeManager::currentNM()->mkNode(
252	252466	kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
253	252466	Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
254	126233	if (cexc.find(i) == cexc.end())
255		{
256	121413	trb.push(i);
257	242826	Node vnr_exp_c;
258	121413	getExplanationFor(
259		trb, sel, vn[i], exp, var_count, et, vnr_c, vnr_exp_c, sz);
260	121413	trb.pop();
261	121413	if (!vnr_c.isNull())
262		{
263	3448	Assert(!vnr_exp_c.isNull());
264	3448	if (vnr_exp_c.isConst() \|\| vnr_exp.isNull())
265		{
266		// recursively satisfied the disunification obligation
267	3448	if (vnr_exp_c.isConst())
268		{
269		// was successful, don't consider further
270	3448	vnr = Node::null();
271		}
272	3448	vnr_exp = vnr_exp_c;
273		}
274		}
275		}
276		else
277		{
278		// if excluded, we may need to add the explanation for this
279	4820	if (vnr_exp.isNull() && !vnr_c.isNull())
280		{
281	8	vnr_exp = getExplanationForEquality(sel, vnr[i]);
282		}
283		}
284		}
285		}
286
287		void SygusExplain::getExplanationFor(Node n,
288		Node vn,
289		std::vector<Node>& exp,
290		SygusInvarianceTest& et,
291		Node vnr,
292		unsigned& sz)
293		{
294		std::map<TypeNode, int> var_count;
295		return getExplanationFor(n, vn, exp, et, vnr, var_count, sz);
296		}
297
298	4456	void SygusExplain::getExplanationFor(Node n,
299		Node vn,
300		std::vector<Node>& exp,
301		SygusInvarianceTest& et,
302		Node vnr,
303		std::map<TypeNode, int>& var_count,
304		unsigned& sz)
305		{
306		// naive :
307		// return getExplanationForEquality( n, vn, exp );
308
309		// set up the recursion object;
310	8912	TermRecBuild trb;
311	4456	trb.init(vn);
312	8912	Node vnr_exp;
313	4456	int sz_use = sz;
314	4456	getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz_use);
315	4456	Assert(sz_use >= 0);
316	4456	sz = sz_use;
317	4456	Assert(vnr.isNull() \|\| !vnr_exp.isNull());
318	4456	if (!vnr_exp.isNull() && !vnr_exp.isConst())
319		{
320	6	exp.push_back(vnr_exp.negate());
321		}
322	4456	}
323
324	18013	void SygusExplain::getExplanationFor(Node n,
325		Node vn,
326		std::vector<Node>& exp,
327		SygusInvarianceTest& et,
328		bool strict)
329		{
330	36026	std::map<TypeNode, int> var_count;
331	18013	getExplanationFor(n, vn, exp, et, var_count, strict);
332	18013	}
333
334	35398	void SygusExplain::getExplanationFor(Node n,
335		Node vn,
336		std::vector<Node>& exp,
337		SygusInvarianceTest& et,
338		std::map<TypeNode, int>& var_count,
339		bool strict)
340		{
341	35398	if (!strict)
342		{
343		// check if it is invariant over the entire node
344	29942	TypeNode vtn = vn.getType();
345	29942	Node x = d_tdb->getFreeVarInc(vtn, var_count);
346	17385	if (et.is_invariant(d_tdb, x, x))
347		{
348	4828	return;
349		}
350	12557	var_count[vtn]--;
351		}
352	30570	int sz = -1;
353	61140	TermRecBuild trb;
354	30570	trb.init(vn);
355	61140	Node vnr;
356	61140	Node vnr_exp;
357	30570	getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz);
358		}
359
360		} // namespace quantifiers
361		} // namespace theory
362	31137	} // namespace cvc5