1 

/********************* */ 
2 

/*! \file prop_engine.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Morgan Deters, Dejan Jovanovic 
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 PropEngine (propositional engine); main interface point 
13 

** between CVC4's SMT infrastructure and the SAT solver 
14 

** 
15 

** The PropEngine (propositional engine); main interface point 
16 

** between CVC4's SMT infrastructure and the SAT solver. 
17 

**/ 
18 


19 

#include "cvc4_private.h" 
20 


21 

#ifndef CVC4__PROP_ENGINE_H 
22 

#define CVC4__PROP_ENGINE_H 
23 


24 

#include "context/cdlist.h" 
25 

#include "expr/node.h" 
26 

#include "theory/output_channel.h" 
27 

#include "theory/trust_node.h" 
28 

#include "util/result.h" 
29 


30 

namespace CVC4 { 
31 


32 

class ResourceManager; 
33 

class DecisionEngine; 
34 

class OutputManager; 
35 

class ProofNodeManager; 
36 

class TheoryEngine; 
37 


38 

namespace prop { 
39 


40 

class CnfStream; 
41 

class CDCLTSatSolverInterface; 
42 

class ProofCnfStream; 
43 

class PropPfManager; 
44 

class TheoryProxy; 
45 


46 

/** 
47 

* PropEngine is the abstraction of a Sat Solver, providing methods for 
48 

* solving the SAT problem and conversion to CNF (via the CnfStream). 
49 

*/ 
50 

class PropEngine 
51 

{ 
52 

public: 
53 

/** 
54 

* Create a PropEngine with a particular decision and theory engine. 
55 

*/ 
56 

PropEngine(TheoryEngine*, 
57 

context::Context* satContext, 
58 

context::UserContext* userContext, 
59 

ResourceManager* rm, 
60 

OutputManager& outMgr, 
61 

ProofNodeManager* pnm); 
62 


63 

/** 
64 

* Destructor. 
65 

*/ 
66 

~PropEngine(); 
67 


68 

/** 
69 

* Finish initialize. Call this after construction just before we are 
70 

* ready to use this class. Should be called after TheoryEngine::finishInit. 
71 

* This method converts and asserts true and false into the CNF stream. 
72 

*/ 
73 

void finishInit(); 
74 


75 

/** 
76 

* This is called by SmtEngine, at shutdown time, just before 
77 

* destruction. It is important because there are destruction 
78 

* ordering issues between some parts of the system (notably between 
79 

* PropEngine and Theory). For now, there's nothing to do here in 
80 

* the PropEngine. 
81 

*/ 
82 
8994 
void shutdown() {} 
83 


84 

/** 
85 

* Preprocess the given node. Return the REWRITE trust node corresponding to 
86 

* rewriting node. New lemmas and skolems are added to ppLemmas and 
87 

* ppSkolems respectively. 
88 

* 
89 

* @param node The assertion to preprocess, 
90 

* @param ppLemmas The lemmas to add to the set of assertions, 
91 

* @param ppSkolems The skolems that newLemmas correspond to, 
92 

* @return The (REWRITE) trust node corresponding to rewritten node via 
93 

* preprocessing. 
94 

*/ 
95 

theory::TrustNode preprocess(TNode node, 
96 

std::vector<theory::TrustNode>& ppLemmas, 
97 

std::vector<Node>& ppSkolems); 
98 

/** 
99 

* Remove term ITEs (and more generally, term formulas) from the given node. 
100 

* Return the REWRITE trust node corresponding to rewriting node. New lemmas 
101 

* and skolems are added to ppLemmas and ppSkolems respectively. This can 
102 

* be seen a subset of the above preprocess method, which also does theory 
103 

* preprocessing and rewriting. 
104 

* 
105 

* @param node The assertion to preprocess, 
106 

* @param ppLemmas The lemmas to add to the set of assertions, 
107 

* @param ppSkolems The skolems that newLemmas correspond to, 
108 

* @return The (REWRITE) trust node corresponding to rewritten node via 
109 

* preprocessing. 
110 

*/ 
111 

theory::TrustNode removeItes(TNode node, 
112 

std::vector<theory::TrustNode>& ppLemmas, 
113 

std::vector<Node>& ppSkolems); 
114 

/** 
115 

* Notify preprocessed assertions. This method is called just before the 
116 

* assertions are asserted to this prop engine. This method notifies the 
117 

* theory engine of the given assertions. Notice this vector includes 
118 

* both the input formulas and the skolem definitions. 
119 

*/ 
120 

void notifyPreprocessedAssertions(const std::vector<Node>& assertions); 
121 


122 

/** 
123 

* Converts the given formula to CNF and assert the CNF to the SAT solver. 
124 

* The formula is asserted permanently for the current context. Note the 
125 

* formula should correspond to an input formula and not a lemma introduced 
126 

* by term formula removal (which instead should use the interface below). 
127 

* @param node the formula to assert 
128 

*/ 
129 

void assertFormula(TNode node); 
130 

/** 
131 

* Same as above, but node corresponds to the skolem definition of the given 
132 

* skolem. 
133 

* @param node the formula to assert 
134 

* @param skolem the skolem that this lemma defines. 
135 

* 
136 

* For example, if k is introduced by ITE removal of (ite C x y), then node 
137 

* is the formula (ite C (= k x) (= k y)). It is important to distinguish 
138 

* these kinds of lemmas from input assertions, as the justification decision 
139 

* heuristic treates them specially. 
140 

*/ 
141 

void assertSkolemDefinition(TNode node, TNode skolem); 
142 


143 

/** 
144 

* Converts the given formula to CNF and assert the CNF to the SAT solver. 
145 

* The formula can be removed by the SAT solver after backtracking lower 
146 

* than the (SAT and SMT) level at which it was asserted. 
147 

* 
148 

* @param trn the trust node storing the formula to assert 
149 

* @param p the properties of the lemma 
150 

*/ 
151 

void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); 
152 


153 

/** 
154 

* If ever n is decided upon, it must be in the given phase. This 
155 

* occurs *globally*, i.e., even if the literal is untranslated by 
156 

* user pop and retranslated, it keeps this phase. The associated 
157 

* variable will _always_ be phaselocked. 
158 

* 
159 

* @param n the node in question; must have an associated SAT literal 
160 

* @param phase the phase to use 
161 

*/ 
162 

void requirePhase(TNode n, bool phase); 
163 


164 

/** 
165 

* Return whether the given literal is a SAT decision. Either phase 
166 

* is permitted; that is, if "lit" is a SAT decision, this function 
167 

* returns true for both lit and the negation of lit. 
168 

*/ 
169 

bool isDecision(Node lit) const; 
170 


171 

/** 
172 

* Checks the current context for satisfiability. 
173 

* 
174 

*/ 
175 

Result checkSat(); 
176 


177 

/** 
178 

* Get the value of a boolean variable. 
179 

* 
180 

* @return mkConst<true>, mkConst<false>, or Node::null() if 
181 

* unassigned. 
182 

*/ 
183 

Node getValue(TNode node) const; 
184 


185 

/** 
186 

* Return true if node has an associated SAT literal. 
187 

*/ 
188 

bool isSatLiteral(TNode node) const; 
189 


190 

/** 
191 

* Check if the node has a value and return it if yes. 
192 

*/ 
193 

bool hasValue(TNode node, bool& value) const; 
194 


195 

/** 
196 

* Returns the Boolean variables known to the SAT solver. 
197 

*/ 
198 

void getBooleanVariables(std::vector<TNode>& outputVariables) const; 
199 


200 

/** 
201 

* Ensure that the given node will have a designated SAT literal 
202 

* that is definitionally equal to it. Note that theory preprocessing is 
203 

* applied to n. The node returned by this method can be subsequently queried 
204 

* via getSatValue(). 
205 

*/ 
206 

Node ensureLiteral(TNode n); 
207 

/** 
208 

* This returns the theorypreprocessed form of term n. This rewrites and 
209 

* preprocesses n, which notice may involve adding clauses to the SAT solver 
210 

* if preprocessing n involves introducing new skolems. 
211 

*/ 
212 

Node getPreprocessedTerm(TNode n); 
213 

/** 
214 

* Same as above, but also compute the skolems in n and in the lemmas 
215 

* corresponding to their definition. 
216 

* 
217 

* Note this will include skolems that occur in the definition lemma 
218 

* for all skolems in sks. This is run until a fixed point is reached. 
219 

* For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is 
220 

* another skolem introduced by term formula removal, then calling this 
221 

* method on (P k1) will include both k1 and k2 in sks, and their definitions 
222 

* in skAsserts. 
223 

* 
224 

* Notice that this method is not frequently used. It is used for algorithms 
225 

* that explicitly care about knowing which skolems occur in the preprocessed 
226 

* form of a term, recursively. 
227 

*/ 
228 

Node getPreprocessedTerm(TNode n, 
229 

std::vector<Node>& skAsserts, 
230 

std::vector<Node>& sks); 
231 


232 

/** 
233 

* Push the context level. 
234 

*/ 
235 

void push(); 
236 


237 

/** 
238 

* Pop the context level. 
239 

*/ 
240 

void pop(); 
241 


242 

/* 
243 

* Reset the decisions in the DPLL(T) SAT solver at the current assertion 
244 

* level. 
245 

*/ 
246 

void resetTrail(); 
247 


248 

/** 
249 

* Get the assertion level of the SAT solver. 
250 

*/ 
251 

unsigned getAssertionLevel() const; 
252 


253 

/** 
254 

* Return true if we are currently searching (either in this or 
255 

* another thread). 
256 

*/ 
257 

bool isRunning() const; 
258 


259 

/** 
260 

* Interrupt a running solver (cause a timeout). 
261 

* 
262 

* Can potentially throw a ModalException. 
263 

*/ 
264 

void interrupt(); 
265 


266 

/** 
267 

* Informs the ResourceManager that a resource has been spent. If out of 
268 

* resources, can throw an UnsafeInterruptException exception. 
269 

*/ 
270 

void spendResource(ResourceManager::Resource r); 
271 


272 

/** 
273 

* For debugging. Return true if "expl" is a wellformed 
274 

* explanation for "node," meaning: 
275 

* 
276 

* 1. expl is either a SAT literal or an AND of SAT literals 
277 

* currently assigned true; 
278 

* 2. node is assigned true; 
279 

* 3. node does not appear in expl; and 
280 

* 4. node was assigned after all of the literals in expl 
281 

*/ 
282 

bool properExplanation(TNode node, TNode expl) const; 
283 


284 

/** Retrieve this modules proof CNF stream. */ 
285 

ProofCnfStream* getProofCnfStream(); 
286 


287 

/** Checks that the proof is closed w.r.t. asserted formulas to this engine as 
288 

* well as to the given assertions. */ 
289 

void checkProof(context::CDList<Node>* assertions); 
290 


291 

/** 
292 

* Return the prop engine proof. This should be called only when proofs are 
293 

* enabled. Returns a proof of false whose free assumptions are the 
294 

* preprocessed assertions. 
295 

*/ 
296 

std::shared_ptr<ProofNode> getProof(); 
297 


298 

/** Is proof enabled? */ 
299 

bool isProofEnabled() const; 
300 

private: 
301 

/** Dump out the satisfying assignment (after SAT result) */ 
302 

void printSatisfyingAssignment(); 
303 


304 

/** 
305 

* Converts the given formula to CNF and asserts the CNF to the SAT solver. 
306 

* The formula can be removed by the SAT solver after backtracking lower 
307 

* than the (SAT and SMT) level at which it was asserted. 
308 

* 
309 

* @param trn the trust node storing the formula to assert 
310 

* @param removable whether this lemma can be quietly removed based 
311 

* on an activity heuristic 
312 

*/ 
313 

void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable); 
314 

/** 
315 

* Assert node as a formula to the CNF stream 
316 

* @param node The formula to assert 
317 

* @param negated Whether to assert the negation of node 
318 

* @param removable Whether the formula is removable 
319 

* @param input Whether the formula came from the input 
320 

* @param pg Pointer to a proof generator that can provide a proof of node 
321 

* (or its negation if negated is true). 
322 

*/ 
323 

void assertInternal(TNode node, 
324 

bool negated, 
325 

bool removable, 
326 

bool input, 
327 

ProofGenerator* pg = nullptr); 
328 

/** 
329 

* Assert lemmas internal, where trn is a trust node corresponding to a 
330 

* formula to assert to the CNF stream, ppLemmas and ppSkolems are the 
331 

* skolem definitions and skolems obtained from preprocessing it, and 
332 

* removable is whether the lemma is removable. 
333 

*/ 
334 

void assertLemmasInternal(theory::TrustNode trn, 
335 

const std::vector<theory::TrustNode>& ppLemmas, 
336 

const std::vector<Node>& ppSkolems, 
337 

bool removable); 
338 


339 

/** 
340 

* Indicates that the SAT solver is currently solving something and we should 
341 

* not mess with it's internal state. 
342 

*/ 
343 

bool d_inCheckSat; 
344 


345 

/** The theory engine we will be using */ 
346 

TheoryEngine* d_theoryEngine; 
347 


348 

/** The decision engine we will be using */ 
349 

std::unique_ptr<DecisionEngine> d_decisionEngine; 
350 


351 

/** The context */ 
352 

context::Context* d_context; 
353 


354 

/** SAT solver's proxy back to theories; kept around for dtor cleanup */ 
355 

TheoryProxy* d_theoryProxy; 
356 


357 

/** The SAT solver proxy */ 
358 

CDCLTSatSolverInterface* d_satSolver; 
359 


360 

/** List of all of the assertions that need to be made */ 
361 

std::vector<Node> d_assertionList; 
362 


363 

/** A pointer to the proof node maneger to be used by this engine. */ 
364 

ProofNodeManager* d_pnm; 
365 


366 

/** The CNF converter in use */ 
367 

CnfStream* d_cnfStream; 
368 

/** Proofproducing CNF converter */ 
369 

std::unique_ptr<ProofCnfStream> d_pfCnfStream; 
370 


371 

/** The proof manager for prop engine */ 
372 

std::unique_ptr<PropPfManager> d_ppm; 
373 


374 

/** Whether we were just interrupted (or not) */ 
375 

bool d_interrupted; 
376 

/** Pointer to resource manager for associated SmtEngine */ 
377 

ResourceManager* d_resourceManager; 
378 


379 

/** Reference to the output manager of the smt engine */ 
380 

OutputManager& d_outMgr; 
381 

}; 
382 


383 

} // namespace prop 
384 

} // namespace CVC4 
385 


386 

#endif /* CVC4__PROP_ENGINE_H */ 