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 = \
doc/cvc4.1_template \
doc/cvc4.5 \
doc/libcvc4.3 \
+ doc/libcvc4.3_template \
doc/libcvc4compat.3 \
doc/libcvc4parser.3
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])
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
+++ /dev/null
-.\" 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/ .
--- /dev/null
+.\" 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 <iostream>
+#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/ .
progPath = argv[0];
// Parse the options
- int firstArgIndex = opts.parseOptions(argc, argv);
+ vector<string> 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();
#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)) {
}
// Auto-detect input language by filename extension
- const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+ const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
if( inputFromStdin ) {
# 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<std::string>
-#:includes <vector> <string>
+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
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 */
@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)))") \
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) {}
};/* class comparator */
struct greater : public comparator<std::greater> {
+ greater(int i) throw() : comparator<std::greater>(i) {}
greater(long l) throw() : comparator<std::greater>(l) {}
greater(double d) throw() : comparator<std::greater>(d) {}
};/* struct greater */
struct greater_equal : public comparator<std::greater_equal> {
+ greater_equal(int i) throw() : comparator<std::greater_equal>(i) {}
greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
};/* struct greater_equal */
struct less : public comparator<std::less> {
+ less(int i) throw() : comparator<std::less>(i) {}
less(long l) throw() : comparator<std::less>(l) {}
less(double d) throw() : comparator<std::less>(d) {}
};/* struct less */
struct less_equal : public comparator<std::less_equal> {
+ less_equal(int i) throw() : comparator<std::less_equal>(i) {}
less_equal(long l) throw() : comparator<std::less_equal>(l) {}
less_equal(double d) throw() : comparator<std::less_equal>(d) {}
};/* struct less_equal */
struct not_equal : public comparator<std::not_equal_to> {
+ not_equal(int i) throw() : comparator<std::not_equal_to>(i) {}
not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
};/* struct not_equal_to */
remaining_documentation=
common_manpage_documentation=
remaining_manpage_documentation=
+common_manpage_smt_documentation=
+remaining_manpage_smt_documentation=
seen_module=false
seen_endmodule=false
\"$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\"
"
}
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
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 \
#include <iostream>
#include <fstream>
#include <string>
+#include <vector>
#include "options/option_exception.h"
#include "util/language.h"
/**
* 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<std::string> parseOptions(int argc, char* argv[]) throw(OptionException);
/**
* Set the output language based on the given string.
}/* 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<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
options::OptionsGuard guard(&s_current, this);
const char *progName = main_argv[0];
int extra_optind = 0, main_optind = 0;
int old_optind;
+ int *optind_ref = &main_optind;
char** argv = main_argv;
+ std::vector<std::string> 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) {
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;
}
}
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
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<std::string>& 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) + "'");
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
}
out << ')';
}
-}/* Printer::toStream() */
+}/* Printer::toStream(SExpr) */
-void Printer::toStream(std::ostream& out, Model* m ) const throw(){
- for( int i=0; i<m->getNumCommands(); 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 */
#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"
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"
projects / cvc5.git / commitdiff