diff options
Diffstat (limited to 'src/util/options.cpp')
-rw-r--r-- | src/util/options.cpp | 96 |
1 files changed, 95 insertions, 1 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index d33064c73..e33fbc263 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -64,6 +64,9 @@ Options::Options() : verbosity(0), inputLanguage(language::input::LANG_AUTO), outputLanguage(language::output::LANG_AUTO), + help(false), + version(false), + languageHelp(false), parseOnly(false), preprocessOnly(false), semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT), @@ -71,6 +74,7 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), + printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), doStaticLearning(true), interactive(false), @@ -93,12 +97,23 @@ Options::Options() : arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value + satVarDecay(0.95), + satClauseDecay(0.999), + satRestartFirst(25), + satRestartInc(3.0), pivotRule(MINIMUM), arithPivotThreshold(16), arithPropagateMaxLength(16), ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), - dioSolver(true) + dioSolver(true), + lemmaOutputChannel(NULL), + lemmaInputChannel(NULL), + threads(2),// default should be 1 probably, but say 2 for now + threadArgv(), + thread_id(-1), + separateOutput(false), + sharingFilterByLength(-1) { } @@ -141,6 +156,7 @@ Additional CVC4 options:\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ + --print-winner enable printing the winning thread (pcvc4 only)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ --show-debug-tags show all avalable tags for debugging\n\ @@ -157,13 +173,19 @@ Additional CVC4 options:\n\ --prop-row-length=N sets the maximum row length to be used in propagation\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ + --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\ + --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --threads=N sets the number of solver threads\n\ + --threadN=string configures thread N (0..#threads-1)\n\ + --filter-lemma-length=N don't share lemmas strictly longer than N\n\ "; + #warning "Change CL options as --disable-variable-removal cannot do anything currently." static const string languageDescription = "\ @@ -322,8 +344,11 @@ enum OptionValue { REPLAY, REPLAY_LOG, PIVOT_RULE, + PRINT_WINNER, RANDOM_FREQUENCY, RANDOM_SEED, + SAT_RESTART_FIRST, + SAT_RESTART_INC, ARITHMETIC_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, @@ -331,6 +356,9 @@ enum OptionValue { ARITHMETIC_DIO_SOLVER, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, + PARALLEL_THREADS, + PARALLEL_SEPARATE_OUTPUT, + PORTFOLIO_FILTER_LENGTH, TIME_LIMIT, TIME_LIMIT_PER, RESOURCE_LIMIT, @@ -409,11 +437,17 @@ static struct option cmdlineOptions[] = { { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, + { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST }, + { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC }, + { "print-winner", no_argument , NULL, PRINT_WINNER }, { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "threads", required_argument, NULL, PARALLEL_THREADS }, + { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT }, + { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH }, { "tlimit" , required_argument, NULL, TIME_LIMIT }, { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, { "rlimit" , required_argument, NULL, RESOURCE_LIMIT }, @@ -428,6 +462,13 @@ throw(OptionException) { const char *progName = argv[0]; int c; + // Reset getopt(), in the case of multiple calls. + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + // find the base name of the program const char *x = strrchr(progName, '/'); if(x != NULL) { @@ -595,6 +636,10 @@ throw(OptionException) { memoryMap = true; break; + case PRINT_WINNER: + printWinner = true; + break; + case STRICT_PARSING: strictParsing = true; break; @@ -807,6 +852,26 @@ throw(OptionException) { optarg + "' is not between 0.0 and 1.0."); } break; + + case SAT_RESTART_FIRST: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-base requires a number bigger than 1"); + } + satRestartFirst = i; + break; + } + + case SAT_RESTART_INC: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-inc requires a number bigger than 1.0"); + } + satRestartInc = i; + } + break; case PIVOT_RULE: if(!strcmp(optarg, "min")) { @@ -905,11 +970,40 @@ throw(OptionException) { printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); + case PARALLEL_THREADS: + threads = atoi(optarg); + break; + + case PARALLEL_SEPARATE_OUTPUT: + separateOutput = true; + break; + + case PORTFOLIO_FILTER_LENGTH: + sharingFilterByLength = atoi(optarg); + break; + case ':': throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); case '?': default: + if(optopt == 0 && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 && + isdigit(argv[optind - 1][8])) { + int tnum = atoi(argv[optind - 1] + 8); + threadArgv.resize(tnum + 1); + if(threadArgv[tnum] != "") { + threadArgv[tnum] += " "; + } + const char* p = strchr(argv[optind - 1] + 9, '='); + if(p == NULL) { // e.g., we have --thread0 "foo" + threadArgv[tnum] += argv[optind++]; + } else { // e.g., we have --thread0="foo" + threadArgv[tnum] += p + 1; + } + break; + } throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); } } |