mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity
16264 commits 23 branches 48 tags 157 MiB
Commit graph

202 commits

Author SHA1 Message Date
Nikolaj Bjorner e1929ca9b9 add regex power to API and for Java per request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-15 19:18:33 -07:00
Margus Veanes be38b256c8
fixed bug in is_char_const_range (#5724) 2021-12-19 17:46:42 -08:00
Margus Veanes a7b1db611c
State graph dgml update and fixes in condition simplifier (#5721) 
* improved generated dgml graph

* fixed simplification of negated ranges and did some code cleanup

* do not make loops with lower=upper=0, this is epsilon

* do not add loops with lower=upper=1

* bug fix in normalization: forgotten eps case
 2021-12-19 11:09:55 -08:00
Margus Veanes 2be93870c8
Cleanup regex info and some fixes in Derivative code (#5709) 
* removed unused regex info fields

* cleanup of info and fixes in antimirov derivatives

* removed extra qualification on operator
 2021-12-15 10:59:34 -08:00
Nikolaj Bjorner 96e871c826 add stub for testing updates to scoped_timer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-12 12:31:23 -08:00
Nikolaj Bjorner 51fa40ece5 fix spelling 2021-12-09 10:23:37 -08:00
Nikolaj Bjorner 518ef9f916 fix #5674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 21:14:50 -08:00
Margus Veanes efcad5ff35
fixed nullability bug in the if-then-else info (#5620) 2021-10-26 09:11:07 +02:00
Nikolaj Bjorner fb9fa1b7d2 updated printer 2021-10-15 17:56:54 -07:00
Margus Veanes cb120c93f4
Regex range bug fix (#5601) 
* added a missing derivative case for nonground range

* further missing cases and a bug fix in re.to_str
 2021-10-15 15:30:55 -07:00
Nikolaj Bjorner 0fc9f1d46a fix max/min length to handle concatenation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-09 16:20:32 -07:00
Margus Veanes 146f4621c5
Updated regex derivative engine (#5567) 
* updated derivative engine

* some edit

* further improvements in derivative code

* more deriv code edits and re::to_str update

* optimized mk_deriv_accept

* fixed PR comments

* small syntax fix

* updated some simplifications

* bugfix:forgot to_re before reverse

* fixed PR comments

* more PR comment fixes

* more PR comment fixes

* forgot to delete

* deleting unused definition

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-08 13:04:49 -07:00
Nikolaj Bjorner f13ccf8969 bv2char and char2bv with Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-13 16:09:03 +02:00
Nikolaj Bjorner 3eb849ad9e rewrite equality too 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-09 15:32:04 -07:00
Margus Veanes 225204e2f4
updates related to issue #5140 (#5463) 
* updates related to issue #5140

* updated/simplified some cases

* fixing feedback comments

* fixed comments and added missing case for get_re_head_tail_reversed

* two bug fixes and some other code improvements
 2021-08-09 10:48:56 -07:00
CEisenhofer 0fa4b63d26
Added sbv2s (#5413) 
* Added sbv2s

* Fixed indention

Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
 2021-07-16 17:58:28 +02:00
Nikolaj Bjorner e5c5caea45 add call to function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 09:19:20 +02:00
Nikolaj Bjorner 1bc10cebc5 add ubv2s step 1 2021-07-12 12:53:00 +02:00
Nikolaj Bjorner 5d3f48cc8d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-07 09:51:39 -07:00
Nikolaj Bjorner 92ec81d108 #5140 
@veanes
mk_bool_app_helper has a bug:
When it simplifies a disjunction or conjunction of regex membership constraints of the form (and (str.in_re "" R) (str.in_re x Q))
then the first term (str.in_re "" R) is omitted in the result.
You have a test here
3da9d91866/src/ast/rewriter/seq_rewriter.cpp (L438)
that means a regex membership with empty first argument is not put in the two buffers with membership/non-membership.
It isn't put into new_args either because the test bypasses these
3da9d91866/src/ast/rewriter/seq_rewriter.cpp (L485)
 2021-06-06 20:30:09 -07:00
Nikolaj Bjorner 262daf5151 symbol/zstring transition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:54:21 -07:00
Nikolaj Bjorner 20a67e47ca remove symbol -> zstring -> symbol round-trips 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:12:49 -07:00
Margus Veanes 8ca6f567d3
fixing issue #5140 (#5268) 2021-05-16 13:53:08 -07:00
Nikolaj Bjorner 8263d20e0d add code review comment 2021-04-20 11:30:25 -07:00
Nikolaj Bjorner 9098084217 reduce overhead of creating seq-plugin, enable parameter cleanup for #5095 2021-03-15 11:54:44 -07:00
Nikolaj Bjorner 612cc5cfba fix #5014 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-12 16:01:33 -08:00
Nikolaj Bjorner 8fffc03263 remove bv dependencies 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 0f29fff836 remove bit-vector dependencies in seq theory 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 4455f6caf8 move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail 2021-02-02 03:58:19 -08:00
Nikolaj Bjorner 520b24aab4 string escaping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 04:58:58 -08:00
Nikolaj Bjorner 909257f856 remove family id externals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:48:24 -08:00
Nikolaj Bjorner d3564f5b50 move unicode toggle to char-plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:42:19 -08:00
Nikolaj Bjorner e969bd1c97 fully remove seq-based characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:26:44 -08:00
Nikolaj Bjorner 696b3c79b9 fixes to self-contained character unicode 2021-01-27 06:13:37 -08:00
Nikolaj Bjorner d0f1d8f59e move to unicode as stand-alone theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 05:46:45 -08:00
Nikolaj Bjorner 20332c6d3e adding char decl plugin for separate theory treatment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 16:28:44 -08:00
Nikolaj Bjorner 33714ceb40 use _ 2021-01-26 14:56:48 -08:00
Nikolaj Bjorner 7dd7d83a36 make it easier to use string literals 2021-01-26 11:01:03 -08:00
Nikolaj Bjorner 47cb1d1207 remove bit-vector dependencies in theory_str_mc. See discussion #4939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 13:03:06 -08:00
Nikolaj Bjorner 03fd251ccb streamline unicode/ascii toggling. Fix bit-width for unicode to 18 2021-01-23 11:11:44 -08:00
Nikolaj Bjorner 4e8ba8b160 regression fix, fix unicode mode 2021-01-21 22:06:15 -08:00
Nikolaj Bjorner dafee71500 reshuffle unicode support to use global parameter, and use bit-vectors on demand 2021-01-21 14:24:26 -08:00
Nikolaj Bjorner 5d10cb7af4 fix #4791 - diff is left associative 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-11 18:07:05 -08:00
Nikolaj Bjorner d64bc795f0 wrong assert, compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 10:10:59 -07:00
Margus Veanes af54a79acc
fixing issue #4651 (#4666) 
* fixing issue #4651

* regression fix

* fix #4662

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate

* removing temp testing variable

* Allow to skip System.loadLibrary() calls from Java Native class (#4667)

* using intended utility methods for sort detection

* adding ack/model

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add smt params dependency

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* order

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* persist fields

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dbg build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* reset caches

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* sr

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix cmake build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* shuffle dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* warnings /errors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* update include

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing cmakelists

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* update cmake

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add depend

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add depend

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* path

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move parameters from ast/rewriter to params

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move fpa

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove pragma

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dbg

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* updated sat_smt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4651

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* encoding options #4665

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* expose name inclusion as optional

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix misc issues around #4661 introduced when adding lazy push/pop to selected theories

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove lazy push from theory_lra

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix dotnet build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* release nodes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* free memory in egraph

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid duplicate class names frame in sat_scc and sat_smt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding euf

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* elaborate on smt/drat format outline, expose euf mode as config

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* mk-var during copy

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* with bounded

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Remove duplicate binary condition. Fixes #4668.

* butterfly effect on fp?

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for theory plugins

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build fix

* remove SMTFD

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* SMTFD is back (#4676)

* fixing issue #4651

* regression fix

* reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate

* removing temp testing variable

* using intended utility methods for sort detection

* misc edits related to nonground regexes

* bug fix of state id off by 1 calculation error and improved pretty printing with regex tooltip generated in dgml state graph

* removed unused method declaration

* improved id to regex value map info in generated dgml

* reorgd callback function for state pretty printer

* updated some comments

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Sergey Vladimirov <vlsergey@gmail.com>
Co-authored-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com>
 2020-09-08 04:13:18 -07:00
Nikolaj Bjorner 6beec7b642 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 02:04:44 -07:00
Margus Veanes 5e5ef50dbc
re info extension (#4659) 
* made loop info calculation more accurate

* made loop info calculation more accurate

* updated formattig and added const declarations
 2020-08-22 15:59:53 -07:00
Margus Veanes 1e29ba76d0 renamed compl method (compl is a reserved c++ keyword) to complement 2020-08-21 17:34:15 -07:00
Margus Veanes 7b478c8406 fixed loop lower bound bug in loop info and default nullable value in invalid_info 2020-08-21 15:59:56 -07:00
Margus Veanes 3fb226dcd6 added missing return statements, reordered def of compl to match declaration order of methods 2020-08-21 13:20:05 -07:00