summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/Makefile.am3
-rw-r--r--src/main/driver.cpp144
-rw-r--r--src/main/driver_portfolio.cpp262
-rw-r--r--src/main/interactive_shell.cpp18
-rw-r--r--src/main/interactive_shell.h1
-rw-r--r--src/main/main.cpp19
-rw-r--r--src/main/main.h2
-rw-r--r--src/main/options38
-rw-r--r--src/main/options_handlers.h101
-rw-r--r--src/main/portfolio.cpp2
-rw-r--r--src/main/portfolio.h2
-rw-r--r--src/main/util.cpp22
12 files changed, 387 insertions, 227 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 594751358..730afa32d 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -65,6 +65,9 @@ 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/driver.cpp b/src/main/driver.cpp
index f24526e6c..ca5dfad93 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -36,7 +36,10 @@
#include "expr/command.h"
#include "util/Assert.h"
#include "util/configuration.h"
-#include "util/options.h"
+#include "options/options.h"
+#include "main/options.h"
+#include "smt/options.h"
+#include "theory/uf/options.h"
#include "util/output.h"
#include "util/dump.h"
#include "util/result.h"
@@ -66,28 +69,28 @@ namespace CVC4 {
}
-void printUsage(Options& options, bool full) {
+void printUsage(Options& opts, bool full) {
stringstream ss;
- ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
+ ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
<< endl
<< "Without an input file, or with `-', CVC4 reads from standard input." << endl
<< endl
<< "CVC4 options:" << endl;
if(full) {
- Options::printUsage( ss.str(), *options.out );
+ Options::printUsage( ss.str(), *opts[options::out] );
} else {
- Options::printShortUsage( ss.str(), *options.out );
+ Options::printShortUsage( ss.str(), *opts[options::out] );
}
}
-int runCvc4(int argc, char* argv[], Options& options) {
+int runCvc4(int argc, char* argv[], Options& opts) {
// Timer statistic
TimerStat s_totalTime("totalTime");
s_totalTime.start();
// For the signal handlers' benefit
- pOptions = &options;
+ pOptions = &opts;
// Initialize the signal handlers
cvc4_init();
@@ -95,26 +98,26 @@ int runCvc4(int argc, char* argv[], Options& options) {
progPath = argv[0];
// Parse the options
- int firstArgIndex = options.parseOptions(argc, argv);
+ int firstArgIndex = opts.parseOptions(argc, argv);
- progName = options.binary_name.c_str();
+ progName = opts[options::binary_name].c_str();
- if( options.help ) {
- printUsage(options, true);
+ if( opts[options::help] ) {
+ printUsage(opts, true);
exit(1);
- } else if( options.languageHelp ) {
- Options::printLanguageHelp(*options.out);
+ } else if( opts[options::languageHelp] ) {
+ Options::printLanguageHelp(*opts[options::out]);
exit(1);
- } else if( options.version ) {
- *options.out << Configuration::about().c_str() << flush;
+ } else if( opts[options::version] ) {
+ *opts[options::out] << Configuration::about().c_str() << flush;
exit(0);
}
- segvNoSpin = options.segvNoSpin;
+ segvNoSpin = opts[options::segvNoSpin];
// If in competition mode, set output stream option to flush immediately
#ifdef CVC4_COMPETITION_MODE
- *options.out << unitbuf;
+ *opts[options::out] << unitbuf;
#endif /* CVC4_COMPETITION_MODE */
// We only accept one input file
@@ -127,8 +130,8 @@ int runCvc4(int argc, char* argv[], Options& options) {
firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
// if we're reading from stdin on a TTY, default to interactive mode
- if(!options.interactiveSetByUser) {
- options.interactive = inputFromStdin && isatty(fileno(stdin));
+ if(!opts.wasSetByUser(options::interactive)) {
+ opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
}
// Determine which messages to show based on smtcomp_mode and verbosity
@@ -141,13 +144,13 @@ int runCvc4(int argc, char* argv[], Options& options) {
Warning.setStream(CVC4::null_os);
Dump.setStream(CVC4::null_os);
} else {
- if(options.verbosity < 2) {
+ if(opts[options::verbosity] < 2) {
Chat.setStream(CVC4::null_os);
}
- if(options.verbosity < 1) {
+ if(opts[options::verbosity] < 1) {
Notice.setStream(CVC4::null_os);
}
- if(options.verbosity < 0) {
+ if(opts[options::verbosity] < 0) {
Message.setStream(CVC4::null_os);
Warning.setStream(CVC4::null_os);
}
@@ -156,28 +159,28 @@ int runCvc4(int argc, char* argv[], Options& options) {
// Auto-detect input language by filename extension
const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
- if(options.inputLanguage == language::input::LANG_AUTO) {
+ if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
- options.inputLanguage = language::input::LANG_CVC4;
+ opts.set(options::inputLanguage, language::input::LANG_CVC4);
} else {
unsigned len = strlen(filename);
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
- options.inputLanguage = language::input::LANG_SMTLIB_V2;
+ opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
} else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
- options.inputLanguage = language::input::LANG_SMTLIB;
+ opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
} else if((len >= 2 && !strcmp(".p", filename + len - 2))
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
- options.inputLanguage = language::input::LANG_TPTP;
+ opts.set(options::inputLanguage, language::input::LANG_TPTP);
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- options.inputLanguage = language::input::LANG_CVC4;
+ opts.set(options::inputLanguage, language::input::LANG_CVC4);
}
}
}
- if(options.outputLanguage == language::output::LANG_AUTO) {
- options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
+ if(opts[options::outputLanguage] == language::output::LANG_AUTO) {
+ opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
}
// Determine which messages to show based on smtcomp_mode and verbosity
@@ -190,70 +193,73 @@ int runCvc4(int argc, char* argv[], Options& options) {
Warning.setStream(CVC4::null_os);
Dump.setStream(CVC4::null_os);
} else {
- if(options.verbosity < 2) {
+ if(opts[options::verbosity] < 2) {
Chat.setStream(CVC4::null_os);
}
- if(options.verbosity < 1) {
+ if(opts[options::verbosity] < 1) {
Notice.setStream(CVC4::null_os);
}
- if(options.verbosity < 0) {
+ if(opts[options::verbosity] < 0) {
Message.setStream(CVC4::null_os);
Warning.setStream(CVC4::null_os);
}
- Debug.getStream() << Expr::setlanguage(options.outputLanguage);
- Trace.getStream() << Expr::setlanguage(options.outputLanguage);
- Notice.getStream() << Expr::setlanguage(options.outputLanguage);
- Chat.getStream() << Expr::setlanguage(options.outputLanguage);
- Message.getStream() << Expr::setlanguage(options.outputLanguage);
- Warning.getStream() << Expr::setlanguage(options.outputLanguage);
- Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+ Debug.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+ Trace.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+ Notice.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+ Chat.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+ Message.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+ Warning.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+ Dump.getStream() << Expr::setlanguage(opts[options::outputLanguage])
<< Expr::setdepth(-1)
<< Expr::printtypes(false);
}
// important even for muzzled builds (to get result output right)
- *options.out << Expr::setlanguage(options.outputLanguage);
+ *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
// Create the expression manager
- ExprManager exprMgr(options);
+ ExprManager exprMgr(opts);
// Create the SmtEngine
+ StatisticsRegistry driverStats("driver");
SmtEngine smt(&exprMgr);
Parser* replayParser = NULL;
- if( options.replayFilename != "" ) {
- ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
+ if( opts[options::replayFilename] != "" ) {
+ ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts);
- if( options.replayFilename == "-") {
+ if( opts[options::replayFilename] == "-") {
if( inputFromStdin ) {
throw OptionException("Replay file and input file can't both be stdin.");
}
replayParserBuilder.withStreamInput(cin);
}
replayParser = replayParserBuilder.build();
- options.replayStream = new Parser::ExprStream(replayParser);
+ opts.set(options::replayStream, new Parser::ExprStream(replayParser));
}
- if( options.replayLog != NULL ) {
- *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
+ if( opts[options::replayLog] != NULL ) {
+ *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
}
// signal handlers need access
pStatistics = smt.getStatisticsRegistry();
+ exprMgr.getStatisticsRegistry()->setName("ExprManager");
pStatistics->registerStat_(exprMgr.getStatisticsRegistry());
+ pStatistics->registerStat_(&driverStats);
// Timer statistic
- RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
+ RegisterStatistic statTotalTime(&driverStats, &s_totalTime);
// Filename statistics
ReferenceStat< const char* > s_statFilename("filename", filename);
- RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
+ RegisterStatistic statFilenameReg(&driverStats, &s_statFilename);
// Parse and execute commands until we are done
Command* cmd;
bool status = true;
- if( options.interactive ) {
- InteractiveShell shell(exprMgr, options);
+ if( opts[options::interactive] ) {
+ InteractiveShell shell(exprMgr, opts);
Message() << Configuration::getPackageName()
<< " " << Configuration::getVersionString();
if(Configuration::isSubversionBuild()) {
@@ -268,11 +274,11 @@ int runCvc4(int argc, char* argv[], Options& options) {
replayParser->useDeclarationsFrom(shell.getParser());
}
while((cmd = shell.readCommand())) {
- status = doCommand(smt,cmd, options) && status;
+ status = doCommand(smt,cmd, opts) && status;
delete cmd;
}
} else {
- ParserBuilder parserBuilder(&exprMgr, filename, options);
+ ParserBuilder parserBuilder(&exprMgr, filename, opts);
if( inputFromStdin ) {
#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -292,23 +298,23 @@ int runCvc4(int argc, char* argv[], Options& options) {
delete cmd;
break;
}
- status = doCommand(smt, cmd, options) && status;
+ status = doCommand(smt, cmd, opts) && status;
delete cmd;
}
// Remove the parser
delete parser;
}
- if( options.replayStream != NULL ) {
+ if( opts[options::replayStream] != NULL ) {
// this deletes the expression parser too
- delete options.replayStream;
- options.replayStream = NULL;
+ delete opts[options::replayStream];
+ opts.set(options::replayStream, NULL);
}
int returnValue;
string result = "unknown";
if(status) {
- result = smt.getInfo(":status").getValue();
+ result = smt.getInfo("status").getValue();
if(result == "sat") {
returnValue = 10;
@@ -329,20 +335,20 @@ int runCvc4(int argc, char* argv[], Options& options) {
#endif /* CVC4_COMPETITION_MODE */
ReferenceStat< Result > s_statSatResult("sat/unsat", result);
- RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
+ RegisterStatistic statSatResultReg(&driverStats, &s_statSatResult);
s_totalTime.stop();
- if(options.statistics) {
- pStatistics->flushInformation(*options.err);
+ if(opts[options::statistics]) {
+ pStatistics->flushInformation(*opts[options::err]);
}
return returnValue;
}
/** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
- if( options.parseOnly ) {
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) {
+ if( opts[options::parseOnly] ) {
return true;
}
@@ -354,15 +360,15 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
for(CommandSequence::iterator subcmd = seq->begin();
subcmd != seq->end();
++subcmd) {
- status = doCommand(smt, *subcmd, options) && status;
+ status = doCommand(smt, *subcmd, opts) && status;
}
} else {
- if(options.verbosity > 0) {
- *options.out << "Invoking: " << *cmd << endl;
+ if(opts[options::verbosity] > 0) {
+ *opts[options::out] << "Invoking: " << *cmd << endl;
}
- if(options.verbosity >= 0) {
- cmd->invoke(&smt, *options.out);
+ if(opts[options::verbosity] >= 0) {
+ cmd->invoke(&smt, *opts[options::out]);
} else {
cmd->invoke(&smt);
}
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index d93e9f872..648c6c9f9 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -40,7 +40,11 @@
#include "expr/command.h"
#include "util/Assert.h"
#include "util/configuration.h"
-#include "util/options.h"
+#include "options/options.h"
+#include "main/options.h"
+#include "smt/options.h"
+#include "prop/options.h"
+#include "theory/uf/options.h"
#include "util/output.h"
#include "util/dump.h"
#include "util/result.h"
@@ -78,7 +82,7 @@ static bool doCommand(SmtEngine&, Command*, Options&);
Result doSmt(SmtEngine &smt, Command *cmd, Options &options);
template<typename T>
-void sharingManager(int numThreads,
+void sharingManager(unsigned numThreads,
SharedChannel<T>* channelsOut[],
SharedChannel<T>* channelsIn[],
SmtEngine* smts[]);
@@ -122,23 +126,25 @@ public:
{}
void notifyNewLemma(Expr lemma) {
- if(Debug.isOn("disable-lemma-sharing")) return;
- const Options *options = Options::current();
- if(options->sharingFilterByLength >= 0) { // 0 would mean no-sharing effectively
- if( int(lemma.getNumChildren()) > options->sharingFilterByLength)
+ if(Debug.isOn("disable-lemma-sharing")) {
+ return;
+ }
+ if(options::sharingFilterByLength() >= 0) { // 0 would mean no-sharing effectively
+ if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
return;
+ }
}
++cnt;
- Trace("sharing") << d_tag << ": " << lemma << std::endl;
+ Trace("sharing") << d_tag << ": " << lemma << endl;
expr::pickle::Pickle pkl;
- try{
+ try {
d_pickler.toPickle(lemma, pkl);
d_sharedChannel->push(pkl);
- if(Trace.isOn("showSharing") and options->thread_id == 0) {
- *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl;
+ if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+ *options::out() << "thread #0: notifyNewLemma: " << lemma << endl;
}
- }catch(expr::pickle::PicklingException& p){
- Trace("sharing::blocked") << lemma << std::endl;
+ } catch(expr::pickle::PicklingException& p){
+ Trace("sharing::blocked") << lemma << endl;
}
}
@@ -172,8 +178,8 @@ public:
expr::pickle::Pickle pkl = d_sharedChannel->pop();
Expr e = d_pickler.fromPickle(pkl);
- if(Trace.isOn("showSharing") and Options::current()->thread_id == 0) {
- *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl;
+ if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+ *options::out() << "thread #0: getNewLemma: " << e << endl;
}
return e;
}
@@ -182,7 +188,7 @@ public:
-int runCvc4(int argc, char *argv[], Options& options) {
+int runCvc4(int argc, char *argv[], Options& opts) {
#ifdef CVC4_CLN_IMP
Warning() << "WARNING:" << endl
@@ -211,7 +217,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
s_beforePortfolioTime.start();
// For the signal handlers' benefit
- pOptions = &options;
+ pOptions = &opts;
// Initialize the signal handlers
cvc4_init();
@@ -222,36 +228,36 @@ int runCvc4(int argc, char *argv[], Options& options) {
/****************************** Options Processing ************************/
// Parse the options
- int firstArgIndex = options.parseOptions(argc, argv);
+ int firstArgIndex = opts.parseOptions(argc, argv);
- progName = options.binary_name.c_str();
+ progName = opts[options::binary_name].c_str();
- if( options.help ) {
- printUsage(options, true);
+ if( opts[options::help] ) {
+ printUsage(opts, true);
exit(1);
- } else if( options.languageHelp ) {
- Options::printLanguageHelp(*options.out);
+ } else if( opts[options::languageHelp] ) {
+ Options::printLanguageHelp(*opts[options::out]);
exit(1);
- } else if( options.version ) {
- *options.out << Configuration::about().c_str() << flush;
+ } else if( opts[options::version] ) {
+ *opts[options::out] << Configuration::about().c_str() << flush;
exit(0);
}
- int numThreads = options.threads;
+ unsigned numThreads = opts[options::threads];
- if(options.threadArgv.size() > size_t(numThreads)) {
+ if(opts[options::threadArgv].size() > size_t(numThreads)) {
stringstream ss;
- ss << "--thread" << (options.threadArgv.size() - 1)
+ ss << "--thread" << (opts[options::threadArgv].size() - 1)
<< " configuration string seen but this portfolio will only contain "
<< numThreads << " thread(s)!";
throw OptionException(ss.str());
}
- segvNoSpin = options.segvNoSpin;
+ segvNoSpin = opts[options::segvNoSpin];
// If in competition mode, set output stream option to flush immediately
#ifdef CVC4_COMPETITION_MODE
- *options.out << unitbuf;
+ *opts[options::out] << unitbuf;
#endif /* CVC4_COMPETITION_MODE */
// We only accept one input file
@@ -264,29 +270,29 @@ int runCvc4(int argc, char *argv[], Options& options) {
firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
// if we're reading from stdin on a TTY, default to interactive mode
- if(!options.interactiveSetByUser) {
- options.interactive = inputFromStdin && isatty(fileno(stdin));
+ if(!opts.wasSetByUser(options::interactive)) {
+ opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
}
// Auto-detect input language by filename extension
const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
- if(options.inputLanguage == language::input::LANG_AUTO) {
+ if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
- options.inputLanguage = language::input::LANG_CVC4;
+ opts.set(options::inputLanguage, language::input::LANG_CVC4);
} else {
unsigned len = strlen(filename);
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
- options.inputLanguage = language::input::LANG_SMTLIB_V2;
+ opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
} else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
- options.inputLanguage = language::input::LANG_SMTLIB;
+ opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
} else if((len >= 2 && !strcmp(".p", filename + len - 2))
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
- options.inputLanguage = language::input::LANG_TPTP;
+ opts.set(options::inputLanguage, language::input::LANG_TPTP);
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- options.inputLanguage = language::input::LANG_CVC4;
+ opts.set(options::inputLanguage, language::input::LANG_CVC4);
}
}
}
@@ -301,54 +307,55 @@ int runCvc4(int argc, char *argv[], Options& options) {
Warning.setStream(CVC4::null_os);
Dump.setStream(CVC4::null_os);
} else {
- if(options.verbosity < 2) {
+ if(opts[options::verbosity] < 2) {
Chat.setStream(CVC4::null_os);
}
- if(options.verbosity < 1) {
+ if(opts[options::verbosity] < 1) {
Notice.setStream(CVC4::null_os);
}
- if(options.verbosity < 0) {
+ if(opts[options::verbosity] < 0) {
Message.setStream(CVC4::null_os);
Warning.setStream(CVC4::null_os);
}
- OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
+ OutputLanguage language = language::toOutputLanguage(opts[options::inputLanguage]);
Debug.getStream() << Expr::setlanguage(language);
Trace.getStream() << Expr::setlanguage(language);
Notice.getStream() << Expr::setlanguage(language);
Chat.getStream() << Expr::setlanguage(language);
Message.getStream() << Expr::setlanguage(language);
Warning.getStream() << Expr::setlanguage(language);
- Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+ Dump.getStream() << Expr::setlanguage(language)
<< Expr::setdepth(-1)
<< Expr::printtypes(false);
}
// important even for muzzled builds (to get result output right)
- *options.out << Expr::setlanguage(options.outputLanguage);
+ *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
vector<Options> threadOptions;
- for(int i = 0; i < numThreads; ++i) {
- threadOptions.push_back(options);
- Options& opts = threadOptions.back();
+ for(unsigned i = 0; i < numThreads; ++i) {
+ threadOptions.push_back(opts);
+ Options& tOpts = threadOptions.back();
// Set thread identifier
- opts.thread_id = i;
+ tOpts.set(options::thread_id, i);
// If the random-seed is negative, pick a random seed randomly
- if(options.satRandomSeed < 0)
- opts.satRandomSeed = (double)rand();
+ if(opts[options::satRandomSeed] < 0) {
+ tOpts.set(options::satRandomSeed, (double)rand());
+ }
- if(i < (int)options.threadArgv.size() && !options.threadArgv[i].empty()) {
+ if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) {
// separate out the thread's individual configuration string
stringstream optidss;
optidss << "--thread" << i;
string optid = optidss.str();
int targc = 1;
- char* tbuf = strdup(options.threadArgv[i].c_str());
+ char* tbuf = strdup(opts[options::threadArgv][i].c_str());
char* p = tbuf;
// string length is certainly an upper bound on size needed
- char** targv = new char*[options.threadArgv[i].size()];
+ char** targv = new char*[opts[options::threadArgv][i].size()];
char** vp = targv;
*vp++ = strdup(optid.c_str());
p = strtok(p, " ");
@@ -360,7 +367,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
*vp++ = NULL;
if(targc > 1) { // this is necessary in case you do e.g. --thread0=" "
try {
- opts.parseOptions(targc, targv);
+ tOpts.parseOptions(targc, targv);
} catch(OptionException& e) {
stringstream ss;
ss << optid << ": " << e.getMessage();
@@ -372,7 +379,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
<< "' in thread configuration " << optid << " !";
throw OptionException(ss.str());
}
- if(opts.threads != numThreads || opts.threadArgv != options.threadArgv) {
+ if(tOpts[options::threads] != numThreads || tOpts[options::threadArgv] != opts[options::threadArgv]) {
stringstream ss;
ss << "not allowed to set thread options in " << optid << " !";
throw OptionException(ss.str());
@@ -387,16 +394,16 @@ int runCvc4(int argc, char *argv[], Options& options) {
// Some more options related stuff
/* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */
- srand((unsigned int)(-options.satRandomSeed));
+ srand((unsigned int)(-opts[options::satRandomSeed]));
assert(numThreads >= 1); //do we need this?
/* Output to string stream */
vector<stringstream*> ss_out(numThreads);
- if(options.verbosity == 0 or options.separateOutput) {
- for(int i = 0;i <numThreads; ++i) {
+ if(opts[options::verbosity] == 0 || opts[options::separateOutput]) {
+ for(unsigned i = 0; i < numThreads; ++i) {
ss_out[i] = new stringstream;
- threadOptions[i].out = ss_out[i];
+ threadOptions[i].set(options::out, ss_out[i]);
}
}
@@ -431,8 +438,8 @@ int runCvc4(int argc, char *argv[], Options& options) {
Command* cmd;
// bool status = true; // Doesn't seem to be use right now: commenting it out
CommandSequence* seq = new CommandSequence();
- if( options.interactive ) {
- InteractiveShell shell(*exprMgr, options);
+ if( opts[options::interactive] ) {
+ InteractiveShell shell(*exprMgr, opts);
Message() << Configuration::getPackageName()
<< " " << Configuration::getVersionString();
if(Configuration::isSubversionBuild()) {
@@ -452,7 +459,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
} else {
ParserBuilder parserBuilder =
ParserBuilder(exprMgr, filename).
- withOptions(options);
+ withOptions(opts);
if( inputFromStdin ) {
#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -465,15 +472,16 @@ int runCvc4(int argc, char *argv[], Options& options) {
Parser *parser = parserBuilder.build();
while((cmd = parser->nextCommand())) {
seq->addCommand(cmd);
- // doCommand(smt, cmd, options);
+ // doCommand(smt, cmd, opts);
// delete cmd;
}
// Remove the parser
delete parser;
}
- if(options.parseOnly)
+ if(opts[options::parseOnly]) {
return 0;
+ }
exprMgr = NULL; // don't want to use that variable
// after this point
@@ -482,7 +490,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty
Command *seqs[numThreads];
seqs[0] = seq; seq = NULL;
- for(int i = 1; i < numThreads; ++i) {
+ for(unsigned i = 1; i < numThreads; ++i) {
vmaps[i] = new ExprManagerMapCollection();
exprMgrs[i] = new ExprManager(threadOptions[i]);
seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) );
@@ -515,14 +523,16 @@ int runCvc4(int argc, char *argv[], Options& options) {
// Create the SmtEngine(s)
SmtEngine *smts[numThreads];
- for(int i = 0; i < numThreads; ++i) {
+ for(unsigned i = 0; i < numThreads; ++i) {
smts[i] = new SmtEngine(exprMgrs[i]);
// Register the statistics registry of the thread
- string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
- smts[i]->getStatisticsRegistry()->setName(tag);
- theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
+ string emTag = "ExprManager thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
+ string smtTag = "SmtEngine thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
+ exprMgrs[i]->getStatisticsRegistry()->setName(emTag);
+ smts[i]->getStatisticsRegistry()->setName(smtTag);
theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() );
+ theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
}
/************************* Lemma sharing init ************************/
@@ -532,12 +542,12 @@ int runCvc4(int argc, char *argv[], Options& options) {
if(numThreads == 1) {
// Disable sharing
- threadOptions[0].sharingFilterByLength = 0;
+ threadOptions[0].set(options::sharingFilterByLength, 0);
} else {
// Setup sharing channels
const unsigned int sharingChannelSize = 1000000;
- for(int i = 0; i<numThreads; ++i){
+ for(unsigned i = 0; i < numThreads; ++i){
if(Debug.isOn("channel-empty")) {
channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
@@ -548,14 +558,14 @@ int runCvc4(int argc, char *argv[], Options& options) {
}
/* Lemma output channel */
- for(int i = 0; i<numThreads; ++i) {
- string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
- threadOptions[i].lemmaOutputChannel =
+ for(unsigned i = 0; i < numThreads; ++i) {
+ string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
+ threadOptions[i].set(options::lemmaOutputChannel,
new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i],
- vmaps[i]->d_from, vmaps[i]->d_to);
- threadOptions[i].lemmaInputChannel =
+ vmaps[i]->d_from, vmaps[i]->d_to));
+ threadOptions[i].set(options::lemmaInputChannel,
new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i],
- vmaps[i]->d_from, vmaps[i]->d_to);
+ vmaps[i]->d_from, vmaps[i]->d_to));
}
}
@@ -564,7 +574,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
/* Portfolio */
boost::function<Result()> fns[numThreads];
- for(int i = 0; i < numThreads; ++i) {
+ for(unsigned i = 0; i < numThreads; ++i) {
fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i]));
}
@@ -580,7 +590,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
/************************* Post printing answer ***********************/
- if(options.printWinner){
+ if(opts[options::printWinner]){
cout << "The winner is #" << winner << endl;
}
@@ -606,29 +616,29 @@ int runCvc4(int argc, char *argv[], Options& options) {
// Stop timers, enough work done
s_totalTime.stop();
- if(options.statistics) {
- pStatistics->flushInformation(*options.err);
+ if(opts[options::statistics]) {
+ pStatistics->flushInformation(*opts[options::err]);
}
- if(options.separateOutput) {
- for(int i = 0; i < numThreads; ++i) {
- *options.out << "--- Output from thread #" << i << " ---" << endl;
- *options.out << ss_out[i]->str();
+ if(opts[options::separateOutput]) {
+ for(unsigned i = 0; i < numThreads; ++i) {
+ *opts[options::out] << "--- Output from thread #" << i << " ---" << endl;
+ *opts[options::out] << ss_out[i]->str();
}
}
- /*if(options.statistics) {
+ /*if(opts[options::statistics]) {
double totalTime = double(s_totalTime.getData().tv_sec) +
double(s_totalTime.getData().tv_nsec)/1000000000.0;
cout.precision(6);
- *options.err << "real time: " << totalTime << "s\n";
- int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt;
+ *opts[options::err] << "real time: " << totalTime << "s\n";
+ int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(opts[options::lemmaOutputChannel])).cnt;
int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt;
- *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl;
- *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl;
- *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
+ *opts[options::err] << "lemmas shared by thread #0: " << th0_lemcnt << endl;
+ *opts[options::err] << "lemmas shared by thread #1: " << th1_lemcnt << endl;
+ *opts[options::err] << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
<< " lem/sec" << endl;
- *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl;
+ *opts[options::err] << "winner: #" << (winner == 0 ? 0 : 1) << endl;
}*/
// destruction is causing segfaults, let us just exit
@@ -663,23 +673,23 @@ namespace CVC4 {
}
}
-void printUsage(Options& options, bool full) {
+void printUsage(Options& opts, bool full) {
stringstream ss;
- ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
+ ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
<< endl
<< "Without an input file, or with `-', CVC4 reads from standard input." << endl
<< endl
<< "CVC4 options:" << endl;
if(full) {
- Options::printUsage( ss.str(), *options.out );
+ Options::printUsage( ss.str(), *opts[options::out] );
} else {
- Options::printShortUsage( ss.str(), *options.out );
+ Options::printShortUsage( ss.str(), *opts[options::out] );
}
}
/** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
- if( options.parseOnly ) {
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) {
+ if( opts[options::parseOnly] ) {
return true;
}
@@ -691,15 +701,15 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
for(CommandSequence::iterator subcmd = seq->begin();
subcmd != seq->end();
++subcmd) {
- status = doCommand(smt, *subcmd, options) && status;
+ status = doCommand(smt, *subcmd, opts) && status;
}
} else {
- if(options.verbosity > 0) {
- *options.out << "Invoking: " << *cmd << endl;
+ if(opts[options::verbosity] > 0) {
+ *opts[options::out] << "Invoking: " << *cmd << endl;
}
- if(options.verbosity >= 0) {
- cmd->invoke(&smt, *options.out);
+ if(opts[options::verbosity] >= 0) {
+ cmd->invoke(&smt, *opts[options::out]);
} else {
cmd->invoke(&smt);
}
@@ -712,48 +722,48 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
/**** End of code shared with driver.cpp ****/
/** Create the SMT engine and execute the commands */
-Result doSmt(SmtEngine &smt, Command *cmd, Options &options) {
+Result doSmt(SmtEngine &smt, Command *cmd, Options &opts) {
try {
// For the signal handlers' benefit
- pOptions = &options;
+ pOptions = &opts;
// Execute the commands
- bool status = doCommand(smt, cmd, options);
+ bool status = doCommand(smt, cmd, opts);
- // if(options.statistics) {
- // smt.getStatisticsRegistry()->flushInformation(*options.err);
- // *options.err << "Statistics printing of my thread complete " << endl;
+ // if(opts[options::statistics]) {
+ // smt.getStatisticsRegistry()->flushInformation(*opts[options::err]);
+ // *opts[options::err] << "Statistics printing of my thread complete " << endl;
// }
return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN;
} catch(OptionException& e) {
- *pOptions->out << "unknown" << endl;
+ *(*pOptions)[options::out] << "unknown" << endl;
cerr << "CVC4 Error:" << endl << e << endl;
printUsage(*pOptions);
} catch(Exception& e) {
#ifdef CVC4_COMPETITION_MODE
- *pOptions->out << "unknown" << endl;
+ *(*pOptions)[options::out] << "unknown" << endl;
#endif
- *pOptions->err << "CVC4 Error:" << endl << e << endl;
- if(pOptions->statistics) {
- pStatistics->flushInformation(*pOptions->err);
+ *(*pOptions)[options::err] << "CVC4 Error:" << endl << e << endl;
+ if((*pOptions)[options::statistics]) {
+ pStatistics->flushInformation(*(*pOptions)[options::err]);
}
}
return Result::SAT_UNKNOWN;
}
template<typename T>
-void sharingManager(int numThreads,
+void sharingManager(unsigned numThreads,
SharedChannel<T> *channelsOut[], // out and in with respect
SharedChannel<T> *channelsIn[],
SmtEngine *smts[]) // to smt engines
{
- Trace("sharing") << "sharing: thread started " << std::endl;
+ Trace("sharing") << "sharing: thread started " << endl;
vector <int> cnt(numThreads); // Debug("sharing")
vector< queue<T> > queues;
- for(int i = 0; i < numThreads; ++i){
+ for(unsigned i = 0; i < numThreads; ++i){
queues.push_back(queue<T>());
}
@@ -768,7 +778,7 @@ void sharingManager(int numThreads,
boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval));
- for(int t = 0; t < numThreads; ++t) {
+ for(unsigned t = 0; t < numThreads; ++t) {
if(channelsOut[t]->empty()) continue; /* No activity on this channel */
@@ -784,22 +794,22 @@ void sharingManager(int numThreads,
<< ". Chunk " << cnt[t] << std :: endl;
}
- for(int u = 0; u < numThreads; ++u) {
+ for(unsigned u = 0; u < numThreads; ++u) {
if(u != t){
- Trace("sharing") << "sharing: adding to queue " << u << std::endl;
+ Trace("sharing") << "sharing: adding to queue " << u << endl;
queues[u].push(data);
}
}/* end of inner for: broadcast activity */
} /* end of outer for: look for activity */
- for(int t = 0; t < numThreads; ++t){
+ for(unsigned t = 0; t < numThreads; ++t){
/* Alert if channel full, so that we increase sharingChannelSize
or decrease sharingBroadcastInterval */
Assert(not channelsIn[t]->full());
while(!queues[t].empty() && !channelsIn[t]->full()){
- Trace("sharing") << "sharing: pushing on channel " << t << std::endl;
+ Trace("sharing") << "sharing: pushing on channel " << t << endl;
T data = queues[t].front();
channelsIn[t]->push(data);
queues[t].pop();
@@ -807,17 +817,17 @@ void sharingManager(int numThreads,
}
} /* end of infinite while */
- Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << std::endl;
+ Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << endl;
- for(int t = 0; t < numThreads; ++t) {
- Trace("interrupt") << "Interrupting thread #" << t << std::endl;
+ for(unsigned t = 0; t < numThreads; ++t) {
+ Trace("interrupt") << "Interrupting thread #" << t << endl;
try{
smts[t]->interrupt();
}catch(ModalException &e){
// It's fine, the thread is probably not there.
- Trace("interrupt") << "Could not interrupt thread #" << t << std::endl;
+ Trace("interrupt") << "Could not interrupt thread #" << t << endl;
}
}
- Trace("sharing") << "sharing: Interrupted, exiting." << std::endl;
+ Trace("sharing") << "sharing: Interrupted, exiting." << endl;
}
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 03a3a0ae3..443404384 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -33,7 +33,7 @@
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
-#include "util/options.h"
+#include "options/options.h"
#include "util/language.h"
#include <string.h>
@@ -85,8 +85,8 @@ static set<string> s_declarations;
InteractiveShell::InteractiveShell(ExprManager& exprManager,
const Options& options) :
- d_in(*options.in),
- d_out(*options.out),
+ d_in(*options[options::in]),
+ d_out(*options[options::out]),
d_options(options),
d_quit(false) {
ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
@@ -99,7 +99,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
::rl_completion_entry_function = commandGenerator;
::using_history();
- switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) {
+ switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) {
case output::LANG_CVC4:
d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
commandsBegin = cvc_commands;
@@ -174,7 +174,7 @@ Command* InteractiveShell::readCommand() {
/* Prompt the user for input. */
if(d_usingReadline) {
#if HAVE_LIBREADLINE
- lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : "");
+ lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : "");
if(lineBuf != NULL && lineBuf[0] != '\0') {
::add_history(lineBuf);
}
@@ -182,7 +182,7 @@ Command* InteractiveShell::readCommand() {
free(lineBuf);
#endif /* HAVE_LIBREADLINE */
} else {
- if(d_options.verbosity >= 0) {
+ if(d_options[options::verbosity] >= 0) {
d_out << "CVC4> " << flush;
}
@@ -239,7 +239,7 @@ Command* InteractiveShell::readCommand() {
input[n] = '\n';
if(d_usingReadline) {
#if HAVE_LIBREADLINE
- lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : "");
+ lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "... > " : "");
if(lineBuf != NULL && lineBuf[0] != '\0') {
::add_history(lineBuf);
}
@@ -247,7 +247,7 @@ Command* InteractiveShell::readCommand() {
free(lineBuf);
#endif /* HAVE_LIBREADLINE */
} else {
- if(d_options.verbosity >= 0) {
+ if(d_options[options::verbosity] >= 0) {
d_out << "... > " << flush;
}
@@ -262,7 +262,7 @@ Command* InteractiveShell::readCommand() {
}
}
- d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME));
+ d_parser->setInput(Input::newStringInput(d_options[options::inputLanguage], input, INPUT_FILENAME));
/* There may be more than one command in the input. Build up a
sequence. */
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 7f17b88d7..214ae0d02 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -21,6 +21,7 @@
#include <string>
#include "util/language.h"
+#include "options/options.h"
namespace CVC4 {
diff --git a/src/main/main.cpp b/src/main/main.cpp
index b90ab433a..70f2783a5 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -34,7 +34,8 @@
#include "expr/command.h"
#include "util/Assert.h"
#include "util/configuration.h"
-#include "util/options.h"
+#include "main/options.h"
+#include "theory/uf/options.h"
#include "util/output.h"
#include "util/result.h"
#include "util/stats.h"
@@ -51,22 +52,22 @@ using namespace CVC4::main;
* Put everything in runCvc4().
*/
int main(int argc, char* argv[]) {
- Options options;
+ Options opts;
try {
- return runCvc4(argc, argv, options);
+ return runCvc4(argc, argv, opts);
} catch(OptionException& e) {
#ifdef CVC4_COMPETITION_MODE
- *options.out << "unknown" << endl;
+ *opts[options::out] << "unknown" << endl;
#endif
cerr << "CVC4 Error:" << endl << e << endl;
- printUsage(options);
+ printUsage(opts);
} catch(Exception& e) {
#ifdef CVC4_COMPETITION_MODE
- *options.out << "unknown" << endl;
+ *opts[options::out] << "unknown" << endl;
#endif
- *options.err << "CVC4 Error:" << endl << e << endl;
- if(options.statistics && pStatistics != NULL) {
- pStatistics->flushInformation(*options.err);
+ *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+ if(opts[options::statistics] && pStatistics != NULL) {
+ pStatistics->flushInformation(*opts[options::err]);
}
}
exit(1);
diff --git a/src/main/main.h b/src/main/main.h
index 4df5ccc49..09ba60c94 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -19,7 +19,7 @@
#include <exception>
#include <string>
-#include "util/options.h"
+#include "options/options.h"
#include "util/exception.h"
#include "util/stats.h"
#include "util/tls.h"
diff --git a/src/main/options b/src/main/options
new file mode 100644
index 000000000..6defc8642
--- /dev/null
+++ b/src/main/options
@@ -0,0 +1,38 @@
+#
+# 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
+
+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
+
+# portfolio options
+option printWinner bool
+ enable printing the winning thread (pcvc4 only)
+option - --threadN=string void
+ configures thread N (0..#threads-1)
+option threadArgv std::vector<std::string>
+#:includes <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 separateOutput bool :default false
+ In multi-threaded setting print output of each thread at the
+ end of run, separated by a divider ("----").
+option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
+ don't share lemmas strictly longer than N
+
+endmodule
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
new file mode 100644
index 000000000..e607e13ce
--- /dev/null
+++ b/src/main/options_handlers.h
@@ -0,0 +1,101 @@
+/********************* */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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::isSubversionBuild()) {
+ printf("subversion : yes [%s r%u%s]\n",
+ Configuration::getSubversionBranchName(),
+ Configuration::getSubversionRevision(),
+ Configuration::hasSubversionModifications() ?
+ " (with modifications)" : "");
+ } else {
+ printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
+ }
+ 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("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);
+}
+
+
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index fc22374cf..10c387b14 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -25,7 +25,7 @@
#include "smt/smt_engine.h"
#include "util/result.h"
-#include "util/options.h"
+#include "options/options.h"
using namespace boost;
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index 9bc911be3..1a82d651b 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -25,7 +25,7 @@
#include "smt/smt_engine.h"
#include "expr/command.h"
-#include "util/options.h"
+#include "options/options.h"
namespace CVC4 {
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5877704ae..756c7d7a9 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -27,7 +27,7 @@
#include "util/Assert.h"
#include "util/exception.h"
-#include "util/options.h"
+#include "options/options.h"
#include "util/stats.h"
#include "cvc4autoconfig.h"
@@ -52,7 +52,7 @@ bool segvNoSpin = false;
/** Handler for SIGXCPU, i.e., timeout. */
void timeout_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by timeout.\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
abort();
@@ -61,7 +61,7 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
/** Handler for SIGINT, i.e., when the user hits control C. */
void sigint_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by user.\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
abort();
@@ -86,7 +86,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
if(segvNoSpin) {
fprintf(stderr, "No-spin requested, aborting...\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
abort();
@@ -106,7 +106,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
} else if(addr < 10*1024) {
cerr << "Looks like a NULL pointer was dereferenced." << endl;
}
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
abort();
@@ -119,7 +119,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
if(segvNoSpin) {
fprintf(stderr, "No-spin requested, aborting...\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
abort();
@@ -132,7 +132,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
}
#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 executed an illegal instruction.\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
abort();
@@ -156,7 +156,7 @@ void cvc4unexpected() {
}
if(segvNoSpin) {
fprintf(stderr, "No-spin requested.\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
set_terminate(default_terminator);
@@ -169,7 +169,7 @@ void cvc4unexpected() {
}
#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
set_terminate(default_terminator);
@@ -182,7 +182,7 @@ void cvc4terminate() {
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding. "
"(Don't do that.)\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
default_terminator();
@@ -190,7 +190,7 @@ void cvc4terminate() {
fprintf(stderr,
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding.\n");
- if(pOptions->statistics && pStatistics != NULL) {
+ if((*pOptions)[options::statistics] && pStatistics != NULL) {
pStatistics->flushInformation(cerr);
}
default_terminator();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback