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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief The proofproducing 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 usercontext dependent manner in a lazy contextdependent (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 nonconjunctive 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 "convertbut 
91 

* don'tassert" 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 viceversa. 
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 usercontextdependent 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 