diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-27 18:34:44 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-27 18:34:44 +0000 |
commit | e56c41f47d43103a6e8bf744e12229ed6e5a8f19 (patch) | |
tree | 39be4124610edf8072206aa85b178b8fe3eab2e2 /src/main | |
parent | 14c22833d05f632eb40eb68cc3c68345d891005c (diff) |
Adding --mmap option to use memory-mapped file input, which provides a marginal improvement (<5%) on big benchmarks.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 6 | ||||
-rw-r--r-- | src/main/main.cpp | 14 | ||||
-rw-r--r-- | src/main/usage.h | 2 |
3 files changed, 20 insertions, 2 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 7ca889592..baad6fe31 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -67,6 +67,7 @@ enum OptionValue { SEGV_NOSPIN, PARSE_ONLY, NO_CHECKING, + USE_MMAP, SHOW_CONFIG };/* enum OptionValue */ @@ -103,6 +104,7 @@ static struct option cmdlineOptions[] = { { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, { "parse-only" , no_argument , NULL, PARSE_ONLY }, { "no-checking", no_argument , NULL, NO_CHECKING }, + { "mmap", no_argument , NULL, USE_MMAP }, { "show-config", no_argument , NULL, SHOW_CONFIG } };/* if you add things to the above, please remember to update usage.h! */ @@ -219,6 +221,10 @@ throw(OptionException) { opts->semanticChecks = false; break; + case USE_MMAP: + opts->memoryMap = true; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/main/main.cpp b/src/main/main.cpp index 745fa30e9..2eea56947 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -142,10 +142,19 @@ int runCvc4(int argc, char *argv[]) { // Create the parser Parser* parser; + istream* input = NULL; + if(inputFromStdin) { - parser = Parser::getNewParser(&exprMgr, options.lang, cin); + parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>"); + } else if( options.memoryMap ) { + parser = Parser::getMemoryMappedParser(&exprMgr, options.lang, argv[firstArgIndex]); } else { - parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]); + string filename = argv[firstArgIndex]; + input = new ifstream(filename.c_str()); + if(input == NULL) { + throw Exception("file does not exist or is unreadable: " + filename); + } + parser = Parser::getNewParser(&exprMgr, options.lang, *input, filename); } if(!options.semanticChecks) { @@ -163,6 +172,7 @@ int runCvc4(int argc, char *argv[]) { // Remove the parser delete parser; + delete input; switch(lastResult.asSatisfiabilityResult().isSAT()) { diff --git a/src/main/usage.h b/src/main/usage.h index 6c44fef5a..3a609d2ec 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -37,6 +37,8 @@ CVC4 options:\n\ --stats give statistics on exit\n\ --segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\ --parse-only exit after parsing input\n\ + --no-checking disable semantic checks in the parser\n\ + --mmap memory map file input\n\ --show-config show CVC4 static configuration\n\ "; |