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

Line Exec Source
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) 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 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 phase-locked.
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 theory-preprocessed 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 well-formed
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
  /** Proof-producing 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 */