Plato doesn't yet accept error messages for constraints.
This is partly by design because when Plato combines constraints it would then
need to generate a new error message for the combination.
Implementationally, it is hard to do that because we're using Snark to compute
the resolution closure.
Suggestion: attach error messages only to the original constraints. For the
case when the resolution closure is just the original theory, everything works
out (which is always true for non-interacting constraints---a common case). Or
even more simply, just keep the error messages around for complete theories.
Syntactically, we can change the input language for constraints so that they
are ...
(formula1 "explanation1" formula2 "explanation2" ....)
Internally, perhaps we can just maintain a simple alist (formulai .
"explanationi"). Then when we convert each formula to clausal form, we just
replicate explanationi for each clause generated from formulai. Finally, when
doing the compilation we simply check if for an error message using sent-equal.
Original issue reported on code.google.com by thinr...@gmail.com on 21 Jun 2012 at 3:06
Original issue reported on code.google.com by
thinr...@gmail.com
on 21 Jun 2012 at 3:06