Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Debug TreeAutomizer #210

Open
alexandernutz opened this issue Jul 21, 2017 · 0 comments
Open

Debug TreeAutomizer #210

alexandernutz opened this issue Jul 21, 2017 · 0 comments
Assignees
@mostafa-mahmoud @alexandernutz
Labels
TreeAutomizer

Comments

@alexandernutz
Copy link
Member

TreeAutomizer is in a state where all the necessary components should be in place. However there are still many (simple) examples where it does not work.
We need to clean the code, find bugs, etc. to make it a robust Horn clause solver
alexandernutz added a commit that referenced this issue Jul 21, 2017
@alexandernutz
introduced IRankedLetter interface --> every letter in a TreeAutomato…
0a86a0d 
…n's alphabet now needs to have an explicit rank.

Also moved helper files for TreeAutomizer from modelcheckerutils/hornutil to its own library (Library-TreeAutomizer)
Should help with #210
alexandernutz added a commit that referenced this issue Aug 2, 2017
@alexandernutz
bugfix concerning our use of Transformulas for the TreeAutomizer:
de73f26 
 - for typical transformulas it is assumed that any program variable that is neither in invars nor in outvars is just left at the same value
 - the concept of program variables does not fit well for the tree automizer
 - in the end we are suppressing the effects of the removeSuperFlousvars operation during Transformula construction by inserting something like "x = x" for a HornClause of the form "I(x, y), z = y -> J(z, x)"
#210
alexandernutz added a commit that referenced this issue Aug 8, 2017
@alexandernutz
allow constants as arguments of predicates in Horn clause head, #210
dee7336
alexandernutz added a commit that referenced this issue Sep 11, 2017
@alexandernutz
TreeAutomizer: HornClauses with "False" as head are special, added a …
9a1495d 
…flag and constructor indicating that, #210
alexandernutz added a commit that referenced this issue Sep 12, 2017
@alexandernutz
TreeAutomizer: bugfixes concerning handling of variables #210
72f550f
alexandernutz added a commit that referenced this issue Sep 12, 2017
@alexandernutz
added some ad-hoc model output for TreeAutomizer, #210
8423879
alexandernutz added a commit that referenced this issue Dec 7, 2017
@alexandernutz
#210, towards "lazy" difference in TreeAutomizer
8918ceb
alexandernutz added a commit that referenced this issue Dec 7, 2017
@alexandernutz
#210, add TreeAutomizerSettings
68de2a7
@alexandernutz alexandernutz reopened this Dec 12, 2017
alexandernutz added a commit that referenced this issue Jan 17, 2018
@alexandernutz
#210, add a comment
4792925
alexandernutz added a commit that referenced this issue May 24, 2018
@alexandernutz
#210, format comments better
5acd495
alexandernutz added a commit that referenced this issue May 25, 2018
@alexandernutz
#210, Horn clause normalization during parsing: substitute repeating …
e25738a 
…arguments in the head predicate
alexandernutz added a commit that referenced this issue May 25, 2018
@alexandernutz
#210, rework smtlib2 Horn clause parsing: convert to CNF first (keepi…
247d629 
…ng the Boolean structure of interpreted parts intact), then generate horn clauses
alexandernutz added a commit that referenced this issue May 26, 2018
@alexandernutz
#210, towards new normal form for HornClauses: uninterpreted predicat…
cf1378c 
…e applications in the antecedent may have arbitrary terms (breaks TreeAutomizer for the moment..)
alexandernutz added a commit that referenced this issue Jun 12, 2018
@alexandernutz
#210, adapt TreeAutomizer to the infrastructure (parsing, symboltable…
3245312 
…, etc) changes made for #349: adapted Ssa building, hoare triple checker
alexandernutz added a commit that referenced this issue Jun 12, 2018
@alexandernutz
#210, cleanup
0087b92
alexandernutz added a commit that referenced this issue Jun 13, 2018
@alexandernutz
#210, more fixes for restoring TreeAutomizer
b135792
alexandernutz added a commit that referenced this issue Jun 13, 2018
@alexandernutz
#210, #349, #356, give HornAnnot a getter for the HornClauses
0b5964e
alexandernutz added a commit that referenced this issue Jun 13, 2018
@alexandernutz
#210, #349, #356, rename chc library package
6eee535
alexandernutz added a commit that referenced this issue Jun 13, 2018
@alexandernutz
#210, fix merging of states (for minimization, determinization) to ad…
be8ac26 
…apt to recent changes
alexandernutz added a commit that referenced this issue Jun 13, 2018
@alexandernutz
#210, #349, add solver check for formula normalization
d29b549
alexandernutz added a commit that referenced this issue Jun 14, 2018
@alexandernutz
#210, ssa builder was not completely ported to new HornClause format …
afa10fc 
…(body pred args can be arbitrary terms now)
alexandernutz added a commit that referenced this issue Jun 14, 2018
@alexandernutz
#210, make tree automata minimization type a setting
4816f2a
alexandernutz added a commit that referenced this issue Jun 14, 2018
@alexandernutz
#210, guard building of debug output
632b5f8
alexandernutz added a commit that referenced this issue Jun 21, 2018
@alexandernutz
#210, backup commit, has problems
e4072c1
alexandernutz added a commit that referenced this issue Jun 22, 2018
@alexandernutz
#210, TreeAutomizer: fix SSA
ace83c2
alexandernutz added a commit that referenced this issue Jun 22, 2018
@alexandernutz
#210, print more tree automata when debugging
763efd4
alexandernutz added a commit that referenced this issue Jun 22, 2018
@alexandernutz
#210, further revert suspicious (perhaps innocent) change to Minimize…
c0fbc79 
…NftaHopcroft
alexandernutz added a commit that referenced this issue Jun 22, 2018
@alexandernutz
#210, add hashCode and equals for "more" determinism of automata oper…
70a34c1 
…ations
alexandernutz added a commit that referenced this issue Mar 19, 2019
@alexandernutz
#210, fix computation of starts of subtrees for TreeAutomizer tree in…
9f4b786 
…terpolant queries
alexandernutz added a commit that referenced this issue Mar 19, 2019
@alexandernutz
#210, cleanup
18cdd70
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mostafa-mahmoud mostafa-mahmoud

@alexandernutz alexandernutz

Labels
TreeAutomizer
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@mostafa-mahmoud @danieldietsch @alexandernutz