Draft
Conversation
to constrain the search space exploration
- forward rewriting (to generate new assumptions) - case splitting - better support for implications - support for arrays - support for quantifier-free formulas (no induction)
+ enhanced simplification of goals/assumptions
* use matchingSet to keep all possible matching of an expression * try rewriting all possible substitutions * use all results instead of front Co-authored-by: Lidiya Chernigovskaya <lidiyachernigovskaya@MacBook-Pro-Lidiya.local>
* fixed the null pointer dereference * reading ADT-constraints as CHCs * fixed ADT preprocessing * Convert CHCs to assumptions and goal for adt-ind * Fix generating goal * Swap equality arguments * enhanced equality elimination + minor fixes * enabled fast SMT implication checks w/timeouts; disabled user-strategies * Add some benchmarks * Try forall for goal * improved nested induction and subgoal handling * Add substitutions in assumptions * Improve substitutions * Create ADT query for all CHCs * Some code refactorings * Copy assumptions before calling adt * Add check that replaced element is not constructor * Keep the last value for return if cannot find anything Co-authored-by: grigoryfedyukovich <grigory.fedyukovich@gmail.com>
* fixed the null pointer dereference * reading ADT-constraints as CHCs * fixed ADT preprocessing * Convert CHCs to assumptions and goal for adt-ind * Fix generating goal * Swap equality arguments * enhanced equality elimination + minor fixes * enabled fast SMT implication checks w/timeouts; disabled user-strategies * Add some benchmarks * Try forall for goal * improved nested induction and subgoal handling * Add substitutions in assumptions * Improve substitutions * Create ADT query for all CHCs * Some code refactorings * Copy assumptions before calling adt * Add check that replaced element is not constructor * Keep the last value for return if cannot find anything * Add new benchmarks and some improvements * Support case when only one variable * Add benchmarks from LEON * add extra lemmas to assumptions * Make changes for Eldarica * Add benchmarks from LEON for adtChc * filter decl ignore function with one argument * fix benchmarks * Support choosing return values * got rid of the LLVM dependency (cherry picked from commit 4aa4e9b) * Use Z3Prover/z3 repository * Fix bsearch-tree10 benchmark * Rename benchmarks Co-authored-by: grigoryfedyukovich <grigory.fedyukovich@gmail.com>
* fixed the null pointer dereference * reading ADT-constraints as CHCs * fixed ADT preprocessing * Convert CHCs to assumptions and goal for adt-ind * Fix generating goal * Swap equality arguments * enhanced equality elimination + minor fixes * enabled fast SMT implication checks w/timeouts; disabled user-strategies * Add some benchmarks * Try forall for goal * improved nested induction and subgoal handling * Add substitutions in assumptions * Improve substitutions * Create ADT query for all CHCs * Some code refactorings * Copy assumptions before calling adt * Add check that replaced element is not constructor * Keep the last value for return if cannot find anything * Add new benchmarks and some improvements * Support case when only one variable * Add benchmarks from LEON * add extra lemmas to assumptions * Make changes for Eldarica * Add benchmarks from LEON for adtChc * filter decl ignore function with one argument * fix benchmarks * Support choosing return values * got rid of the LLVM dependency (cherry picked from commit 4aa4e9b) * Use Z3Prover/z3 repository * Fix bsearch-tree10 benchmark * Rename benchmarks * update leon benchmarks * Add simple unit propagation * Add some clam benchmarks * Check lemmas in adtind benchmarks * Add some fixes to CHC proving process * Fix benchmarks * libraries/dependencies update * Improve algorithm * lemma generalization for nested induction; new benchs * Improve creating definitions * Fixes after merging * Improve converting CHC to function * Fixes for generating and proving definition * Add new benchmarks * Fix finding inductive definition when body consists of 1 conjunct * Add fix to keep non-ADT arguments of the constructors * Use the default adt-ind parameters * Add missing change * Fix generating goal * Fix list_len_butlast benchmark * Return simplifyArithm * add ite to tree_insert_all_size benchmark * Replace findMatchingFromLeftSide with findMatchingFromRule Co-authored-by: grigoryfedyukovich <grigory.fedyukovich@gmail.com>
…to brainstorm ADT-CHC: handling OP_DT_ACCESSOR ad a constructor Handle accessor as a variable Testing delta
Conjuncts: removed not needed class of accessors Conjuncts: removed not needed class of accessors Conjuncts: removed not needed class of accessors Conjuncts: removed not needed class of accessors Conjuncts: debugging Conjuncts: debugging
Conjuncts: TODO Constructor additions: found a place to edit matching between accessors and vars Constructor additions: hacky tamp solution
Accessors: removed comments in CHCSolver Accessors: removed comments in CHCSolver Accessors: removed comments and prints in CHCSolver Accessors: quick replacement fix(it is possible that constructor is done with function call inside, so arity is not necessary 1)
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
No description provided.