Spacer Global Guidance #6026
Merged
Spacer Global Guidance #6026
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
agurfinkel
force-pushed
the
spacer-gg
branch
4 times, most recently
from
4154ed6
to
4d478de
Compare
|
@NikolajBjorner this is ready for another look. Lightly tested, so don't merge yet. There are issues with formatting (will fix). I left many of the original comments. They don't all make sense now, but they are indicative. |
Minor functions to compute number of free variables, detect presence of certain sub-expressions, etc. The diff is ugly because of clang-format
A cluster of lemmas is a set of lemmas that are all instances of the same pattern, where a pattern is a qff formula with free variables. Currently, the instances are required to be explicit, that is, they are all obtained by substituting concrete values (i.e., numbers) for free variables of the pattern. Lemmas are clustered in cluster_db in each predicate transformer.
spacer_context.(cpp|h) are large and have inconsistent formatting. Disable clang-format for them until merge with main z3 branch and re-format.
Various LA functions. The implementations are somewhat preliminary. Convex closure is simplemented via syntactic convex closure procedure. Kernel computation considers many common cases. spacer_arith_kernel_sage implements kernel computation by call external Sage binary. It is used only for debugging and experiments. There is no link dependence on Sage. If desired, it can be removed.
Generalizes arithmetic inequality literals of the form x <= c, by changing constant c to other constants found in the problem.
Global generalizer checks every new lemma against a cluster of previously learned lemmas, and, if possible, conjectures a new pob, that, when blocked, generalizes multiple existing lemmas.
The option is used to dump state of spacer into json for debugging. It has been replaced by `fp.spacer.trace_file` that allows dumping an execution of spacer. The json file can be reconstructed from the trace file elsewhere.
Issue #3 in hgvk94/z3 Segfault in some proof reduction. Avoid by bailing out on reduction.
The matcher creates substitution using std_order, which is reverse of expected order (variable 0 is last). Adjust the code appropriately for that.
chose level based on pob as well as lemmas
desired_level indicates at which level pob should be proved. A pob will be pushed to desired_level if necessary
the name of success/failed was switched
By default, equality literal t=p is expanded into t<=p && t>=p Disable the expansion in case t contains 'mod' operator since such expansion is usually not helpful for divisibility
A pob might be undef, so weakness must be bumped up
the new level should not be higher than the pob that was generalized
If a generalized pob exist and closed, do not re-create it.
A better implementation of inductive generalizer that in addition to dropping literals also attempts to weaken them. Current implementation is a sketch to be extended based on examples/requirements.
Old code would forget to reset the substitution provided to the sem_matcher. Thus, if the substitution was matched once (i.e., one literal of interest is found), no other literal would be matched.
used for debugging only
pob expressions are normalized to increase syntactic matching. Some of the normalization rules seem out of place, so removing them for now.
If conjecture fails, do not try other generalization strategies -- they will not apply.
do not check that may pob is blocked by existing lemmas. It is likely to be blocked. Our goal is to block it again and generalize to a new lemma. This can be further improved by moving directly to generalization when pob is blocked by existing lemmas...
|
@NikolajBjorner provided that the CI succeeds, this is ready to be merged. |
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.
Global guidance for Spacer
Based on the paper:
Hari Govind VK, Yuting Chen, Sharon Shoham, Arie Gurfinkel: Global Guidance for
Local Generalization in Model Checking. CAV (2) 2020: 101-125
Adds rules to infer patterns in lemmas and generate conjectures based on them.
To enable, use
fp.spacer.global=true, which is disabled by default to preserveexisting behavior. To control individual strategies, see options under
fp.spacer.gg..