diff options
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 48 |
1 files changed, 25 insertions, 23 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c29ba55a4..df78df0f3 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -13,39 +13,38 @@ ** sequential and portfolio versions **/ +#include <stdio.h> +#include <unistd.h> + #include <cstdlib> #include <cstring> #include <fstream> #include <iostream> #include <new> -#include <unistd.h> - -#include <stdio.h> -#include <unistd.h> +#include "base/output.h" #include "cvc4autoconfig.h" -#include "main/main.h" -#include "main/interactive_shell.h" -#include "main/options.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "parser/parser_exception.h" #include "expr/expr_manager.h" -#include "expr/command.h" -#include "util/configuration.h" -#include "options/options.h" -#include "theory/quantifiers/options.h" +#include "expr/result.h" +#include "expr/statistics_registry.h" #include "main/command_executor.h" #ifdef PORTFOLIO_BUILD # include "main/command_executor_portfolio.h" #endif -#include "main/options.h" -#include "smt/options.h" -#include "util/output.h" -#include "util/result.h" -#include "util/statistics_registry.h" +#include "main/interactive_shell.h" +#include "main/main.h" +#include "options/main_options.h" +#include "options/options.h" +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_exception.h" +#include "smt/smt_options_handler.h" +#include "smt_util/command.h" +#include "util/configuration.h" using namespace std; using namespace CVC4; @@ -130,8 +129,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { progPath = argv[0]; +#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." + smt::SmtOptionsHandler optionsHandler(NULL); + // Parse the options - vector<string> filenames = opts.parseOptions(argc, argv); + vector<string> filenames = opts.parseOptions(argc, argv, &optionsHandler); # ifndef PORTFOLIO_BUILD if( opts.wasSetByUser(options::threads) || @@ -302,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #ifndef PORTFOLIO_BUILD if(!opts.wasSetByUser(options::incrementalSolving)) { - cmd = new SetOptionCommand("incremental", true); + cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; @@ -349,7 +351,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { throw OptionException("--tear-down-incremental incompatible with --incremental"); } - cmd = new SetOptionCommand("incremental", false); + cmd = new SetOptionCommand("incremental", SExpr(false)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; @@ -488,7 +490,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete parser; } else { if(!opts.wasSetByUser(options::incrementalSolving)) { - cmd = new SetOptionCommand("incremental", false); + cmd = new SetOptionCommand("incremental", SExpr(false)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; |