diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 4 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 20 | ||||
-rw-r--r-- | src/main/command_executor.h | 12 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 25 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 48 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 44 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 4 | ||||
-rw-r--r-- | src/main/main.cpp | 19 | ||||
-rw-r--r-- | src/main/main.h | 12 | ||||
-rw-r--r-- | src/main/options | 63 | ||||
-rw-r--r-- | src/main/options_handlers.h | 115 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 9 | ||||
-rw-r--r-- | src/main/portfolio.h | 6 | ||||
-rw-r--r-- | src/main/portfolio_util.cpp | 18 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 8 | ||||
-rw-r--r-- | src/main/util.cpp | 13 |
16 files changed, 122 insertions, 298 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 3ac0db7cb..478d3f3ee 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -30,7 +30,6 @@ pcvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ - @builddir@/../util/libstatistics.la \ $(READLINE_LIBS) if CVC4_NEEDS_REPLACEMENT_FUNCTIONS pcvc4_LDADD += \ @@ -55,7 +54,6 @@ cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ - @builddir@/../util/libstatistics.la \ $(READLINE_LIBS) if CVC4_NEEDS_REPLACEMENT_FUNCTIONS cvc4_LDADD += \ @@ -80,8 +78,6 @@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ -EXTRA_DIST = \ - options_handlers.h clean-local: rm -f $(BUILT_SOURCES) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 460274515..0b53c3cbe 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -12,22 +12,22 @@ ** \brief An additional layer between commands and invoking them. **/ -#include <iostream> -#include <string> - #include "main/command_executor.h" -#include "expr/command.h" - -#include "main/main.h" - -#include "main/options.h" -#include "smt/options.h" -#include "printer/options.h" #ifndef __WIN32__ # include <sys/resource.h> #endif /* ! __WIN32__ */ +#include <iostream> +#include <string> + +#include "main/main.h" +#include "options/main_options.h" +#include "options/printer_options.h" +#include "options/smt_options.h" +#include "smt_util/command.h" + + namespace CVC4 { namespace main { diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 9fe6347be..49d18a153 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -15,14 +15,14 @@ #ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H #define __CVC4__MAIN__COMMAND_EXECUTOR_H +#include <iostream> +#include <string> + #include "expr/expr_manager.h" -#include "smt/smt_engine.h" -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "options/options.h" -#include "expr/command.h" - -#include <string> -#include <iostream> +#include "smt/smt_engine.h" +#include "smt_util/command.h" namespace CVC4 { namespace main { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index f0d87cdf2..bb6487bf0 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -15,27 +15,28 @@ ** threads. **/ -#include <boost/thread.hpp> -#include <boost/thread/condition.hpp> +#include "main/command_executor_portfolio.h" + +#if HAVE_UNISTD_H +# include <unistd.h> +#endif /* HAVE_UNISTD_H */ + #include <boost/exception_ptr.hpp> #include <boost/lexical_cast.hpp> +#include <boost/thread.hpp> +#include <boost/thread/condition.hpp> #include <string> -#include "expr/command.h" +#include "cvc4autoconfig.h" #include "expr/pickler.h" -#include "main/command_executor_portfolio.h" #include "main/main.h" -#include "main/options.h" #include "main/portfolio.h" +#include "options/main_options.h" #include "options/options.h" -#include "smt/options.h" -#include "printer/options.h" - -#include "cvc4autoconfig.h" +#include "options/printer_options.h" +#include "options/smt_options.h" +#include "smt_util/command.h" -#if HAVE_UNISTD_H -# include <unistd.h> -#endif /* HAVE_UNISTD_H */ using namespace std; 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; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 3b237f6a4..da2813e24 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -14,31 +14,17 @@ ** This file is the implementation for the CVC4 interactive shell. ** The shell supports the readline library. **/ +#include "main/interactive_shell.h" -#include <iostream> +#include <algorithm> +#include <cassert> #include <cstdlib> -#include <vector> -#include <string> +#include <iostream> #include <set> -#include <algorithm> -#include <utility> - -#include "cvc4autoconfig.h" - -#include "main/interactive_shell.h" - -#include "expr/command.h" -#include "parser/input.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "options/options.h" -#include "smt/options.h" -#include "main/options.h" -#include "util/language.h" -#include "util/output.h" - #include <string.h> -#include <cassert> +#include <string> +#include <utility> +#include <vector> #if HAVE_LIBREADLINE # include <readline/readline.h> @@ -48,6 +34,19 @@ # endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBREADLINE */ + +#include "base/output.h" +#include "cvc4autoconfig.h" +#include "options/language.h" +#include "options/main_options.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "theory/logic_info.h" +#include "smt_util/command.h" + using namespace std; namespace CVC4 { @@ -99,7 +98,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); if(d_options.wasSetByUser(options::forceLogic)) { - d_parser->forceLogic(d_options[options::forceLogic].getLogicString()); + d_parser->forceLogic(d_options[options::forceLogic]->getLogicString()); } #if HAVE_LIBREADLINE @@ -401,4 +400,3 @@ char* commandGenerator(const char* text, int state) { #endif /* HAVE_LIBREADLINE */ }/* CVC4 namespace */ - diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index ef55919a1..1b1031776 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -18,9 +18,9 @@ #include <iostream> #include <string> -#include "util/language.h" -#include "util/unsafe_interrupt_exception.h" +#include "options/language.h" #include "options/options.h" +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { diff --git a/src/main/main.cpp b/src/main/main.cpp index 1c825bc35..36a339d94 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -13,30 +13,29 @@ ** ** Main driver for CVC4 executable. **/ +#include "main/main.h" #include <cstdlib> #include <cstring> #include <fstream> #include <iostream> - #include <stdio.h> #include <unistd.h> -#include "main/main.h" -#include "main/interactive_shell.h" +#include "base/output.h" +#include "expr/expr_manager.h" +#include "expr/result.h" +#include "expr/statistics.h" #include "main/command_executor.h" +#include "main/interactive_shell.h" +#include "options/language.h" +#include "options/main_options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" -#include "expr/expr_manager.h" #include "smt/smt_engine.h" -#include "expr/command.h" +#include "smt_util/command.h" #include "util/configuration.h" -#include "main/options.h" -#include "util/output.h" -#include "util/result.h" -#include "util/statistics.h" -#include "util/language.h" using namespace std; using namespace CVC4; diff --git a/src/main/main.h b/src/main/main.h index a2e813c6c..7dda429af 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -17,14 +17,14 @@ #include <exception> #include <string> -#include "options/options.h" +#include "base/exception.h" +#include "base/tls.h" +#include "cvc4autoconfig.h" #include "expr/expr_manager.h" +#include "expr/statistics.h" +#include "expr/statistics_registry.h" +#include "options/options.h" #include "smt/smt_engine.h" -#include "util/exception.h" -#include "util/statistics.h" -#include "util/tls.h" -#include "util/statistics_registry.h" -#include "cvc4autoconfig.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H diff --git a/src/main/options b/src/main/options deleted file mode 100644 index f523ea499..000000000 --- a/src/main/options +++ /dev/null @@ -1,63 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module DRIVER "main/options.h" Driver - -common-option version -V --version/ bool - identify this CVC4 binary -undocumented-alias --license = --version - -common-option help -h --help/ bool - full command line reference - -common-option - --show-config void :handler CVC4::main::showConfiguration :handler-include "main/options_handlers.h" - show CVC4 static configuration - -option - --show-debug-tags void :handler CVC4::main::showDebugTags :handler-include "main/options_handlers.h" - show all available tags for debugging -option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-include "main/options_handlers.h" - show all available tags for tracing - -expert-option earlyExit --early-exit bool :default true - do not run destructors at exit; default on except in debug builds - -# portfolio options -option threads --threads=N unsigned :default 2 :predicate options::greater(0) - Total number of threads for portfolio -option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h" - configures portfolio thread N (0..#threads-1) -option threadStackSize --thread-stack=N unsigned :default 0 - stack size for worker threads in MB (0 means use Boost/thread lib default) -option threadArgv std::vector<std::string> :include <vector> <string> - Thread configuration (a string to be passed to parseOptions) -option thread_id int :default -1 - Thread ID, for internal use in case of multi-threaded run -option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write - don't share (among portfolio threads) lemmas strictly longer than N -option fallbackSequential --fallback-sequential bool :default false - Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode -option incrementalParallel --incremental-parallel bool :default false :link --incremental - Use parallel solver even in incremental mode (may print 'unknown's at times) - -option interactive : --interactive bool :read-write - force interactive/non-interactive mode -undocumented-option interactivePrompt /--no-interactive-prompt bool :default true - turn off interactive prompting while in interactive mode - -# error behaviors (--immediate-exit is default in cases we support, thus no options) -option continuedExecution --continued-execution/ bool :default false :link "--interactive --no-interactive-prompt"/ - continue executing commands, even on error - -option segvSpin --segv-spin bool :default false - spin on segfault/other crash waiting for gdb -undocumented-alias --segv-nospin = --no-segv-spin - -expert-option tearDownIncremental : --tear-down-incremental bool :default false - implement PUSH/POP/multi-query by destroying and recreating SmtEngine - -expert-option waitToJoin --wait-to-join bool :default true - wait for other threads to join before quitting - -endmodule diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h deleted file mode 100644 index 00f192d2f..000000000 --- a/src/main/options_handlers.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Custom handlers and predicates for main driver options - ** - ** Custom handlers and predicates for main driver options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H -#define __CVC4__MAIN__OPTIONS_HANDLERS_H - -namespace CVC4 { -namespace main { - -inline void showConfiguration(std::string option, SmtEngine* smt) { - fputs(Configuration::about().c_str(), stdout); - printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); - if(Configuration::isGitBuild()) { - const char* branchName = Configuration::getGitBranchName(); - if(*branchName == '\0') { - branchName = "-"; - } - printf("scm : git [%s %s%s]\n", - branchName, - std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), - Configuration::hasGitModifications() ? - " (with modifications)" : ""); - } else if(Configuration::isSubversionBuild()) { - printf("scm : svn [%s r%u%s]\n", - Configuration::getSubversionBranchName(), - Configuration::getSubversionRevision(), - Configuration::hasSubversionModifications() ? - " (with modifications)" : ""); - } else { - printf("scm : no\n"); - } - printf("\n"); - printf("library : %u.%u.%u\n", - Configuration::getVersionMajor(), - Configuration::getVersionMinor(), - Configuration::getVersionRelease()); - printf("\n"); - printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); - printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); - printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); - printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); - printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); - printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); - printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); - printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); - printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); - printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); - printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); - printf("\n"); - printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); - printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); - printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); - printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); - printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); - printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); - printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); - exit(0); -} - -inline void showDebugTags(std::string option, SmtEngine* smt) { - if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - printf("available tags:"); - unsigned ntags = Configuration::getNumDebugTags(); - char const* const* tags = Configuration::getDebugTags(); - for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - } else if(! Configuration::isDebugBuild()) { - throw OptionException("debug tags not available in non-debug builds"); - } else { - throw OptionException("debug tags not available in non-tracing builds"); - } - exit(0); -} - -inline void showTraceTags(std::string option, SmtEngine* smt) { - if(Configuration::isTracingBuild()) { - printf("available tags:"); - unsigned ntags = Configuration::getNumTraceTags(); - char const* const* tags = Configuration::getTraceTags(); - for (unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - } else { - throw OptionException("trace tags not available in non-tracing build"); - } - exit(0); -} - -inline void threadN(std::string option, SmtEngine* smt) { - throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); -} - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */ diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 51b4779cc..884c3eda7 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -19,11 +19,12 @@ #include <boost/thread/condition.hpp> #include <boost/exception_ptr.hpp> -#include "smt/smt_engine.h" -#include "util/output.h" -#include "util/result.h" -#include "util/statistics_registry.h" +#include "base/output.h" +#include "expr/result.h" +#include "expr/statistics_registry.h" #include "options/options.h" +#include "smt/smt_engine.h" + namespace CVC4 { diff --git a/src/main/portfolio.h b/src/main/portfolio.h index f89c8f548..5a730c005 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -19,10 +19,10 @@ #include <boost/function.hpp> #include <utility> -#include "smt/smt_engine.h" -#include "expr/command.h" +#include "expr/statistics_registry.h" #include "options/options.h" -#include "util/statistics_registry.h" +#include "smt/smt_engine.h" +#include "smt_util/command.h" namespace CVC4 { diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index 7a4beb0d0..6b5fe4723 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -12,13 +12,16 @@ ** \brief Code relevant only for portfolio builds **/ +#include <unistd.h> + #include <cassert> #include <vector> -#include <unistd.h> + +#include "options/main_options.h" #include "options/options.h" -#include "main/options.h" -#include "prop/options.h" -#include "smt/options.h" +#include "options/prop_options.h" +#include "options/smt_options.h" +#include "smt/smt_options_handler.h" using namespace std; @@ -28,6 +31,9 @@ vector<Options> parseThreadSpecificOptions(Options opts) { vector<Options> threadOptions; +#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." + smt::SmtOptionsHandler optionsHandler(NULL); + unsigned numThreads = opts[options::threads]; for(unsigned i = 0; i < numThreads; ++i) { @@ -37,7 +43,7 @@ vector<Options> parseThreadSpecificOptions(Options opts) // Set thread identifier tOpts.set(options::thread_id, i); - if(i < opts[options::threadArgv].size() && + if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) { // separate out the thread's individual configuration string @@ -60,7 +66,7 @@ vector<Options> parseThreadSpecificOptions(Options opts) *vp++ = NULL; if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " try { - tOpts.parseOptions(targc, targv); + tOpts.parseOptions(targc, targv, &optionsHandler); } catch(OptionException& e) { stringstream ss; ss << optid << ": " << e.getMessage(); diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 8ae730506..d6d6a2d02 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -17,12 +17,12 @@ #include <queue> +#include "base/output.h" #include "expr/pickler.h" +#include "options/main_options.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" #include "util/channel.h" -#include "util/lemma_input_channel.h" -#include "util/lemma_output_channel.h" -#include "util/output.h" -#include "main/options.h" namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index f0cab25fa..86272ee53 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -28,15 +28,14 @@ #endif /* __WIN32__ */ -#include "util/exception.h" -#include "options/options.h" -#include "util/statistics.h" -#include "util/tls.h" -#include "smt/smt_engine.h" - +#include "base/exception.h" +#include "base/tls.h" #include "cvc4autoconfig.h" -#include "main/main.h" +#include "expr/statistics.h" #include "main/command_executor.h" +#include "main/main.h" +#include "options/options.h" +#include "smt/smt_engine.h" using CVC4::Exception; using namespace std; |