3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Commit graph

2110 commits

Author SHA1 Message Date
Nikolaj Bjorner
a74ef394ec some more rewrites 2020-07-30 10:19:32 -07:00
Nikolaj Bjorner
4628cb8e79 check for negation, not complement 2020-07-28 11:30:35 -07:00
Nikolaj Bjorner
f7b2407a11 for #4588 2020-07-28 10:14:56 -07:00
Nikolaj Bjorner
b71a64365d sketch fixed-length heuristic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-27 19:34:32 -07:00
Caleb Stanford
5664b570a3
Seq rewriter integration (#4599)
* 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>
2020-07-27 19:08:45 -07:00
Nikolaj Bjorner
6910c0d5eb
Revert "Seq rewriter integration (#4597)" (#4598)
This reverts commit e90f01006c.
2020-07-27 18:10:14 -07:00
Nikolaj Bjorner
e90f01006c
Seq rewriter integration (#4597)
* 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>
2020-07-27 18:08:51 -07:00
Nikolaj Bjorner
a08082e392 fix #4594
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-27 09:22:53 -07:00
Nikolaj Bjorner
c7704ef9af pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 17:52:28 -07:00
Nikolaj Bjorner
e63992c8bd fix #4589
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-24 15:46:54 -07:00
Nikolaj Bjorner
780346c7ca address model generation bugs raised in #4518 and #4324
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-24 13:22:19 -07:00
Nikolaj Bjorner
a6a041ec5d setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. Fixing conservative setting to be after constructor in asserted_formulas. fixes #4586
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-23 13:43:54 -07:00
Nikolaj Bjorner
ebce0b3612 fix #4577
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 14:40:45 -07:00
Christoph M. Wintersteiger
a298091322
Fix for fp.roundToIntegral of tiny, denormal floats. Fixes #4190. 2020-07-17 15:58:01 +00:00
Christoph M. Wintersteiger
2ef57d7f8d
Fix FP rounding of huge exponents. Fixes #3776. 2020-07-17 13:42:12 +00:00
Christoph M. Wintersteiger
ccdae7af24
Fix for corner-case in fp.roundToIntegral. Fixes #2894. 2020-07-16 11:58:18 +00:00
Nuno Lopes
122f5a1464 remove unused field 2020-07-12 23:12:00 +01:00
Nuno Lopes
bb26f219fe remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
Nuno Lopes
23e6adcad3 fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
Nikolaj Bjorner
65e6b73873 fix #4538 - regression when renaming family from special_relations to specrels
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-08 14:46:40 -07:00
Nikolaj Bjorner
80cc45c5c1 display justifications compactly for tracing #4575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-08 13:32:41 -07:00
Christoph M. Wintersteiger
3776588375
Clarify bit-blasting of fp.neg. Fixes #4466. 2020-07-08 18:24:08 +00:00
Christoph M. Wintersteiger
c59519bf9c
Add missing FP conversion. Fixes #4470. 2020-07-08 17:56:25 +00:00
Nikolaj Bjorner
d0e20e44ff booyah
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
5987d9ae20 cache computing strings and regexes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-02 11:14:29 -07:00
Nikolaj Bjorner
d91ca423ab enforce reference count ownership in context of mk_derivative calls.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-01 13:13:17 -07:00
Nikolaj Bjorner
9a642215eb avoid infinite loop between is-nullable and mk-bool-app
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-28 10:27:47 -07:00
Nikolaj Bjorner
8758baf24e perf and div/mod axioms #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-22 14:51:58 -07:00
Nuno Lopes
fdeba2102c fix deref of free'd memory in mk_fresh_const 2020-06-18 19:25:32 +01:00
Nikolaj Bjorner
3b1149330d enable theory propagation of regex accept condition
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-17 13:42:40 -07:00
Nikolaj Bjorner
41430cd128 register unhandled expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-12 16:12:24 -07:00
Nikolaj Bjorner
5a2b6d9c92 bounds on loop expressions 2020-06-11 00:04:41 -07:00
Nikolaj Bjorner
e3d45b9850 refcount leaks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-09 14:19:26 -07:00
Nikolaj Bjorner
4fdfc65b37 tune seq rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-09 13:30:39 -07:00
Nikolaj Bjorner
08cc5bc2e5 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-09 11:39:26 -07:00
calebstanford-msr
1fd567d1e9
fix bug in seq rewriter op_cache::find (#4509)
* remove unneeded reverse case in derivative; placeholder for generalized lifted derivative

* experimental tweaks to RE rewriter to improve performance

* if-then-else lifting
(broken code -- preserving this commit in case this idea is useful later)

* if-then-else derivative optimizations: new approach templates

* implement if-then-else BDD normal form for derivatives
(code compiles but is still buggy)

* remove std::cout debugging for PR

* Revert "remove std::cout debugging for PR"

This reverts commit c7bdc44d31.

* debugging

* fix derivative interaction with reverse; add flags for left/right derivative and lifting over union/intersection

* remove debugging statements for PR

* Revert "remove debugging statements for PR"

This reverts commit 38e85a7288.

* revert some purely cosmetic changes from upstream; fix a bug

* revert unnecessary changes

* remove some redundant rewrites and add a new one for str.in_re(s, comp(r))

* add disabled rewrite for complement

* fix bug in op cache find (result was not saved)

* remove debugging std::cout for PR
2020-06-09 11:36:31 -07:00
Nikolaj Bjorner
d2a12f6db5 tuning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-07 12:52:13 -07:00
Nikolaj Bjorner
ba1ca33637 normalization of union/intersection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-06 12:54:44 -07:00
Nikolaj Bjorner
1b9fcc7098 integrate ite-normalized derivatives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-05 17:28:48 -07:00
Nikolaj Bjorner
4dbf7b183d inline conditions with derivative computation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-05 13:51:31 -07:00
Nikolaj Bjorner
59e388ece1 handle bind proof constructor and print lambda
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-04 11:59:59 -07:00
Nikolaj Bjorner
b013df9a9f fix #4431
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-04 00:47:27 -07:00
Nuno Lopes
e844aef896 remove a few more copy constructors, though still not enough to enable the assertion in vector
I give up for now; there are too many copies left for little return..
2020-06-03 20:32:13 +01:00
Nuno Lopes
7ac2791482 remove a bunch of constructors to avoid copies
still not enough to guarantee that vector::expand doesnt copy (WIP)
2020-06-03 17:09:27 +01:00
Nuno Lopes
98b5abb1d4 buffer: require a move constructor to avoid copies
remove unneded copy constructors from several classes
2020-06-03 11:57:49 +01:00
Nikolaj Bjorner
d3e20d41b2 fix $4457
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-02 18:31:28 -07:00
Nikolaj Bjorner
bfb5c95b9a use op-cache for is-nullable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-02 13:30:18 -07:00
Nikolaj Bjorner
e388055a33 connecting op-cache
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-02 13:13:32 -07:00
Nikolaj Bjorner
4ef480e2a5 add op cache
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-02 12:52:42 -07:00
Nikolaj Bjorner
2da7a8dd70 fix #4491
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-01 20:12:41 -07:00