summaryrefslogtreecommitdiff
path: root/src/util/options.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/options.cpp')
-rw-r--r--src/util/options.cpp113
1 files changed, 100 insertions, 13 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 2352ae503..e9efab5dd 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -149,14 +149,22 @@ Options::Options() :
instWhenMode(INST_WHEN_FULL_LAST_CALL),
eagerInstQuant(false),
finiteModelFind(false),
- fmfRegionSat(false),
+ ufssEagerSplits(false),
+ ufssRegions(true),
+ ufssColoringSat(false),
fmfModelBasedInst(true),
+ fmfInstGen(true),
+ fmfOneInstPerRound(false),
+ fmfInstEngine(false),
+ fmfRelevantDomain(false),
efficientEMatching(false),
literalMatchMode(LITERAL_MATCH_NONE),
cbqi(false),
cbqiSetByUser(false),
userPatternsQuant(true),
flipDecision(false),
+ printInstEngine(false),
+ printModelEngine(false),
lemmaOutputChannel(NULL),
lemmaInputChannel(NULL),
threads(2),// default should be 1 probably, but say 2 for now
@@ -275,6 +283,7 @@ 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\
+ QUANTIFIERS:\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\
@@ -282,18 +291,26 @@ Additional CVC4 options:\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\
+ --register-quant-body-terms consider ground 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\
+ FINITE_MODEL_FINDING:\n\
+ --finite-model-find use finite model finding heuristic for quantifier instantiation\n\
+ --disable-uf-ss-regions disable region-based method for discovering cliques and splits in uf strong solver\n\
+ --uf-ss-eager-split add splits eagerly for uf strong solver\n\
+ --uf-ss-coloring-sat use coloring-based SAT heuristic for uf strong solver\n\
+ --disable-fmf-mbqi disable model-based quantifier instantiation for finite model finding\n\
+ --disable-fmf-inst-gen disable Inst-Gen instantiation techniques for finite model finding\n\
+ --fmf-one-inst-per-round only add one instantiation per quantifier per round for fmf\n\
+ --fmf-inst-engine use instantiation engine in conjunction with finite model finding\n\
+ --fmf-relevant-domain use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)\n\
+ OTHER:\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\
@@ -379,6 +396,36 @@ justification-must\n\
+ near leaves (don't expect it to work well) [Unimplemented]\n\
";
+static const string instWhenHelp = "\
+Modes currently supported by the --inst-when option:\n\
+\n\
+full\n\
++ Run instantiation round at full effort, before theory combination.\n\
+\n\
+full-last-call (default)\n\
++ Alternate running instantiation rounds at full effort and last\n\
+ call. In other words, interleave instantiation and theory combination.\n\
+\n\
+last-call\n\
++ Run instantiation at last call effort, after theory combination.\n\
+\n\
+";
+
+static const string literalMatchHelp = "\
+Literal match modes currently supported by the --literal-match option:\n\
+\n\
+none (default)\n\
++ Do not use literal matching.\n\
+\n\
+predicate\n\
++ Consider the phase requirements of predicate literals when applying heuristic\n\
+ quantifier instantiation. For example, the trigger P( x ) in the quantified \n\
+ formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
+ terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
+ Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+\n\
+";
+
static const string dumpHelp = "\
Dump modes currently supported by the --dump option:\n\
\n\
@@ -581,14 +628,22 @@ enum OptionValue {
INST_WHEN,
EAGER_INST_QUANT,
FINITE_MODEL_FIND,
- FMF_REGION_SAT,
+ DISABLE_UF_SS_REGIONS,
+ UF_SS_EAGER_SPLIT,
+ UF_SS_COLORING_SAT,
DISABLE_FMF_MODEL_BASED_INST,
+ DISABLE_FMF_INST_GEN,
+ FMF_ONE_INST_PER_ROUND,
+ FMF_INST_ENGINE,
+ FMF_RELEVANT_DOMAIN,
EFFICIENT_E_MATCHING,
LITERAL_MATCHING,
ENABLE_CBQI,
DISABLE_CBQI,
IGNORE_USER_PATTERNS,
ENABLE_FLIP_DECISION,
+ PRINT_MODEL_ENGINE,
+ PRINT_INST_ENGINE,
PARALLEL_THREADS,
PARALLEL_SEPARATE_OUTPUT,
PORTFOLIO_FILTER_LENGTH,
@@ -710,14 +765,22 @@ static struct option cmdlineOptions[] = {
{ "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 },
+ { "disable-uf-ss-regions", no_argument, NULL, DISABLE_UF_SS_REGIONS },
+ { "uf-ss-eager-split", no_argument, NULL, UF_SS_EAGER_SPLIT },
+ { "uf-ss-coloring-sat", no_argument, NULL, UF_SS_COLORING_SAT },
+ { "disable-fmf-mbqi", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST },
+ { "disable-fmf-inst-gen", no_argument, NULL, DISABLE_FMF_INST_GEN },
+ { "fmf-one-inst-per-round", no_argument, NULL, FMF_ONE_INST_PER_ROUND },
+ { "fmf-inst-engine", no_argument, NULL, FMF_INST_ENGINE },
+ { "fmf-relevant-domain", no_argument, NULL, FMF_RELEVANT_DOMAIN },
{ "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 },
+ { "print-m-e", no_argument, NULL, PRINT_MODEL_ENGINE },
+ { "print-i-e", no_argument, NULL, PRINT_INST_ENGINE },
{ "threads", required_argument, NULL, PARALLEL_THREADS },
{ "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
{ "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
@@ -1071,7 +1134,7 @@ throw(OptionException) {
if(i == 0) {
Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
<< std::endl << " removing this option." << std::endl;
-
+
}
decisionOptions.maxRelTimeAsPermille = (unsigned short)i;
}
@@ -1247,7 +1310,7 @@ throw(OptionException) {
} else if(!strcmp(optarg, "last-call")) {
instWhenMode = INST_WHEN_LAST_CALL;
} else if(!strcmp(optarg, "help")) {
- //puts(instWhenHelp.c_str());
+ puts(instWhenHelp.c_str());
exit(1);
} else {
throw OptionException(string("unknown option for --inst-when: `") +
@@ -1260,12 +1323,30 @@ throw(OptionException) {
case FINITE_MODEL_FIND:
finiteModelFind = true;
break;
- case FMF_REGION_SAT:
- fmfRegionSat = true;
+ case DISABLE_UF_SS_REGIONS:
+ ufssRegions = false;
+ break;
+ case UF_SS_EAGER_SPLIT:
+ ufssEagerSplits = true;
+ break;
+ case UF_SS_COLORING_SAT:
+ ufssColoringSat = true;
break;
case DISABLE_FMF_MODEL_BASED_INST:
fmfModelBasedInst = false;
break;
+ case DISABLE_FMF_INST_GEN:
+ fmfInstGen = false;
+ break;
+ case FMF_ONE_INST_PER_ROUND:
+ fmfOneInstPerRound = true;
+ break;
+ case FMF_INST_ENGINE:
+ fmfInstEngine = true;
+ break;
+ case FMF_RELEVANT_DOMAIN:
+ fmfRelevantDomain = true;
+ break;
case EFFICIENT_E_MATCHING:
efficientEMatching = true;
break;
@@ -1277,7 +1358,7 @@ throw(OptionException) {
} else if(!strcmp(optarg, "equality")) {
literalMatchMode = LITERAL_MATCH_EQUALITY;
} else if(!strcmp(optarg, "help")) {
- //puts(literalMatchHelp.c_str());
+ puts(literalMatchHelp.c_str());
exit(1);
} else {
throw OptionException(string("unknown option for --literal-matching: `") +
@@ -1298,6 +1379,12 @@ throw(OptionException) {
case ENABLE_FLIP_DECISION:
flipDecision = true;
break;
+ case PRINT_MODEL_ENGINE:
+ printModelEngine = true;
+ break;
+ case PRINT_INST_ENGINE:
+ printInstEngine = true;
+ break;
case TIME_LIMIT:
{
int i = atoi(optarg);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback