Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/fun_def_evaluator.cpp	Lines:	138	152	90.8 %
Date:	2021-11-07	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(Env& env) : EnvObj(env) {}

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::evaluateDefinitions(Node n) const
{
  // should do standard rewrite before this call
  Assert(rewrite(n) == n);
  Trace("fd-eval") << "FunDefEvaluator: evaluateDefinitions " << 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 = evaluate(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 = 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	1900	FunDefEvaluator::FunDefEvaluator(Env& env) : EnvObj(env) {}
30
31	36	void FunDefEvaluator::assertDefinition(Node q)
32		{
33	36	Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
34	72	Node h = QuantAttributes::getFunDefHead(q);
35	36	if (h.isNull())
36		{
37		// not a function definition
38		return;
39		}
40		// h possibly with zero arguments?
41	72	Node f = h.hasOperator() ? h.getOperator() : h;
42	36	Assert(d_funDefMap.find(f) == d_funDefMap.end())
43		<< "FunDefEvaluator::assertDefinition: function already defined";
44	36	d_funDefs.push_back(q);
45	36	FunDefInfo& fdi = d_funDefMap[f];
46	36	fdi.d_quant = q;
47	36	fdi.d_body = QuantAttributes::getFunDefBody(q);
48	36	Assert(!fdi.d_body.isNull());
49	36	fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
50	72	Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
51	36	<< fdi.d_args << " / " << fdi.d_body << std::endl;
52		}
53
54	1678	Node FunDefEvaluator::evaluateDefinitions(Node n) const
55		{
56		// should do standard rewrite before this call
57	1678	Assert(rewrite(n) == n);
58	1678	Trace("fd-eval") << "FunDefEvaluator: evaluateDefinitions " << n << std::endl;
59	1678	NodeManager* nm = NodeManager::currentNM();
60	3356	std::unordered_map<TNode, unsigned> funDefCount;
61	1678	std::unordered_map<TNode, unsigned>::iterator itCount;
62	3356	std::unordered_map<TNode, Node> visited;
63	1678	std::unordered_map<TNode, Node>::iterator it;
64	1678	std::map<Node, FunDefInfo>::const_iterator itf;
65	3356	std::vector<TNode> visit;
66	3356	TNode cur;
67	3356	TNode curEval;
68	3356	Node f;
69	1678	visit.push_back(n);
70	49050	do
71		{
72	50728	cur = visit.back();
73	50728	visit.pop_back();
74	50728	it = visited.find(cur);
75	50728	Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
76
77	50728	if (it == visited.end())
78		{
79	23998	if (cur.isConst())
80		{
81	7747	Trace("fd-eval-debug") << "constant " << cur << std::endl;
82	7747	visited[cur] = cur;
83		}
84	16251	else if (cur.getKind() == ITE)
85		{
86	1201	Trace("fd-eval-debug") << "ITE " << cur << std::endl;
87	1201	visited[cur] = Node::null();
88	1201	visit.push_back(cur);
89	1201	visit.push_back(cur[0]);
90		}
91		else
92		{
93	15050	Trace("fd-eval-debug") << "recurse " << cur << std::endl;
94	15050	visited[cur] = Node::null();
95	15050	visit.push_back(cur);
96	43547	for (const Node& cn : cur)
97		{
98	28497	visit.push_back(cn);
99		}
100		}
101		}
102		else
103		{
104	26730	curEval = it->second;
105	26730	if (curEval.isNull())
106		{
107	14736	Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
108	28311	Node ret = cur;
109	14736	bool childChanged = false;
110	28311	std::vector<Node> children;
111	14736	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	14736	if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
115		{
116	2143	children.push_back(cur.getOperator());
117		}
118	12593	else if (ck == ITE)
119		{
120		// get evaluation of condition
121	1161	it = visited.find(cur[0]);
122	1161	Assert(it != visited.end());
123	1161	Assert(!it->second.isNull());
124	1161	if (!it->second.isConst())
125		{
126	638	Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
127		"ITE to const, FAIL\n";
128	638	return Node::null();
129		}
130		// pick child to evaluate depending on condition eval
131	523	unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
132	1046	Trace("fd-eval-debug2")
133	523	<< "FunDefEvaluator: result of ITE condition : "
134	523	<< it->second.getConst<bool>() << "\n";
135		// the result will be the result of evaluation the child
136	523	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	523	visit.push_back(cur);
140	523	visit.push_back(cur[childIdxToEval]);
141	1046	Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
142	523	<< cur[childIdxToEval] << "\n";
143	523	continue;
144		}
145	13575	unsigned child CVC5_UNUSED = 0;
146	39140	for (const Node& cn : cur)
147		{
148	25565	it = visited.find(cn);
149	25565	Assert(it != visited.end());
150	25565	Assert(!it->second.isNull());
151	25565	childChanged = childChanged \|\| cn != it->second;
152	25565	children.push_back(it->second);
153	51130	Trace("fd-eval-debug2") << "argument " << child++
154	25565	<< " eval : " << it->second << std::endl;
155		}
156	13575	if (cur.getKind() == APPLY_UF)
157		{
158		// need to evaluate it
159	4823	f = cur.getOperator();
160	9646	Trace("fd-eval-debug2")
161	4823	<< "FunDefEvaluator: need to eval " << f << "\n";
162	4823	itf = d_funDefMap.find(f);
163	4823	itCount = funDefCount.find(f);
164	4823	if (itCount == funDefCount.end())
165		{
166	1995	funDefCount[f] = 0;
167	1995	itCount = funDefCount.find(f);
168		}
169	9646	if (itf == d_funDefMap.end()
170	4823	\|\| 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	4823	++funDefCount[f];
180		// get the function definition
181	9646	Node sbody = itf->second.d_body;
182	9646	Trace("fd-eval-debug2")
183	4823	<< "FunDefEvaluator: definition: " << sbody << "\n";
184	4823	const std::vector<Node>& args = itf->second.d_args;
185	4823	if (!args.empty())
186		{
187		// invoke it on arguments using the evaluator
188	4823	sbody = evaluate(sbody, args, children);
189	4823	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	4823	Assert(!sbody.isNull());
201		}
202		// our result is the result of the body
203	4823	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	4823	if (!sbody.isConst())
208		{
209	5628	Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
210	2814	<< " from body " << sbody << "\n";
211	2814	visit.push_back(cur);
212	2814	visit.push_back(sbody);
213		}
214		}
215		else
216		{
217	8752	if (childChanged)
218		{
219	3051	ret = nm->mkNode(cur.getKind(), children);
220	3051	ret = rewrite(ret);
221		}
222	8752	Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
223	8752	visited[cur] = ret;
224		}
225		}
226	11994	else if (cur != curEval && !curEval.isConst())
227		{
228	2485	Trace("fd-eval-debug") << "from body " << cur << std::endl;
229	2485	Trace("fd-eval-debug") << "and eval " << curEval << std::endl;
230		// we had to evaluate our body, which should have a definition now
231	2485	it = visited.find(curEval);
232	2485	if (it == visited.end())
233		{
234	2	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	2	visited[cur] = curEval;
238		}
239		else
240		{
241	4966	Trace("fd-eval-debug2")
242	2483	<< "eval with definition " << it->second << "\n";
243	2483	visited[cur] = it->second;
244		}
245		}
246		}
247	50090	} while (!visit.empty());
248	1040	Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
249	1040	Assert(visited.find(n) != visited.end());
250	1040	Assert(!visited.find(n)->second.isNull());
251	1040	return visited[n];
252		}
253
254	137729	bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
255
256	740	const std::vector<Node>& FunDefEvaluator::getDefinitions() const
257		{
258	740	return d_funDefs;
259		}
260	315	Node FunDefEvaluator::getDefinitionFor(Node f) const
261		{
262	315	std::map<Node, FunDefInfo>::const_iterator it = d_funDefMap.find(f);
263	315	if (it != d_funDefMap.end())
264		{
265	62	return it->second.d_quant;
266		}
267	253	return Node::null();
268		}
269
270		} // namespace quantifiers
271		} // namespace theory
272	31137	} // namespace cvc5