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

Seq rewriter integration #4597

Merged
merged 66 commits into from
Jul 28, 2020
Merged

Seq rewriter integration #4597

merged 66 commits into from
Jul 28, 2020

Conversation

NikolajBjorner
Copy link
Contributor

No description provided.

calebstanford-msr and others added 30 commits June 9, 2020 16:43
@calebstanford-msr
std::cout debugging statements
2e676ff
@calebstanford-msr
comment out std::cout debugging as this is now a shared fork
03b05f2
@calebstanford-msr
Merge remote-tracking branch 'upstream/master'
a3a16fa
@calebstanford-msr
convert std::cout to TRACE statements for seq_rewriter and seq_regex
231f0d6
@calebstanford-msr
Merge remote-tracking branch 'upstream/master'
02a83f3
@calebstanford-msr
add cases to min_length and max_length for regexes
fb7ffe9
@calebstanford-msr
bug fix
20962e2
@calebstanford-msr
Merge remote-tracking branch 'upstream/master'
3359864
@calebstanford-msr
Merge remote-tracking branch 'upstream/master'
3086e8c
@calebstanford-msr
update min_length and max_length functions for REs
8b129ce
@calebstanford-msr
initial pass on simplifying derivative normal forms by eliminating re…
a98ca80 
…dundant predicates locally
@calebstanford-msr
add seq_regex_brief trace statements
42cb8b6
@calebstanford-msr
working on debugging ref count issue
177b04a
@cdstanford
fix ref count bug and convert trace statements to seq_regex_brief
06bc1cd
@cdstanford
Merge remote-tracking branch 'upstream/master'
b17c2f5 
(and revert an experimental change where BDDs aren't sorted by get_id)
@cdstanford
add compact tracing for cache hits/misses
94d9db3
@cdstanford
seq_regex fix cache hit/miss tracing and wrapper around is_nullable
7f53dca
@cdstanford
Merge remote-tracking branch 'upstream/master'
4a09176
@cdstanford
Merge remote-tracking branch 'upstream/master'
8c87c0d
@cdstanford
minor
ed804dc
@cdstanford
Merge remote-tracking branch 'upstream/master'
8e43538
@cdstanford
label and disable more experimental changes for testing
a7df4e5
@cdstanford
minor documentation / tracing
e074fb3
@cdstanford
a few more @exp annotations
4e2ba58
@cdstanford
dead state elimination skeleton code
f610d3a
@cdstanford
progress on dead state elimination
4e5873e
@cdstanford
more progress on dead state elimination
1f1f127
@cdstanford
refactor dead state class to separate self-contained state_graph class
d96a274
@cdstanford
finish factoring state_graph to only work with unsigned values, and i…
47f45fa 
…mplement separate functionality for expr* logic
@cdstanford
Merge remote-tracking branch 'upstream/master'
552e627
cdstanford added 25 commits June 30, 2020 22:10
@cdstanford
order derivative conditions by character code
1543ca7
@cdstanford
fix confusing names m_to and m_from
11bda7e
@cdstanford
assign increasing state IDs from 1 instead of using get_id on AST node
4b5a89e
@cdstanford
remove elim_condition call in get_dall_derivatives
e12bf86
@cdstanford
use u_map instead of uint_map to avoid memory leak
938dc43
@cdstanford
remove unnecessary call to is_ground
2a735b7
@cdstanford
debugging
448e673
@cdstanford
small improvements to seq_regex_brief tracing
0fd25e0
@cdstanford
Merge remote-tracking branch 'upstream/master'
62fe8c4
@cdstanford
fix bug on evil2 example
1fc751f
@cdstanford
save work
0fa8396
@cdstanford
new propagate code
5623024
@cdstanford
work in progress on using same seq sort for deriv calls
17e0ef1
@cdstanford
avoid re-computing derivatives: use same head var for every derivativ…
6cb1ef9 
…e call
@cdstanford
use min_length on regexes to prune search
becbdba
@cdstanford
simple implementation of can_be_in_cycle using rank function idea
a1da9ae
@cdstanford
add a disabled experimental change
2000012
@cdstanford
minor cleanup comments, etc.
3f55875
@cdstanford
Merge remote-tracking branch 'upstream/master'
1ed1c9d
@cdstanford
Merge remote-tracking branch 'upstream/master'
dd00829
@cdstanford
seq_rewriter cleanup for PR
0c33f03
@cdstanford
Merge remote-tracking branch 'upstream/master'
ccbf741
@cdstanford
remove cache hit/miss counts tracing
4766192
@cdstanford
remove changes not in the rewriter
8761356
@cdstanford
remove cache hit/miss count tracing
95d65f5
@NikolajBjorner
Copy link
Contributor Author

Caleb's updates

@NikolajBjorner NikolajBjorner merged commit e90f010 into Z3Prover:master Jul 28, 2020
NikolajBjorner added a commit that referenced this pull request Jul 28, 2020
@NikolajBjorner
Revert "Seq rewriter integration (#4597)"
d1e9660 
This reverts commit e90f010.
@NikolajBjorner NikolajBjorner mentioned this pull request Jul 28, 2020
Merged
NikolajBjorner added a commit that referenced this pull request Jul 28, 2020
@NikolajBjorner
Revert "Seq rewriter integration (#4597)" (#4598)
6910c0d 
This reverts commit e90f010.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@NikolajBjorner @calebstanford-msr @cdstanford