GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_proof_step_buffer.cpp Lines: 83 100 83.0 %
Date: 2021-03-22 Branches: 142 342 41.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_proof_step_buffer.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 theory proof step buffer utility
13
 **/
14
15
#include "theory/theory_proof_step_buffer.h"
16
17
#include "expr/proof.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
24
6419
TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
25
6419
    : ProofStepBuffer(pc)
26
{
27
6419
}
28
29
24543
bool TheoryProofStepBuffer::applyEqIntro(Node src,
30
                                         Node tgt,
31
                                         const std::vector<Node>& exp,
32
                                         MethodId ids,
33
                                         MethodId idr)
34
{
35
49086
  std::vector<Node> args;
36
24543
  args.push_back(src);
37
24543
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
38
49086
  Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
39
24543
  if (res.isNull())
40
  {
41
    // failed to apply
42
    return false;
43
  }
44
  // should have concluded the expected equality
45
49086
  Node expected = src.eqNode(tgt);
46
24543
  if (res != expected)
47
  {
48
    // did not provide the correct target
49
1
    popStep();
50
1
    return false;
51
  }
52
  // successfully proved src == tgt.
53
24542
  return true;
54
}
55
56
1711
bool TheoryProofStepBuffer::applyPredTransform(Node src,
57
                                               Node tgt,
58
                                               const std::vector<Node>& exp,
59
                                               MethodId ids,
60
                                               MethodId idr)
61
{
62
  // symmetric equalities
63
1711
  if (CDProof::isSame(src, tgt))
64
  {
65
557
    return true;
66
  }
67
2308
  std::vector<Node> children;
68
1154
  children.push_back(src);
69
2308
  std::vector<Node> args;
70
  // try to prove that tgt rewrites to src
71
1154
  children.insert(children.end(), exp.begin(), exp.end());
72
1154
  args.push_back(tgt);
73
1154
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
74
2308
  Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
75
1154
  if (res.isNull())
76
  {
77
    // failed to apply
78
108
    return false;
79
  }
80
  // should definitely have concluded tgt
81
1046
  Assert(res == tgt);
82
1046
  return true;
83
}
84
85
bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
86
                                           const std::vector<Node>& exp,
87
                                           MethodId ids,
88
                                           MethodId idr)
89
{
90
  std::vector<Node> args;
91
  args.push_back(tgt);
92
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
93
  Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
94
  if (res.isNull())
95
  {
96
    return false;
97
  }
98
  Assert(res == tgt);
99
  return true;
100
}
101
102
82
Node TheoryProofStepBuffer::applyPredElim(Node src,
103
                                          const std::vector<Node>& exp,
104
                                          MethodId ids,
105
                                          MethodId idr)
106
{
107
164
  std::vector<Node> children;
108
82
  children.push_back(src);
109
82
  children.insert(children.end(), exp.begin(), exp.end());
110
164
  std::vector<Node> args;
111
82
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
112
82
  Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
113
82
  if (CDProof::isSame(src, srcRew))
114
  {
115
20
    popStep();
116
  }
117
164
  return srcRew;
118
}
119
120
221516
Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
121
{
122
221516
  if (n.getKind() != kind::OR)
123
  {
124
    return elimDoubleNegLit(n);
125
  }
126
221516
  NodeManager* nm = NodeManager::currentNM();
127
443032
  std::vector<Node> children{n.begin(), n.end()};
128
443032
  std::vector<Node> childrenEqs;
129
  // eliminate double neg for each lit. Do it first because it may expose
130
  // duplicates
131
221516
  bool hasDoubleNeg = false;
132
1047401
  for (unsigned i = 0; i < children.size(); ++i)
133
  {
134
1651770
    if (children[i].getKind() == kind::NOT
135
1651770
        && children[i][0].getKind() == kind::NOT)
136
    {
137
55012
      hasDoubleNeg = true;
138
55012
      childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
139
220048
      addStep(PfRule::MACRO_SR_PRED_INTRO,
140
              {},
141
55012
              {childrenEqs.back()},
142
110024
              childrenEqs.back());
143
      // update child
144
55012
      children[i] = children[i][0][0];
145
    }
146
    else
147
    {
148
770873
      childrenEqs.push_back(children[i].eqNode(children[i]));
149
770873
      addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
150
    }
151
  }
152
221516
  if (hasDoubleNeg)
153
  {
154
77566
    Node oldn = n;
155
38783
    n = nm->mkNode(kind::OR, children);
156
    // Create a congruence step to justify replacement of each doubly negated
157
    // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
158
    // from the old clause to the new one, which, under the standard rewriter,
159
    // may not hold. An example is
160
    //
161
    //   ---------------------------------------------------------------------
162
    //   (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
163
    //
164
    // which fails due to factoring not happening after flattening.
165
    //
166
    // Using congruence only the
167
    //
168
    //  ------------------ MACRO_SR_PRED_INTRO
169
    //  (not (not t)) = t
170
    //
171
    // steps are added, which, since double negation is eliminated in a
172
    // pre-rewrite in the Boolean rewriter, will always hold under the
173
    // standard rewriter.
174
77566
    Node congEq = oldn.eqNode(n);
175
77566
    addStep(PfRule::CONG,
176
            childrenEqs,
177
            {ProofRuleChecker::mkKindNode(kind::OR)},
178
38783
            congEq);
179
    // add an equality resolution step to derive normalize clause
180
38783
    addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
181
  }
182
221516
  children.clear();
183
  // remove duplicates while keeping the order of children
184
443032
  std::unordered_set<TNode, TNodeHashFunction> clauseSet;
185
221516
  unsigned size = n.getNumChildren();
186
1047401
  for (unsigned i = 0; i < size; ++i)
187
  {
188
825885
    if (clauseSet.count(n[i]))
189
    {
190
537
      continue;
191
    }
192
825348
    children.push_back(n[i]);
193
825348
    clauseSet.insert(n[i]);
194
  }
195
  // if factoring changed
196
221516
  if (children.size() < size)
197
  {
198
416
    Node factored = children.empty()
199
                        ? nm->mkConst<bool>(false)
200
416
                        : children.size() == 1 ? children[0]
201
1248
                                               : nm->mkNode(kind::OR, children);
202
    // don't overwrite what already has a proof step to avoid cycles
203
416
    addStep(PfRule::FACTORING, {n}, {}, factored);
204
416
    n = factored;
205
  }
206
  // nothing to order
207
221516
  if (children.size() < 2)
208
  {
209
    return n;
210
  }
211
  // order
212
221516
  std::sort(children.begin(), children.end());
213
443032
  Node ordered = nm->mkNode(kind::OR, children);
214
  // if ordering changed
215
221516
  if (ordered != n)
216
  {
217
    // don't overwrite what already has a proof step to avoid cycles
218
159398
    addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
219
  }
220
221516
  return ordered;
221
}
222
223
Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
224
{
225
  // eliminate double neg
226
  if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
227
  {
228
    addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
229
    return n[0][0];
230
  }
231
  return n;
232
}
233
234
}  // namespace theory
235
26676
}  // namespace CVC4