GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/proof_checker.cpp Lines: 102 115 88.7 %
Date: 2021-03-23 Branches: 175 564 31.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, 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 Implementation of equality proof checker
13
 **/
14
15
#include "theory/uf/proof_checker.h"
16
17
#include "theory/uf/theory_uf_rewriter.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace uf {
24
25
962
void UfProofRuleChecker::registerTo(ProofChecker* pc)
26
{
27
  // add checkers
28
962
  pc->registerChecker(PfRule::REFL, this);
29
962
  pc->registerChecker(PfRule::SYMM, this);
30
962
  pc->registerChecker(PfRule::TRANS, this);
31
962
  pc->registerChecker(PfRule::CONG, this);
32
962
  pc->registerChecker(PfRule::TRUE_INTRO, this);
33
962
  pc->registerChecker(PfRule::TRUE_ELIM, this);
34
962
  pc->registerChecker(PfRule::FALSE_INTRO, this);
35
962
  pc->registerChecker(PfRule::FALSE_ELIM, this);
36
962
  pc->registerChecker(PfRule::HO_CONG, this);
37
962
  pc->registerChecker(PfRule::HO_APP_ENCODE, this);
38
962
}
39
40
1992038
Node UfProofRuleChecker::checkInternal(PfRule id,
41
                                       const std::vector<Node>& children,
42
                                       const std::vector<Node>& args)
43
{
44
  // compute what was proven
45
1992038
  if (id == PfRule::REFL)
46
  {
47
451868
    Assert(children.empty());
48
451868
    Assert(args.size() == 1);
49
451868
    return args[0].eqNode(args[0]);
50
  }
51
1540170
  else if (id == PfRule::SYMM)
52
  {
53
777232
    Assert(children.size() == 1);
54
777232
    Assert(args.empty());
55
777232
    bool polarity = children[0].getKind() != NOT;
56
1554464
    Node eqp = polarity ? children[0] : children[0][0];
57
777232
    if (eqp.getKind() != EQUAL)
58
    {
59
      // not a (dis)equality
60
      return Node::null();
61
    }
62
1554464
    Node conc = eqp[1].eqNode(eqp[0]);
63
777232
    return polarity ? conc : conc.notNode();
64
  }
65
762938
  else if (id == PfRule::TRANS)
66
  {
67
265784
    Assert(children.size() > 0);
68
265784
    Assert(args.empty());
69
531568
    Node first;
70
531568
    Node curr;
71
1016818
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
72
    {
73
1502068
      Node eqp = children[i];
74
751034
      if (eqp.getKind() != EQUAL)
75
      {
76
        return Node::null();
77
      }
78
751034
      if (first.isNull())
79
      {
80
265784
        first = eqp[0];
81
      }
82
485250
      else if (eqp[0] != curr)
83
      {
84
        return Node::null();
85
      }
86
751034
      curr = eqp[1];
87
    }
88
265784
    return first.eqNode(curr);
89
  }
90
497154
  else if (id == PfRule::CONG)
91
  {
92
461854
    Assert(children.size() > 0);
93
461854
    Assert(args.size() >= 1 && args.size() <= 2);
94
    // We do congruence over builtin kinds using operatorToKind
95
923708
    std::vector<Node> lchildren;
96
923708
    std::vector<Node> rchildren;
97
    // get the kind encoded as args[0]
98
    Kind k;
99
461854
    if (!getKind(args[0], k))
100
    {
101
      return Node::null();
102
    }
103
461854
    if (k == kind::UNDEFINED_KIND)
104
    {
105
      return Node::null();
106
    }
107
923708
    Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k
108
461854
                        << ", metakind=" << kind::metaKindOf(k) << std::endl;
109
461854
    if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
110
    {
111
182630
      if (args.size() <= 1)
112
      {
113
        return Node::null();
114
      }
115
      // parameterized kinds require the operator
116
182630
      lchildren.push_back(args[1]);
117
182630
      rchildren.push_back(args[1]);
118
    }
119
279224
    else if (args.size() > 1)
120
    {
121
      return Node::null();
122
    }
123
1599170
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
124
    {
125
2274632
      Node eqp = children[i];
126
1137316
      if (eqp.getKind() != EQUAL)
127
      {
128
        return Node::null();
129
      }
130
1137316
      lchildren.push_back(eqp[0]);
131
1137316
      rchildren.push_back(eqp[1]);
132
    }
133
461854
    NodeManager* nm = NodeManager::currentNM();
134
923708
    Node l = nm->mkNode(k, lchildren);
135
923708
    Node r = nm->mkNode(k, rchildren);
136
461854
    return l.eqNode(r);
137
  }
138
35300
  else if (id == PfRule::TRUE_INTRO)
139
  {
140
9155
    Assert(children.size() == 1);
141
9155
    Assert(args.empty());
142
18310
    Node trueNode = NodeManager::currentNM()->mkConst(true);
143
9155
    return children[0].eqNode(trueNode);
144
  }
145
26145
  else if (id == PfRule::TRUE_ELIM)
146
  {
147
7275
    Assert(children.size() == 1);
148
7275
    Assert(args.empty());
149
21825
    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
150
21825
        || !children[0][1].getConst<bool>())
151
    {
152
      return Node::null();
153
    }
154
7275
    return children[0][0];
155
  }
156
18870
  else if (id == PfRule::FALSE_INTRO)
157
  {
158
14108
    Assert(children.size() == 1);
159
14108
    Assert(args.empty());
160
14108
    if (children[0].getKind() != kind::NOT)
161
    {
162
      return Node::null();
163
    }
164
28216
    Node falseNode = NodeManager::currentNM()->mkConst(false);
165
14108
    return children[0][0].eqNode(falseNode);
166
  }
167
4762
  else if (id == PfRule::FALSE_ELIM)
168
  {
169
4491
    Assert(children.size() == 1);
170
4491
    Assert(args.empty());
171
13473
    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
172
13473
        || children[0][1].getConst<bool>())
173
    {
174
      return Node::null();
175
    }
176
4491
    return children[0][0].notNode();
177
  }
178
271
  if (id == PfRule::HO_CONG)
179
  {
180
235
    Assert(children.size() > 0);
181
470
    std::vector<Node> lchildren;
182
470
    std::vector<Node> rchildren;
183
863
    for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
184
    {
185
1256
      Node eqp = children[i];
186
628
      if (eqp.getKind() != EQUAL)
187
      {
188
        return Node::null();
189
      }
190
628
      lchildren.push_back(eqp[0]);
191
628
      rchildren.push_back(eqp[1]);
192
    }
193
235
    NodeManager* nm = NodeManager::currentNM();
194
470
    Node l = nm->mkNode(kind::APPLY_UF, lchildren);
195
470
    Node r = nm->mkNode(kind::APPLY_UF, rchildren);
196
235
    return l.eqNode(r);
197
  }
198
36
  else if (id == PfRule::HO_APP_ENCODE)
199
  {
200
36
    Assert(args.size() == 1);
201
72
    Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
202
36
    return args[0].eqNode(ret);
203
  }
204
  // no rule
205
  return Node::null();
206
}
207
208
}  // namespace uf
209
}  // namespace theory
210
26685
}  // namespace CVC4