diff options
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. |