Counter Example generation #652
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ple bodies, causing no counter example to be generated. Actually fetches counter examples from the smt solve now.
…uses (if any). Put feature gate behind counter example generation.
…void infinite recursion on cyclic kvars.
…unterexample files with incorrect spelling
…ample now uses the local bind environment to get accurate types.
…conjuncted in Counterexample checker
…ded JSON output for Counterexample
…d issue where head constraint was removed from the environment.
…ssert and underconstraint kvars when recursion depth was reached
… caused the checker to do nothing
…ate lists of the correct length. Renamed counterexample SMT functions.
…d it from the counterexample generation.
…nements if it included kvars
…ntical module transitively equivalent variables)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Here's a pull request for the counter example generation. It seems to produce sensible outputs for most programs.
The one key thing that should still be added is adding all relevant bindings to the final counter example. Currently, we just get all bindings for constraints that don't have a KVar on the rhs. This should be changed to fetch the bindings for all constraints.
The issue then is that sometimes there may be multiple assignments for a binding (I think at least) and we have to distinguish which assignment was the offending one. There's two cases for this.
The first one being from a loop, where I think that just taking the first occurrence should be fine.
The second one being from the usage of a variable in two different branches. Here it is not immediately obvious how to get back the correct assignment.