Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/theory_uf_rewriter.cpp	Lines:	76	91	83.5 %
Date:	2021-05-22	Branches:	209	482	43.4 %


/******************************************************************************
 * 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 "options/uf_options.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"

namespace cvc5 {
namespace theory {
namespace uf {

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 (options::ufHo())
      {
        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 (options::ufHo())
      {
        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);
    }
  }
  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(); }

}  // 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 "options/uf_options.h"
20		#include "theory/rewriter.h"
21		#include "theory/substitutions.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace uf {
26
27	849438	RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
28		{
29	849438	if (node.getKind() == kind::EQUAL)
30		{
31	177829	if (node[0] == node[1])
32		{
33		return RewriteResponse(REWRITE_DONE,
34	87	NodeManager::currentNM()->mkConst(true));
35		}
36	177742	else if (node[0].isConst() && node[1].isConst())
37		{
38		// uninterpreted constants are all distinct
39		return RewriteResponse(REWRITE_DONE,
40	28	NodeManager::currentNM()->mkConst(false));
41		}
42	177714	if (node[0] > node[1])
43		{
44		Node newNode =
45	67240	NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
46	33620	return RewriteResponse(REWRITE_DONE, newNode);
47		}
48		}
49	815703	if (node.getKind() == kind::APPLY_UF)
50		{
51	645990	if (node.getOperator().getKind() == kind::LAMBDA)
52		{
53	22434	Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing all args of : " << node
54	11217	<< "\n";
55	22434	TNode lambda = node.getOperator();
56	22434	Node ret;
57		// build capture-avoiding substitution since in HOL shadowing may have
58		// been introduced
59	11217	if (options::ufHo())
60		{
61	1166	std::vector<Node> vars;
62	1166	std::vector<Node> subs;
63	1571	for (const Node& v : lambda[0])
64		{
65	988	vars.push_back(v);
66		}
67	1571	for (const Node& s : node)
68		{
69	988	subs.push_back(s);
70		}
71	583	if (Trace.isOn("uf-ho-beta"))
72		{
73		Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
74		<< " vars into " << subs.size() << " terms :\n";
75		for (unsigned i = 0, size = subs.size(); i < size; ++i)
76		{
77		Trace("uf-ho-beta")
78		<< "uf-ho-beta: .... " << vars[i] << " \|-> " << subs[i] << "\n";
79		}
80		}
81	583	ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
82	583	Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
83		}
84		else
85		{
86	21268	std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
87	21268	std::vector<TNode> subs(node.begin(), node.end());
88	10634	ret = lambda[1].substitute(
89		vars.begin(), vars.end(), subs.begin(), subs.end());
90		}
91	11217	return RewriteResponse(REWRITE_AGAIN_FULL, ret);
92		}
93	634773	else if (!canUseAsApplyUfOperator(node.getOperator()))
94		{
95	113	return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
96		}
97		}
98	169713	else if (node.getKind() == kind::HO_APPLY)
99		{
100	20333	if (node[0].getKind() == kind::LAMBDA)
101		{
102		// resolve one argument of the lambda
103	750	Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing one argument of : "
104	375	<< node[0] << " with " << node[1] << "\n";
105
106		// reconstruct the lambda first to avoid variable shadowing
107	750	Node new_body = node[0][1];
108	375	if (node[0][0].getNumChildren() > 1)
109		{
110	594	std::vector<Node> new_vars(node[0][0].begin() + 1, node[0][0].end());
111	594	std::vector<Node> largs;
112	297	largs.push_back(
113	594	NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, new_vars));
114	297	largs.push_back(new_body);
115	297	new_body = NodeManager::currentNM()->mkNode(kind::LAMBDA, largs);
116	594	Trace("uf-ho-beta")
117	297	<< "uf-ho-beta : ....new lambda : " << new_body << "\n";
118		}
119
120		// build capture-avoiding substitution since in HOL shadowing may have
121		// been introduced
122	375	if (options::ufHo())
123		{
124	750	Node arg = Rewriter::rewrite(node[1]);
125	750	Node var = node[0][0][0];
126	375	new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
127		}
128		else
129		{
130		TNode arg = Rewriter::rewrite(node[1]);
131		TNode var = node[0][0][0];
132		new_body = new_body.substitute(var, arg);
133		}
134	375	Trace("uf-ho-beta") << "uf-ho-beta : ..new body : " << new_body << "\n";
135	375	return RewriteResponse(REWRITE_AGAIN_FULL, new_body);
136		}
137		}
138	803998	return RewriteResponse(REWRITE_DONE, node);
139		}
140
141	446388	RewriteResponse TheoryUfRewriter::preRewrite(TNode node)
142		{
143	446388	if (node.getKind() == kind::EQUAL)
144		{
145	100010	if (node[0] == node[1])
146		{
147		return RewriteResponse(REWRITE_DONE,
148	3341	NodeManager::currentNM()->mkConst(true));
149		}
150	96669	else if (node[0].isConst() && node[1].isConst())
151		{
152		// uninterpreted constants are all distinct
153		return RewriteResponse(REWRITE_DONE,
154	6380	NodeManager::currentNM()->mkConst(false));
155		}
156		}
157	436667	return RewriteResponse(REWRITE_DONE, node);
158		}
159
160	14084	Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n)
161		{
162	14084	Assert(n.getKind() == kind::APPLY_UF);
163	14084	Node curr = n.getOperator();
164	38764	for (unsigned i = 0; i < n.getNumChildren(); i++)
165		{
166	24680	curr = NodeManager::currentNM()->mkNode(kind::HO_APPLY, curr, n[i]);
167		}
168	14084	return curr;
169		}
170		Node TheoryUfRewriter::getApplyUfForHoApply(TNode n)
171		{
172		Assert(n.getType().getNumChildren() == 2);
173		std::vector<TNode> children;
174		TNode curr = decomposeHoApply(n, children, true);
175		// if operator is standard
176		if (canUseAsApplyUfOperator(curr))
177		{
178		return NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
179		}
180		// cannot construct APPLY_UF if operator is partially applied or is not
181		// standard
182		return Node::null();
183		}
184	361	Node TheoryUfRewriter::decomposeHoApply(TNode n,
185		std::vector<TNode>& args,
186		bool opInArgs)
187		{
188	722	TNode curr = n;
189	1545	while (curr.getKind() == kind::HO_APPLY)
190		{
191	592	args.push_back(curr[1]);
192	592	curr = curr[0];
193		}
194	361	if (opInArgs)
195		{
196	121	args.push_back(curr);
197		}
198	361	std::reverse(args.begin(), args.end());
199	722	return curr;
200		}
201	635015	bool TheoryUfRewriter::canUseAsApplyUfOperator(TNode n) { return n.isVar(); }
202
203		} // namespace uf
204		} // namespace theory
205	28194	} // namespace cvc5