GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/theory_rewrite_eq.cpp Lines: 53 53 100.0 %
Date: 2021-05-24 Branches: 109 236 46.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
9459
TheoryRewriteEq::TheoryRewriteEq(PreprocessingPassContext* preprocContext)
29
9459
    : PreprocessingPass(preprocContext, "theory-rewrite-eq"){};
30
31
12881
PreprocessingPassResult TheoryRewriteEq::applyInternal(
32
    AssertionPipeline* assertions)
33
{
34
  // apply ppRewrite to all equalities in assertions
35
117601
  for (std::size_t i = 0, size = assertions->size(); i < size; ++i)
36
  {
37
209440
    Node assertion = (*assertions)[i];
38
209440
    TrustNode trn = rewriteAssertion(assertion);
39
104720
    if (!trn.isNull())
40
    {
41
      // replace based on the trust node
42
2289
      assertions->replaceTrusted(i, trn);
43
    }
44
  }
45
12881
  return PreprocessingPassResult::NO_CONFLICT;
46
}
47
48
104720
theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
49
{
50
104720
  NodeManager* nm = NodeManager::currentNM();
51
104720
  TheoryEngine* te = d_preprocContext->getTheoryEngine();
52
209440
  std::unordered_map<TNode, Node> visited;
53
104720
  std::unordered_map<TNode, Node>::iterator it;
54
209440
  std::vector<TNode> visit;
55
209440
  TNode cur;
56
104720
  visit.push_back(n);
57
5651058
  do
58
  {
59
5755778
    cur = visit.back();
60
5755778
    visit.pop_back();
61
5755778
    it = visited.find(cur);
62
63
5755778
    if (it == visited.end())
64
    {
65
2042895
      if (cur.getNumChildren()==0)
66
      {
67
454430
        visited[cur] = cur;
68
      }
69
      else
70
      {
71
1588465
        visited[cur] = Node::null();
72
1588465
        visit.push_back(cur);
73
1588465
        visit.insert(visit.end(), cur.begin(), cur.end());
74
      }
75
    }
76
3712883
    else if (it->second.isNull())
77
    {
78
3176930
      Node ret = cur;
79
1588465
      bool childChanged = false;
80
3176930
      std::vector<Node> children;
81
1588465
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
82
      {
83
196400
        children.push_back(cur.getOperator());
84
      }
85
5651058
      for (const Node& cn : cur)
86
      {
87
4062593
        it = visited.find(cn);
88
4062593
        Assert(it != visited.end());
89
4062593
        Assert(!it->second.isNull());
90
4062593
        childChanged = childChanged || cn != it->second;
91
4062593
        children.push_back(it->second);
92
      }
93
1588465
      if (childChanged)
94
      {
95
40901
        ret = nm->mkNode(cur.getKind(), children);
96
      }
97
1588465
      if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
98
      {
99
        // For example, (= x y) ---> (and (>= x y) (<= x y))
100
407050
        theory::TrustNode trn = te->ppRewriteEquality(ret);
101
        // can make proof producing by using proof generator from trn
102
203525
        ret = trn.isNull() ? Node(ret) : trn.getNode();
103
      }
104
1588465
      visited[cur] = ret;
105
    }
106
5755778
  } while (!visit.empty());
107
104720
  Assert(visited.find(n) != visited.end());
108
104720
  Assert(!visited.find(n)->second.isNull());
109
209440
  Node ret = visited[n];
110
104720
  if (ret == n)
111
  {
112
102431
    return TrustNode::null();
113
  }
114
  // can make proof producing by providing a term conversion generator here
115
2289
  return TrustNode::mkTrustRewrite(n, ret, nullptr);
116
}
117
118
}  // namespace passes
119
}  // namespace preprocessing
120
28191
}  // namespace cvc5