Create a custom ADT for Th_util.answer #1304
Conversation
Halbaroth
force-pushed
the
answer-type
branch
from
24b83cf to
0b0d18d
Compare
An option type is not self-documenting code.
src/lib/reasoners/th_util.mli
Outdated
| (** One does not encounter a contradiction when assuming the negation of the | ||
| literal. It does not imply that the literal is false in the environment, | ||
| as the decision procedures might be incomplete. *) |
There was a problem hiding this comment.
This comment seems misleading — even with a complete decision procedure, if a literal is not entailed, it does not imply that its negation is entailed (there might be models where the literal is true and other models where it is false).
Incompleteness means that the literal might still be entailed even though we were not able to prove that, so I'd suggest something along the line of:
The theory couldn't prove that the literal is entailed by the current environment. This might mean one of several things:
The negation of the literal is entailed by the current environment, or
The truth value of the literal is independent of the current environment (it is true in some models and false in other models), or
The literal is entailed by the current environment but we failed to prove so (in which case the decision procedure used is incomplete).
src/lib/reasoners/th_util.mli
Outdated
| - The explanation [ex] justifies why the literal holds in the | ||
| environment. |
There was a problem hiding this comment.
Might be worth insisting here that this means:
exholds in the current environmentex => litis a tautology
An option type is not self-documenting code.