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-05	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	1190	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	2794	Node FunDefEvaluator::evaluate(Node n) const
55		{
56		// should do standard rewrite before this call
57	2794	Assert(Rewriter::rewrite(n) == n);
58	2794	Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
59	2794	NodeManager* nm = NodeManager::currentNM();
60	5588	std::unordered_map<TNode, unsigned> funDefCount;
61	2794	std::unordered_map<TNode, unsigned>::iterator itCount;
62	5588	std::unordered_map<TNode, Node> visited;
63	2794	std::unordered_map<TNode, Node>::iterator it;
64	2794	std::map<Node, FunDefInfo>::const_iterator itf;
65	5588	std::vector<TNode> visit;
66	5588	TNode cur;
67	5588	TNode curEval;
68	5588	Node f;
69	2794	visit.push_back(n);
70	79824	do
71		{
72	82618	cur = visit.back();
73	82618	visit.pop_back();
74	82618	it = visited.find(cur);
75	82618	Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
76
77	82618	if (it == visited.end())
78		{
79	40732	if (cur.isConst())
80		{
81	13291	Trace("fd-eval-debug") << "constant " << cur << std::endl;
82	13291	visited[cur] = cur;
83		}
84	27441	else if (cur.getKind() == ITE)
85		{
86	2135	Trace("fd-eval-debug") << "ITE " << cur << std::endl;
87	2135	visited[cur] = Node::null();
88	2135	visit.push_back(cur);
89	2135	visit.push_back(cur[0]);
90		}
91		else
92		{
93	25306	Trace("fd-eval-debug") << "recurse " << cur << std::endl;
94	25306	visited[cur] = Node::null();
95	25306	visit.push_back(cur);
96	75029	for (const Node& cn : cur)
97		{
98	49723	visit.push_back(cn);
99		}
100		}
101		}
102		else
103		{
104	41886	curEval = it->second;
105	41886	if (curEval.isNull())
106		{
107	23874	Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
108	45896	Node ret = cur;
109	23874	bool childChanged = false;
110	45896	std::vector<Node> children;
111	23874	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	23874	if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
115		{
116	5250	children.push_back(cur.getOperator());
117		}
118	18624	else if (ck == ITE)
119		{
120		// get evaluation of condition
121	1852	it = visited.find(cur[0]);
122	1852	Assert(it != visited.end());
123	1852	Assert(!it->second.isNull());
124	1852	if (!it->second.isConst())
125		{
126	874	Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
127		"ITE to const, FAIL\n";
128	874	return Node::null();
129		}
130		// pick child to evaluate depending on condition eval
131	978	unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
132	1956	Trace("fd-eval-debug2")
133	978	<< "FunDefEvaluator: result of ITE condition : "
134	978	<< it->second.getConst<bool>() << "\n";
135		// the result will be the result of evaluation the child
136	978	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	978	visit.push_back(cur);
140	978	visit.push_back(cur[childIdxToEval]);
141	1956	Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
142	978	<< cur[childIdxToEval] << "\n";
143	978	continue;
144		}
145	22022	unsigned child CVC5_UNUSED = 0;
146	64884	for (const Node& cn : cur)
147		{
148	42862	it = visited.find(cn);
149	42862	Assert(it != visited.end());
150	42862	Assert(!it->second.isNull());
151	42862	childChanged = childChanged \|\| cn != it->second;
152	42862	children.push_back(it->second);
153	85724	Trace("fd-eval-debug2") << "argument " << child++
154	42862	<< " eval : " << it->second << std::endl;
155		}
156	22022	if (cur.getKind() == APPLY_UF)
157		{
158		// need to evaluate it
159	5325	f = cur.getOperator();
160	10650	Trace("fd-eval-debug2")
161	5325	<< "FunDefEvaluator: need to eval " << f << "\n";
162	5325	itf = d_funDefMap.find(f);
163	5325	itCount = funDefCount.find(f);
164	5325	if (itCount == funDefCount.end())
165		{
166	3215	funDefCount[f] = 0;
167	3215	itCount = funDefCount.find(f);
168		}
169	10650	if (itf == d_funDefMap.end()
170	5325	\|\| 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	5325	++funDefCount[f];
180		// get the function definition
181	10650	Node sbody = itf->second.d_body;
182	10650	Trace("fd-eval-debug2")
183	5325	<< "FunDefEvaluator: definition: " << sbody << "\n";
184	5325	const std::vector<Node>& args = itf->second.d_args;
185	5325	if (!args.empty())
186		{
187		// invoke it on arguments using the evaluator
188	5325	sbody = d_eval.eval(sbody, args, children);
189	5325	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	5325	Assert(!sbody.isNull());
201		}
202		// our result is the result of the body
203	5325	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	5325	if (!sbody.isConst())
208		{
209	7416	Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
210	3708	<< " from body " << sbody << "\n";
211	3708	visit.push_back(cur);
212	3708	visit.push_back(sbody);
213		}
214		}
215		else
216		{
217	16697	if (childChanged)
218		{
219	4311	ret = nm->mkNode(cur.getKind(), children);
220	4311	ret = Rewriter::rewrite(ret);
221		}
222	16697	Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
223	16697	visited[cur] = ret;
224		}
225		}
226	18012	else if (cur != curEval && !curEval.isConst())
227		{
228	2702	Trace("fd-eval-debug") << "from body " << cur << std::endl;
229	2702	Trace("fd-eval-debug") << "and eval " << curEval << std::endl;
230		// we had to evaluate our body, which should have a definition now
231	2702	it = visited.find(curEval);
232	2702	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	5402	Trace("fd-eval-debug2")
242	2701	<< "eval with definition " << it->second << "\n";
243	2701	visited[cur] = it->second;
244		}
245		}
246		}
247	81744	} while (!visit.empty());
248	1920	Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
249	1920	Assert(visited.find(n) != visited.end());
250	1920	Assert(!visited.find(n)->second.isNull());
251	1920	return visited[n];
252		}
253
254	171357	bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
255
256	424	const std::vector<Node>& FunDefEvaluator::getDefinitions() const
257		{
258	424	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	29505	} // namespace cvc5