GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/proof_cnf_stream.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_cnf_stream.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Dejan Jovanovic, Liana Hadarean
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 The proof-producing CNF stream
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__PROP__PROOF_CNF_STREAM_H
18
#define CVC4__PROP__PROOF_CNF_STREAM_H
19
20
#include "context/cdhashmap.h"
21
#include "expr/lazy_proof.h"
22
#include "expr/node.h"
23
#include "expr/proof_node.h"
24
#include "expr/proof_node_manager.h"
25
#include "prop/cnf_stream.h"
26
#include "prop/sat_proof_manager.h"
27
#include "theory/eager_proof_generator.h"
28
#include "theory/theory_proof_step_buffer.h"
29
30
namespace CVC4 {
31
namespace prop {
32
33
class SatProofManager;
34
35
/**
36
 * A proof generator for CNF transformation. It is a layer on top of CNF stream,
37
 * tracking the justifications for clauses added into the underlying SAT solver
38
 * in a user-context dependent manner in a lazy context-dependent (LazyCDProof)
39
 * object. The proof is lazy because formulas asserted to this class may also
40
 * take proof generators (which is the case, for example, for theory lemmas), so
41
 * that getting the proof of a clausified formula will also extend to its
42
 * registered proof generator.
43
 */
44
1932
class ProofCnfStream : public ProofGenerator
45
{
46
 public:
47
  ProofCnfStream(context::UserContext* u,
48
                 CnfStream& cnfStream,
49
                 SatProofManager* satPM,
50
                 ProofNodeManager* pnm);
51
52
  /** Invokes getProofFor of the underlying LazyCDProof */
53
  std::shared_ptr<ProofNode> getProofFor(Node f) override;
54
  /** Whether there is a concrete step or a generator associated with f in the
55
   * underlying LazyCDProof. */
56
  bool hasProofFor(Node f) override;
57
  /** identify */
58
  std::string identify() const override;
59
  /**
60
   * Converts a formula into CNF into CNF and asserts the generated clauses into
61
   * the underlying SAT solver of d_cnfStream. Every transformation the formula
62
   * goes through is saved as a concrete step in d_proof.
63
   *
64
   * The given formula has arbitrary Boolean structure via kinds AND, OR, EQUAL,
65
   * XOR, IMPLIES. ITE and NOT. The conversion is done polynomially via Tseitin
66
   * transformation, with the children of non-conjunctive kinds being abstracted
67
   * as new literals, which are clausified with the respective "handle" methods
68
   * below.
69
70
   * @param node formula to convert and assert
71
   * @param negated whether we are asserting the node negated
72
   * @param removable whether the SAT solver can choose to remove the clauses
73
   * @param pg a proof generator for node
74
   */
75
  void convertAndAssert(TNode node,
76
                        bool negated,
77
                        bool removable,
78
                        ProofGenerator* pg);
79
80
  /**
81
   * Clausifies the given propagation lemma *without* registering the
82
   * resoluting clause in the SAT solver, as this is handled internally by the
83
   * SAT solver. The clausification steps and the generator within the trust
84
   * node are saved in d_proof. */
85
  void convertPropagation(theory::TrustNode ttn);
86
87
  /**
88
   * Ensure that the given node will have a designated SAT literal that is
89
   * definitionally equal to it.  The result of this function is that the Node
90
   * can be queried via getSatValue(). Essentially, this is like a "convert-but-
91
   * don't-assert" version of convertAndAssert().
92
   */
93
  void ensureLiteral(TNode n);
94
95
  /**
96
   * Blocks a proof, so that it is not further updated by a post processor of
97
   * this class's proof. */
98
  void addBlocked(std::shared_ptr<ProofNode> pfn);
99
100
  /**
101
   * Whether a given proof is blocked for further updates.  An example of a
102
   * blocked proof node is one integrated into this class via an external proof
103
   * generator. */
104
  bool isBlocked(std::shared_ptr<ProofNode> pfn);
105
106
 private:
107
  /**
108
   * Same as above, except that uses the saved d_removable flag. It calls the
109
   * dedicated converter for the possible formula kinds.
110
   */
111
  void convertAndAssert(TNode node, bool negated);
112
  /** Specific converters for each formula kind. */
113
  void convertAndAssertAnd(TNode node, bool negated);
114
  void convertAndAssertOr(TNode node, bool negated);
115
  void convertAndAssertXor(TNode node, bool negated);
116
  void convertAndAssertIff(TNode node, bool negated);
117
  void convertAndAssertImplies(TNode node, bool negated);
118
  void convertAndAssertIte(TNode node, bool negated);
119
  /**
120
   * Transforms the node into CNF recursively and yields a literal
121
   * definitionally equal to it.
122
   *
123
   * This method also populates caches, kept in d_cnfStream, between formulas
124
   * and literals to avoid redundant work and to retrieve formulas from literals
125
   * and vice-versa.
126
   *
127
   * @param node the formula to transform
128
   * @param negated whether the literal is negated
129
   * @return the literal representing the root of the formula
130
   */
131
  SatLiteral toCNF(TNode node, bool negated = false);
132
  /**
133
   * Specific clausifiers, based on the formula kinds, that clausify a formula,
134
   * by calling toCNF into each of the formula's children under the respective
135
   * kind, and introduce a literal definitionally equal to it. */
136
  SatLiteral handleNot(TNode node);
137
  SatLiteral handleXor(TNode node);
138
  SatLiteral handleImplies(TNode node);
139
  SatLiteral handleIff(TNode node);
140
  SatLiteral handleIte(TNode node);
141
  SatLiteral handleAnd(TNode node);
142
  SatLiteral handleOr(TNode node);
143
144
  /** Normalizes a clause node and registers it in the SAT proof manager.
145
   *
146
   * Normalization (factoring, reordering, double negation elimination) is done
147
   * via the TheoryProofStepBuffer of this class, which will register the
148
   * respective steps, if any. This normalization is necessary so that the
149
   * resulting clauses of the clausification process are synchronized with the
150
   * clauses used in the underlying SAT solver, which automatically performs the
151
   * above normalizations on all added clauses.
152
   */
153
  void normalizeAndRegister(TNode clauseNode);
154
  /** Reference to the underlying cnf stream. */
155
  CnfStream& d_cnfStream;
156
  /** The proof manager of underlying SAT solver associated with this stream. */
157
  SatProofManager* d_satPM;
158
  /** The proof node manager. */
159
  ProofNodeManager* d_pnm;
160
  /** The user-context-dependent proof object. */
161
  LazyCDProof d_proof;
162
  /** An accumulator of steps that may be applied to normalize the clauses
163
   * generated during clausification. */
164
  theory::TheoryProofStepBuffer d_psb;
165
  /** Blocked proofs.
166
   *
167
   * These are proof nodes added to this class by external generators. */
168
  context::CDHashSet<std::shared_ptr<ProofNode>, ProofNodeHashFunction>
169
      d_blocked;
170
};
171
172
}  // namespace prop
173
}  // namespace CVC4
174
175
#endif