summaryrefslogtreecommitdiff
path: root/src/main/command_executor.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/command_executor.h')
-rw-r--r--src/main/command_executor.h9
1 files changed, 7 insertions, 2 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index ff7b89928..e8c2d25ac 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -40,7 +40,7 @@ class CommandExecutor
* The solver object, which is allocated by this class and is used for
* executing most commands (e.g. check-sat).
*/
- std::unique_ptr<api::Solver> d_solver;
+ std::unique_ptr<api::Solver>& d_solver;
/**
* The symbol manager, which is allocated by this class. This manages
* all things related to definitions of symbols and their impact on behaviors
@@ -56,7 +56,7 @@ class CommandExecutor
api::Result d_result;
public:
- CommandExecutor(const Options& options);
+ CommandExecutor(std::unique_ptr<api::Solver>& solver);
virtual ~CommandExecutor();
@@ -83,6 +83,11 @@ class CommandExecutor
SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); }
+ /** Get the current options from the solver */
+ Options& getOptions();
+ /** Store the current options as the original options */
+ void storeOptionsAsOriginal();
+
/**
* Prints statistics to an output stream.
* Checks whether statistics should be printed according to the options.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback