summaryrefslogtreecommitdiff
path: root/src/main/driver.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/driver.cpp')
-rw-r--r--src/main/driver.cpp144
1 files changed, 75 insertions, 69 deletions
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback