Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/fun_def_evaluator.cpp	Lines:	129	143	90.2 %
Date:	2021-05-24	Branches:	321	764	42.0 %


/******************************************************************************
 * 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";
  FunDefInfo& fdi = d_funDefMap[f];
  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(); }

}  // 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	1529	FunDefEvaluator::FunDefEvaluator() {}
30
31	32	void FunDefEvaluator::assertDefinition(Node q)
32		{
33	32	Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
34	64	Node h = QuantAttributes::getFunDefHead(q);
35	32	if (h.isNull())
36		{
37		// not a function definition
38		return;
39		}
40		// h possibly with zero arguments?
41	64	Node f = h.hasOperator() ? h.getOperator() : h;
42	32	Assert(d_funDefMap.find(f) == d_funDefMap.end())
43		<< "FunDefEvaluator::assertDefinition: function already defined";
44	32	FunDefInfo& fdi = d_funDefMap[f];
45	32	fdi.d_body = QuantAttributes::getFunDefBody(q);
46	32	Assert(!fdi.d_body.isNull());
47	32	fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
48	64	Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
49	32	<< fdi.d_args << " / " << fdi.d_body << std::endl;
50		}
51
52	2524	Node FunDefEvaluator::evaluate(Node n) const
53		{
54		// should do standard rewrite before this call
55	2524	Assert(Rewriter::rewrite(n) == n);
56	2524	Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
57	2524	NodeManager* nm = NodeManager::currentNM();
58	5048	std::unordered_map<TNode, unsigned> funDefCount;
59	2524	std::unordered_map<TNode, unsigned>::iterator itCount;
60	5048	std::unordered_map<TNode, Node> visited;
61	2524	std::unordered_map<TNode, Node>::iterator it;
62	2524	std::map<Node, FunDefInfo>::const_iterator itf;
63	5048	std::vector<TNode> visit;
64	5048	TNode cur;
65	5048	TNode curEval;
66	5048	Node f;
67	2524	visit.push_back(n);
68	77616	do
69		{
70	80140	cur = visit.back();
71	80140	visit.pop_back();
72	80140	it = visited.find(cur);
73	80140	Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
74
75	80140	if (it == visited.end())
76		{
77	39239	if (cur.isConst())
78		{
79	12729	Trace("fd-eval-debug") << "constant " << cur << std::endl;
80	12729	visited[cur] = cur;
81		}
82	26510	else if (cur.getKind() == ITE)
83		{
84	2087	Trace("fd-eval-debug") << "ITE " << cur << std::endl;
85	2087	visited[cur] = Node::null();
86	2087	visit.push_back(cur);
87	2087	visit.push_back(cur[0]);
88		}
89		else
90		{
91	24423	Trace("fd-eval-debug") << "recurse " << cur << std::endl;
92	24423	visited[cur] = Node::null();
93	24423	visit.push_back(cur);
94	72752	for (const Node& cn : cur)
95		{
96	48329	visit.push_back(cn);
97		}
98		}
99		}
100		else
101		{
102	40901	curEval = it->second;
103	40901	if (curEval.isNull())
104		{
105	23067	Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
106	44330	Node ret = cur;
107	23067	bool childChanged = false;
108	44330	std::vector<Node> children;
109	23067	Kind ck = cur.getKind();
110		// If a parameterized node that is not APPLY_UF (which is handled below,
111		// we add it to the children vector.
112	23067	if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
113		{
114	5253	children.push_back(cur.getOperator());
115		}
116	17814	else if (ck == ITE)
117		{
118		// get evaluation of condition
119	1804	it = visited.find(cur[0]);
120	1804	Assert(it != visited.end());
121	1804	Assert(!it->second.isNull());
122	1804	if (!it->second.isConst())
123		{
124	826	Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
125		"ITE to const, FAIL\n";
126	826	return Node::null();
127		}
128		// pick child to evaluate depending on condition eval
129	978	unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
130	1956	Trace("fd-eval-debug2")
131	978	<< "FunDefEvaluator: result of ITE condition : "
132	978	<< it->second.getConst<bool>() << "\n";
133		// the result will be the result of evaluation the child
134	978	visited[cur] = cur[childIdxToEval];
135		// push back self and child. The child will be evaluated first and
136		// result will be the result of evaluation child
137	978	visit.push_back(cur);
138	978	visit.push_back(cur[childIdxToEval]);
139	1956	Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
140	978	<< cur[childIdxToEval] << "\n";
141	978	continue;
142		}
143	21263	unsigned child CVC5_UNUSED = 0;
144	62979	for (const Node& cn : cur)
145		{
146	41716	it = visited.find(cn);
147	41716	Assert(it != visited.end());
148	41716	Assert(!it->second.isNull());
149	41716	childChanged = childChanged \|\| cn != it->second;
150	41716	children.push_back(it->second);
151	83432	Trace("fd-eval-debug2") << "argument " << child++
152	41716	<< " eval : " << it->second << std::endl;
153		}
154	21263	if (cur.getKind() == APPLY_UF)
155		{
156		// need to evaluate it
157	5236	f = cur.getOperator();
158	10472	Trace("fd-eval-debug2")
159	5236	<< "FunDefEvaluator: need to eval " << f << "\n";
160	5236	itf = d_funDefMap.find(f);
161	5236	itCount = funDefCount.find(f);
162	5236	if (itCount == funDefCount.end())
163		{
164	3138	funDefCount[f] = 0;
165	3138	itCount = funDefCount.find(f);
166		}
167	10472	if (itf == d_funDefMap.end()
168	10472	\|\| itCount->second > options::sygusRecFunEvalLimit())
169		{
170		Trace("fd-eval")
171		<< "FunDefEvaluator: "
172		<< (itf == d_funDefMap.end() ? "no definition for "
173		: "too many evals for ")
174		<< f << ", FAIL" << std::endl;
175		return Node::null();
176		}
177	5236	++funDefCount[f];
178		// get the function definition
179	10472	Node sbody = itf->second.d_body;
180	10472	Trace("fd-eval-debug2")
181	5236	<< "FunDefEvaluator: definition: " << sbody << "\n";
182	5236	const std::vector<Node>& args = itf->second.d_args;
183	5236	if (!args.empty())
184		{
185		// invoke it on arguments using the evaluator
186	5236	sbody = d_eval.eval(sbody, args, children);
187	5236	if (Trace.isOn("fd-eval-debug2"))
188		{
189		Trace("fd-eval-debug2")
190		<< "FunDefEvaluator: evaluation with args:\n";
191		for (const Node& ch : children)
192		{
193		Trace("fd-eval-debug2") << "..." << ch << "\n";
194		}
195		Trace("fd-eval-debug2")
196		<< "FunDefEvaluator: results in " << sbody << "\n";
197		}
198	5236	Assert(!sbody.isNull());
199		}
200		// our result is the result of the body
201	5236	visited[cur] = sbody;
202		// If its not constant, we push back self and the substituted body.
203		// Thus, we evaluate the body first; our result will be the result of
204		// evaluating the body.
205	5236	if (!sbody.isConst())
206		{
207	7296	Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
208	3648	<< " from body " << sbody << "\n";
209	3648	visit.push_back(cur);
210	3648	visit.push_back(sbody);
211		}
212		}
213		else
214		{
215	16027	if (childChanged)
216		{
217	4279	ret = nm->mkNode(cur.getKind(), children);
218	4279	ret = Rewriter::rewrite(ret);
219		}
220	16027	Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
221	16027	visited[cur] = ret;
222		}
223		}
224	17834	else if (cur != curEval && !curEval.isConst())
225		{
226	2690	Trace("fd-eval-debug") << "from body " << cur << std::endl;
227	2690	Trace("fd-eval-debug") << "and eval " << curEval << std::endl;
228		// we had to evaluate our body, which should have a definition now
229	2690	it = visited.find(curEval);
230	2690	if (it == visited.end())
231		{
232	1	Trace("fd-eval-debug2") << "eval without definition\n";
233		// this is the case where curEval was not a constant but it was
234		// irreducible, for example (DT_SYGUS_EVAL e args)
235	1	visited[cur] = curEval;
236		}
237		else
238		{
239	5378	Trace("fd-eval-debug2")
240	2689	<< "eval with definition " << it->second << "\n";
241	2689	visited[cur] = it->second;
242		}
243		}
244		}
245	79314	} while (!visit.empty());
246	1698	Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
247	1698	Assert(visited.find(n) != visited.end());
248	1698	Assert(!visited.find(n)->second.isNull());
249	1698	return visited[n];
250		}
251
252	163409	bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
253
254		} // namespace quantifiers
255		} // namespace theory
256	33427	} // namespace cvc5