diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-01-29 00:05:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-01-29 00:05:16 +0000 |
commit | 2a9e6970b971eb0a9ac4c216fe5f5f1542e195e0 (patch) | |
tree | 23631643798b923b7e9883286296269c8f5e772d /src/main/getopt.cpp | |
parent | 1e59e3f37ecb7b84371691358f3eb3804a845c04 (diff) |
fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
Diffstat (limited to 'src/main/getopt.cpp')
-rw-r--r-- | src/main/getopt.cpp | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 123bc3204..388e58a3b 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -46,9 +46,16 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt | smtlib SMT-LIB format\n\ "; +static const char cnf_help[] = "\ +CNF conversions currently supported as arguments to the --cnf option:\n\ + direct put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\ + var variable-introduction method (new vars, no exp. blow up in # clauses)\n\ +"; + // FIXME add a comment here describing the purpose of this enum OptionValue { - SMTCOMP = 256, /* no clash with char options */ + CNF = 256, /* no clash with char options */ + SMTCOMP, STATS };/* enum OptionValue */ @@ -61,6 +68,7 @@ static struct option cmdlineOptions[] = { { "quiet" , no_argument , NULL, 'q' }, { "lang" , required_argument, NULL, 'L' }, { "debug" , required_argument, NULL, 'd' }, + { "cnf" , required_argument, NULL, CNF }, { "smtcomp", no_argument , NULL, SMTCOMP }, { "stats" , no_argument , NULL, STATS } };/* if you add things to the above, please remember to update usage.h! */ @@ -117,6 +125,21 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti fputs(lang_help, stdout); exit(1); + case CNF: + if(!strcmp(optarg, "direct")) { + opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL; + break; + } else if(!strcmp(optarg, "var")) { + opts->d_cnfConversion = CNF_VAR_INTRODUCTION; + break; + } else if(strcmp(optarg, "help")) { + throw OptionException(string("unknown CNF conversion for --cnf: `") + + optarg + "'. Try --cnf help."); + } + + fputs(cnf_help, stdout); + exit(1); + case 'd': Debug.on(optarg); /* fall-through */ |