Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/prop_engine.h	Lines:	1	1	100.0 %
Date:	2021-05-22	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The PropEngine (propositional engine).
 *
 * Main interface point between cvc5's SMT infrastructure and the SAT solver.
 */

#include "cvc5_private.h"

#ifndef CVC5__PROP_ENGINE_H
#define CVC5__PROP_ENGINE_H

#include "context/cdlist.h"
#include "expr/node.h"
#include "prop/skolem_def_manager.h"
#include "theory/output_channel.h"
#include "theory/trust_node.h"
#include "util/result.h"

namespace cvc5 {

class Env;
class ResourceManager;
class OutputManager;
class ProofNodeManager;
class TheoryEngine;

namespace decision {
class DecisionEngine;
}

namespace prop {

class CnfStream;
class CDCLTSatSolverInterface;
class ProofCnfStream;
class PropPfManager;
class TheoryProxy;

/**
 * PropEngine is the abstraction of a Sat Solver, providing methods for
 * solving the SAT problem and conversion to CNF (via the CnfStream).
 */
class PropEngine
{
 public:
  /**
   * Create a PropEngine with a particular decision and theory engine.
   */
  PropEngine(TheoryEngine* te,
             Env& env,
             OutputManager& outMgr,
             ProofNodeManager* pnm);

  /**
   * Destructor.
   */
  ~PropEngine();

  /**
   * Finish initialize. Call this after construction just before we are
   * ready to use this class. Should be called after TheoryEngine::finishInit.
   * This method converts and asserts true and false into the CNF stream.
   */
  void finishInit();

  /**
   * This is called by SmtEngine, at shutdown time, just before
   * destruction.  It is important because there are destruction
   * ordering issues between some parts of the system (notably between
   * PropEngine and Theory).  For now, there's nothing to do here in
   * the PropEngine.
   */
  void shutdown() {}

  /**
   * Preprocess the given node. Return the REWRITE trust node corresponding to
   * rewriting node. New lemmas and skolems are added to ppLemmas and
   * ppSkolems respectively.
   *
   * @param node The assertion to preprocess,
   * @param ppLemmas The lemmas to add to the set of assertions,
   * @param ppSkolems The skolems that newLemmas correspond to,
   * @return The (REWRITE) trust node corresponding to rewritten node via
   * preprocessing.
   */
  theory::TrustNode preprocess(TNode node,
                               std::vector<theory::TrustNode>& ppLemmas,
                               std::vector<Node>& ppSkolems);
  /**
   * Remove term ITEs (and more generally, term formulas) from the given node.
   * Return the REWRITE trust node corresponding to rewriting node. New lemmas
   * and skolems are added to ppLemmas and ppSkolems respectively. This can
   * be seen a subset of the above preprocess method, which also does theory
   * preprocessing and rewriting.
   *
   * @param node The assertion to preprocess,
   * @param ppLemmas The lemmas to add to the set of assertions,
   * @param ppSkolems The skolems that newLemmas correspond to,
   * @return The (REWRITE) trust node corresponding to rewritten node via
   * preprocessing.
   */
  theory::TrustNode removeItes(TNode node,
                               std::vector<theory::TrustNode>& ppLemmas,
                               std::vector<Node>& ppSkolems);

  /**
   * Converts the given formulas to CNF and assert the CNF to the SAT solver.
   * These formulas are asserted permanently for the current context.
   * Information about which assertions correspond to skolem definitions is
   * contained in skolemMap.
   *
   * @param assertions the formulas to assert
   * @param skolemMap a map which says which skolem (if any) each assertion
   * corresponds to. For example, if (ite C (= k a) (= k b)) is the i^th
   * assertion, then skolemMap may contain the entry { i -> k }.
   */
  void assertInputFormulas(const std::vector<Node>& assertions,
                           std::unordered_map<size_t, Node>& skolemMap);

  /**
   * Converts the given formula to CNF and assert the CNF to the SAT solver.
   * The formula can be removed by the SAT solver after backtracking lower
   * than the (SAT and SMT) level at which it was asserted.
   *
   * @param trn the trust node storing the formula to assert
   * @param p the properties of the lemma
   */
  void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);

  /**
   * If ever n is decided upon, it must be in the given phase.  This
   * occurs *globally*, i.e., even if the literal is untranslated by
   * user pop and retranslated, it keeps this phase.  The associated
   * variable will _always_ be phase-locked.
   *
   * @param n the node in question; must have an associated SAT literal
   * @param phase the phase to use
   */
  void requirePhase(TNode n, bool phase);

  /**
   * Return whether the given literal is a SAT decision.  Either phase
   * is permitted; that is, if "lit" is a SAT decision, this function
   * returns true for both lit and the negation of lit.
   */
  bool isDecision(Node lit) const;

  /**
   * Return the current decision level of `lit`.
   *
   * @param lit: The node in question, must have an associated SAT literal.
   * @return Decision level of the SAT variable of `lit` (phase is disregarded),
   *         or -1 if `lit` has not been assigned yet.
   */
  int32_t getDecisionLevel(Node lit) const;

  /**
   * Return the user-context level when `lit` was introduced..
   *
   * @return User-context level or -1 if not yet introduced.
   */
  int32_t getIntroLevel(Node lit) const;

  /**
   * Checks the current context for satisfiability.
   *
   */
  Result checkSat();

  /**
   * Get the value of a boolean variable.
   *
   * @return mkConst<true>, mkConst<false>, or Node::null() if
   * unassigned.
   */
  Node getValue(TNode node) const;

  /**
   * Return true if node has an associated SAT literal.
   */
  bool isSatLiteral(TNode node) const;

  /**
   * Check if the node has a value and return it if yes.
   */
  bool hasValue(TNode node, bool& value) const;

  /**
   * Returns the Boolean variables known to the SAT solver.
   */
  void getBooleanVariables(std::vector<TNode>& outputVariables) const;

  /**
   * Ensure that the given node will have a designated SAT literal
   * that is definitionally equal to it. Note that theory preprocessing is
   * applied to n. The node returned by this method can be subsequently queried
   * via getSatValue().
   */
  Node ensureLiteral(TNode n);
  /**
   * This returns the theory-preprocessed form of term n. This rewrites and
   * preprocesses n, which notice may involve adding clauses to the SAT solver
   * if preprocessing n involves introducing new skolems.
   */
  Node getPreprocessedTerm(TNode n);
  /**
   * Same as above, but also compute the skolems in n and in the lemmas
   * corresponding to their definition.
   *
   * Note this will include skolems that occur in the definition lemma
   * for all skolems in sks. This is run until a fixed point is reached.
   * For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is
   * another skolem introduced by term formula removal, then calling this
   * method on (P k1) will include both k1 and k2 in sks, and their definitions
   * in skAsserts.
   *
   * Notice that this method is not frequently used. It is used for algorithms
   * that explicitly care about knowing which skolems occur in the preprocessed
   * form of a term, recursively.
   */
  Node getPreprocessedTerm(TNode n,
                           std::vector<Node>& skAsserts,
                           std::vector<Node>& sks);

  /**
   * Push the context level.
   */
  void push();

  /**
   * Pop the context level.
   */
  void pop();

  /*
   * Reset the decisions in the DPLL(T) SAT solver at the current assertion
   * level.
   */
  void resetTrail();

  /**
   * Get the assertion level of the SAT solver.
   */
  unsigned getAssertionLevel() const;

  /**
   * Return true if we are currently searching (either in this or
   * another thread).
   */
  bool isRunning() const;

  /**
   * Interrupt a running solver (cause a timeout).
   *
   * Can potentially throw a ModalException.
   */
  void interrupt();

  /**
   * Informs the ResourceManager that a resource has been spent.  If out of
   * resources, can throw an UnsafeInterruptException exception.
   */
  void spendResource(Resource r);

  /**
   * For debugging.  Return true if "expl" is a well-formed
   * explanation for "node," meaning:
   *
   * 1. expl is either a SAT literal or an AND of SAT literals
   *    currently assigned true;
   * 2. node is assigned true;
   * 3. node does not appear in expl; and
   * 4. node was assigned after all of the literals in expl
   */
  bool properExplanation(TNode node, TNode expl) const;

  /** Retrieve this modules proof CNF stream. */
  ProofCnfStream* getProofCnfStream();

  /** Checks that the proof is closed w.r.t. asserted formulas to this engine as
   * well as to the given assertions. */
  void checkProof(context::CDList<Node>* assertions);

  /**
   * Return the prop engine proof. This should be called only when proofs are
   * enabled. Returns a proof of false whose free assumptions are the
   * preprocessed assertions.
   */
  std::shared_ptr<ProofNode> getProof();

  /** Is proof enabled? */
  bool isProofEnabled() const;

  /** Retrieve unsat core from SAT solver for assumption-based unsat cores. */
  void getUnsatCore(std::vector<Node>& core);

  /** Return the prop engine proof for assumption-based unsat cores. */
  std::shared_ptr<ProofNode> getRefutation();

 private:
  /** Dump out the satisfying assignment (after SAT result) */
  void printSatisfyingAssignment();

  /**
   * Converts the given formula to CNF and asserts the CNF to the SAT solver.
   * The formula can be removed by the SAT solver after backtracking lower
   * than the (SAT and SMT) level at which it was asserted.
   *
   * @param trn the trust node storing the formula to assert
   * @param removable whether this lemma can be quietly removed based
   * on an activity heuristic
   */
  void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable);
  /**
   * Assert node as a formula to the CNF stream
   * @param node The formula to assert
   * @param negated Whether to assert the negation of node
   * @param removable Whether the formula is removable
   * @param input Whether the formula came from the input
   * @param pg Pointer to a proof generator that can provide a proof of node
   * (or its negation if negated is true).
   */
  void assertInternal(TNode node,
                      bool negated,
                      bool removable,
                      bool input,
                      ProofGenerator* pg = nullptr);
  /**
   * Assert lemmas internal, where trn is a trust node corresponding to a
   * formula to assert to the CNF stream, ppLemmas and ppSkolems are the
   * skolem definitions and skolems obtained from preprocessing it, and
   * removable is whether the lemma is removable.
   */
  void assertLemmasInternal(theory::TrustNode trn,
                            const std::vector<theory::TrustNode>& ppLemmas,
                            const std::vector<Node>& ppSkolems,
                            bool removable);

  /**
   * Indicates that the SAT solver is currently solving something and we should
   * not mess with it's internal state.
   */
  bool d_inCheckSat;

  /** The theory engine we will be using */
  TheoryEngine* d_theoryEngine;

  /** Reference to the environment */
  Env& d_env;

  /** The decision engine we will be using */
  std::unique_ptr<decision::DecisionEngine> d_decisionEngine;

  /** The skolem definition manager */
  std::unique_ptr<SkolemDefManager> d_skdm;

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

  /** The SAT solver proxy */
  CDCLTSatSolverInterface* d_satSolver;

  /** List of all of the assertions that need to be made */
  std::vector<Node> d_assertionList;

  /** A pointer to the proof node maneger to be used by this engine. */
  ProofNodeManager* d_pnm;

  /** The CNF converter in use */
  CnfStream* d_cnfStream;
  /** Proof-producing CNF converter */
  std::unique_ptr<ProofCnfStream> d_pfCnfStream;

  /** The proof manager for prop engine */
  std::unique_ptr<PropPfManager> d_ppm;

  /** Whether we were just interrupted (or not) */
  bool d_interrupted;

  /** Reference to the output manager of the smt engine */
  OutputManager& d_outMgr;

  /**
   * Stores assumptions added via assertInternal() if assumption-based unsat
   * cores are enabled.
   */
  context::CDList<Node> d_assumptions;
};

}  // namespace prop
}  // namespace cvc5

#endif /* CVC5__PROP_ENGINE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Dejan Jovanovic
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* The PropEngine (propositional engine).
14		*
15		* Main interface point between cvc5's SMT infrastructure and the SAT solver.
16		*/
17
18		#include "cvc5_private.h"
19
20		#ifndef CVC5__PROP_ENGINE_H
21		#define CVC5__PROP_ENGINE_H
22
23		#include "context/cdlist.h"
24		#include "expr/node.h"
25		#include "prop/skolem_def_manager.h"
26		#include "theory/output_channel.h"
27		#include "theory/trust_node.h"
28		#include "util/result.h"
29
30		namespace cvc5 {
31
32		class Env;
33		class ResourceManager;
34		class OutputManager;
35		class ProofNodeManager;
36		class TheoryEngine;
37
38		namespace decision {
39		class DecisionEngine;
40		}
41
42		namespace prop {
43
44		class CnfStream;
45		class CDCLTSatSolverInterface;
46		class ProofCnfStream;
47		class PropPfManager;
48		class TheoryProxy;
49
50		/**
51		* PropEngine is the abstraction of a Sat Solver, providing methods for
52		* solving the SAT problem and conversion to CNF (via the CnfStream).
53		*/
54		class PropEngine
55		{
56		public:
57		/**
58		* Create a PropEngine with a particular decision and theory engine.
59		*/
60		PropEngine(TheoryEngine* te,
61		Env& env,
62		OutputManager& outMgr,
63		ProofNodeManager* pnm);
64
65		/**
66		* Destructor.
67		*/
68		~PropEngine();
69
70		/**
71		* Finish initialize. Call this after construction just before we are
72		* ready to use this class. Should be called after TheoryEngine::finishInit.
73		* This method converts and asserts true and false into the CNF stream.
74		*/
75		void finishInit();
76
77		/**
78		* This is called by SmtEngine, at shutdown time, just before
79		* destruction. It is important because there are destruction
80		* ordering issues between some parts of the system (notably between
81		* PropEngine and Theory). For now, there's nothing to do here in
82		* the PropEngine.
83		*/
84	9459	void shutdown() {}
85
86		/**
87		* Preprocess the given node. Return the REWRITE trust node corresponding to
88		* rewriting node. New lemmas and skolems are added to ppLemmas and
89		* ppSkolems respectively.
90		*
91		* @param node The assertion to preprocess,
92		* @param ppLemmas The lemmas to add to the set of assertions,
93		* @param ppSkolems The skolems that newLemmas correspond to,
94		* @return The (REWRITE) trust node corresponding to rewritten node via
95		* preprocessing.
96		*/
97		theory::TrustNode preprocess(TNode node,
98		std::vector<theory::TrustNode>& ppLemmas,
99		std::vector<Node>& ppSkolems);
100		/**
101		* Remove term ITEs (and more generally, term formulas) from the given node.
102		* Return the REWRITE trust node corresponding to rewriting node. New lemmas
103		* and skolems are added to ppLemmas and ppSkolems respectively. This can
104		* be seen a subset of the above preprocess method, which also does theory
105		* preprocessing and rewriting.
106		*
107		* @param node The assertion to preprocess,
108		* @param ppLemmas The lemmas to add to the set of assertions,
109		* @param ppSkolems The skolems that newLemmas correspond to,
110		* @return The (REWRITE) trust node corresponding to rewritten node via
111		* preprocessing.
112		*/
113		theory::TrustNode removeItes(TNode node,
114		std::vector<theory::TrustNode>& ppLemmas,
115		std::vector<Node>& ppSkolems);
116
117		/**
118		* Converts the given formulas to CNF and assert the CNF to the SAT solver.
119		* These formulas are asserted permanently for the current context.
120		* Information about which assertions correspond to skolem definitions is
121		* contained in skolemMap.
122		*
123		* @param assertions the formulas to assert
124		* @param skolemMap a map which says which skolem (if any) each assertion
125		* corresponds to. For example, if (ite C (= k a) (= k b)) is the i^th
126		* assertion, then skolemMap may contain the entry { i -> k }.
127		*/
128		void assertInputFormulas(const std::vector<Node>& assertions,
129		std::unordered_map<size_t, Node>& skolemMap);
130
131		/**
132		* Converts the given formula to CNF and assert the CNF to the SAT solver.
133		* The formula can be removed by the SAT solver after backtracking lower
134		* than the (SAT and SMT) level at which it was asserted.
135		*
136		* @param trn the trust node storing the formula to assert
137		* @param p the properties of the lemma
138		*/
139		void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
140
141		/**
142		* If ever n is decided upon, it must be in the given phase. This
143		* occurs globally, i.e., even if the literal is untranslated by
144		* user pop and retranslated, it keeps this phase. The associated
145		* variable will _always_ be phase-locked.
146		*
147		* @param n the node in question; must have an associated SAT literal
148		* @param phase the phase to use
149		*/
150		void requirePhase(TNode n, bool phase);
151
152		/**
153		* Return whether the given literal is a SAT decision. Either phase
154		* is permitted; that is, if "lit" is a SAT decision, this function
155		* returns true for both lit and the negation of lit.
156		*/
157		bool isDecision(Node lit) const;
158
159		/**
160		* Return the current decision level of `lit`.
161		*
162		* @param lit: The node in question, must have an associated SAT literal.
163		* @return Decision level of the SAT variable of `lit` (phase is disregarded),
164		* or -1 if `lit` has not been assigned yet.
165		*/
166		int32_t getDecisionLevel(Node lit) const;
167
168		/**
169		* Return the user-context level when `lit` was introduced..
170		*
171		* @return User-context level or -1 if not yet introduced.
172		*/
173		int32_t getIntroLevel(Node lit) const;
174
175		/**
176		* Checks the current context for satisfiability.
177		*
178		*/
179		Result checkSat();
180
181		/**
182		* Get the value of a boolean variable.
183		*
184		* @return mkConst<true>, mkConst<false>, or Node::null() if
185		* unassigned.
186		*/
187		Node getValue(TNode node) const;
188
189		/**
190		* Return true if node has an associated SAT literal.
191		*/
192		bool isSatLiteral(TNode node) const;
193
194		/**
195		* Check if the node has a value and return it if yes.
196		*/
197		bool hasValue(TNode node, bool& value) const;
198
199		/**
200		* Returns the Boolean variables known to the SAT solver.
201		*/
202		void getBooleanVariables(std::vector<TNode>& outputVariables) const;
203
204		/**
205		* Ensure that the given node will have a designated SAT literal
206		* that is definitionally equal to it. Note that theory preprocessing is
207		* applied to n. The node returned by this method can be subsequently queried
208		* via getSatValue().
209		*/
210		Node ensureLiteral(TNode n);
211		/**
212		* This returns the theory-preprocessed form of term n. This rewrites and
213		* preprocesses n, which notice may involve adding clauses to the SAT solver
214		* if preprocessing n involves introducing new skolems.
215		*/
216		Node getPreprocessedTerm(TNode n);
217		/**
218		* Same as above, but also compute the skolems in n and in the lemmas
219		* corresponding to their definition.
220		*
221		* Note this will include skolems that occur in the definition lemma
222		* for all skolems in sks. This is run until a fixed point is reached.
223		* For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is
224		* another skolem introduced by term formula removal, then calling this
225		* method on (P k1) will include both k1 and k2 in sks, and their definitions
226		* in skAsserts.
227		*
228		* Notice that this method is not frequently used. It is used for algorithms
229		* that explicitly care about knowing which skolems occur in the preprocessed
230		* form of a term, recursively.
231		*/
232		Node getPreprocessedTerm(TNode n,
233		std::vector<Node>& skAsserts,
234		std::vector<Node>& sks);
235
236		/**
237		* Push the context level.
238		*/
239		void push();
240
241		/**
242		* Pop the context level.
243		*/
244		void pop();
245
246		/*
247		* Reset the decisions in the DPLL(T) SAT solver at the current assertion
248		* level.
249		*/
250		void resetTrail();
251
252		/**
253		* Get the assertion level of the SAT solver.
254		*/
255		unsigned getAssertionLevel() const;
256
257		/**
258		* Return true if we are currently searching (either in this or
259		* another thread).
260		*/
261		bool isRunning() const;
262
263		/**
264		* Interrupt a running solver (cause a timeout).
265		*
266		* Can potentially throw a ModalException.
267		*/
268		void interrupt();
269
270		/**
271		* Informs the ResourceManager that a resource has been spent. If out of
272		* resources, can throw an UnsafeInterruptException exception.
273		*/
274		void spendResource(Resource r);
275
276		/**
277		* For debugging. Return true if "expl" is a well-formed
278		* explanation for "node," meaning:
279		*
280		* 1. expl is either a SAT literal or an AND of SAT literals
281		* currently assigned true;
282		* 2. node is assigned true;
283		* 3. node does not appear in expl; and
284		* 4. node was assigned after all of the literals in expl
285		*/
286		bool properExplanation(TNode node, TNode expl) const;
287
288		/** Retrieve this modules proof CNF stream. */
289		ProofCnfStream* getProofCnfStream();
290
291		/** Checks that the proof is closed w.r.t. asserted formulas to this engine as
292		* well as to the given assertions. */
293		void checkProof(context::CDList<Node>* assertions);
294
295		/**
296		* Return the prop engine proof. This should be called only when proofs are
297		* enabled. Returns a proof of false whose free assumptions are the
298		* preprocessed assertions.
299		*/
300		std::shared_ptr<ProofNode> getProof();
301
302		/** Is proof enabled? */
303		bool isProofEnabled() const;
304
305		/** Retrieve unsat core from SAT solver for assumption-based unsat cores. */
306		void getUnsatCore(std::vector<Node>& core);
307
308		/** Return the prop engine proof for assumption-based unsat cores. */
309		std::shared_ptr<ProofNode> getRefutation();
310
311		private:
312		/** Dump out the satisfying assignment (after SAT result) */
313		void printSatisfyingAssignment();
314
315		/**
316		* Converts the given formula to CNF and asserts the CNF to the SAT solver.
317		* The formula can be removed by the SAT solver after backtracking lower
318		* than the (SAT and SMT) level at which it was asserted.
319		*
320		* @param trn the trust node storing the formula to assert
321		* @param removable whether this lemma can be quietly removed based
322		* on an activity heuristic
323		*/
324		void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable);
325		/**
326		* Assert node as a formula to the CNF stream
327		* @param node The formula to assert
328		* @param negated Whether to assert the negation of node
329		* @param removable Whether the formula is removable
330		* @param input Whether the formula came from the input
331		* @param pg Pointer to a proof generator that can provide a proof of node
332		* (or its negation if negated is true).
333		*/
334		void assertInternal(TNode node,
335		bool negated,
336		bool removable,
337		bool input,
338		ProofGenerator* pg = nullptr);
339		/**
340		* Assert lemmas internal, where trn is a trust node corresponding to a
341		* formula to assert to the CNF stream, ppLemmas and ppSkolems are the
342		* skolem definitions and skolems obtained from preprocessing it, and
343		* removable is whether the lemma is removable.
344		*/
345		void assertLemmasInternal(theory::TrustNode trn,
346		const std::vector<theory::TrustNode>& ppLemmas,
347		const std::vector<Node>& ppSkolems,
348		bool removable);
349
350		/**
351		* Indicates that the SAT solver is currently solving something and we should
352		* not mess with it's internal state.
353		*/
354		bool d_inCheckSat;
355
356		/** The theory engine we will be using */
357		TheoryEngine* d_theoryEngine;
358
359		/** Reference to the environment */
360		Env& d_env;
361
362		/** The decision engine we will be using */
363		std::unique_ptr<decision::DecisionEngine> d_decisionEngine;
364
365		/** The skolem definition manager */
366		std::unique_ptr<SkolemDefManager> d_skdm;
367
368		/** SAT solver's proxy back to theories; kept around for dtor cleanup */
369		TheoryProxy* d_theoryProxy;
370
371		/** The SAT solver proxy */
372		CDCLTSatSolverInterface* d_satSolver;
373
374		/** List of all of the assertions that need to be made */
375		std::vector<Node> d_assertionList;
376
377		/** A pointer to the proof node maneger to be used by this engine. */
378		ProofNodeManager* d_pnm;
379
380		/** The CNF converter in use */
381		CnfStream* d_cnfStream;
382		/** Proof-producing CNF converter */
383		std::unique_ptr<ProofCnfStream> d_pfCnfStream;
384
385		/** The proof manager for prop engine */
386		std::unique_ptr<PropPfManager> d_ppm;
387
388		/** Whether we were just interrupted (or not) */
389		bool d_interrupted;
390
391		/** Reference to the output manager of the smt engine */
392		OutputManager& d_outMgr;
393
394		/**
395		* Stores assumptions added via assertInternal() if assumption-based unsat
396		* cores are enabled.
397		*/
398		context::CDList<Node> d_assumptions;
399		};
400
401		} // namespace prop
402		} // namespace cvc5
403
404		#endif /* CVC5__PROP_ENGINE_H */