Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/fun_def_evaluator.cpp	Lines:	138	152	90.8 %
Date:	2021-09-18	Branches:	326	768	42.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
 *
 * 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 evaluating terms with recursively
 * defined functions.
 */

#include "theory/quantifiers/fun_def_evaluator.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

FunDefEvaluator::FunDefEvaluator() {}

void FunDefEvaluator::assertDefinition(Node q)
{
  Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
  Node h = QuantAttributes::getFunDefHead(q);
  if (h.isNull())
  {
    // not a function definition
    return;
  }
  // h possibly with zero arguments?
  Node f = h.hasOperator() ? h.getOperator() : h;
  Assert(d_funDefMap.find(f) == d_funDefMap.end())
      << "FunDefEvaluator::assertDefinition: function already defined";
  d_funDefs.push_back(q);
  FunDefInfo& fdi = d_funDefMap[f];
  fdi.d_quant = q;
  fdi.d_body = QuantAttributes::getFunDefBody(q);
  Assert(!fdi.d_body.isNull());
  fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
  Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
                   << fdi.d_args << " / " << fdi.d_body << std::endl;
}

Node FunDefEvaluator::evaluate(Node n) const
{
  // should do standard rewrite before this call
  Assert(Rewriter::rewrite(n) == n);
  Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<TNode, unsigned> funDefCount;
  std::unordered_map<TNode, unsigned>::iterator itCount;
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::map<Node, FunDefInfo>::const_iterator itf;
  std::vector<TNode> visit;
  TNode cur;
  TNode curEval;
  Node f;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);
    Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;

    if (it == visited.end())
    {
      if (cur.isConst())
      {
        Trace("fd-eval-debug") << "constant " << cur << std::endl;
        visited[cur] = cur;
      }
      else if (cur.getKind() == ITE)
      {
        Trace("fd-eval-debug") << "ITE " << cur << std::endl;
        visited[cur] = Node::null();
        visit.push_back(cur);
        visit.push_back(cur[0]);
      }
      else
      {
        Trace("fd-eval-debug") << "recurse " << cur << std::endl;
        visited[cur] = Node::null();
        visit.push_back(cur);
        for (const Node& cn : cur)
        {
          visit.push_back(cn);
        }
      }
    }
    else
    {
      curEval = it->second;
      if (curEval.isNull())
      {
        Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
        Node ret = cur;
        bool childChanged = false;
        std::vector<Node> children;
        Kind ck = cur.getKind();
        // If a parameterized node that is not APPLY_UF (which is handled below,
        // we add it to the children vector.
        if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
        {
          children.push_back(cur.getOperator());
        }
        else if (ck == ITE)
        {
          // get evaluation of condition
          it = visited.find(cur[0]);
          Assert(it != visited.end());
          Assert(!it->second.isNull());
          if (!it->second.isConst())
          {
            Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
                                "ITE to const, FAIL\n";
            return Node::null();
          }
          // pick child to evaluate depending on condition eval
          unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
          Trace("fd-eval-debug2")
              << "FunDefEvaluator: result of ITE condition : "
              << it->second.getConst<bool>() << "\n";
          // the result will be the result of evaluation the child
          visited[cur] = cur[childIdxToEval];
          // push back self and child. The child will be evaluated first and
          // result will be the result of evaluation child
          visit.push_back(cur);
          visit.push_back(cur[childIdxToEval]);
          Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
                                  << cur[childIdxToEval] << "\n";
          continue;
        }
        unsigned child CVC5_UNUSED = 0;
        for (const Node& cn : cur)
        {
          it = visited.find(cn);
          Assert(it != visited.end());
          Assert(!it->second.isNull());
          childChanged = childChanged || cn != it->second;
          children.push_back(it->second);
          Trace("fd-eval-debug2") << "argument " << child++
                                  << " eval : " << it->second << std::endl;
        }
        if (cur.getKind() == APPLY_UF)
        {
          // need to evaluate it
          f = cur.getOperator();
          Trace("fd-eval-debug2")
              << "FunDefEvaluator: need to eval " << f << "\n";
          itf = d_funDefMap.find(f);
          itCount = funDefCount.find(f);
          if (itCount == funDefCount.end())
          {
            funDefCount[f] = 0;
            itCount = funDefCount.find(f);
          }
          if (itf == d_funDefMap.end()
              || itCount->second > options::sygusRecFunEvalLimit())
          {
            Trace("fd-eval")
                << "FunDefEvaluator: "
                << (itf == d_funDefMap.end() ? "no definition for "
                                             : "too many evals for ")
                << f << ", FAIL" << std::endl;
            return Node::null();
          }
          ++funDefCount[f];
          // get the function definition
          Node sbody = itf->second.d_body;
          Trace("fd-eval-debug2")
              << "FunDefEvaluator: definition: " << sbody << "\n";
          const std::vector<Node>& args = itf->second.d_args;
          if (!args.empty())
          {
            // invoke it on arguments using the evaluator
            sbody = d_eval.eval(sbody, args, children);
            if (Trace.isOn("fd-eval-debug2"))
            {
              Trace("fd-eval-debug2")
                  << "FunDefEvaluator: evaluation with args:\n";
              for (const Node& ch : children)
              {
                Trace("fd-eval-debug2") << "..." << ch << "\n";
              }
              Trace("fd-eval-debug2")
                  << "FunDefEvaluator: results in " << sbody << "\n";
            }
            Assert(!sbody.isNull());
          }
          // our result is the result of the body
          visited[cur] = sbody;
          // If its not constant, we push back self and the substituted body.
          // Thus, we evaluate the body first; our result will be the result of
          // evaluating the body.
          if (!sbody.isConst())
          {
            Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
                                    << " from body " << sbody << "\n";
            visit.push_back(cur);
            visit.push_back(sbody);
          }
        }
        else
        {
          if (childChanged)
          {
            ret = nm->mkNode(cur.getKind(), children);
            ret = Rewriter::rewrite(ret);
          }
          Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
          visited[cur] = ret;
        }
      }
      else if (cur != curEval && !curEval.isConst())
      {
        Trace("fd-eval-debug") << "from body " << cur << std::endl;
        Trace("fd-eval-debug") << "and eval  " << curEval << std::endl;
        // we had to evaluate our body, which should have a definition now
        it = visited.find(curEval);
        if (it == visited.end())
        {
          Trace("fd-eval-debug2") << "eval without definition\n";
          // this is the case where curEval was not a constant but it was
          // irreducible, for example (DT_SYGUS_EVAL e args)
          visited[cur] = curEval;
        }
        else
        {
          Trace("fd-eval-debug2")
              << "eval with definition " << it->second << "\n";
          visited[cur] = it->second;
      }
    }
    }
  } while (!visit.empty());
  Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  return visited[n];
}

bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }

const std::vector<Node>& FunDefEvaluator::getDefinitions() const
{
  return d_funDefs;
}
Node FunDefEvaluator::getDefinitionFor(Node f) const
{
  std::map<Node, FunDefInfo>::const_iterator it = d_funDefMap.find(f);
  if (it != d_funDefMap.end())
  {
    return it->second.d_quant;
  }
  return Node::null();
}

}  // 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, Haniel Barbosa, Mathias Preiner
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 evaluating terms with recursively
14		* defined functions.
15		*/
16
17		#include "theory/quantifiers/fun_def_evaluator.h"
18
19		#include "options/quantifiers_options.h"
20		#include "theory/quantifiers/quantifiers_attributes.h"
21		#include "theory/rewriter.h"
22
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29	1233	FunDefEvaluator::FunDefEvaluator() {}
30
31	33	void FunDefEvaluator::assertDefinition(Node q)
32		{
33	33	Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
34	66	Node h = QuantAttributes::getFunDefHead(q);
35	33	if (h.isNull())
36		{
37		// not a function definition
38		return;
39		}
40		// h possibly with zero arguments?
41	66	Node f = h.hasOperator() ? h.getOperator() : h;
42	33	Assert(d_funDefMap.find(f) == d_funDefMap.end())
43		<< "FunDefEvaluator::assertDefinition: function already defined";
44	33	d_funDefs.push_back(q);
45	33	FunDefInfo& fdi = d_funDefMap[f];
46	33	fdi.d_quant = q;
47	33	fdi.d_body = QuantAttributes::getFunDefBody(q);
48	33	Assert(!fdi.d_body.isNull());
49	33	fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
50	66	Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
51	33	<< fdi.d_args << " / " << fdi.d_body << std::endl;
52		}
53
54	975	Node FunDefEvaluator::evaluate(Node n) const
55		{
56		// should do standard rewrite before this call
57	975	Assert(Rewriter::rewrite(n) == n);
58	975	Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
59	975	NodeManager* nm = NodeManager::currentNM();
60	1950	std::unordered_map<TNode, unsigned> funDefCount;
61	975	std::unordered_map<TNode, unsigned>::iterator itCount;
62	1950	std::unordered_map<TNode, Node> visited;
63	975	std::unordered_map<TNode, Node>::iterator it;
64	975	std::map<Node, FunDefInfo>::const_iterator itf;
65	1950	std::vector<TNode> visit;
66	1950	TNode cur;
67	1950	TNode curEval;
68	1950	Node f;
69	975	visit.push_back(n);
70	34865	do
71		{
72	35840	cur = visit.back();
73	35840	visit.pop_back();
74	35840	it = visited.find(cur);
75	35840	Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
76
77	35840	if (it == visited.end())
78		{
79	16359	if (cur.isConst())
80		{
81	5131	Trace("fd-eval-debug") << "constant " << cur << std::endl;
82	5131	visited[cur] = cur;
83		}
84	11228	else if (cur.getKind() == ITE)
85		{
86	934	Trace("fd-eval-debug") << "ITE " << cur << std::endl;
87	934	visited[cur] = Node::null();
88	934	visit.push_back(cur);
89	934	visit.push_back(cur[0]);
90		}
91		else
92		{
93	10294	Trace("fd-eval-debug") << "recurse " << cur << std::endl;
94	10294	visited[cur] = Node::null();
95	10294	visit.push_back(cur);
96	30686	for (const Node& cn : cur)
97		{
98	20392	visit.push_back(cn);
99		}
100		}
101		}
102		else
103		{
104	19481	curEval = it->second;
105	19481	if (curEval.isNull())
106		{
107	10106	Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
108	19318	Node ret = cur;
109	10106	bool childChanged = false;
110	19318	std::vector<Node> children;
111	10106	Kind ck = cur.getKind();
112		// If a parameterized node that is not APPLY_UF (which is handled below,
113		// we add it to the children vector.
114	10106	if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
115		{
116	1875	children.push_back(cur.getOperator());
117		}
118	8231	else if (ck == ITE)
119		{
120		// get evaluation of condition
121	894	it = visited.find(cur[0]);
122	894	Assert(it != visited.end());
123	894	Assert(!it->second.isNull());
124	894	if (!it->second.isConst())
125		{
126	370	Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
127		"ITE to const, FAIL\n";
128	370	return Node::null();
129		}
130		// pick child to evaluate depending on condition eval
131	524	unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
132	1048	Trace("fd-eval-debug2")
133	524	<< "FunDefEvaluator: result of ITE condition : "
134	524	<< it->second.getConst<bool>() << "\n";
135		// the result will be the result of evaluation the child
136	524	visited[cur] = cur[childIdxToEval];
137		// push back self and child. The child will be evaluated first and
138		// result will be the result of evaluation child
139	524	visit.push_back(cur);
140	524	visit.push_back(cur[childIdxToEval]);
141	1048	Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
142	524	<< cur[childIdxToEval] << "\n";
143	524	continue;
144		}
145	9212	unsigned child CVC5_UNUSED = 0;
146	27477	for (const Node& cn : cur)
147		{
148	18265	it = visited.find(cn);
149	18265	Assert(it != visited.end());
150	18265	Assert(!it->second.isNull());
151	18265	childChanged = childChanged \|\| cn != it->second;
152	18265	children.push_back(it->second);
153	36530	Trace("fd-eval-debug2") << "argument " << child++
154	18265	<< " eval : " << it->second << std::endl;
155		}
156	9212	if (cur.getKind() == APPLY_UF)
157		{
158		// need to evaluate it
159	3404	f = cur.getOperator();
160	6808	Trace("fd-eval-debug2")
161	3404	<< "FunDefEvaluator: need to eval " << f << "\n";
162	3404	itf = d_funDefMap.find(f);
163	3404	itCount = funDefCount.find(f);
164	3404	if (itCount == funDefCount.end())
165		{
166	1373	funDefCount[f] = 0;
167	1373	itCount = funDefCount.find(f);
168		}
169	6808	if (itf == d_funDefMap.end()
170	3404	\|\| itCount->second > options::sygusRecFunEvalLimit())
171		{
172		Trace("fd-eval")
173		<< "FunDefEvaluator: "
174		<< (itf == d_funDefMap.end() ? "no definition for "
175		: "too many evals for ")
176		<< f << ", FAIL" << std::endl;
177		return Node::null();
178		}
179	3404	++funDefCount[f];
180		// get the function definition
181	6808	Node sbody = itf->second.d_body;
182	6808	Trace("fd-eval-debug2")
183	3404	<< "FunDefEvaluator: definition: " << sbody << "\n";
184	3404	const std::vector<Node>& args = itf->second.d_args;
185	3404	if (!args.empty())
186		{
187		// invoke it on arguments using the evaluator
188	3404	sbody = d_eval.eval(sbody, args, children);
189	3404	if (Trace.isOn("fd-eval-debug2"))
190		{
191		Trace("fd-eval-debug2")
192		<< "FunDefEvaluator: evaluation with args:\n";
193		for (const Node& ch : children)
194		{
195		Trace("fd-eval-debug2") << "..." << ch << "\n";
196		}
197		Trace("fd-eval-debug2")
198		<< "FunDefEvaluator: results in " << sbody << "\n";
199		}
200	3404	Assert(!sbody.isNull());
201		}
202		// our result is the result of the body
203	3404	visited[cur] = sbody;
204		// If its not constant, we push back self and the substituted body.
205		// Thus, we evaluate the body first; our result will be the result of
206		// evaluating the body.
207	3404	if (!sbody.isConst())
208		{
209	3804	Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
210	1902	<< " from body " << sbody << "\n";
211	1902	visit.push_back(cur);
212	1902	visit.push_back(sbody);
213		}
214		}
215		else
216		{
217	5808	if (childChanged)
218		{
219	2471	ret = nm->mkNode(cur.getKind(), children);
220	2471	ret = Rewriter::rewrite(ret);
221		}
222	5808	Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
223	5808	visited[cur] = ret;
224		}
225		}
226	9375	else if (cur != curEval && !curEval.isConst())
227		{
228	1839	Trace("fd-eval-debug") << "from body " << cur << std::endl;
229	1839	Trace("fd-eval-debug") << "and eval " << curEval << std::endl;
230		// we had to evaluate our body, which should have a definition now
231	1839	it = visited.find(curEval);
232	1839	if (it == visited.end())
233		{
234	1	Trace("fd-eval-debug2") << "eval without definition\n";
235		// this is the case where curEval was not a constant but it was
236		// irreducible, for example (DT_SYGUS_EVAL e args)
237	1	visited[cur] = curEval;
238		}
239		else
240		{
241	3676	Trace("fd-eval-debug2")
242	1838	<< "eval with definition " << it->second << "\n";
243	1838	visited[cur] = it->second;
244		}
245		}
246		}
247	35470	} while (!visit.empty());
248	605	Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
249	605	Assert(visited.find(n) != visited.end());
250	605	Assert(!visited.find(n)->second.isNull());
251	605	return visited[n];
252		}
253
254	48776	bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
255
256	376	const std::vector<Node>& FunDefEvaluator::getDefinitions() const
257		{
258	376	return d_funDefs;
259		}
260	178	Node FunDefEvaluator::getDefinitionFor(Node f) const
261		{
262	178	std::map<Node, FunDefInfo>::const_iterator it = d_funDefMap.find(f);
263	178	if (it != d_funDefMap.end())
264		{
265	35	return it->second.d_quant;
266		}
267	143	return Node::null();
268		}
269
270		} // namespace quantifiers
271		} // namespace theory
272	29574	} // namespace cvc5