Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/solver_engine_state.h	Lines:	1	1	100.0 %
Date:	2021-11-07	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/env_obj.h"
#include "smt/smt_mode.h"
#include "util/result.h"

namespace cvc5 {

class SolverEngine;

namespace smt {

/**
 * This utility is responsible for maintaining the basic state of the
 * SolverEngine.
 *
 * It has no concept of anything related to the assertions of the SolverEngine,
 * or more generally it does not depend on Node.
 *
 * This class has three sets of interfaces:
 * (1) notification methods that are used by SolverEngine 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 SolverEngine, (3) general information
 * queries, including the mode that the SolverEngine is in, based on the
 * notifications it has received.
 *
 * It maintains a reference to the SolverEngine for the sake of making
 * callbacks.
 */
class SolverEngineState : protected EnvObj
{
 public:
  SolverEngineState(Env& env, SolverEngine& smt);
  ~SolverEngineState() {}
  /**
   * 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 SolverEngine 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 SolverEngine, 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 SolverEngine, 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 SolverEngine, 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 SolverEngine before using any of its
   * members that rely on the context (e.g. PropEngine or TheoryEngine).
   */
  void doPendingPops();
  /**
   * Called when the user of SolverEngine issues a push. This corresponds to
   * the SMT-LIB command push.
   */
  void userPush();
  /**
   * Called when the user of SolverEngine issues a pop. This corresponds to
   * the SMT-LIB command pop.
   */
  void userPop();
  //---------------------------- end context management

  //---------------------------- queries
  /**
   * Return true if the SolverEngine is fully initialized (post-construction).
   * This post-construction initialization is automatically triggered by the
   * use of the SolverEngine; 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 SolverEngine 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 SolverEngine.
   */
  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:
  /** 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 SolverEngine */
  SolverEngine& d_slv;
  /** 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 SolverEngine is fully initialized (post-construction).
   * This post-construction initialization is automatically triggered by the
   * use of the SolverEngine 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 SolverEngine.  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
   * SolverEngine via SolverEngine::notifyPostSolvePre/notifyPostSolvePost.
   */
  bool d_needPostsolve;

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