diff options
Diffstat (limited to 'src/util/options.cpp')
| -rw-r--r-- | src/util/options.cpp | 176 |
1 files changed, 169 insertions, 7 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index 26881e052..1296fa5af 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -130,6 +130,25 @@ Options::Options() : arithRewriteEqSetByUser(false), ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), + miniscopeQuant(true), + miniscopeQuantFreeVar(true), + prenexQuant(true), + varElimQuant(false), + cnfQuant(false), + preSkolemQuant(false), + smartTriggers(true), + registerQuantBodyTerms(false), + instWhenMode(INST_WHEN_FULL_LAST_CALL), + eagerInstQuant(false), + finiteModelFind(false), + fmfRegionSat(false), + fmfModelBasedInst(true), + efficientEMatching(false), + literalMatchMode(LITERAL_MATCH_NONE), + cbqi(false), + cbqiSetByUser(false), + userPatternsQuant(true), + flipDecision(false), lemmaOutputChannel(NULL), lemmaInputChannel(NULL), threads(2),// default should be 1 probably, but say 2 for now @@ -240,6 +259,27 @@ Additional CVC4 options:\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\ CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ + --disable-miniscope-quant disable miniscope quantifiers\n\ + --disable-miniscope-quant-fv disable miniscope quantifiers for ground subformulas\n\ + --disable-prenex-quant disable prenexing of quantified formulas\n\ + --var-elim-quant enable variable elimination of quantified formulas\n\ + --cnf-quant apply CNF conversion to quantified formulas\n\ + --pre-skolem-quant apply skolemization eagerly to bodies of quantified formulas\n\ + --disable-smart-triggers disable smart triggers\n\ + --register-quant-body-terms consider terms within bodies of quantified formulas for matching\n\ + --inst-when=MODE when to apply instantiation\n\ + --eager-inst-quant apply quantifier instantiation eagerly\n\ + --finite-model-find use finite model finding heuristic for quantifier instantiation\n\ + --use-fmf-region-sat use region-based SAT heuristic for finite model finding\n\ + --disable-fmf-model-inst disable model-based instantiation for finite model finding\n\ + --efficient-e-matching use efficient E-matching\n\ + --literal-matching=MODE choose literal matching mode\n\ + --enable-cbqi turns on counterexample-based quantifier instantiation [off by default]\n\ + --disable-cbqi turns off counterexample-based quantifier instantiation\n\ + --ignore-user-patterns ignore user-provided patterns for quantifier instantiation\n\ + --enable-flip-decision turns on flip decision heuristic\n\ + --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\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\ @@ -439,7 +479,7 @@ void Options::printLanguageHelp(std::ostream& out) { */ enum OptionValue { OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */ - SMTCOMP, + SMTCOMP, STATS, SEGV_NOSPIN, OUTPUT_LANGUAGE, @@ -496,6 +536,25 @@ enum OptionValue { DISABLE_ARITHMETIC_REWRITE_EQUALITIES, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, + DISABLE_MINISCOPE_QUANT, + DISABLE_MINISCOPE_QUANT_FV, + DISABLE_PRENEX_QUANT, + VAR_ELIM_QUANT, + CNF_QUANT, + PRE_SKOLEM_QUANT, + DISABLE_SMART_TRIGGERS, + REGISTER_QUANT_BODY_TERMS, + INST_WHEN, + EAGER_INST_QUANT, + FINITE_MODEL_FIND, + FMF_REGION_SAT, + DISABLE_FMF_MODEL_BASED_INST, + EFFICIENT_E_MATCHING, + LITERAL_MATCHING, + ENABLE_CBQI, + DISABLE_CBQI, + IGNORE_USER_PATTERNS, + ENABLE_FLIP_DECISION, PARALLEL_THREADS, PARALLEL_SEPARATE_OUTPUT, PORTFOLIO_FILTER_LENGTH, @@ -602,6 +661,25 @@ static struct option cmdlineOptions[] = { { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "disable-miniscope-quant", no_argument, NULL, DISABLE_MINISCOPE_QUANT }, + { "disable-miniscope-quant-fv", no_argument, NULL, DISABLE_MINISCOPE_QUANT_FV }, + { "disable-prenex-quant", no_argument, NULL, DISABLE_PRENEX_QUANT }, + { "var-elim-quant", no_argument, NULL, VAR_ELIM_QUANT }, + { "cnf-quant", no_argument, NULL, CNF_QUANT }, + { "pre-skolem-quant", no_argument, NULL, PRE_SKOLEM_QUANT }, + { "disable-smart-triggers", no_argument, NULL, DISABLE_SMART_TRIGGERS }, + { "register-quant-body-terms", no_argument, NULL, REGISTER_QUANT_BODY_TERMS }, + { "inst-when", required_argument, NULL, INST_WHEN }, + { "eager-inst-quant", no_argument, NULL, EAGER_INST_QUANT }, + { "finite-model-find", no_argument, NULL, FINITE_MODEL_FIND }, + { "use-fmf-region-sat", no_argument, NULL, FMF_REGION_SAT }, + { "disable-fmf-model-inst", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST }, + { "efficient-e-matching", no_argument, NULL, EFFICIENT_E_MATCHING }, + { "literal-matching", required_argument, NULL, LITERAL_MATCHING }, + { "enable-cbqi", no_argument, NULL, ENABLE_CBQI }, + { "disable-cbqi", no_argument, NULL, DISABLE_CBQI }, + { "ignore-user-patterns", no_argument, NULL, IGNORE_USER_PATTERNS }, + { "enable-flip-decision", no_argument, NULL, ENABLE_FLIP_DECISION }, { "threads", required_argument, NULL, PARALLEL_THREADS }, { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT }, { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH }, @@ -984,7 +1062,7 @@ throw(OptionException) { case 'm': produceModels = true; break; - + case PRODUCE_ASSIGNMENTS: produceAssignments = true; break; @@ -1016,7 +1094,7 @@ throw(OptionException) { throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used"); #endif /* CVC4_PROOF */ break; - + case NO_TYPE_CHECKING: typeChecking = false; earlyTypeChecking = false; @@ -1073,7 +1151,91 @@ throw(OptionException) { ufSymmetryBreaker = false; ufSymmetryBreakerSetByUser = true; break; - + case DISABLE_MINISCOPE_QUANT: + miniscopeQuant = false; + break; + case DISABLE_MINISCOPE_QUANT_FV: + miniscopeQuantFreeVar = false; + break; + case DISABLE_PRENEX_QUANT: + prenexQuant = false; + break; + case VAR_ELIM_QUANT: + varElimQuant = true; + break; + case CNF_QUANT: + cnfQuant = true; + break; + case PRE_SKOLEM_QUANT: + preSkolemQuant = true; + break; + case DISABLE_SMART_TRIGGERS: + smartTriggers = false; + break; + case REGISTER_QUANT_BODY_TERMS: + registerQuantBodyTerms = true; + break; + case INST_WHEN: + if(!strcmp(optarg, "pre-full")) { + instWhenMode = INST_WHEN_PRE_FULL; + } else if(!strcmp(optarg, "full")) { + instWhenMode = INST_WHEN_FULL; + } else if(!strcmp(optarg, "full-last-call")) { + instWhenMode = INST_WHEN_FULL_LAST_CALL; + } else if(!strcmp(optarg, "last-call")) { + instWhenMode = INST_WHEN_LAST_CALL; + } else if(!strcmp(optarg, "help")) { + //puts(instWhenHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --inst-when: `") + + optarg + "'. Try --inst-when help."); + } + break; + case EAGER_INST_QUANT: + eagerInstQuant = true; + break; + case FINITE_MODEL_FIND: + finiteModelFind = true; + break; + case FMF_REGION_SAT: + fmfRegionSat = true; + break; + case DISABLE_FMF_MODEL_BASED_INST: + fmfModelBasedInst = false; + break; + case EFFICIENT_E_MATCHING: + efficientEMatching = true; + break; + case LITERAL_MATCHING: + if(!strcmp(optarg, "none")) { + literalMatchMode = LITERAL_MATCH_NONE; + } else if(!strcmp(optarg, "predicate")) { + literalMatchMode = LITERAL_MATCH_PREDICATE; + } else if(!strcmp(optarg, "equality")) { + literalMatchMode = LITERAL_MATCH_EQUALITY; + } else if(!strcmp(optarg, "help")) { + //puts(literalMatchHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --literal-matching: `") + + optarg + "'. Try --literal-matching help."); + } + break; + case ENABLE_CBQI: + cbqi = true; + cbqiSetByUser = true; + break; + case DISABLE_CBQI: + cbqi = false; + cbqiSetByUser = true; + break; + case IGNORE_USER_PATTERNS: + userPatternsQuant = false; + break; + case ENABLE_FLIP_DECISION: + flipDecision = true; + break; case TIME_LIMIT: { int i = atoi(optarg); @@ -1141,7 +1303,7 @@ throw(OptionException) { optarg + "' is not between 0.0 and 1.0."); } break; - + case SAT_RESTART_FIRST: { int i = atoi(optarg); @@ -1151,7 +1313,7 @@ throw(OptionException) { satRestartFirst = i; break; } - + case SAT_RESTART_INC: { int i = atoi(optarg); @@ -1341,7 +1503,7 @@ throw(OptionException) { case PORTFOLIO_FILTER_LENGTH: sharingFilterByLength = atoi(optarg); - break; + break; case ':': // This can be a long or short option, and the way to get at the name of it is different. |