Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/smt_engine_state.h	Lines:	1	1	100.0 %
Date:	2021-09-19	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;
class Env;

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(Env& env, 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();

  //---------------------------- 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();
  //---------------------------- 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;
  //---------------------------- end queries

 private:
  /** get the sat context we are using */
  context::Context* getContext();
  /** get the user context we are using */
  context::UserContext* getUserContext();
  /** 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;
  /** Reference to the env of the parent SmtEngine */
  Env& d_env;
  /** 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;
};

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