GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/theory_rewrite_eq.cpp Lines: 53 53 100.0 %
Date: 2021-03-22 Branches: 109 236 46.2 %

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