Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/theory_uf_rewriter.cpp	Lines:	106	121	87.6 %
Date:	2021-11-06	Branches:	295	694	42.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Theory UF rewriter
 */

#include "theory/uf/theory_uf_rewriter.h"

#include "expr/node_algorithm.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
#include "theory/uf/function_const.h"

namespace cvc5 {
namespace theory {
namespace uf {

TheoryUfRewriter::TheoryUfRewriter(bool isHigherOrder)
    : d_isHigherOrder(isHigherOrder)
{
}

RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
{
  if (node.getKind() == kind::EQUAL)
  {
    if (node[0] == node[1])
    {
      return RewriteResponse(REWRITE_DONE,
                             NodeManager::currentNM()->mkConst(true));
    }
    else if (node[0].isConst() && node[1].isConst())
    {
      // uninterpreted constants are all distinct
      return RewriteResponse(REWRITE_DONE,
                             NodeManager::currentNM()->mkConst(false));
    }
    if (node[0] > node[1])
    {
      Node newNode =
          NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
      return RewriteResponse(REWRITE_DONE, newNode);
    }
  }
  if (node.getKind() == kind::APPLY_UF)
  {
    if (node.getOperator().getKind() == kind::LAMBDA)
    {
      Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing all args of : " << node
                          << "\n";
      TNode lambda = node.getOperator();
      Node ret;
      // build capture-avoiding substitution since in HOL shadowing may have
      // been introduced
      if (d_isHigherOrder)
      {
        std::vector<Node> vars;
        std::vector<Node> subs;
        for (const Node& v : lambda[0])
        {
          vars.push_back(v);
        }
        for (const Node& s : node)
        {
          subs.push_back(s);
        }
        if (Trace.isOn("uf-ho-beta"))
        {
          Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
                              << " vars into " << subs.size() << " terms :\n";
          for (unsigned i = 0, size = subs.size(); i < size; ++i)
          {
            Trace("uf-ho-beta")
                << "uf-ho-beta: .... " << vars[i] << " |-> " << subs[i] << "\n";
          }
        }
        ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
        Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
      }
      else
      {
        std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
        std::vector<TNode> subs(node.begin(), node.end());
        ret = lambda[1].substitute(
            vars.begin(), vars.end(), subs.begin(), subs.end());
      }
      return RewriteResponse(REWRITE_AGAIN_FULL, ret);
    }
    else if (!canUseAsApplyUfOperator(node.getOperator()))
    {
      return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
    }
  }
  else if (node.getKind() == kind::HO_APPLY)
  {
    if (node[0].getKind() == kind::LAMBDA)
    {
      // resolve one argument of the lambda
      Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing one argument of : "
                          << node[0] << " with " << node[1] << "\n";

      // reconstruct the lambda first to avoid variable shadowing
      Node new_body = node[0][1];
      if (node[0][0].getNumChildren() > 1)
      {
        std::vector<Node> new_vars(node[0][0].begin() + 1, node[0][0].end());
        std::vector<Node> largs;
        largs.push_back(
            NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, new_vars));
        largs.push_back(new_body);
        new_body = NodeManager::currentNM()->mkNode(kind::LAMBDA, largs);
        Trace("uf-ho-beta")
            << "uf-ho-beta : ....new lambda : " << new_body << "\n";
      }

      // build capture-avoiding substitution since in HOL shadowing may have
      // been introduced
      if (d_isHigherOrder)
      {
        Node arg = Rewriter::rewrite(node[1]);
        Node var = node[0][0][0];
        new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
      }
      else
      {
        TNode arg = Rewriter::rewrite(node[1]);
        TNode var = node[0][0][0];
        new_body = new_body.substitute(var, arg);
      }
      Trace("uf-ho-beta") << "uf-ho-beta : ..new body : " << new_body << "\n";
      return RewriteResponse(REWRITE_AGAIN_FULL, new_body);
    }
  }
  else if (node.getKind() == kind::LAMBDA)
  {
    Node ret = rewriteLambda(node);
    return RewriteResponse(REWRITE_DONE, ret);
  }
  return RewriteResponse(REWRITE_DONE, node);
}

RewriteResponse TheoryUfRewriter::preRewrite(TNode node)
{
  if (node.getKind() == kind::EQUAL)
  {
    if (node[0] == node[1])
    {
      return RewriteResponse(REWRITE_DONE,
                             NodeManager::currentNM()->mkConst(true));
    }
    else if (node[0].isConst() && node[1].isConst())
    {
      // uninterpreted constants are all distinct
      return RewriteResponse(REWRITE_DONE,
                             NodeManager::currentNM()->mkConst(false));
    }
  }
  return RewriteResponse(REWRITE_DONE, node);
}

Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n)
{
  Assert(n.getKind() == kind::APPLY_UF);
  Node curr = n.getOperator();
  for (unsigned i = 0; i < n.getNumChildren(); i++)
  {
    curr = NodeManager::currentNM()->mkNode(kind::HO_APPLY, curr, n[i]);
  }
  return curr;
}
Node TheoryUfRewriter::getApplyUfForHoApply(TNode n)
{
  Assert(n.getType().getNumChildren() == 2);
  std::vector<TNode> children;
  TNode curr = decomposeHoApply(n, children, true);
  // if operator is standard
  if (canUseAsApplyUfOperator(curr))
  {
    return NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
  }
  // cannot construct APPLY_UF if operator is partially applied or is not
  // standard
  return Node::null();
}
Node TheoryUfRewriter::decomposeHoApply(TNode n,
                                        std::vector<TNode>& args,
                                        bool opInArgs)
{
  TNode curr = n;
  while (curr.getKind() == kind::HO_APPLY)
  {
    args.push_back(curr[1]);
    curr = curr[0];
  }
  if (opInArgs)
  {
    args.push_back(curr);
  }
  std::reverse(args.begin(), args.end());
  return curr;
}
bool TheoryUfRewriter::canUseAsApplyUfOperator(TNode n) { return n.isVar(); }

Node TheoryUfRewriter::rewriteLambda(Node node)
{
  Assert(node.getKind() == kind::LAMBDA);
  // The following code ensures that if node is equivalent to a constant
  // lambda, then we return the canonical representation for the lambda, which
  // in turn ensures that two constant lambdas are equivalent if and only
  // if they are the same node.
  // We canonicalize lambdas by turning them into array constants, applying
  // normalization on array constants, and then converting the array constant
  // back to a lambda.
  Trace("builtin-rewrite") << "Rewriting lambda " << node << "..." << std::endl;
  Node anode = FunctionConst::getArrayRepresentationForLambda(node);
  // Only rewrite constant array nodes, since these are the only cases
  // where we require canonicalization of lambdas. Moreover, applying the
  // below code is not correct if the arguments to the lambda occur
  // in return values. For example, lambda x. ite( x=1, f(x), c ) would
  // be converted to (store (storeall ... c) 1 f(x)), and then converted
  // to lambda y. ite( y=1, f(x), c), losing the relation between x and y.
  if (!anode.isNull() && anode.isConst())
  {
    Assert(anode.getType().isArray());
    // must get the standard bound variable list
    Node varList = NodeManager::currentNM()->getBoundVarListForFunctionType(
        node.getType());
    Node retNode =
        FunctionConst::getLambdaForArrayRepresentation(anode, varList);
    if (!retNode.isNull() && retNode != node)
    {
      Trace("builtin-rewrite") << "Rewrote lambda : " << std::endl;
      Trace("builtin-rewrite") << "     input  : " << node << std::endl;
      Trace("builtin-rewrite")
          << "     output : " << retNode << ", constant = " << retNode.isConst()
          << std::endl;
      Trace("builtin-rewrite")
          << "  array rep : " << anode << ", constant = " << anode.isConst()
          << std::endl;
      Assert(anode.isConst() == retNode.isConst());
      Assert(retNode.getType() == node.getType());
      Assert(expr::hasFreeVar(node) == expr::hasFreeVar(retNode));
      return retNode;
    }
  }
  else
  {
    Trace("builtin-rewrite-debug")
        << "...failed to get array representation." << std::endl;
  }
  return node;
}

}  // namespace uf
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Theory UF rewriter
14		*/
15
16		#include "theory/uf/theory_uf_rewriter.h"
17
18		#include "expr/node_algorithm.h"
19		#include "theory/rewriter.h"
20		#include "theory/substitutions.h"
21		#include "theory/uf/function_const.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace uf {
26
27	15272	TheoryUfRewriter::TheoryUfRewriter(bool isHigherOrder)
28	15272	: d_isHigherOrder(isHigherOrder)
29		{
30	15272	}
31
32	811844	RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
33		{
34	811844	if (node.getKind() == kind::EQUAL)
35		{
36	164870	if (node[0] == node[1])
37		{
38		return RewriteResponse(REWRITE_DONE,
39	54	NodeManager::currentNM()->mkConst(true));
40		}
41	164816	else if (node[0].isConst() && node[1].isConst())
42		{
43		// uninterpreted constants are all distinct
44		return RewriteResponse(REWRITE_DONE,
45	30	NodeManager::currentNM()->mkConst(false));
46		}
47	164786	if (node[0] > node[1])
48		{
49		Node newNode =
50	61366	NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
51	30683	return RewriteResponse(REWRITE_DONE, newNode);
52		}
53		}
54	781077	if (node.getKind() == kind::APPLY_UF)
55		{
56	619650	if (node.getOperator().getKind() == kind::LAMBDA)
57		{
58	23808	Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing all args of : " << node
59	11904	<< "\n";
60	23808	TNode lambda = node.getOperator();
61	23808	Node ret;
62		// build capture-avoiding substitution since in HOL shadowing may have
63		// been introduced
64	11904	if (d_isHigherOrder)
65		{
66	758	std::vector<Node> vars;
67	758	std::vector<Node> subs;
68	1122	for (const Node& v : lambda[0])
69		{
70	743	vars.push_back(v);
71		}
72	1122	for (const Node& s : node)
73		{
74	743	subs.push_back(s);
75		}
76	379	if (Trace.isOn("uf-ho-beta"))
77		{
78		Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
79		<< " vars into " << subs.size() << " terms :\n";
80		for (unsigned i = 0, size = subs.size(); i < size; ++i)
81		{
82		Trace("uf-ho-beta")
83		<< "uf-ho-beta: .... " << vars[i] << " \|-> " << subs[i] << "\n";
84		}
85		}
86	379	ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
87	379	Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
88		}
89		else
90		{
91	23050	std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
92	23050	std::vector<TNode> subs(node.begin(), node.end());
93	11525	ret = lambda[1].substitute(
94		vars.begin(), vars.end(), subs.begin(), subs.end());
95		}
96	11904	return RewriteResponse(REWRITE_AGAIN_FULL, ret);
97		}
98	607746	else if (!canUseAsApplyUfOperator(node.getOperator()))
99		{
100	38	return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
101		}
102		}
103	161427	else if (node.getKind() == kind::HO_APPLY)
104		{
105	18578	if (node[0].getKind() == kind::LAMBDA)
106		{
107		// resolve one argument of the lambda
108	316	Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing one argument of : "
109	158	<< node[0] << " with " << node[1] << "\n";
110
111		// reconstruct the lambda first to avoid variable shadowing
112	316	Node new_body = node[0][1];
113	158	if (node[0][0].getNumChildren() > 1)
114		{
115	186	std::vector<Node> new_vars(node[0][0].begin() + 1, node[0][0].end());
116	186	std::vector<Node> largs;
117	93	largs.push_back(
118	186	NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, new_vars));
119	93	largs.push_back(new_body);
120	93	new_body = NodeManager::currentNM()->mkNode(kind::LAMBDA, largs);
121	186	Trace("uf-ho-beta")
122	93	<< "uf-ho-beta : ....new lambda : " << new_body << "\n";
123		}
124
125		// build capture-avoiding substitution since in HOL shadowing may have
126		// been introduced
127	158	if (d_isHigherOrder)
128		{
129	316	Node arg = Rewriter::rewrite(node[1]);
130	316	Node var = node[0][0][0];
131	158	new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
132		}
133		else
134		{
135		TNode arg = Rewriter::rewrite(node[1]);
136		TNode var = node[0][0][0];
137		new_body = new_body.substitute(var, arg);
138		}
139	158	Trace("uf-ho-beta") << "uf-ho-beta : ..new body : " << new_body << "\n";
140	158	return RewriteResponse(REWRITE_AGAIN_FULL, new_body);
141		}
142		}
143	142849	else if (node.getKind() == kind::LAMBDA)
144		{
145	9808	Node ret = rewriteLambda(node);
146	4904	return RewriteResponse(REWRITE_DONE, ret);
147		}
148	764073	return RewriteResponse(REWRITE_DONE, node);
149		}
150
151	425624	RewriteResponse TheoryUfRewriter::preRewrite(TNode node)
152		{
153	425624	if (node.getKind() == kind::EQUAL)
154		{
155	92401	if (node[0] == node[1])
156		{
157		return RewriteResponse(REWRITE_DONE,
158	2842	NodeManager::currentNM()->mkConst(true));
159		}
160	89559	else if (node[0].isConst() && node[1].isConst())
161		{
162		// uninterpreted constants are all distinct
163		return RewriteResponse(REWRITE_DONE,
164	6370	NodeManager::currentNM()->mkConst(false));
165		}
166		}
167	416412	return RewriteResponse(REWRITE_DONE, node);
168		}
169
170	684286	Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n)
171		{
172	684286	Assert(n.getKind() == kind::APPLY_UF);
173	684286	Node curr = n.getOperator();
174	2051144	for (unsigned i = 0; i < n.getNumChildren(); i++)
175		{
176	1366858	curr = NodeManager::currentNM()->mkNode(kind::HO_APPLY, curr, n[i]);
177		}
178	684286	return curr;
179		}
180		Node TheoryUfRewriter::getApplyUfForHoApply(TNode n)
181		{
182		Assert(n.getType().getNumChildren() == 2);
183		std::vector<TNode> children;
184		TNode curr = decomposeHoApply(n, children, true);
185		// if operator is standard
186		if (canUseAsApplyUfOperator(curr))
187		{
188		return NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
189		}
190		// cannot construct APPLY_UF if operator is partially applied or is not
191		// standard
192		return Node::null();
193		}
194	359	Node TheoryUfRewriter::decomposeHoApply(TNode n,
195		std::vector<TNode>& args,
196		bool opInArgs)
197		{
198	718	TNode curr = n;
199	1539	while (curr.getKind() == kind::HO_APPLY)
200		{
201	590	args.push_back(curr[1]);
202	590	curr = curr[0];
203		}
204	359	if (opInArgs)
205		{
206	119	args.push_back(curr);
207		}
208	359	std::reverse(args.begin(), args.end());
209	718	return curr;
210		}
211	607984	bool TheoryUfRewriter::canUseAsApplyUfOperator(TNode n) { return n.isVar(); }
212
213	4904	Node TheoryUfRewriter::rewriteLambda(Node node)
214		{
215	4904	Assert(node.getKind() == kind::LAMBDA);
216		// The following code ensures that if node is equivalent to a constant
217		// lambda, then we return the canonical representation for the lambda, which
218		// in turn ensures that two constant lambdas are equivalent if and only
219		// if they are the same node.
220		// We canonicalize lambdas by turning them into array constants, applying
221		// normalization on array constants, and then converting the array constant
222		// back to a lambda.
223	4904	Trace("builtin-rewrite") << "Rewriting lambda " << node << "..." << std::endl;
224	9808	Node anode = FunctionConst::getArrayRepresentationForLambda(node);
225		// Only rewrite constant array nodes, since these are the only cases
226		// where we require canonicalization of lambdas. Moreover, applying the
227		// below code is not correct if the arguments to the lambda occur
228		// in return values. For example, lambda x. ite( x=1, f(x), c ) would
229		// be converted to (store (storeall ... c) 1 f(x)), and then converted
230		// to lambda y. ite( y=1, f(x), c), losing the relation between x and y.
231	4904	if (!anode.isNull() && anode.isConst())
232		{
233	1396	Assert(anode.getType().isArray());
234		// must get the standard bound variable list
235		Node varList = NodeManager::currentNM()->getBoundVarListForFunctionType(
236	2169	node.getType());
237		Node retNode =
238	2169	FunctionConst::getLambdaForArrayRepresentation(anode, varList);
239	1396	if (!retNode.isNull() && retNode != node)
240		{
241	623	Trace("builtin-rewrite") << "Rewrote lambda : " << std::endl;
242	623	Trace("builtin-rewrite") << " input : " << node << std::endl;
243	1246	Trace("builtin-rewrite")
244	1246	<< " output : " << retNode << ", constant = " << retNode.isConst()
245	623	<< std::endl;
246	1246	Trace("builtin-rewrite")
247	1246	<< " array rep : " << anode << ", constant = " << anode.isConst()
248	623	<< std::endl;
249	623	Assert(anode.isConst() == retNode.isConst());
250	623	Assert(retNode.getType() == node.getType());
251	623	Assert(expr::hasFreeVar(node) == expr::hasFreeVar(retNode));
252	623	return retNode;
253		}
254		}
255		else
256		{
257	7016	Trace("builtin-rewrite-debug")
258	3508	<< "...failed to get array representation." << std::endl;
259		}
260	4281	return node;
261		}
262
263		} // namespace uf
264		} // namespace theory
265	31137	} // namespace cvc5