summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--RELEASE-NOTES6
-rw-r--r--src/main/command_executor.h2
-rw-r--r--src/main/driver_unified.cpp193
-rwxr-xr-xsrc/options/mkoptions2
4 files changed, 106 insertions, 97 deletions
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 243fa9215..a68801d32 100644
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -5,8 +5,8 @@ Release Notes for CVC4 1.0, October 2012
If you run CVC4 without arguments, you will find yourself in an interactive
CVC4 session, which expects commands in CVC4's native language (the so-called
"presentation" language). To use SMT-LIB, use the "--lang smt" option on the
-command line. For stricter adherence to the standard, use "--smtlib2"
-(see below).
+command line. For stricter adherence to the standard, use "--smtlib"
+(see below regarding SMT-LIB compliance).
When a filename is given on the command line, the file's extension determines
the language parser that's used (e.g., file.smt is SMT-LIB 1.2, file.smt2
@@ -69,7 +69,7 @@ Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0
standard (http://smtlib.org/). However, when parsing SMT-LIB input,
certain default settings don't match what is stated in the official
standard. To make CVC4 adhere more strictly to the standard, use the
-"--smtlib2" command-line option. Even with this setting, CVC4 is
+"--smtlib" command-line option. Even with this setting, CVC4 is
somewhat lenient; some non-conforming input may still be parsed and
processed.
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index a5bd78abe..38a20b1cb 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -40,6 +40,8 @@ protected:
public:
CommandExecutor(ExprManager &exprMgr, Options &options);
+ virtual ~CommandExecutor() {}
+
/**
* Executes a command. Recursively handles if cmd is a command
* sequence. Eventually uses doCommandSingleton (which can be
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 3eba7ff6a..8f8e19f81 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -63,7 +63,7 @@ namespace CVC4 {
const char *progName;
/** A pointer to the CommandExecutor (the signal handlers need it) */
- CVC4::main::CommandExecutor* pExecutor;
+ CVC4::main::CommandExecutor* pExecutor = NULL;
}/* CVC4::main namespace */
}/* CVC4 namespace */
@@ -185,24 +185,21 @@ int runCvc4(int argc, char* argv[], Options& opts) {
// Create the expression manager using appropriate options
# ifndef PORTFOLIO_BUILD
- ExprManager exprMgr(opts);
+ ExprManager* exprMgr = new ExprManager(opts);
# else
vector<Options> threadOpts = parseThreadSpecificOptions(opts);
- ExprManager exprMgr(threadOpts[0]);
+ ExprManager* exprMgr = new ExprManager(threadOpts[0]);
# endif
# ifndef PORTFOLIO_BUILD
- CommandExecutor cmdExecutor(exprMgr, opts);
+ pExecutor = new CommandExecutor(*exprMgr, opts);
# else
- CommandExecutorPortfolio cmdExecutor(exprMgr, opts, threadOpts);
+ pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
# endif
- // give access to the signal handlers for stats output
- pExecutor = &cmdExecutor;
-
Parser* replayParser = NULL;
if( opts[options::replayFilename] != "" ) {
- ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts);
+ ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts);
if( opts[options::replayFilename] == "-") {
if( inputFromStdin ) {
@@ -217,114 +214,122 @@ int runCvc4(int argc, char* argv[], Options& opts) {
*opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
}
- // Timer statistic
- RegisterStatistic statTotalTime(&cmdExecutor.getStatisticsRegistry(), &s_totalTime);
-
- // Filename statistics
- ReferenceStat< const char* > s_statFilename("filename", filename);
- RegisterStatistic statFilenameReg(&cmdExecutor.getStatisticsRegistry(), &s_statFilename);
-
- // Parse and execute commands until we are done
- Command* cmd;
- bool status = true;
- if( opts[options::interactive] ) {
- InteractiveShell shell(exprMgr, opts);
- Message() << Configuration::getPackageName()
- << " " << Configuration::getVersionString();
- if(Configuration::isSubversionBuild()) {
- Message() << " [" << Configuration::getSubversionId() << "]";
- }
- Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
- << " assertions:"
- << (Configuration::isAssertionBuild() ? "on" : "off")
- << endl;
- if(replayParser != NULL) {
- // have the replay parser use the declarations input interactively
- replayParser->useDeclarationsFrom(shell.getParser());
- }
- while((cmd = shell.readCommand())) {
- status = cmdExecutor.doCommand(cmd) && status;
- delete cmd;
- }
- } else {
- ParserBuilder parserBuilder(&exprMgr, filename, opts);
+ int returnValue = 0;
+ {
+ // Timer statistic
+ RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), &s_totalTime);
+
+ // Filename statistics
+ ReferenceStat< const char* > s_statFilename("filename", filename);
+ RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename);
+
+ // Parse and execute commands until we are done
+ Command* cmd;
+ bool status = true;
+ if( opts[options::interactive] ) {
+ InteractiveShell shell(*exprMgr, opts);
+ Message() << Configuration::getPackageName()
+ << " " << Configuration::getVersionString();
+ if(Configuration::isSubversionBuild()) {
+ Message() << " [" << Configuration::getSubversionId() << "]";
+ }
+ Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+ << " assertions:"
+ << (Configuration::isAssertionBuild() ? "on" : "off")
+ << endl;
+ if(replayParser != NULL) {
+ // have the replay parser use the declarations input interactively
+ replayParser->useDeclarationsFrom(shell.getParser());
+ }
+ while((cmd = shell.readCommand())) {
+ status = pExecutor->doCommand(cmd) && status;
+ delete cmd;
+ }
+ } else {
+ ParserBuilder parserBuilder(exprMgr, filename, opts);
- if( inputFromStdin ) {
+ if( inputFromStdin ) {
#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
- parserBuilder.withStreamInput(cin);
+ parserBuilder.withStreamInput(cin);
#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
- parserBuilder.withLineBufferedStreamInput(cin);
+ parserBuilder.withLineBufferedStreamInput(cin);
#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
- }
+ }
- Parser *parser = parserBuilder.build();
- if(replayParser != NULL) {
- // have the replay parser use the file's declarations
- replayParser->useDeclarationsFrom(parser);
- }
- while(status && (cmd = parser->nextCommand())) {
- if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+ Parser *parser = parserBuilder.build();
+ if(replayParser != NULL) {
+ // have the replay parser use the file's declarations
+ replayParser->useDeclarationsFrom(parser);
+ }
+ while(status && (cmd = parser->nextCommand())) {
+ if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+ delete cmd;
+ break;
+ }
+ status = pExecutor->doCommand(cmd);
delete cmd;
- break;
}
- status = cmdExecutor.doCommand(cmd);
- delete cmd;
+ // Remove the parser
+ delete parser;
}
- // Remove the parser
- delete parser;
- }
- if( opts[options::replayStream] != NULL ) {
- // this deletes the expression parser too
- delete opts[options::replayStream];
- opts.set(options::replayStream, NULL);
- }
+ if( opts[options::replayStream] != NULL ) {
+ // this deletes the expression parser too
+ delete opts[options::replayStream];
+ opts.set(options::replayStream, NULL);
+ }
- int returnValue;
- string result = "unknown";
- if(status) {
- result = cmdExecutor.getSmtEngineStatus();
+ string result = "unknown";
+ if(status) {
+ result = pExecutor->getSmtEngineStatus();
- if(result == "sat") {
- returnValue = 10;
- } else if(result == "unsat") {
- returnValue = 20;
+ if(result == "sat") {
+ returnValue = 10;
+ } else if(result == "unsat") {
+ returnValue = 20;
+ } else {
+ returnValue = 0;
+ }
} else {
- returnValue = 0;
+ // there was some kind of error
+ returnValue = 1;
}
- } else {
- // there was some kind of error
- returnValue = 1;
- }
#ifdef CVC4_COMPETITION_MODE
- // exit, don't return (don't want destructors to run)
- // _exit() from unistd.h doesn't run global destructors
- // or other on_exit/atexit stuff.
- _exit(returnValue);
+ // exit, don't return (don't want destructors to run)
+ // _exit() from unistd.h doesn't run global destructors
+ // or other on_exit/atexit stuff.
+ _exit(returnValue);
#endif /* CVC4_COMPETITION_MODE */
- ReferenceStat< Result > s_statSatResult("sat/unsat", result);
- RegisterStatistic statSatResultReg(&cmdExecutor.getStatisticsRegistry(), &s_statSatResult);
+ ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+ RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult);
- s_totalTime.stop();
+ s_totalTime.stop();
- // Set the global executor pointer to NULL first. If we get a
- // signal while dumping statistics, we don't want to try again.
- pExecutor = NULL;
- if(opts[options::statistics]) {
- cmdExecutor.flushStatistics(*opts[options::err]);
- }
+ // Set the global executor pointer to NULL first. If we get a
+ // signal while dumping statistics, we don't want to try again.
+ if(opts[options::statistics]) {
+ pExecutor->flushStatistics(*opts[options::err]);
+ }
#ifdef CVC4_DEBUG
- if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
- _exit(returnValue);
- }
+ if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
+ _exit(returnValue);
+ }
#else /* CVC4_DEBUG */
- if(opts[options::earlyExit]) {
- _exit(returnValue);
- }
+ if(opts[options::earlyExit]) {
+ _exit(returnValue);
+ }
#endif /* CVC4_DEBUG */
+ }
+
+ // On exceptional exit, these are leaked, but that's okay... they
+ // need to be around in that case for main() to print statistics.
+ delete pExecutor;
+ delete exprMgr;
+
+ pExecutor = NULL;
return returnValue;
}
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 79ef35f5b..ffaff9927 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -852,6 +852,8 @@ function handle_alias {
# false positive: =SOMETHING, where SOMETHING != ARG
linkarg=
fi
+ else
+ linkarg=
fi
links="$links
#line $lineno \"$kf\"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback