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.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 92b0cd166..d7899020e 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -44,7 +44,7 @@ class CommandExecutor
SmtEngine* d_smtEngine;
Options& d_options;
StatisticsRegistry d_stats;
- Result d_result;
+ api::Result d_result;
public:
CommandExecutor(Options& options);
@@ -67,7 +67,7 @@ class CommandExecutor
/** Get a pointer to the solver object owned by this CommandExecutor. */
api::Solver* getSolver() { return d_solver.get(); }
- Result getResult() const { return d_result; }
+ api::Result getResult() const { return d_result; }
void reset();
StatisticsRegistry& getStatisticsRegistry() {
@@ -101,7 +101,7 @@ private:
}; /* class CommandExecutor */
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
+bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out);
}/* CVC4::main namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback