diff options
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 */ |