3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

14252 commits

Author SHA1 Message Date
Nikolaj Bjorner 4628cb8e79 check for negation, not complement 2020-07-28 11:30:35 -07:00
Nikolaj Bjorner 42b42dd89a use bounded pp for cubes 2020-07-28 10:15:16 -07:00
Nikolaj Bjorner f7b2407a11 for #4588 2020-07-28 10:14:56 -07:00
Nikolaj Bjorner 8857a67e4f fix model return after shutdown, reported in #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-27 23:48:19 -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
Murphy Berzish afdfc5e8a6
z3str3: fix incorrect automaton polarity in intersection check, and clean up code (#4595) 2020-07-27 20:11:38 -05: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
Murphy Berzish 2fb914d2a2
z3str3: construct correct counterexamples for string-integer in model construction (#4562) 2020-07-27 14:15:41 -05:00
Nikolaj Bjorner d591bf62c1 add to readme #4575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-27 09:35:50 -07:00
Nikolaj Bjorner 9624df942f na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-27 09:24:35 -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 ae502bc2c4 simplify a few of the several axiom trace commands 2020-07-26 18:02:34 -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 ac39ddb43f flush gmc for sat-preprocessor model bug #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 14:30:48 -07:00
Nikolaj Bjorner e8ef9a85a4 fix #4327
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 13:22:13 -07:00
Nikolaj Bjorner 4be6927460 unused variable warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 13:22:12 -07:00
Nikolaj Bjorner 78afa2527c unused variable warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 13:22:12 -07:00
Nikolaj Bjorner 4d586c2c13 remove stale references to gac/csc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 12:03:03 -07:00
Nikolaj Bjorner 105f97d3ee #4582 again 2020-07-25 15:12:25 -07:00
Nikolaj Bjorner 2133ba06a7 prepare for theory variables othe rthan seq/re 2020-07-25 15:11:13 -07:00
Nikolaj Bjorner f789573d12 prepare for alternative axiom 2020-07-25 15:10:39 -07:00
Nikolaj Bjorner 2d4839f89e #4582 again 2020-07-25 15:09:30 -07:00
Nikolaj Bjorner 1059f6d3b8 #4582 again 2020-07-25 11:54:05 -07:00
Nikolaj Bjorner 963daab268 #4582 again 2020-07-25 11:18:20 -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 e1d2b88a82 access polynomial expressions from algebraic numerals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-23 15:08:11 -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 71a32f5bb2 remove unused
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-22 11:38:27 -07:00
Nikolaj Bjorner 45855fce06 fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-22 10:45:29 -07:00
Nikolaj Bjorner dd5e2e8930 check for 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-22 10:44:00 -07:00
Nikolaj Bjorner 640cf1809d
Merge pull request #4585 from iscottb122/dotnet_fp_significand
Return significand bits correctly (dotnet API). Fixes #4584
2020-07-22 09:59:30 -07:00
Iain Scott b6867d69c2
Return significand bits correctly (dotnet API). Fixes #4584 2020-07-22 16:57:33 +01:00
Nikolaj Bjorner ed58175e1b issue #4582
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-21 18:23:41 -07:00
Nikolaj Bjorner aab50ff3f5 fixing bugs reported in #4518
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-21 15:50:19 -07:00
Nikolaj Bjorner b1824fea10 fix lifetimes for crashes in #4525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-21 12:53:56 -07:00
Nikolaj Bjorner f17ead21f9 fix #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-21 10:11:39 -07:00
Nikolaj Bjorner 1d8d85add9 fix #4575 - correction set resolution only works with uniform weights
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 15:05:06 -07:00
Nikolaj Bjorner ebce0b3612 fix #4577
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 14:40:45 -07:00
Nikolaj Bjorner 61b85d7123 verbosity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 14:11:59 -07:00
Nikolaj Bjorner e8b5abe63e revert - copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 11:17:29 -07:00
Nikolaj Bjorner a7b71239ae copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 10:22:57 -07:00
Nikolaj Bjorner 00491148f0 string
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 10:22:57 -07:00
Nikolaj Bjorner 549ef0e052 fix typos #4573
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 10:22:57 -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 d3ae40130a
Fix rounding bug in mpf_manager. Fixes #2970. 2020-07-16 12:39:12 +00:00
Christoph M. Wintersteiger ccdae7af24
Fix for corner-case in fp.roundToIntegral. Fixes #2894. 2020-07-16 11:58:18 +00:00