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

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Haniel Barbosa, 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
 * Implementation of equality proof checker.
14
 */
15
16
#include "theory/uf/proof_checker.h"
17
18
#include "theory/uf/theory_uf_rewriter.h"
19
20
using namespace cvc5::kind;
21
22
namespace cvc5 {
23
namespace theory {
24
namespace uf {
25
26
3756
void UfProofRuleChecker::registerTo(ProofChecker* pc)
27
{
28
  // add checkers
29
3756
  pc->registerChecker(PfRule::REFL, this);
30
3756
  pc->registerChecker(PfRule::SYMM, this);
31
3756
  pc->registerChecker(PfRule::TRANS, this);
32
3756
  pc->registerChecker(PfRule::CONG, this);
33
3756
  pc->registerChecker(PfRule::TRUE_INTRO, this);
34
3756
  pc->registerChecker(PfRule::TRUE_ELIM, this);
35
3756
  pc->registerChecker(PfRule::FALSE_INTRO, this);
36
3756
  pc->registerChecker(PfRule::FALSE_ELIM, this);
37
3756
  pc->registerChecker(PfRule::HO_CONG, this);
38
3756
  pc->registerChecker(PfRule::HO_APP_ENCODE, this);
39
3756
}
40
41
2190684
Node UfProofRuleChecker::checkInternal(PfRule id,
42
                                       const std::vector<Node>& children,
43
                                       const std::vector<Node>& args)
44
{
45
  // compute what was proven
46
2190684
  if (id == PfRule::REFL)
47
  {
48
744788
    Assert(children.empty());
49
744788
    Assert(args.size() == 1);
50
744788
    return args[0].eqNode(args[0]);
51
  }
52
1445896
  else if (id == PfRule::SYMM)
53
  {
54
563563
    Assert(children.size() == 1);
55
563563
    Assert(args.empty());
56
563563
    bool polarity = children[0].getKind() != NOT;
57
1127126
    Node eqp = polarity ? children[0] : children[0][0];
58
563563
    if (eqp.getKind() != EQUAL)
59
    {
60
      // not a (dis)equality
61
      return Node::null();
62
    }
63
1127126
    Node conc = eqp[1].eqNode(eqp[0]);
64
563563
    return polarity ? conc : conc.notNode();
65
  }
66
882333
  else if (id == PfRule::TRANS)
67
  {
68
273211
    Assert(children.size() > 0);
69
273211
    Assert(args.empty());
70
546422
    Node first;
71
546422
    Node curr;
72
1000522
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
73
    {
74
1454622
      Node eqp = children[i];
75
727311
      if (eqp.getKind() != EQUAL)
76
      {
77
        return Node::null();
78
      }
79
727311
      if (first.isNull())
80
      {
81
273211
        first = eqp[0];
82
      }
83
454100
      else if (eqp[0] != curr)
84
      {
85
        return Node::null();
86
      }
87
727311
      curr = eqp[1];
88
    }
89
273211
    return first.eqNode(curr);
90
  }
91
609122
  else if (id == PfRule::CONG)
92
  {
93
561263
    Assert(children.size() > 0);
94
561263
    Assert(args.size() >= 1 && args.size() <= 2);
95
    // We do congruence over builtin kinds using operatorToKind
96
1122526
    std::vector<Node> lchildren;
97
1122526
    std::vector<Node> rchildren;
98
    // get the kind encoded as args[0]
99
    Kind k;
100
561263
    if (!getKind(args[0], k))
101
    {
102
      return Node::null();
103
    }
104
561263
    if (k == kind::UNDEFINED_KIND)
105
    {
106
      return Node::null();
107
    }
108
1122526
    Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k
109
561263
                        << ", metakind=" << kind::metaKindOf(k) << std::endl;
110
561263
    if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
111
    {
112
180884
      if (args.size() <= 1)
113
      {
114
        return Node::null();
115
      }
116
      // parameterized kinds require the operator
117
180884
      lchildren.push_back(args[1]);
118
180884
      rchildren.push_back(args[1]);
119
    }
120
380379
    else if (args.size() > 1)
121
    {
122
      return Node::null();
123
    }
124
2082078
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
125
    {
126
3041630
      Node eqp = children[i];
127
1520815
      if (eqp.getKind() != EQUAL)
128
      {
129
        return Node::null();
130
      }
131
1520815
      lchildren.push_back(eqp[0]);
132
1520815
      rchildren.push_back(eqp[1]);
133
    }
134
561263
    NodeManager* nm = NodeManager::currentNM();
135
1122526
    Node l = nm->mkNode(k, lchildren);
136
1122526
    Node r = nm->mkNode(k, rchildren);
137
561263
    return l.eqNode(r);
138
  }
139
47859
  else if (id == PfRule::TRUE_INTRO)
140
  {
141
9613
    Assert(children.size() == 1);
142
9613
    Assert(args.empty());
143
19226
    Node trueNode = NodeManager::currentNM()->mkConst(true);
144
9613
    return children[0].eqNode(trueNode);
145
  }
146
38246
  else if (id == PfRule::TRUE_ELIM)
147
  {
148
22326
    Assert(children.size() == 1);
149
22326
    Assert(args.empty());
150
66978
    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
151
66978
        || !children[0][1].getConst<bool>())
152
    {
153
      return Node::null();
154
    }
155
22326
    return children[0][0];
156
  }
157
15920
  else if (id == PfRule::FALSE_INTRO)
158
  {
159
11196
    Assert(children.size() == 1);
160
11196
    Assert(args.empty());
161
11196
    if (children[0].getKind() != kind::NOT)
162
    {
163
      return Node::null();
164
    }
165
22392
    Node falseNode = NodeManager::currentNM()->mkConst(false);
166
11196
    return children[0][0].eqNode(falseNode);
167
  }
168
4724
  else if (id == PfRule::FALSE_ELIM)
169
  {
170
4445
    Assert(children.size() == 1);
171
4445
    Assert(args.empty());
172
13335
    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
173
13335
        || children[0][1].getConst<bool>())
174
    {
175
      return Node::null();
176
    }
177
4445
    return children[0][0].notNode();
178
  }
179
279
  if (id == PfRule::HO_CONG)
180
  {
181
243
    Assert(children.size() > 0);
182
486
    std::vector<Node> lchildren;
183
486
    std::vector<Node> rchildren;
184
912
    for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
185
    {
186
1338
      Node eqp = children[i];
187
669
      if (eqp.getKind() != EQUAL)
188
      {
189
        return Node::null();
190
      }
191
669
      lchildren.push_back(eqp[0]);
192
669
      rchildren.push_back(eqp[1]);
193
    }
194
243
    NodeManager* nm = NodeManager::currentNM();
195
486
    Node l = nm->mkNode(kind::APPLY_UF, lchildren);
196
486
    Node r = nm->mkNode(kind::APPLY_UF, rchildren);
197
243
    return l.eqNode(r);
198
  }
199
36
  else if (id == PfRule::HO_APP_ENCODE)
200
  {
201
36
    Assert(args.size() == 1);
202
72
    Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
203
36
    return args[0].eqNode(ret);
204
  }
205
  // no rule
206
  return Node::null();
207
}
208
209
}  // namespace uf
210
}  // namespace theory
211
29280
}  // namespace cvc5