Plato: Error Messages

[GoogleCodeExporter]

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 [email protected] on 21 Jun 2012 at 3:06