diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-22 11:33:38 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-22 09:33:38 -0500 |
| commit | bc928d24d7454d81f39006b4129a29286fcd10eb (patch) | |
| tree | 7daf38a8285dc7aad89ae61666e61809cecd8912 /src/smt/proof_manager.h | |
| parent | 3527400d2af35d96a47971db83891b31c47f57ef (diff) | |
Reconciling proofs and unsat cores (#6405)
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
Diffstat (limited to 'src/smt/proof_manager.h')
| -rw-r--r-- | src/smt/proof_manager.h | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index e34947be6..60e93306a 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -46,13 +46,24 @@ class ProofPostproccess; * SmtEngine will not have proofs in the sense of this proof manager. * * - If we are producing unsat cores using this proof infrastructure, then the - * SmtEngine will have proofs using this proof manager (if --produce-proofs - * was not passed by the user it will be activated), but these proofs will - * only cover preprocessing and the prop engine, i.e., the theory engine will - * not have proofs. + * SmtEngine will have proofs using this proof manager, according to the unsat + * core mode: + * + * - assumption mode: proofs only for preprocessing, not in sat solver or + * theory engine, and level of granularity set to off (unless otherwise + * specified by the user) + * + * - sat-proof mode: proofs for preprocessing + sat solver, not in theory + * engine and level of granularity set to off (unless otherwise specified by + * the user) + * + * - full-proof mode: proofs for the whole solver as normal + * + * Note that if --produce-proofs is set then full-proof mode of unsat cores is + * forced. * * - If we are not producing unsat cores then the SmtEngine will have proofs as - * long as --produce-proofs was given. + * long as --produce-proofs is on. * * - If SmtEngine has been configured in a way that is incompatible with proofs * then unsat core production will be disabled. |