From: Morgan Deters Date: Fri, 14 Sep 2012 15:13:37 +0000 (+0000) Subject: Fix a few minor issues in options processing, improving usability, consistency, error... X-Git-Tag: cvc5-1.0.0~7813 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;ds=sidebyside;h=080fc73c61ca11a539fd5239146a828e86b9e29a;p=cvc5.git Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation. --- diff --git a/Makefile.am b/Makefile.am index c887b74b2..267e10bc2 100644 --- a/Makefile.am +++ b/Makefile.am @@ -106,7 +106,7 @@ EXTRA_DIST = \ config/doxygen.cfg \ doc/cvc4.1_template.in \ doc/cvc4.5.in \ - doc/libcvc4.3.in \ + doc/libcvc4.3_template.in \ doc/libcvc4parser.3.in \ doc/libcvc4compat.3.in man_MANS = \ @@ -133,5 +133,6 @@ DISTCLEANFILES = \ doc/cvc4.1_template \ doc/cvc4.5 \ doc/libcvc4.3 \ + doc/libcvc4.3_template \ doc/libcvc4compat.3 \ doc/libcvc4parser.3 diff --git a/configure.ac b/configure.ac index 1c14f8c6e..310cd4095 100644 --- a/configure.ac +++ b/configure.ac @@ -1113,7 +1113,7 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3]) diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in index 23eff6110..ad8226261 100644 --- a/doc/cvc4.1_template.in +++ b/doc/cvc4.1_template.in @@ -45,10 +45,15 @@ is unspecified and is connected to a terminal, interactive mode is assumed. .SH COMMON OPTIONS + +.IP "Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the option." + ${common_manpage_documentation} ${remaining_manpage_documentation} +.IP "Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the option." + .\".SH FILES .\".SH ENVIRONMENT .SH DIAGNOSTICS diff --git a/doc/libcvc4.3.in b/doc/libcvc4.3.in deleted file mode 100644 index 245db524e..000000000 --- a/doc/libcvc4.3.in +++ /dev/null @@ -1,15 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii libcvc4.3 -.\" -.TH LIBCVC4 3 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" -.SH NAME -libcvc4 \- a library interface for the CVC4 theorem prover -.SH DESCRIPTION -.SH "SEE ALSO" -.BR cvc4 (1), -.BR libcvc4parser (3), -.BR libcvc4compat (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://goedel.cs.nyu.edu/wiki/ . diff --git a/doc/libcvc4.3_template.in b/doc/libcvc4.3_template.in new file mode 100644 index 000000000..5483099c3 --- /dev/null +++ b/doc/libcvc4.3_template.in @@ -0,0 +1,80 @@ +.\" Process this file with +.\" groff -man -Tascii libcvc4.3 +.\" +.TH LIBCVC4 3 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" +.SH NAME +libcvc4 \- a library interface for the CVC4 theorem prover +.SH SYNOPSIS + +A small program like: + +.RS +.nf +#include +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" + +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + Expr onePlusTwo = em.mkExpr(kind::PLUS, + em.mkConst(Rational(1)), + em.mkConst(Rational(2))); + std::cout << Expr::setlanguage(language::output::LANG_CVC4) + << smt.getInfo("name") + << " says that 1 + 2 = " + << smt.simplify(onePlusTwo) + << std::endl; + + return 0; +} +.fi +.RE + +gives the output: + +.RS +"cvc4" says that 1 + 2 = 3 +.RE + +.SH DESCRIPTION + +The main classes of interest in CVC4's API are +.I ExprManager, +.I SmtEngine, +and a few related ones like +.I Expr +and +.I Type. + +The +.I ExprManager +is used to build up expressions and types, and the +.I SmtEngine +is used primarily to make assertions, check satisfiability/validity, and extract models and proofs. + +The SmtEngine is also in charge of setting and getting information and options. +.I SmtEngine::setOption() +and +.I SmtEngine::getOption() +use the following option keys. + +.RS +.TP 10 +.I "COMMON OPTIONS" +${common_manpage_smt_documentation} + +${remaining_manpage_smt_documentation} +.PD +.RE + +.SH "SEE ALSO" +.BR cvc4 (1), +.BR libcvc4parser (3), +.BR libcvc4compat (3) + +Additionally, the CVC4 wiki contains useful information about the +design and internals of CVC4. It is maintained at +.BR http://goedel.cs.nyu.edu/wiki/ . diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index f91f951c6..b89d43cc9 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -98,7 +98,14 @@ int runCvc4(int argc, char* argv[], Options& opts) { progPath = argv[0]; // Parse the options - int firstArgIndex = opts.parseOptions(argc, argv); + vector filenames = opts.parseOptions(argc, argv); + +# ifndef PORTFOLIO_BUILD + if( opts.wasSetByUser(options::threads) || + ! opts[options::threadArgv].empty() ) { + throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); + } +# endif progName = opts[options::binary_name].c_str(); @@ -121,13 +128,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { #endif /* CVC4_COMPETITION_MODE */ // We only accept one input file - if(argc > firstArgIndex + 1) { + if(filenames.size() > 1) { throw Exception("Too many input files specified."); } // If no file supplied we will read from standard input - const bool inputFromStdin = - firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; // if we're reading from stdin on a TTY, default to interactive mode if(!opts.wasSetByUser(options::interactive)) { @@ -157,7 +163,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // Auto-detect input language by filename extension - const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; + const char* filename = inputFromStdin ? "" : filenames[0].c_str(); if(opts[options::inputLanguage] == language::input::LANG_AUTO) { if( inputFromStdin ) { diff --git a/src/main/options b/src/main/options index 47e397d11..47d8da598 100644 --- a/src/main/options +++ b/src/main/options @@ -22,10 +22,11 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl # portfolio options option printWinner bool enable printing the winning thread (pcvc4 only) -option - --threadN=string void +option threads --threads=N unsigned :default 2 :predicate greater(0) + Total number of threads +option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h" configures thread N (0..#threads-1) -option threadArgv std::vector -#:includes +option threadArgv std::vector :include 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 diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index e607e13ce..7d5d35e08 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -94,6 +94,9 @@ inline void showTraceTags(std::string option, SmtEngine* smt) { 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 */ diff --git a/src/options/Makefile.am b/src/options/Makefile.am index f89fca922..1eb3fdac4 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -176,6 +176,7 @@ options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options @srcdir@/options_template.cpp @builddir@/options.cpp \ @srcdir@/../smt/smt_options_template.cpp @builddir@/../smt/smt_options.cpp \ @top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \ + @top_builddir@/doc/libcvc4.3_template @top_builddir@/doc/libcvc4.3 \ -t \ @srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \ $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(patsubst %/,%,$(dir $(o)))") \ diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index 6cb74c637..76ba9e295 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -127,6 +127,7 @@ class comparator { bool d_hasLbound; public: + comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {} @@ -142,26 +143,31 @@ public: };/* class comparator */ struct greater : public comparator { + greater(int i) throw() : comparator(i) {} greater(long l) throw() : comparator(l) {} greater(double d) throw() : comparator(d) {} };/* struct greater */ struct greater_equal : public comparator { + greater_equal(int i) throw() : comparator(i) {} greater_equal(long l) throw() : comparator(l) {} greater_equal(double d) throw() : comparator(d) {} };/* struct greater_equal */ struct less : public comparator { + less(int i) throw() : comparator(i) {} less(long l) throw() : comparator(l) {} less(double d) throw() : comparator(d) {} };/* struct less */ struct less_equal : public comparator { + less_equal(int i) throw() : comparator(i) {} less_equal(long l) throw() : comparator(l) {} less_equal(double d) throw() : comparator(d) {} };/* struct less_equal */ struct not_equal : public comparator { + not_equal(int i) throw() : comparator(i) {} not_equal(long l) throw() : comparator(l) {} not_equal(double d) throw() : comparator(d) {} };/* struct not_equal_to */ diff --git a/src/options/mkoptions b/src/options/mkoptions index 2c514293b..73a2b94a3 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -62,6 +62,8 @@ common_documentation= remaining_documentation= common_manpage_documentation= remaining_manpage_documentation= +common_manpage_smt_documentation= +remaining_manpage_smt_documentation= seen_module=false seen_endmodule=false @@ -121,6 +123,10 @@ function module { \"$module_name options:" remaining_manpage_documentation="${remaining_manpage_documentation} .SH `echo "$module_name" | tr a-z A-Z` OPTIONS +" + remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation} +.TP +.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\" " } @@ -831,73 +837,104 @@ function doc { return fi - if ! $options_already_documented; then - options_already_documented=true - the_opt= - if [ "$long_option" ]; then - the_opt="--$long_option" - if [ "$short_option" ]; then - shortoptarg= - if expr "$the_opt" : '.*=' &>/dev/null; then - shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')" - fi - the_opt="$the_opt | -$short_option$shortoptarg" + the_opt= + if [ "$long_option" ]; then + the_opt="--$long_option" + if [ "$short_option" ]; then + shortoptarg= + if expr "$the_opt" : '.*=' &>/dev/null; then + shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')" fi - elif [ "$short_option" ]; then - the_opt="-$short_option" - fi - if [ -z "$the_opt" ]; then - # nothing to document - return + the_opt="$the_opt | -$short_option$shortoptarg" fi + elif [ "$short_option" ]; then + the_opt="-$short_option" + elif [ -z "$smtname" ]; then + # nothing to document + return + fi + + if ! $options_already_documented; then + options_already_documented=true the_doc="$@" + mandoc="$@" + mansmtdoc="$@" if [ "$category" = EXPERT ]; then the_doc="$the_doc (EXPERTS only)" + mandoc="$mandoc (EXPERTS only)" + mansmtdoc="$mansmtdoc (EXPERTS only)" fi if [ "$type" = bool -a -n "$long_option" -a "$long_option_alternate" = "no-$long_option" ]; then the_doc="$the_doc [*]" + mandoc="$mandoc [*]" fi - doc_line= - while [ -n "$the_doc" ]; do - remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')" - the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')" - if [ -z "$doc_line" ]; then - if expr "$the_opt" : '.\{23\}' &>/dev/null; then - # break into two lines - doc_line="$(printf ' %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")" + if [ "$the_opt" ]; then + doc_line= + while [ -n "$the_doc" ]; do + remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')" + the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')" + if [ -z "$doc_line" ]; then + if expr "$the_opt" : '.\{23\}' &>/dev/null; then + # break into two lines + doc_line="$(printf ' %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")" + else + doc_line="$(printf ' %-22s %s' "$the_opt" "$the_doc")" + fi else - doc_line="$(printf ' %-22s %s' "$the_opt" "$the_doc")" + doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")" fi - else - doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")" - fi - the_doc="$(expr "$remaining_doc" : '\(.*\) ')" - done + the_doc="$(expr "$remaining_doc" : '\(.*\) ')" + done - if [ "$category" = COMMON ]; then - common_documentation="${common_documentation}\\n\" + if [ "$category" = COMMON ]; then + common_documentation="${common_documentation}\\n\" #line $lineno \"$kf\" \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" - common_manpage_documentation="${common_manpage_documentation} + common_manpage_documentation="${common_manpage_documentation} .IP \"$the_opt\" -$@" - else - remaining_documentation="${remaining_documentation}\\n\" +$mandoc" + else + remaining_documentation="${remaining_documentation}\\n\" #line $lineno \"$kf\" \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" - remaining_manpage_documentation="${remaining_manpage_documentation} + remaining_manpage_documentation="${remaining_manpage_documentation} .IP \"$the_opt\" -$@" +$mandoc" + fi + fi + + if [ "$smtname" ]; then + if [ "$category" = COMMON ]; then + common_manpage_smt_documentation="${common_manpage_smt_documentation} +.TP +.B \"$smtname\" +($type) $mansmtdoc" + else + remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation} +.TP +.B \"$smtname\" +($type) $mansmtdoc" + fi fi else - if [ "$category" = COMMON ]; then - common_manpage_documentation="${common_manpage_documentation} + if [ "$the_opt" ]; then + if [ "$category" = COMMON ]; then + common_manpage_documentation="${common_manpage_documentation} +$@" + else + remaining_manpage_documentation="${remaining_manpage_documentation} +$@" + fi + fi + + if [ "$smtname" ]; then + common_manpage_smt_documentation="${common_manpage_smt_documentation} $@" else - remaining_manpage_documentation="${remaining_manpage_documentation} + remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation} $@" fi fi @@ -1202,6 +1239,8 @@ for var in \ remaining_documentation \ common_manpage_documentation \ remaining_manpage_documentation \ + common_manpage_smt_documentation \ + remaining_manpage_smt_documentation \ smt_getoption_handlers \ smt_setoption_handlers \ long_option_value_begin \ diff --git a/src/options/options.h b/src/options/options.h index c966670f5..4f7e2a692 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -24,6 +24,7 @@ #include #include #include +#include #include "options/option_exception.h" #include "util/language.h" @@ -120,8 +121,10 @@ public: /** * Initialize the options based on the given command-line arguments. + * The return value is what's left of the command line (that is, the + * non-option arguments). */ - int parseOptions(int argc, char* argv[]) throw(OptionException); + std::vector parseOptions(int argc, char* argv[]) throw(OptionException); /** * Set the output language based on the given string. diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index ff863bf61..bae0ef169 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -343,8 +343,12 @@ public: }/* CVC4::options namespace */ -/** Parse argc/argv and put the result into a CVC4::Options. */ -int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { +/** + * Parse argc/argv and put the result into a CVC4::Options. + * The return value is what's left of the command line (that is, the + * non-option arguments). + */ +std::vector Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { options::OptionsGuard guard(&s_current, this); const char *progName = main_argv[0]; @@ -371,21 +375,29 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { int extra_optind = 0, main_optind = 0; int old_optind; + int *optind_ref = &main_optind; char** argv = main_argv; + std::vector nonOptions; + for(;;) { int c = -1; + optopt = 0; Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl; if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) { #if HAVE_DECL_OPTRESET optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this #endif /* HAVE_DECL_OPTRESET */ old_optind = optind = extra_optind; + optind_ref = &extra_optind; argv = extra_argv; Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl; + if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') { + InternalError("preempted args cannot give non-options command-line args (found `%s')", extra_argv[extra_optind == 0 ? 1 : extra_optind]); + } c = getopt_long(extra_argc, extra_argv, - ":${all_modules_short_options}", + "+:${all_modules_short_options}", cmdlineOptions, NULL); Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl; if(optind >= extra_argc) { @@ -407,12 +419,25 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this #endif /* HAVE_DECL_OPTRESET */ old_optind = optind = main_optind; + optind_ref = &main_optind; argv = main_argv; + if(main_optind < argc && main_argv[main_optind][0] != '-') { + do { + if(main_optind != 0) { + nonOptions.push_back(main_argv[main_optind]); + } + ++main_optind; + } while(main_optind < argc && main_argv[main_optind][0] != '-'); + continue; + } c = getopt_long(argc, main_argv, - ":${all_modules_short_options}", + "+:${all_modules_short_options}", cmdlineOptions, NULL); main_optind = optind; + Debug("options") << "[ next option will be at pos: " << optind << " ]" << std::endl; + if(optind < argc) Debug("options") << "next is option: " << argv[optind] << std::endl; if(c == -1) { + Debug("options") << "done with option parsing" << std::endl; break; } } @@ -422,7 +447,7 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { switch(c) { ${all_modules_option_handlers} -#line 426 "${template}" +#line 451 "${template}" case ':': // This can be a long or short option, and the way to get at the @@ -438,27 +463,45 @@ ${all_modules_option_handlers} case '?': default: - if(optopt == 0 && - !strncmp(argv[optind - 1], "--thread", 8) && - strlen(argv[optind - 1]) > 8 && - isdigit(argv[optind - 1][8])) { + if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 ) { + if(! isdigit(argv[optind - 1][8])) { + throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); + } std::vector& threadArgv = d_holder->threadArgv; - int tnum = atoi(argv[optind - 1] + 8); - threadArgv.resize(tnum + 1); + char *end; + long tnum = strtol(argv[optind - 1] + 8, &end, 10); + if(tnum < 0 || (*end != '\0' && *end != '=')) { + throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); + } + if(threadArgv.size() <= size_t(tnum)) { + threadArgv.resize(tnum + 1); + } if(threadArgv[tnum] != "") { threadArgv[tnum] += " "; } - const char* p = strchr(argv[optind - 1] + 9, '='); - if(p == NULL) { // e.g., we have --thread0 "foo" - threadArgv[tnum] += argv[optind++]; + if(*end == '\0') { // e.g., we have --thread0 "foo" + if(argc <= optind) { + throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); + } + Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl; + threadArgv[tnum] += argv[(*optind_ref)++]; } else { // e.g., we have --thread0="foo" - threadArgv[tnum] += p + 1; + if(end[1] == '\0') { + throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); + } + Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl; + threadArgv[tnum] += end + 1; } + Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] << std::endl; break; } // This can be a long or short option, and the way to get at the name of it is different. - if(optopt == 0) { // was a long option + if(optopt == 0 || + ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { + // was a long option throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'"); } else { // was a short option throw OptionException(std::string("can't understand option `-") + char(optopt) + "'"); @@ -470,7 +513,9 @@ ${all_modules_option_handlers} throw OptionException(std::string("The use of --incremental with --proof is not yet supported")); } - return optind; + Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl; + + return nonOptions; } #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 24baafa14..54482a8c3 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -125,12 +125,12 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { } out << ')'; } -}/* Printer::toStream() */ +}/* Printer::toStream(SExpr) */ -void Printer::toStream(std::ostream& out, Model* m ) const throw(){ - for( int i=0; igetNumCommands(); i++ ){ - toStream( out, m, m->getCommand( i ), m->getCommandType( i ) ); +void Printer::toStream(std::ostream& out, Model* m) const throw() { + for(size_t i = 0; i < m->getNumCommands(); i++ ){ + toStream(out, m, m->getCommand(i), m->getCommandType(i)); } -} +}/* Printer::toStream(Model) */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index a82e1b735..d9f3f798a 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -29,6 +29,7 @@ #include "util/Assert.h" #include "options/options.h" #include "smt/options.h" +#include "main/options.h" #include "util/output.h" #include "util/result.h" #include "expr/expr.h" diff --git a/src/smt/options b/src/smt/options index 81891acf7..508c03a66 100644 --- a/src/smt/options +++ b/src/smt/options @@ -80,8 +80,6 @@ option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplay option replayStream ExprStream* # portfolio options -option threads --threads=N unsigned :default 2 - Total number of threads option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h" The input channel to receive notfication events for new lemmas option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"