* added support for saving state graph in dot format
* moved write_dgml and write_dot under CASSERT
* updated dgml and dot generation a bit so that a state that is both and alive state is detected as having green background but red border when the invariant is vioalted
* Rocco first commit
* Rocco: clean the log
* Rocco: version 0.1 beta of the causality graph
* Rocco: minimal fix to separate lines
* Rocco: fix the enodes
* Rocco: our trace has to reflect same behaviour of the native trace for what concern used_enodes
* Rocco: disable trace when dummy instantiations
* Rocco: fix to enodes
* Update README.md
* Rocco: remove causality details and add the pattern (trigger)
* Rocco: add ; at the end of the bindings
* Rocco: add triggers as separate trace
* Rocco README file
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Update README.md
* Rocco: bug in tout flush
* Update README.md
* Update README.md
* Rocco: clean code
* Ready for pull request
* Remove commented line bindings
* Add space between // and first char
* Substitute or with || for compatibility; Add space around >
* std::cout debugging statements
* comment out std::cout debugging as this is now a shared fork
* convert std::cout to TRACE statements for seq_rewriter and seq_regex
* add cases to min_length and max_length for regexes
* bug fix
* update min_length and max_length functions for REs
* initial pass on simplifying derivative normal forms by eliminating redundant predicates locally
* add seq_regex_brief trace statements
* working on debugging ref count issue
* fix ref count bug and convert trace statements to seq_regex_brief
* add compact tracing for cache hits/misses
* seq_regex fix cache hit/miss tracing and wrapper around is_nullable
* minor
* label and disable more experimental changes for testing
* minor documentation / tracing
* a few more @EXP annotations
* dead state elimination skeleton code
* progress on dead state elimination
* more progress on dead state elimination
* refactor dead state class to separate self-contained state_graph class
* finish factoring state_graph to only work with unsigned values, and implement separate functionality for expr* logic
* implement get_all_derivatives, add debug tracing
* trace statements for debugging is_nullable loop bug
* fix is_nullable loop bug
* comment out local nullable change and mark experimental
* pretty printing for state_graph
* rewrite state graph to remove the fragile assumption that all edges from a state are added at a time
* start of general cycle detection check + fix some comments
* implement full cycle detection procedure
* normalize derivative conditions to form 'ele <= a'
* order derivative conditions by character code
* fix confusing names m_to and m_from
* assign increasing state IDs from 1 instead of using get_id on AST node
* remove elim_condition call in get_dall_derivatives
* use u_map instead of uint_map to avoid memory leak
* remove unnecessary call to is_ground
* debugging
* small improvements to seq_regex_brief tracing
* fix bug on evil2 example
* save work
* new propagate code
* work in progress on using same seq sort for deriv calls
* avoid re-computing derivatives: use same head var for every derivative call
* use min_length on regexes to prune search
* simple implementation of can_be_in_cycle using rank function idea
* add a disabled experimental change
* minor cleanup comments, etc.
* seq_rewriter cleanup for PR
* typo noticed by Nikolaj
* move state graph to util/state_graph
* re-add accidentally removed line
* clean up seq_regex code removing obsolete functions and comments
* a few more cleanup items
* remove experimental functionality for integration
* fix compilation
* remove some tracing and TODOs
* remove old comment
* update copyright dates to 2020
* feedback from Nikolaj
* use [] for map access
* make state_graph methods constant
* avoid recursion in mark_dead_recursive and mark_live_recursive
* a possible bug fix in propagate_nonempty
* write down list of invariants in state_graph
* implement partial invariant check and insert CASSERT statements
* expand on invariant check and tracing
* finish state graph invariant check
* minor tweaks
* regex propagation: convert first two axioms to propagations
* remove obsolete regex solver functionality
Co-authored-by: calebstanford-msr <t-casta@microsoft.com>
* std::cout debugging statements
* comment out std::cout debugging as this is now a shared fork
* convert std::cout to TRACE statements for seq_rewriter and seq_regex
* add cases to min_length and max_length for regexes
* bug fix
* update min_length and max_length functions for REs
* initial pass on simplifying derivative normal forms by eliminating redundant predicates locally
* add seq_regex_brief trace statements
* working on debugging ref count issue
* fix ref count bug and convert trace statements to seq_regex_brief
* add compact tracing for cache hits/misses
* seq_regex fix cache hit/miss tracing and wrapper around is_nullable
* minor
* label and disable more experimental changes for testing
* minor documentation / tracing
* a few more @EXP annotations
* dead state elimination skeleton code
* progress on dead state elimination
* more progress on dead state elimination
* refactor dead state class to separate self-contained state_graph class
* finish factoring state_graph to only work with unsigned values, and implement separate functionality for expr* logic
* implement get_all_derivatives, add debug tracing
* trace statements for debugging is_nullable loop bug
* fix is_nullable loop bug
* comment out local nullable change and mark experimental
* pretty printing for state_graph
* rewrite state graph to remove the fragile assumption that all edges from a state are added at a time
* start of general cycle detection check + fix some comments
* implement full cycle detection procedure
* normalize derivative conditions to form 'ele <= a'
* order derivative conditions by character code
* fix confusing names m_to and m_from
* assign increasing state IDs from 1 instead of using get_id on AST node
* remove elim_condition call in get_dall_derivatives
* use u_map instead of uint_map to avoid memory leak
* remove unnecessary call to is_ground
* debugging
* small improvements to seq_regex_brief tracing
* fix bug on evil2 example
* save work
* new propagate code
* work in progress on using same seq sort for deriv calls
* avoid re-computing derivatives: use same head var for every derivative call
* use min_length on regexes to prune search
* simple implementation of can_be_in_cycle using rank function idea
* add a disabled experimental change
* minor cleanup comments, etc.
* seq_rewriter cleanup for PR
* remove cache hit/miss counts tracing
* remove changes not in the rewriter
* remove cache hit/miss count tracing
Co-authored-by: calebstanford-msr <t-casta@microsoft.com>
* std::cout debugging statements
* comment out std::cout debugging as this is now a shared fork
* convert std::cout to TRACE statements for seq_rewriter and seq_regex
* add cases to min_length and max_length for regexes
* bug fix
* update min_length and max_length functions for REs
* initial pass on simplifying derivative normal forms by eliminating redundant predicates locally
* add seq_regex_brief trace statements
* working on debugging ref count issue
* fix ref count bug and convert trace statements to seq_regex_brief
* add compact tracing for cache hits/misses
* seq_regex fix cache hit/miss tracing and wrapper around is_nullable
* minor
* label and disable more experimental changes for testing
* minor documentation / tracing
* a few more @EXP annotations
* dead state elimination skeleton code
* progress on dead state elimination
* more progress on dead state elimination
* refactor dead state class to separate self-contained state_graph class
* finish factoring state_graph to only work with unsigned values, and implement separate functionality for expr* logic
* implement get_all_derivatives, add debug tracing
* trace statements for debugging is_nullable loop bug
* fix is_nullable loop bug
* comment out local nullable change and mark experimental
* pretty printing for state_graph
* rewrite state graph to remove the fragile assumption that all edges from a state are added at a time
* start of general cycle detection check + fix some comments
* implement full cycle detection procedure
* normalize derivative conditions to form 'ele <= a'
* order derivative conditions by character code
* fix confusing names m_to and m_from
* assign increasing state IDs from 1 instead of using get_id on AST node
* remove elim_condition call in get_dall_derivatives
* use u_map instead of uint_map to avoid memory leak
* remove unnecessary call to is_ground
* debugging
* small improvements to seq_regex_brief tracing
* fix bug on evil2 example
* save work
* new propagate code
* work in progress on using same seq sort for deriv calls
* avoid re-computing derivatives: use same head var for every derivative call
* use min_length on regexes to prune search
* simple implementation of can_be_in_cycle using rank function idea
* add a disabled experimental change
* minor cleanup comments, etc.
* seq_rewriter cleanup for PR
* remove cache hit/miss counts tracing
* remove changes not in the rewriter
* remove cache hit/miss count tracing
Co-authored-by: calebstanford-msr <t-casta@microsoft.com>
Co-authored-by: Caleb Stanford <caleb.pirsquared@gmail.com>
* z3str3: check consistency of str.to_int in fixed length solver
* z3str3: add similar check for int.to_str as well
* z3str3: refactor string-integer conversion check and add post checks for model construction
* regex needs lesson; m.mk_eq not ctx.mk_eq
* when unsat core is of size 0, then do naive learning
* remove two extra comments, and correct positive regex learning
* replace magic numbers for fixed-length lessons with constants
The fix is to remove a hack that used a theory rewriter to simplify
the conversion. Now the conversion happens less often than possible.
Will need more thinking to fix properly.
The unsoundness at this point would cause SPACER to generate lemmas
that do not block a proof obligation and then get stuck in an infinite loop
blocking and generating the same lemma.
