summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/Makefile.am4
-rw-r--r--src/main/command_executor.cpp20
-rw-r--r--src/main/command_executor.h12
-rw-r--r--src/main/command_executor_portfolio.cpp25
-rw-r--r--src/main/driver_unified.cpp48
-rw-r--r--src/main/interactive_shell.cpp44
-rw-r--r--src/main/interactive_shell.h4
-rw-r--r--src/main/main.cpp19
-rw-r--r--src/main/main.h12
-rw-r--r--src/main/options63
-rw-r--r--src/main/options_handlers.h115
-rw-r--r--src/main/portfolio.cpp9
-rw-r--r--src/main/portfolio.h6
-rw-r--r--src/main/portfolio_util.cpp18
-rw-r--r--src/main/portfolio_util.h8
-rw-r--r--src/main/util.cpp13
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback