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/smt/set_defaults.cpp | |
| 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/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 6e7939ff7..a226de807 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -81,6 +81,14 @@ void SetDefaults::setDefaultsPre(Options& opts) { opts.driver.dumpUnsatCores = true; } + if (opts.smt.produceDifficulty) + { + if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) + { + opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY; + } + opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; + } if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) @@ -1142,8 +1150,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, bool SetDefaults::safeUnsatCores(const Options& opts) const { // whether we want to force safe unsat cores, i.e., if we are in the default - // ASSUMPTIONS mode, since other ones are experimental - return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS; + // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental + return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS + || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY; } bool SetDefaults::incompatibleWithQuantifiers(Options& opts, |