Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/theory_rewrite_eq.cpp	Lines:	53	53	100.0 %
Date:	2021-05-21	Branches:	109	236	46.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * The TheoryRewriteEq preprocessing pass.
 */

#include "preprocessing/passes/theory_rewrite_eq.h"

#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/theory_engine.h"

using namespace cvc5::theory;

namespace cvc5 {
namespace preprocessing {
namespace passes {

TheoryRewriteEq::TheoryRewriteEq(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "theory-rewrite-eq"){};

PreprocessingPassResult TheoryRewriteEq::applyInternal(
    AssertionPipeline* assertions)
{
  // apply ppRewrite to all equalities in assertions
  for (std::size_t i = 0, size = assertions->size(); i < size; ++i)
  {
    Node assertion = (*assertions)[i];
    TrustNode trn = rewriteAssertion(assertion);
    if (!trn.isNull())
    {
      // replace based on the trust node
      assertions->replaceTrusted(i, trn);
    }
  }
  return PreprocessingPassResult::NO_CONFLICT;
}

theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
{
  NodeManager* nm = NodeManager::currentNM();
  TheoryEngine* te = d_preprocContext->getTheoryEngine();
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      if (cur.getNumChildren()==0)
      {
        visited[cur] = cur;
      }
      else
      {
        visited[cur] = Node::null();
        visit.push_back(cur);
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        children.push_back(cur.getOperator());
      }
      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);
      }
      if (childChanged)
      {
        ret = nm->mkNode(cur.getKind(), children);
      }
      if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
      {
        // For example, (= x y) ---> (and (>= x y) (<= x y))
        theory::TrustNode trn = te->ppRewriteEquality(ret);
        // can make proof producing by using proof generator from trn
        ret = trn.isNull() ? Node(ret) : trn.getNode();
      }
      visited[cur] = ret;
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  Node ret = visited[n];
  if (ret == n)
  {
    return TrustNode::null();
  }
  // can make proof producing by providing a term conversion generator here
  return TrustNode::mkTrustRewrite(n, ret, nullptr);
}

}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
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		* The TheoryRewriteEq preprocessing pass.
14		*/
15
16		#include "preprocessing/passes/theory_rewrite_eq.h"
17
18		#include "preprocessing/assertion_pipeline.h"
19		#include "preprocessing/preprocessing_pass_context.h"
20		#include "theory/theory_engine.h"
21
22		using namespace cvc5::theory;
23
24		namespace cvc5 {
25		namespace preprocessing {
26		namespace passes {
27
28	8954	TheoryRewriteEq::TheoryRewriteEq(PreprocessingPassContext* preprocContext)
29	8954	: PreprocessingPass(preprocContext, "theory-rewrite-eq"){};
30
31	11638	PreprocessingPassResult TheoryRewriteEq::applyInternal(
32		AssertionPipeline* assertions)
33		{
34		// apply ppRewrite to all equalities in assertions
35	111040	for (std::size_t i = 0, size = assertions->size(); i < size; ++i)
36		{
37	198804	Node assertion = (*assertions)[i];
38	198804	TrustNode trn = rewriteAssertion(assertion);
39	99402	if (!trn.isNull())
40		{
41		// replace based on the trust node
42	1960	assertions->replaceTrusted(i, trn);
43		}
44		}
45	11638	return PreprocessingPassResult::NO_CONFLICT;
46		}
47
48	99402	theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
49		{
50	99402	NodeManager* nm = NodeManager::currentNM();
51	99402	TheoryEngine* te = d_preprocContext->getTheoryEngine();
52	198804	std::unordered_map<TNode, Node> visited;
53	99402	std::unordered_map<TNode, Node>::iterator it;
54	198804	std::vector<TNode> visit;
55	198804	TNode cur;
56	99402	visit.push_back(n);
57	5447325	do
58		{
59	5546727	cur = visit.back();
60	5546727	visit.pop_back();
61	5546727	it = visited.find(cur);
62
63	5546727	if (it == visited.end())
64		{
65	1957186	if (cur.getNumChildren()==0)
66		{
67	433311	visited[cur] = cur;
68		}
69		else
70		{
71	1523875	visited[cur] = Node::null();
72	1523875	visit.push_back(cur);
73	1523875	visit.insert(visit.end(), cur.begin(), cur.end());
74		}
75		}
76	3589541	else if (it->second.isNull())
77		{
78	3047750	Node ret = cur;
79	1523875	bool childChanged = false;
80	3047750	std::vector<Node> children;
81	1523875	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
82		{
83	194664	children.push_back(cur.getOperator());
84		}
85	5447325	for (const Node& cn : cur)
86		{
87	3923450	it = visited.find(cn);
88	3923450	Assert(it != visited.end());
89	3923450	Assert(!it->second.isNull());
90	3923450	childChanged = childChanged \|\| cn != it->second;
91	3923450	children.push_back(it->second);
92		}
93	1523875	if (childChanged)
94		{
95	40527	ret = nm->mkNode(cur.getKind(), children);
96		}
97	1523875	if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
98		{
99		// For example, (= x y) ---> (and (>= x y) (<= x y))
100	402524	theory::TrustNode trn = te->ppRewriteEquality(ret);
101		// can make proof producing by using proof generator from trn
102	201262	ret = trn.isNull() ? Node(ret) : trn.getNode();
103		}
104	1523875	visited[cur] = ret;
105		}
106	5546727	} while (!visit.empty());
107	99402	Assert(visited.find(n) != visited.end());
108	99402	Assert(!visited.find(n)->second.isNull());
109	198804	Node ret = visited[n];
110	99402	if (ret == n)
111		{
112	97442	return TrustNode::null();
113		}
114		// can make proof producing by providing a term conversion generator here
115	1960	return TrustNode::mkTrustRewrite(n, ret, nullptr);
116		}
117
118		} // namespace passes
119		} // namespace preprocessing
120	27735	} // namespace cvc5