Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/smt_engine_state.h	Lines:	1	1	100.0 %
Date:	2021-08-03	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Ying Sheng, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Utility for maintaining the state of the SMT engine.
 */

#include "cvc5_private.h"

#ifndef CVC5__SMT__SMT_ENGINE_STATE_H
#define CVC5__SMT__SMT_ENGINE_STATE_H

#include <string>

#include "context/context.h"
#include "smt/smt_mode.h"
#include "util/result.h"

namespace cvc5 {

class SmtEngine;

namespace smt {

/**
 * This utility is responsible for maintaining the basic state of the SmtEngine.
 *
 * It has no concept of anything related to the assertions of the SmtEngine,
 * or more generally it does not depend on Node.
 *
 * This class has three sets of interfaces:
 * (1) notification methods that are used by SmtEngine to notify when an event
 * occurs (e.g. the beginning of a check-sat call),
 * (2) maintaining the SAT and user contexts to be used by the SmtEngine,
 * (3) general information queries, including the mode that the SmtEngine is
 * in, based on the notifications it has received.
 *
 * It maintains a reference to the SmtEngine for the sake of making callbacks.
 */
class SmtEngineState
{
 public:
  SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt);
  ~SmtEngineState() {}
  /**
   * Notify that the expected status of the next check-sat is given by the
   * string status, which should be one of "sat", "unsat" or "unknown".
   */
  void notifyExpectedStatus(const std::string& status);
  /**
   * Notify that the SmtEngine is fully initialized, which is called when
   * options are finalized.
   */
  void notifyFullyInited();
  /**
   * Notify that we are resetting the assertions, called when a reset-assertions
   * command is issued by the user.
   */
  void notifyResetAssertions();
  /**
   * Notify that we are about to call check-sat. This call is made prior to
   * initializing the assertions. It processes pending pops and pushes a
   * (user) context if necessary.
   *
   * @param hasAssumptions Whether the call to check-sat has assumptions. If
   * so, we push a context.
   */
  void notifyCheckSat(bool hasAssumptions);
  /**
   * Notify that the result of the last check-sat was r. This should be called
   * once immediately following notifyCheckSat() if the check-sat call
   * returned normal (i.e. it was not interupted).
   *
   * @param hasAssumptions Whether the prior call to check-sat had assumptions.
   * If so, we pop a context.
   * @param r The result of the check-sat call.
   */
  void notifyCheckSatResult(bool hasAssumptions, Result r);
  /**
   * Notify that we finished an abduction query, where success is whether the
   * command was successful. This is managed independently of the above
   * calls for notifying check-sat. In other words, if a get-abduct command
   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
   * to solve the abduction query. This method is called *in addition* to
   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
   * In particular, it is called after these two methods are completed.
   * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction
   * was successful.
   */
  void notifyGetAbduct(bool success);
  /**
   * Notify that we finished an interpolation query, where success is whether
   * the command was successful. This is managed independently of the above
   * calls for notifying check-sat. In other words, if a get-interpol command
   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
   * to solve the interpolation query. This method is called *in addition* to
   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
   * In particular, it is called after these two methods are completed.
   * This overwrites the SMT mode to the "INTERPOL" mode if the call to
   * interpolation was successful.
   */
  void notifyGetInterpol(bool success);
  /**
   * Setup the context, which makes a single push to maintain a global
   * context around everything.
   */
  void setup();
  /**
   * Set that we are in a fully initialized state.
   */
  void finishInit();
  /**
   * Prepare for a shutdown of the SmtEngine, which does pending pops and
   * pops the user context to zero.
   */
  void shutdown();
  /**
   * Cleanup, which pops all contexts to level zero.
   */
  void cleanup();
  /**
   * Set that the file name of the current instance is the given string. This
   * is used for various purposes (e.g. get-info, SZS status).
   */
  void setFilename(const std::string& filename);

  //---------------------------- context management
  /**
   * Do all pending pops, which ensures that the context levels are up-to-date.
   * This method should be called by the SmtEngine before using any of its
   * members that rely on the context (e.g. PropEngine or TheoryEngine).
   */
  void doPendingPops();
  /**
   * Called when the user of SmtEngine issues a push. This corresponds to
   * the SMT-LIB command push.
   */
  void userPush();
  /**
   * Called when the user of SmtEngine issues a pop. This corresponds to
   * the SMT-LIB command pop.
   */
  void userPop();
  /** Get a pointer to the UserContext owned by this SmtEngine. */
  context::UserContext* getUserContext();
  /** Get a pointer to the Context owned by this SmtEngine. */
  context::Context* getContext();
  //---------------------------- end context management

  //---------------------------- queries
  /**
   * Return true if the SmtEngine is fully initialized (post-construction).
   * This post-construction initialization is automatically triggered by the
   * use of the SmtEngine; e.g. when the first formula is asserted, a call
   * to simplify() is issued, a scope is pushed, etc.
   */
  bool isFullyInited() const;
  /**
   * Return true if the SmtEngine is fully initialized and there are no
   * pending pops.
   */
  bool isFullyReady() const;
  /**
   * Return true if a notifyCheckSat call has been made, e.g. a query has been
   * issued to the SmtEngine.
   */
  bool isQueryMade() const;
  /** Return the user context level.  */
  size_t getNumUserLevels() const;
  /** Get the status of the last check-sat */
  Result getStatus() const;
  /** Get the SMT mode we are in */
  SmtMode getMode() const;
  /** return the input name (if any) */
  const std::string& getFilename() const;
  //---------------------------- end queries

 private:
  /** Pushes the user and SAT contexts */
  void push();
  /** Pops the user and SAT contexts */
  void pop();
  /** Pops the user and SAT contexts to the given level */
  void popto(int toLevel);
  /**
   * Internal push, which processes any pending pops, and pushes (if in
   * incremental mode).
   */
  void internalPush();
  /**
   * Internal pop. If immediate is true, this processes any pending pops, and
   * pops (if in incremental mode). Otherwise, it increments the pending pop
   * counter and does nothing.
   */
  void internalPop(bool immediate = false);
  /** Reference to the SmtEngine */
  SmtEngine& d_smt;
  /** Expr manager context */
  context::Context* d_context;
  /** User level context */
  context::UserContext* d_userContext;
  /** The context levels of user pushes */
  std::vector<int> d_userLevels;

  /**
   * Number of internal pops that have been deferred.
   */
  unsigned d_pendingPops;

  /**
   * Whether or not the SmtEngine is fully initialized (post-construction).
   * This post-construction initialization is automatically triggered by the
   * use of the SmtEngine which calls the finishInit method above; e.g. when
   * the first formula is asserted, a call to simplify() is issued, a scope is
   * pushed, etc.
   */
  bool d_fullyInited;

  /**
   * Whether or not a notifyCheckSat call has been made, which corresponds to
   * when a checkEntailed() or checkSatisfiability() has already been
   * made through the SmtEngine.  If true, and incrementalSolving is false,
   * then attempting an additional checks for satisfiability will fail with
   * a ModalException during notifyCheckSat.
   */
  bool d_queryMade;

  /**
   * Internal status flag to indicate whether we have been issued a
   * notifyCheckSat call and have yet to process the "postsolve" methods of
   * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost.
   */
  bool d_needPostsolve;

  /**
   * Most recent result of last checkSatisfiability/checkEntailed in the
   * SmtEngine.
   */
  Result d_status;

  /**
   * The expected status of the next satisfiability check.
   */
  Result d_expectedStatus;

  /** The SMT mode, for details see enumeration above. */
  SmtMode d_smtMode;

  /**
   * The input file name or the name set through (set-info :filename ...), if
   * any.
   */
  std::string d_filename;
};

}  // namespace smt
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Ying Sheng, Morgan Deters
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		* Utility for maintaining the state of the SMT engine.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__SMT__SMT_ENGINE_STATE_H
19		#define CVC5__SMT__SMT_ENGINE_STATE_H
20
21		#include <string>
22
23		#include "context/context.h"
24		#include "smt/smt_mode.h"
25		#include "util/result.h"
26
27		namespace cvc5 {
28
29		class SmtEngine;
30
31		namespace smt {
32
33		/**
34		* This utility is responsible for maintaining the basic state of the SmtEngine.
35		*
36		* It has no concept of anything related to the assertions of the SmtEngine,
37		* or more generally it does not depend on Node.
38		*
39		* This class has three sets of interfaces:
40		* (1) notification methods that are used by SmtEngine to notify when an event
41		* occurs (e.g. the beginning of a check-sat call),
42		* (2) maintaining the SAT and user contexts to be used by the SmtEngine,
43		* (3) general information queries, including the mode that the SmtEngine is
44		* in, based on the notifications it has received.
45		*
46		* It maintains a reference to the SmtEngine for the sake of making callbacks.
47		*/
48		class SmtEngineState
49		{
50		public:
51		SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt);
52	10484	~SmtEngineState() {}
53		/**
54		* Notify that the expected status of the next check-sat is given by the
55		* string status, which should be one of "sat", "unsat" or "unknown".
56		*/
57		void notifyExpectedStatus(const std::string& status);
58		/**
59		* Notify that the SmtEngine is fully initialized, which is called when
60		* options are finalized.
61		*/
62		void notifyFullyInited();
63		/**
64		* Notify that we are resetting the assertions, called when a reset-assertions
65		* command is issued by the user.
66		*/
67		void notifyResetAssertions();
68		/**
69		* Notify that we are about to call check-sat. This call is made prior to
70		* initializing the assertions. It processes pending pops and pushes a
71		* (user) context if necessary.
72		*
73		* @param hasAssumptions Whether the call to check-sat has assumptions. If
74		* so, we push a context.
75		*/
76		void notifyCheckSat(bool hasAssumptions);
77		/**
78		* Notify that the result of the last check-sat was r. This should be called
79		* once immediately following notifyCheckSat() if the check-sat call
80		* returned normal (i.e. it was not interupted).
81		*
82		* @param hasAssumptions Whether the prior call to check-sat had assumptions.
83		* If so, we pop a context.
84		* @param r The result of the check-sat call.
85		*/
86		void notifyCheckSatResult(bool hasAssumptions, Result r);
87		/**
88		* Notify that we finished an abduction query, where success is whether the
89		* command was successful. This is managed independently of the above
90		* calls for notifying check-sat. In other words, if a get-abduct command
91		* is issued to an SmtEngine, it may use a satisfiability call (if desired)
92		* to solve the abduction query. This method is called in addition to
93		* the above calls to notifyCheckSat / notifyCheckSatResult in this case.
94		* In particular, it is called after these two methods are completed.
95		* This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction
96		* was successful.
97		*/
98		void notifyGetAbduct(bool success);
99		/**
100		* Notify that we finished an interpolation query, where success is whether
101		* the command was successful. This is managed independently of the above
102		* calls for notifying check-sat. In other words, if a get-interpol command
103		* is issued to an SmtEngine, it may use a satisfiability call (if desired)
104		* to solve the interpolation query. This method is called in addition to
105		* the above calls to notifyCheckSat / notifyCheckSatResult in this case.
106		* In particular, it is called after these two methods are completed.
107		* This overwrites the SMT mode to the "INTERPOL" mode if the call to
108		* interpolation was successful.
109		*/
110		void notifyGetInterpol(bool success);
111		/**
112		* Setup the context, which makes a single push to maintain a global
113		* context around everything.
114		*/
115		void setup();
116		/**
117		* Set that we are in a fully initialized state.
118		*/
119		void finishInit();
120		/**
121		* Prepare for a shutdown of the SmtEngine, which does pending pops and
122		* pops the user context to zero.
123		*/
124		void shutdown();
125		/**
126		* Cleanup, which pops all contexts to level zero.
127		*/
128		void cleanup();
129		/**
130		* Set that the file name of the current instance is the given string. This
131		* is used for various purposes (e.g. get-info, SZS status).
132		*/
133		void setFilename(const std::string& filename);
134
135		//---------------------------- context management
136		/**
137		* Do all pending pops, which ensures that the context levels are up-to-date.
138		* This method should be called by the SmtEngine before using any of its
139		* members that rely on the context (e.g. PropEngine or TheoryEngine).
140		*/
141		void doPendingPops();
142		/**
143		* Called when the user of SmtEngine issues a push. This corresponds to
144		* the SMT-LIB command push.
145		*/
146		void userPush();
147		/**
148		* Called when the user of SmtEngine issues a pop. This corresponds to
149		* the SMT-LIB command pop.
150		*/
151		void userPop();
152		/** Get a pointer to the UserContext owned by this SmtEngine. */
153		context::UserContext* getUserContext();
154		/** Get a pointer to the Context owned by this SmtEngine. */
155		context::Context* getContext();
156		//---------------------------- end context management
157
158		//---------------------------- queries
159		/**
160		* Return true if the SmtEngine is fully initialized (post-construction).
161		* This post-construction initialization is automatically triggered by the
162		* use of the SmtEngine; e.g. when the first formula is asserted, a call
163		* to simplify() is issued, a scope is pushed, etc.
164		*/
165		bool isFullyInited() const;
166		/**
167		* Return true if the SmtEngine is fully initialized and there are no
168		* pending pops.
169		*/
170		bool isFullyReady() const;
171		/**
172		* Return true if a notifyCheckSat call has been made, e.g. a query has been
173		* issued to the SmtEngine.
174		*/
175		bool isQueryMade() const;
176		/** Return the user context level. */
177		size_t getNumUserLevels() const;
178		/** Get the status of the last check-sat */
179		Result getStatus() const;
180		/** Get the SMT mode we are in */
181		SmtMode getMode() const;
182		/** return the input name (if any) */
183		const std::string& getFilename() const;
184		//---------------------------- end queries
185
186		private:
187		/** Pushes the user and SAT contexts */
188		void push();
189		/** Pops the user and SAT contexts */
190		void pop();
191		/** Pops the user and SAT contexts to the given level */
192		void popto(int toLevel);
193		/**
194		* Internal push, which processes any pending pops, and pushes (if in
195		* incremental mode).
196		*/
197		void internalPush();
198		/**
199		* Internal pop. If immediate is true, this processes any pending pops, and
200		* pops (if in incremental mode). Otherwise, it increments the pending pop
201		* counter and does nothing.
202		*/
203		void internalPop(bool immediate = false);
204		/** Reference to the SmtEngine */
205		SmtEngine& d_smt;
206		/** Expr manager context */
207		context::Context* d_context;
208		/** User level context */
209		context::UserContext* d_userContext;
210		/** The context levels of user pushes */
211		std::vector<int> d_userLevels;
212
213		/**
214		* Number of internal pops that have been deferred.
215		*/
216		unsigned d_pendingPops;
217
218		/**
219		* Whether or not the SmtEngine is fully initialized (post-construction).
220		* This post-construction initialization is automatically triggered by the
221		* use of the SmtEngine which calls the finishInit method above; e.g. when
222		* the first formula is asserted, a call to simplify() is issued, a scope is
223		* pushed, etc.
224		*/
225		bool d_fullyInited;
226
227		/**
228		* Whether or not a notifyCheckSat call has been made, which corresponds to
229		* when a checkEntailed() or checkSatisfiability() has already been
230		* made through the SmtEngine. If true, and incrementalSolving is false,
231		* then attempting an additional checks for satisfiability will fail with
232		* a ModalException during notifyCheckSat.
233		*/
234		bool d_queryMade;
235
236		/**
237		* Internal status flag to indicate whether we have been issued a
238		* notifyCheckSat call and have yet to process the "postsolve" methods of
239		* SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost.
240		*/
241		bool d_needPostsolve;
242
243		/**
244		* Most recent result of last checkSatisfiability/checkEntailed in the
245		* SmtEngine.
246		*/
247		Result d_status;
248
249		/**
250		* The expected status of the next satisfiability check.
251		*/
252		Result d_expectedStatus;
253
254		/** The SMT mode, for details see enumeration above. */
255		SmtMode d_smtMode;
256
257		/**
258		* The input file name or the name set through (set-info :filename ...), if
259		* any.
260		*/
261		std::string d_filename;
262		};
263
264		} // namespace smt
265		} // namespace cvc5
266
267		#endif