Conversation
Co-Authored-By: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com>
rcosta358
force-pushed
the
counterexamples
branch
from
bc066d5 to
5e003b7
Compare
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
Awesome! I think we are almost there. I've just left a comment on changing from boolean -> Counterexample for the return value, and returning null's. This isn't the best practice, see if you understand the comment and can make that change
| } | ||
|
|
||
| @Override | ||
| public String getDetails() { |
There was a problem hiding this comment.
shouldnt this be getCounterExample?
There was a problem hiding this comment.
No, that's the specific method from LJDiagnostic to provide additional information in the diagnostic message, so it appears like this:
Error:
(...)
---> <string returned by getDetails>
There was a problem hiding this comment.
Maybe we can split it and call the getCounterexampleString() in the getDetails() because we might want to add more hints besides the counterexample in the future and don't want to mix it up.
| * @throws LJError | ||
| */ | ||
| public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError { | ||
| public Counterexample smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError { |
There was a problem hiding this comment.
I don't love that we just send the Counterexample and if it fails is null :( Maybe we can create an object for SMTResult with fields of boolean checks and List of assignements and functions like .smtChecks or similar and .getCounterExample that can be empty or not. What do you think?
Using null's can lead to nullpointers that we havent anticipated so it would be good to avoid them
There was a problem hiding this comment.
Actually it only fails if the counterexample is not null (no counterexample found).
There was a problem hiding this comment.
But yeah, we should avoid using nulls. I'll try to improve that using your suggestion.
| Symbol name = decl.getName(); | ||
| Expr<?> value = model.getConstInterp(decl); | ||
| // Skip values of uninterpreted sorts | ||
| if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT) |
There was a problem hiding this comment.
What are uninterpreted sorts do we allow them? can you give an example
There was a problem hiding this comment.
Those are the ones that Z3 returns as e.g. !val!0 in the SMT model and we want to skip them there and only deal with them below.
2 participants
This PR adds counterexamples to refinement errors by extracting the SMT model from Z3.
Changes
getCounterexamplemethod toTranslatorToZ3that extracts variable assignments (for constants only)SMTEvaluator, when the SMT returnsSATwe get the SMT model and throw theTypeCheckErrorcontaining the counterexamplebooleanit now returnsCounterexample- if counterexample is null, then the check succeeded, otherwise it failedRefinementError, we override thegetDetailsmethod to add the counterexamples as extra information in the error message. Also, it filters out fresh variables which don't even exist in the source code, and if the counterexample is the same as the found type (already included in the message), then the counterexample is not shown.TranslatorToZ3, we keep track of the function applications and expressions sent to Z3 so we can reconstruct them from the counterexample when dealing with uninterpreted ghost functionsExamples