diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 10 | ||||
-rw-r--r-- | src/util/options.h | 5 |
2 files changed, 14 insertions, 1 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index e9efab5dd..c2b632b32 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -161,6 +161,7 @@ Options::Options() : literalMatchMode(LITERAL_MATCH_NONE), cbqi(false), cbqiSetByUser(false), + rewriteRulesAsAxioms(false), userPatternsQuant(true), flipDecision(false), printInstEngine(false), @@ -294,12 +295,14 @@ Additional CVC4 options:\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\ - --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\ + REWRITERULES:\n\ + --efficient-e-matching use efficient E-matching (only for rewrite rules)\n\ + --rewrite-rules-as-axioms convert rewrite rules into usual axioms (for debugging only)\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\ @@ -642,6 +645,7 @@ enum OptionValue { DISABLE_CBQI, IGNORE_USER_PATTERNS, ENABLE_FLIP_DECISION, + REWRITE_RULES_AS_AXIOMS, PRINT_MODEL_ENGINE, PRINT_INST_ENGINE, PARALLEL_THREADS, @@ -779,6 +783,7 @@ static struct option cmdlineOptions[] = { { "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 }, + { "rewrite-rules-as-axioms", no_argument, NULL, REWRITE_RULES_AS_AXIOMS }, { "print-m-e", no_argument, NULL, PRINT_MODEL_ENGINE }, { "print-i-e", no_argument, NULL, PRINT_INST_ENGINE }, { "threads", required_argument, NULL, PARALLEL_THREADS }, @@ -1379,6 +1384,9 @@ throw(OptionException) { case ENABLE_FLIP_DECISION: flipDecision = true; break; + case REWRITE_RULES_AS_AXIOMS: + rewriteRulesAsAxioms = true; + break; case PRINT_MODEL_ENGINE: printModelEngine = true; break; diff --git a/src/util/options.h b/src/util/options.h index d89265b55..17d393e88 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -484,6 +484,11 @@ struct CVC4_PUBLIC Options { bool cbqiSetByUser; /** + * Whether to convert rewrite rules to usual axioms (for debugging only) + */ + bool rewriteRulesAsAxioms; + + /** * Whether to use user patterns for pattern-based instantiation */ bool userPatternsQuant; |