GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/prop_engine.h Lines: 1 1 100.0 %
Date: 2021-03-22 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
8992
  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
  Node getPreprocessedTerm(TNode n,
225
                           std::vector<Node>& skAsserts,
226
                           std::vector<Node>& sks);
227
228
  /**
229
   * Push the context level.
230
   */
231
  void push();
232
233
  /**
234
   * Pop the context level.
235
   */
236
  void pop();
237
238
  /*
239
   * Reset the decisions in the DPLL(T) SAT solver at the current assertion
240
   * level.
241
   */
242
  void resetTrail();
243
244
  /**
245
   * Get the assertion level of the SAT solver.
246
   */
247
  unsigned getAssertionLevel() const;
248
249
  /**
250
   * Return true if we are currently searching (either in this or
251
   * another thread).
252
   */
253
  bool isRunning() const;
254
255
  /**
256
   * Interrupt a running solver (cause a timeout).
257
   *
258
   * Can potentially throw a ModalException.
259
   */
260
  void interrupt();
261
262
  /**
263
   * Informs the ResourceManager that a resource has been spent.  If out of
264
   * resources, can throw an UnsafeInterruptException exception.
265
   */
266
  void spendResource(ResourceManager::Resource r);
267
268
  /**
269
   * For debugging.  Return true if "expl" is a well-formed
270
   * explanation for "node," meaning:
271
   *
272
   * 1. expl is either a SAT literal or an AND of SAT literals
273
   *    currently assigned true;
274
   * 2. node is assigned true;
275
   * 3. node does not appear in expl; and
276
   * 4. node was assigned after all of the literals in expl
277
   */
278
  bool properExplanation(TNode node, TNode expl) const;
279
280
  /** Retrieve this modules proof CNF stream. */
281
  ProofCnfStream* getProofCnfStream();
282
283
  /** Checks that the proof is closed w.r.t. asserted formulas to this engine as
284
   * well as to the given assertions. */
285
  void checkProof(context::CDList<Node>* assertions);
286
287
  /**
288
   * Return the prop engine proof. This should be called only when proofs are
289
   * enabled. Returns a proof of false whose free assumptions are the
290
   * preprocessed assertions.
291
   */
292
  std::shared_ptr<ProofNode> getProof();
293
294
  /** Is proof enabled? */
295
  bool isProofEnabled() const;
296
 private:
297
  /** Dump out the satisfying assignment (after SAT result) */
298
  void printSatisfyingAssignment();
299
300
  /**
301
   * Converts the given formula to CNF and asserts the CNF to the SAT solver.
302
   * The formula can be removed by the SAT solver after backtracking lower
303
   * than the (SAT and SMT) level at which it was asserted.
304
   *
305
   * @param trn the trust node storing the formula to assert
306
   * @param removable whether this lemma can be quietly removed based
307
   * on an activity heuristic
308
   */
309
  void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable);
310
  /**
311
   * Assert node as a formula to the CNF stream
312
   * @param node The formula to assert
313
   * @param negated Whether to assert the negation of node
314
   * @param removable Whether the formula is removable
315
   * @param input Whether the formula came from the input
316
   * @param pg Pointer to a proof generator that can provide a proof of node
317
   * (or its negation if negated is true).
318
   */
319
  void assertInternal(TNode node,
320
                      bool negated,
321
                      bool removable,
322
                      bool input,
323
                      ProofGenerator* pg = nullptr);
324
  /**
325
   * Assert lemmas internal, where trn is a trust node corresponding to a
326
   * formula to assert to the CNF stream, ppLemmas and ppSkolems are the
327
   * skolem definitions and skolems obtained from preprocessing it, and
328
   * removable is whether the lemma is removable.
329
   */
330
  void assertLemmasInternal(theory::TrustNode trn,
331
                            const std::vector<theory::TrustNode>& ppLemmas,
332
                            const std::vector<Node>& ppSkolems,
333
                            bool removable);
334
335
  /**
336
   * Indicates that the SAT solver is currently solving something and we should
337
   * not mess with it's internal state.
338
   */
339
  bool d_inCheckSat;
340
341
  /** The theory engine we will be using */
342
  TheoryEngine* d_theoryEngine;
343
344
  /** The decision engine we will be using */
345
  std::unique_ptr<DecisionEngine> d_decisionEngine;
346
347
  /** The context */
348
  context::Context* d_context;
349
350
  /** SAT solver's proxy back to theories; kept around for dtor cleanup */
351
  TheoryProxy* d_theoryProxy;
352
353
  /** The SAT solver proxy */
354
  CDCLTSatSolverInterface* d_satSolver;
355
356
  /** List of all of the assertions that need to be made */
357
  std::vector<Node> d_assertionList;
358
359
  /** A pointer to the proof node maneger to be used by this engine. */
360
  ProofNodeManager* d_pnm;
361
362
  /** The CNF converter in use */
363
  CnfStream* d_cnfStream;
364
  /** Proof-producing CNF converter */
365
  std::unique_ptr<ProofCnfStream> d_pfCnfStream;
366
367
  /** The proof manager for prop engine */
368
  std::unique_ptr<PropPfManager> d_ppm;
369
370
  /** Whether we were just interrupted (or not) */
371
  bool d_interrupted;
372
  /** Pointer to resource manager for associated SmtEngine */
373
  ResourceManager* d_resourceManager;
374
375
  /** Reference to the output manager of the smt engine */
376
  OutputManager& d_outMgr;
377
};
378
379
}  // namespace prop
380
}  // namespace CVC4
381
382
#endif /* CVC4__PROP_ENGINE_H */