diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-13 15:04:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-13 20:04:09 +0000 |
| commit | 09cbf1c5746c69854a7578263240101e2430173e (patch) | |
| tree | d68ce1f69fa048a5512de895e38147775be8e730 /src/options | |
| parent | 3a67082f2155760917e72efbd08d15af9d06ab13 (diff) | |
Connect difficulty manager to TheoryEngine (#7161)
This also introduces the produceDifficulty option which is analogous to produceUnsatCores.
It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/smt_options.toml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 7d0dab720..26af86ca2 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -196,6 +196,9 @@ name = "SMT Layer" [[option.mode.ASSUMPTIONS]] name = "assumptions" help = "Produce unsat cores using solving under assumptions and preprocessing proofs." +[[option.mode.PP_ONLY]] + name = "pp-only" + help = "Not producing unsat cores, but tracking proofs of preprocessing (internal only)." [[option]] name = "minimalUnsatCores" @@ -221,6 +224,14 @@ name = "SMT Layer" help = "turn on unsat assumptions generation" [[option]] + name = "produceDifficulty" + category = "regular" + long = "produce-difficulty" + type = "bool" + default = "false" + help = "enable tracking of difficulty." + +[[option]] name = "difficultyMode" category = "regular" long = "difficulty-mode=MODE" |