GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/proof_circuit_propagator.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_circuit_propagator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer
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 Proofs for the non-clausal circuit propagator.
13
 **
14
 ** Proofs for the non-clausal circuit propagator.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
20
#define CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
21
22
#include <memory>
23
24
#include "expr/node.h"
25
#include "expr/proof_rule.h"
26
27
namespace CVC4 {
28
29
class ProofNode;
30
class ProofNodeManager;
31
32
namespace theory {
33
namespace booleans {
34
35
/**
36
 * Base class for for CircuitPropagatorProofs.
37
 * This class collects common functionality for proofs of backward and forward
38
 * propagation.
39
 */
40
class ProofCircuitPropagator
41
{
42
 public:
43
  ProofCircuitPropagator(ProofNodeManager* pnm);
44
45
  /** Assuming the given node */
46
  std::shared_ptr<ProofNode> assume(Node n);
47
  /** Apply CONTRA rule. Takes care of switching a and b if necessary */
48
  std::shared_ptr<ProofNode> conflict(const std::shared_ptr<ProofNode>& a,
49
                                      const std::shared_ptr<ProofNode>& b);
50
51
  /** (and true ... holdout true ...)  -->  holdout */
52
  std::shared_ptr<ProofNode> andFalse(Node parent, TNode::iterator holdout);
53
54
  /** (or false ... holdout false ...)  ->  holdout */
55
  std::shared_ptr<ProofNode> orTrue(Node parent, TNode::iterator holdout);
56
57
  /** (not x) is true  -->  x is false (and vice versa) */
58
  std::shared_ptr<ProofNode> Not(bool negate, Node parent);
59
60
  /** (=> X false)  -->  (not X) */
61
  std::shared_ptr<ProofNode> impliesXFromY(Node parent);
62
  /** (=> true Y)  -->  Y */
63
  std::shared_ptr<ProofNode> impliesYFromX(Node parent);
64
65
  /** Derive X from (= X Y) */
66
  std::shared_ptr<ProofNode> eqXFromY(bool y, Node parent);
67
  /** Derive Y from (= X Y) */
68
  std::shared_ptr<ProofNode> eqYFromX(bool x, Node parent);
69
  /** Derive X from (not (= X Y)) */
70
  std::shared_ptr<ProofNode> neqXFromY(bool y, Node parent);
71
  /** Derive Y from (not (= X Y)) */
72
  std::shared_ptr<ProofNode> neqYFromX(bool x, Node parent);
73
74
  /**
75
   * Uses (xor X Y) to derive the value of X.
76
   * (xor X false)  -->  X
77
   * (xor X true)  -->  (not X)
78
   * (not (xor X false))  -->  (not X)
79
   * (not (xor X true))  -->  X
80
   */
81
  std::shared_ptr<ProofNode> xorXFromY(bool negated, bool y, Node parent);
82
  /**
83
   * Uses (xor X Y) to derive the value of Y.
84
   * (xor false Y)  -->  Y
85
   * (xor true Y)  -->  (not Y)
86
   * (not (xor false Y))  -->  (not Y)
87
   * (not (xor true Y))  -->  Y
88
   */
89
  std::shared_ptr<ProofNode> xorYFromX(bool negated, bool x, Node parent);
90
91
 protected:
92
  /** Shorthand to check whether proof generation is disabled */
93
  bool disabled() const;
94
95
  /** Construct proof using the given rule, children and args */
96
  std::shared_ptr<ProofNode> mkProof(
97
      PfRule rule,
98
      const std::vector<std::shared_ptr<ProofNode>>& children,
99
      const std::vector<Node>& args = {});
100
  /**
101
   * Apply CHAIN_RESOLUTION rule.
102
   * Constructs the args from the given literals and polarities (called ids in
103
   * the proof rule). Automatically adds the clauses to resolve with as
104
   * assumptions, depending on their polarity.
105
   */
106
  std::shared_ptr<ProofNode> mkCResolution(
107
      const std::shared_ptr<ProofNode>& clause,
108
      const std::vector<Node>& lits,
109
      const std::vector<bool>& polarity);
110
  /** Shorthand for mkCResolution(clause, lits, {polarity, ...}) */
111
  std::shared_ptr<ProofNode> mkCResolution(
112
      const std::shared_ptr<ProofNode>& clause,
113
      const std::vector<Node>& lits,
114
      bool polarity);
115
  /** Apply RESOLUTION rule */
116
  std::shared_ptr<ProofNode> mkResolution(
117
      const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity);
118
  /** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */
119
  std::shared_ptr<ProofNode> mkNot(const std::shared_ptr<ProofNode>& n);
120
121
  /** The proof node manager */
122
  ProofNodeManager* d_pnm;
123
};
124
125
/**
126
 * Proof generator for backward propagation
127
 * A backward propagation is triggered by the assignment of the parent node.
128
 */
129
553895
class ProofCircuitPropagatorBackward : public ProofCircuitPropagator
130
{
131
 public:
132
  ProofCircuitPropagatorBackward(ProofNodeManager* pnm,
133
                                 TNode parent,
134
                                 bool parentAssignment);
135
136
  /** and true  -->  child is true */
137
  std::shared_ptr<ProofNode> andTrue(TNode::iterator i);
138
139
  /** or false  -->  child is false */
140
  std::shared_ptr<ProofNode> orFalse(TNode::iterator i);
141
142
  /**
143
   * Propagate on ite with evaluate condition
144
   * (ite true t e)  -->  t
145
   * (not (ite true t e))  -->  (not t)
146
   * (ite false t e)  -->  e
147
   * (not (ite false t e))  -->  (not e)
148
   */
149
  std::shared_ptr<ProofNode> iteC(bool c);
150
  /**
151
   * For (ite c t e), we can derive the value for c
152
   * c = 1: c = true
153
   * c = 0: c = false
154
   */
155
  std::shared_ptr<ProofNode> iteIsCase(unsigned c);
156
157
  /** (not (=> X Y))  -->  X */
158
  std::shared_ptr<ProofNode> impliesNegX();
159
  /** (not (=> X Y))  -->  (not Y) */
160
  std::shared_ptr<ProofNode> impliesNegY();
161
162
 private:
163
  /** The parent node */
164
  TNode d_parent;
165
  /** The assignment of d_parent */
166
  bool d_parentAssignment;
167
};
168
169
/**
170
 * Proof generator for forward propagation
171
 * A forward propagation is triggered by the assignment of a child node.
172
 */
173
525276
class ProofCircuitPropagatorForward : public ProofCircuitPropagator
174
{
175
 public:
176
  ProofCircuitPropagatorForward(ProofNodeManager* pnm,
177
                                Node child,
178
                                bool childAssignment,
179
                                Node parent);
180
181
  /** All children are true  -->  and is true */
182
  std::shared_ptr<ProofNode> andAllTrue();
183
  /** One child is false  -->  and is false */
184
  std::shared_ptr<ProofNode> andOneFalse();
185
186
  /** One child is true  -->  or is true */
187
  std::shared_ptr<ProofNode> orOneTrue();
188
  /** or false  -->  all children are false */
189
  std::shared_ptr<ProofNode> orFalse();
190
191
  /** Evaluate (ite true X _) from X */
192
  std::shared_ptr<ProofNode> iteEvalThen(bool x);
193
  /** Evaluate (ite false _ Y) from Y */
194
  std::shared_ptr<ProofNode> iteEvalElse(bool y);
195
196
  /** Evaluate (= X Y) from X,Y */
197
  std::shared_ptr<ProofNode> eqEval(bool x, bool y);
198
199
  /** Evaluate (=> X Y) from X,Y */
200
  std::shared_ptr<ProofNode> impliesEval(bool premise, bool conclusion);
201
  /** Evaluate (xor X Y) from X,Y */
202
  std::shared_ptr<ProofNode> xorEval(bool x, bool y);
203
204
 private:
205
  /** The current child that triggered the propagations */
206
  Node d_child;
207
  /** The assignment of d_child */
208
  bool d_childAssignment;
209
  /** The parent node used for propagation */
210
  Node d_parent;
211
};
212
213
}  // namespace booleans
214
}  // namespace theory
215
}  // namespace CVC4
216
217
#endif