From a486cdde94366aa6b4a1f558eecc0130ba25ad5e Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Fri, 22 Oct 2010 22:50:33 +0000 Subject: [PATCH] Merging main/getopt.cpp, main/usage.h, and smt/options.h in util/options.h,cpp --- src/main/Makefile.am | 1 - src/main/main.cpp | 91 ++++++++---- src/main/main.h | 21 +-- src/main/util.cpp | 4 +- src/prop/prop_engine.cpp | 4 +- src/prop/prop_engine.h | 4 +- src/prop/sat.h | 4 +- src/smt/smt_engine.cpp | 20 +-- src/smt/smt_engine.h | 20 +-- src/theory/theory_engine.cpp | 8 +- src/theory/theory_engine.h | 2 +- src/util/Makefile.am | 2 + src/{main/getopt.cpp => util/options.cpp} | 138 ++++++++++++------- src/{smt => util}/options.h | 51 ++++++- test/unit/prop/cnf_stream_black.h | 1 - test/unit/theory/shared_term_manager_black.h | 6 +- test/unit/theory/theory_engine_white.h | 6 +- 17 files changed, 243 insertions(+), 140 deletions(-) rename src/{main/getopt.cpp => util/options.cpp} (74%) rename src/{smt => util}/options.h (74%) diff --git a/src/main/Makefile.am b/src/main/Makefile.am index b6cdbb1f4..05a451d52 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -6,7 +6,6 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas bin_PROGRAMS = cvc4 cvc4_SOURCES = \ - getopt.cpp \ interactive_shell.h \ interactive_shell.cpp \ main.h \ diff --git a/src/main/main.cpp b/src/main/main.cpp index 8ed938351..544c6fd29 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -28,7 +28,6 @@ #include "cvc4autoconfig.h" #include "main.h" #include "interactive_shell.h" -#include "usage.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -37,8 +36,8 @@ #include "expr/command.h" #include "util/Assert.h" #include "util/configuration.h" +#include "util/options.h" #include "util/output.h" -#include "smt/options.h" #include "util/result.h" #include "util/stats.h" @@ -47,14 +46,41 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -namespace CVC4 { - namespace main { - struct Options options; - }/* CVC4::main namespace */ -}/* CVC4 namespace */ - int runCvc4(int argc, char* argv[]); void doCommand(SmtEngine&, Command*); +void printUsage(); + +namespace CVC4 { + namespace main {/* Global options variable */ + Options options; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + } +} + + +// no more % chars in here without being escaped; it's used as a +// printf() format string +const string usageMessage = "\ +usage: %s [options] [input-file]\n\ +\n\ +Without an input file, or with `-', CVC4 reads from standard input.\n\ +\n\ +CVC4 options:\n"; + +void printUsage() { + stringstream ss; + ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', CVC4 reads from standard input." << endl + << endl + << "CVC4 options:" << endl; + Options::printUsage( ss.str(), options.out ); +} /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. @@ -68,34 +94,34 @@ int main(int argc, char* argv[]) { return runCvc4(argc, argv); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; - printf(usage, options.binary_name.c_str()); + printUsage(); exit(1); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 Error:" << endl << e << endl; + options.err << "CVC4 Error:" << endl << e << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } exit(1); } catch(bad_alloc) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 ran out of memory." << endl; + options.err << "CVC4 ran out of memory." << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } exit(1); } catch(...) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 threw an exception of unknown type." << endl; + options.err << "CVC4 threw an exception of unknown type." << endl; exit(1); } } @@ -106,12 +132,29 @@ int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers cvc4_init(); + progPath = argv[0]; + // Parse the options - int firstArgIndex = parseOptions(argc, argv, &options); + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(options.out); + exit(1); + } else if( options.version ) { + options.out << Configuration::about().c_str() << flush; + exit(0); + } + + segvNoSpin = options.segvNoSpin; // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE - cout << unitbuf; + options.out << unitbuf; #endif // We only accept one input file @@ -201,7 +244,7 @@ int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; if( options.interactive ) { - InteractiveShell shell(cin,cout,parserBuilder); + InteractiveShell shell(options.in,options.out,parserBuilder); while((cmd = shell.readCommand())) { doCommand(smt,cmd); delete cmd; @@ -237,7 +280,7 @@ int runCvc4(int argc, char* argv[]) { StatisticsRegistry::registerStat(&s_statSatResult); if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } StatisticsRegistry::unregisterStat(&s_statSatResult); @@ -261,11 +304,11 @@ void doCommand(SmtEngine& smt, Command* cmd) { } } else { if(options.verbosity > 0) { - cout << "Invoking: " << *cmd << endl; + options.out << "Invoking: " << *cmd << endl; } if(options.verbosity >= 0) { - cmd->invoke(&smt, cout); + cmd->invoke(&smt, options.out); } else { cmd->invoke(&smt); } diff --git a/src/main/main.h b/src/main/main.h index 350578ffa..b6a8bcfb1 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -19,26 +19,16 @@ #include #include +#include "util/options.h" #include "cvc4autoconfig.h" -#include "util/exception.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H namespace CVC4 { -struct Options; - namespace main { -/** Class representing an option-parsing exception. */ -class OptionException : public CVC4::Exception { -public: - OptionException(const std::string& s) throw() : - CVC4::Exception("Error in option parsing: " + s) { - } -};/* class OptionException */ - /** Full argv[0] */ extern const char *progPath; @@ -52,14 +42,7 @@ extern const char *progName; */ extern bool segvNoSpin; -/** - * Keep a copy of the options around globally, so that signal handlers can - * access it. - */ -extern struct Options options; - -/** Parse argc/argv and put the result into a CVC4::Options struct. */ -int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); +extern Options options; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(); diff --git a/src/main/util.cpp b/src/main/util.cpp index 70cb85c93..4ec1c1bee 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -23,9 +23,9 @@ #include #include -#include "util/exception.h" -#include "smt/options.h" #include "util/Assert.h" +#include "util/exception.h" +#include "util/options.h" #include "util/stats.h" #include "cvc4autoconfig.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f503efae2..5851f3990 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -21,10 +21,10 @@ #include "sat.h" #include "theory/theory_engine.h" -#include "util/decision_engine.h" #include "util/Assert.h" +#include "util/decision_engine.h" +#include "util/options.h" #include "util/output.h" -#include "smt/options.h" #include "util/result.h" #include diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1c7c506ee..ecef29ac2 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,9 +24,9 @@ #define __CVC4__PROP_ENGINE_H #include "expr/node.h" -#include "util/result.h" #include "util/decision_engine.h" -#include "smt/options.h" +#include "util/options.h" +#include "util/result.h" namespace CVC4 { diff --git a/src/prop/sat.h b/src/prop/sat.h index 17bf447f8..550de5527 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -25,9 +25,9 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT -#include "util/stats.h" #include "theory/theory.h" -#include "smt/options.h" +#include "util/options.h" +#include "util/stats.h" #ifdef __CVC4_USE_MINISAT diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 149c3620d..81930a5ea 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -20,22 +20,22 @@ #include #include -#include "smt/smt_engine.h" -#include "smt/modal_exception.h" -#include "smt/bad_option_exception.h" -#include "smt/no_such_function_exception.h" -#include "context/context.h" #include "context/cdlist.h" #include "context/cdset.h" -#include "expr/expr.h" +#include "context/context.h" #include "expr/command.h" +#include "expr/expr.h" #include "expr/node_builder.h" -#include "util/output.h" -#include "util/exception.h" -#include "smt/options.h" -#include "util/configuration.h" #include "prop/prop_engine.h" +#include "smt/bad_option_exception.h" +#include "smt/modal_exception.h" +#include "smt/no_such_function_exception.h" +#include "smt/smt_engine.h" #include "theory/theory_engine.h" +#include "util/configuration.h" +#include "util/exception.h" +#include "util/options.h" +#include "util/output.h" using namespace std; using namespace CVC4; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0831a0447..35bfb0bcc 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -23,19 +23,19 @@ #include -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "context/cdlist_forward.h" #include "context/cdmap_forward.h" #include "context/cdset_forward.h" -#include "context/cdlist_forward.h" -#include "util/result.h" -#include "util/model.h" -#include "util/sexpr.h" -#include "util/hash.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "smt/bad_option_exception.h" #include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" -#include "smt/options.h" -#include "smt/bad_option_exception.h" +#include "util/hash.h" +#include "util/model.h" +#include "util/options.h" +#include "util/result.h" +#include "util/sexpr.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -47,7 +47,7 @@ template class NodeTemplate; typedef NodeTemplate Node; typedef NodeTemplate TNode; class NodeHashFunction; -class Command; + class TheoryEngine; class DecisionEngine; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2fcfc9626..40debc7c7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -19,13 +19,13 @@ #include #include -#include "theory/theory_engine.h" -#include "expr/node.h" #include "expr/attribute.h" -#include "theory/theory.h" +#include "expr/node.h" #include "expr/node_builder.h" -#include "smt/options.h" +#include "util/options.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0bca372ca..7e08a29d5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -23,10 +23,10 @@ #include "expr/node.h" #include "prop/prop_engine.h" -#include "smt/options.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/theoryof_table.h" +#include "util/options.h" #include "util/stats.h" namespace CVC4 { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 61c0bf885..e75735f82 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -18,6 +18,8 @@ libutil_la_SOURCES = \ hash.h \ bool.h \ model.h \ + options.h \ + options.cpp \ output.cpp \ output.h \ result.h \ diff --git a/src/main/getopt.cpp b/src/util/options.cpp similarity index 74% rename from src/main/getopt.cpp rename to src/util/options.cpp index 25badb7e5..f6d3c3092 100644 --- a/src/main/getopt.cpp +++ b/src/util/options.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file getopt.cpp +/*! \file options.cpp ** \verbatim ** Original author: mdeters ** Major contributors: cconway @@ -26,24 +26,48 @@ #include -#include "util/exception.h" +#include "expr/expr.h" #include "util/configuration.h" -#include "util/output.h" -#include "smt/options.h" +#include "util/exception.h" #include "util/language.h" -#include "expr/expr.h" +#include "util/options.h" +#include "util/output.h" #include "cvc4autoconfig.h" -#include "main.h" -#include "usage.h" using namespace std; using namespace CVC4; namespace CVC4 { -namespace main { -static const char lang_help[] = "\ +static const string optionsDescription = "\ + --lang | -L force input language (default is `auto'; see --lang help)\n\ + --version | -V identify this CVC4 binary\n\ + --help | -h this command line reference\n\ + --parse-only exit after parsing input\n\ + --mmap memory map file input\n\ + --show-config show CVC4 static configuration\n\ + --segv-nospin don't spin on segfault waiting for gdb\n\ + --lazy-type-checking type check expressions only when necessary (default)\n\ + --eager-type-checking type check expressions immediately on creation\n\ + --no-type-checking never type check expressions\n\ + --no-checking disable ALL semantic checks, including type checks \n\ + --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ + --verbose | -v increase verbosity (repeatable)\n\ + --quiet | -q decrease verbosity (repeatable)\n\ + --trace | -t tracing for something (e.g. --trace pushpop)\n\ + --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ + --stats give statistics on exit\n\ + --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ + --print-expr-types print types with variables when printing exprs\n\ + --uf=morgan|tim select uninterpreted function theory implementation\n\ + --interactive run interactively\n\ + --no-interactive do not run interactively\n\ + --produce-models support the get-value command\n\ + --produce-assignments support the get-assignment command\n\ + --lazy-definition-expansion expand define-fun lazily\n"; + +static const string languageDescription = "\ Languages currently supported as arguments to the -L / --lang option:\n\ auto attempt to automatically determine the input language\n\ pl | cvc4 CVC4 presentation language\n\ @@ -51,6 +75,20 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2 | smtlib2 SMT-LIB format 2.0\n\ "; +string Options::getDescription() const { + return optionsDescription; +} + +void Options::printUsage(const string msg, std::ostream& out) { + out << msg << optionsDescription << endl << flush; + // printf(usage + options.getDescription(), options.binary_name.c_str()); + // printf(usage, binary_name.c_str()); +} + +void Options::printLanguageHelp(std::ostream& out) { + out << languageDescription << flush; +} + /** * For the main getopt() routine, we need ways to switch on long * options without clashing with short option characters. This is an @@ -136,16 +174,11 @@ static struct option cmdlineOptions[] = { { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ -/** Full argv[0] */ -const char *progPath; - -/** Just the basename component of argv[0] */ -const char *progName; /** Parse argc/argv and put the result into a CVC4::Options struct. */ -int parseOptions(int argc, char* argv[], CVC4::Options* opts) +int Options::parseOptions(int argc, char* argv[]) throw(OptionException) { - progPath = progName = argv[0]; + const char *progName = argv[0]; int c; // find the base name of the program @@ -153,7 +186,7 @@ throw(OptionException) { if(x != NULL) { progName = x + 1; } - opts->binary_name = string(progName); + binary_name = string(progName); // The strange string in this call is the short option string. The // initial '+' means that option processing stops as soon as a @@ -172,33 +205,37 @@ throw(OptionException) { switch(c) { case 'h': - printf(usage, opts->binary_name.c_str()); - exit(1); + help = true; + break; + // options.printUsage(usage); + // exit(1); case 'V': - fputs(Configuration::about().c_str(), stdout); - exit(0); + version = true; + break; + // fputs(Configuration::about().c_str(), stdout); + // exit(0); case 'v': - ++opts->verbosity; + ++verbosity; break; case 'q': - --opts->verbosity; + --verbosity; break; case 'L': if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { - opts->inputLanguage = language::input::LANG_CVC4; + inputLanguage = language::input::LANG_CVC4; break; } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { - opts->inputLanguage = language::input::LANG_SMTLIB; + inputLanguage = language::input::LANG_SMTLIB; break; } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) { - opts->inputLanguage = language::input::LANG_SMTLIB_V2; + inputLanguage = language::input::LANG_SMTLIB_V2; break; } else if(!strcmp(optarg, "auto")) { - opts->inputLanguage = language::input::LANG_AUTO; + inputLanguage = language::input::LANG_AUTO; break; } @@ -207,8 +244,8 @@ throw(OptionException) { optarg + "'. Try --lang help."); } - fputs(lang_help, stdout); - exit(1); + languageHelp = true; + break; case 't': Trace.on(optarg); @@ -220,7 +257,7 @@ throw(OptionException) { break; case STATS: - opts->statistics = true; + statistics = true; break; case SEGV_NOSPIN: @@ -228,21 +265,21 @@ throw(OptionException) { break; case PARSE_ONLY: - opts->parseOnly = true; + parseOnly = true; break; case NO_CHECKING: - opts->semanticChecks = false; - opts->typeChecking = false; - opts->earlyTypeChecking = false; + semanticChecks = false; + typeChecking = false; + earlyTypeChecking = false; break; case USE_MMAP: - opts->memoryMap = true; + memoryMap = true; break; case STRICT_PARSING: - opts->strictParsing = true; + strictParsing = true; break; case DEFAULT_EXPR_DEPTH: @@ -271,9 +308,9 @@ throw(OptionException) { case UF_THEORY: { if(!strcmp(optarg, "tim")) { - opts->uf_implementation = Options::TIM; + uf_implementation = Options::TIM; } else if(!strcmp(optarg, "morgan")) { - opts->uf_implementation = Options::MORGAN; + uf_implementation = Options::MORGAN; } else if(!strcmp(optarg, "help")) { printf("UF implementations available:\n"); printf("tim\n"); @@ -287,39 +324,39 @@ throw(OptionException) { break; case LAZY_DEFINITION_EXPANSION: - opts->lazyDefinitionExpansion = true; + lazyDefinitionExpansion = true; break; case INTERACTIVE: - opts->interactive = true; - opts->interactiveSetByUser = true; + interactive = true; + interactiveSetByUser = true; break; case NO_INTERACTIVE: - opts->interactive = false; - opts->interactiveSetByUser = true; + interactive = false; + interactiveSetByUser = true; break; case PRODUCE_MODELS: - opts->produceModels = true; + produceModels = true; break; case PRODUCE_ASSIGNMENTS: - opts->produceAssignments = true; + produceAssignments = true; break; case NO_TYPE_CHECKING: - opts->typeChecking = false; - opts->earlyTypeChecking = false; + typeChecking = false; + earlyTypeChecking = false; break; case LAZY_TYPE_CHECKING: - opts->earlyTypeChecking = false; + earlyTypeChecking = false; break; case EAGER_TYPE_CHECKING: - opts->typeChecking = true; - opts->earlyTypeChecking = true; + typeChecking = true; + earlyTypeChecking = true; break; case SHOW_CONFIG: @@ -356,5 +393,4 @@ throw(OptionException) { return optind; } -}/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/smt/options.h b/src/util/options.h similarity index 74% rename from src/smt/options.h rename to src/util/options.h index 73c38545f..b56741fba 100644 --- a/src/smt/options.h +++ b/src/util/options.h @@ -30,18 +30,28 @@ #include #include -#include "util/language.h" +#include "exception.h" +#include "language.h" namespace CVC4 { +/** Class representing an option-parsing exception. */ +class OptionException : public CVC4::Exception { +public: + OptionException(const std::string& s) throw() : + CVC4::Exception("Error in option parsing: " + s) { + } +};/* class OptionException */ + struct CVC4_PUBLIC Options { std::string binary_name; bool statistics; - std::ostream *out; - std::ostream *err; + std::istream& in; + std::ostream& out; + std::ostream& err; /* -1 means no output */ /* 0 is normal (and default) -- warnings only */ @@ -59,6 +69,15 @@ struct CVC4_PUBLIC Options { /** Which implementation of uninterpreted function theory to use */ UfImplementation uf_implementation; + /** Should we print the help message? */ + bool help; + + /** Should we print the release information? */ + bool version; + + /** Should we print the language help information? */ + bool languageHelp; + /** Should we exit after parsing? */ bool parseOnly; @@ -83,6 +102,9 @@ struct CVC4_PUBLIC Options { */ bool interactiveSetByUser; + /** Whether we should "spin" on a SIG_SEGV. */ + bool segvNoSpin; + /** Whether we support SmtEngine::getValue() for this run. */ bool produceModels; @@ -98,8 +120,9 @@ struct CVC4_PUBLIC Options { Options() : binary_name(), statistics(false), - out(0), - err(0), + in(std::cin), + out(std::cout), + err(std::cerr), verbosity(0), inputLanguage(language::input::LANG_AUTO), uf_implementation(MORGAN), @@ -110,11 +133,27 @@ struct CVC4_PUBLIC Options { lazyDefinitionExpansion(false), interactive(false), interactiveSetByUser(false), + segvNoSpin(false), produceModels(false), produceAssignments(false), typeChecking(true), earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { } + + /** + * Get a description of the command-line flags accepted by + * parseOptions. The returned string will be escaped so that it is + * suitable as an argument to printf. */ + std::string getDescription() const; + + static void printUsage(const std::string msg, std::ostream& out); + static void printLanguageHelp(std::ostream& out); + + /** + * Initialize the options based on the given command-line arguments. + */ + int parseOptions(int argc, char* argv[]) + throw(OptionException); };/* struct Options */ inline std::ostream& operator<<(std::ostream& out, @@ -133,6 +172,8 @@ inline std::ostream& operator<<(std::ostream& out, return out; } + + }/* CVC4 namespace */ #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index b340beb50..cee8a6a64 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -30,7 +30,6 @@ #include "prop/prop_engine.h" #include "prop/sat.h" #include "smt/smt_engine.h" -#include "smt/options.h" #include "util/decision_engine.h" using namespace CVC4; diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 5007f43ed..7340f6ae7 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -31,7 +31,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" -#include "smt/options.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -51,7 +51,6 @@ class SharedTermManagerBlack : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; TheoryEngine* d_theoryEngine; - Options d_options; public: @@ -61,7 +60,8 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_theoryEngine = new TheoryEngine(d_ctxt, d_options); + Options options; + d_theoryEngine = new TheoryEngine(d_ctxt, options); } void tearDown() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 00766ec90..bd6ec515b 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -35,7 +35,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" -#include "smt/options.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -227,7 +227,6 @@ class TheoryEngineWhite : public CxxTest::TestSuite { FakeOutputChannel *d_nullChannel; FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv; TheoryEngine* d_theoryEngine; - Options d_options; public: @@ -248,7 +247,8 @@ public: d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV"); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt, d_options); + Options options; + d_theoryEngine = new TheoryEngine(d_ctxt, options); // insert our fake versions into the TheoryEngine's theoryOf table d_theoryEngine->d_theoryOfTable. -- 2.30.2