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

removing dependencies on simplifier #1226

Merged
merged 81 commits into from
Sep 10, 2017
Merged

removing dependencies on simplifier #1226

merged 81 commits into from
Sep 10, 2017

Conversation

NikolajBjorner
Copy link
Contributor

No description provided.

@delcypher
Copy link
Contributor

Are the commits that add the APIs to manipulate models meant to be in this PR?

@NikolajBjorner
Copy link
Contributor Author

sure, but I am not too organized

@NikolajBjorner
Copy link
Contributor Author

Yes they are included. Just a couple of files

@NikolajBjorner
trying to get rid of last simplifier dependency in macros
ce04c18 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix build
e5826b9 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
removing dependency on simplifier in pattern_inference
655b3d9 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplifier dependencies from ufbv tactics
f062e17 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplifier dependencies from cmakelist.txt files
7dd2878 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Merge branch 'master' of https://github.com/z3prover/z3
8ff8470
@NikolajBjorner
pruning simplifier dependencies
f91496f 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
using rewrite in push_app_ite
8b2d60e 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix build issues
a7bb41f 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
move pull/push files
23d1c0a 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove dead code
5141477 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
update new assertions
ebcacaa 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
moved files
9438ff8 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplify dependencies
ac0bb6a 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplify dependencies
d3c0018 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplify dependencies
b16a4ac 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplify dependencies
2897b98 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplify dependencies
881f90d 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove simplify dependencies
5371315 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
merge
c03be16 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
mising files
14e6b5b 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
mising files
9b53646 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
build fixes
ee4ae33 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
build fixes
10f7343 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
build fixes
eb6b281 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
build fixes
7b9b714 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
doctest fix
09386e4 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
hide new datatype plugin
a3dba5b 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
aligning simplifier and rewriter for regression tests
f12a4f0 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
aligning simplifier and rewriter for regression tests
93474c0 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
re-introduce eq2ineq name for rewriting parameter
5492d0e 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
support for smtlib2.6 datatype parsing
5d17e28 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
support for smtlib2.6 datatype parsing
aac7773 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
support for legacy datatype test
06087c1 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
merge
a1cc21d 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove extra token
1f551f1 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
merge
c708691 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
rename del to remove to avoid compiler error
dabf88b 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix front-end for datatype
9f5bd2f 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix instantiations
d05d3ba 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix parse/print of ADTs
fe02a5f 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fixes
f40a66c 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
merge
68a2db8 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
adding declarations for regression tests
7f127cd 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove unstable sequence interpolant from doc test
2ea9bfa 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
expand select/store in pre-processor
19fa5f8 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
copy declarations
0c9711a 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
iterator -> for
ed6e23f 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
na
04e57e0 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix plugin translation
4fe55cf 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
remove V2 reference
070c699 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner NikolajBjorner merged commit 77008dc into Z3Prover:master Sep 10, 2017
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 @delcypher @msftclas