mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
15988 commits 23 branches 48 tags 156 MiB
Commit graph

15988 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner a00d68fe5a update release scripts and notes in master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 11:43:38 -08:00
Margus Veanes 5afb95b34a
improved subset checking for regexes with counters (#5731) 2021-12-22 17:53:34 -08:00
Nikolaj Bjorner 71b868d7f6 #5722 - internalize unary xnor 2021-12-22 13:32:53 -08:00
Nikolaj Bjorner 4d8bf2a874 wrong unit for xor in aig tactic #5722 2021-12-22 13:14:06 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00
Nikolaj Bjorner 78222f274c remove action that fails too often 2021-12-22 07:56:09 -08:00
Anton Kochkov f3af2193d0
Use Stdlib. instead of Pervasives. due to deprecation (#5730) 2021-12-22 07:53:47 -08:00
Nikolaj Bjorner cf6486f990 bug in flatten/and/or introduced when skipping sub-expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-22 07:43:37 -08:00
Nikolaj Bjorner 4b5ee91b44 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 20:40:58 -08:00
Nikolaj Bjorner 09ee60ccce update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 11:04:07 -08:00
zhouzhenghui 9d82c1d8a9
fix deadlock in scoped_timer destructor (#5371) 2021-12-21 18:47:13 +00:00
Nuno Lopes 94a2c91f39 fix a few compiler warnings 2021-12-21 18:30:22 +00:00
Margus Veanes 1d9aad6ea9
improved regex merging avoiding unsat nontermination (#5728) 2021-12-20 17:44:06 -08:00
Nikolaj Bjorner e0d6e04493 fix c++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-20 16:09:39 -08:00
Nikolaj Bjorner 7a6070506d #5727 
Expose diff function,
expose allchar in Java API
expose op codes for replace/re/all
 2021-12-20 10:17:06 -08:00
Nikolaj Bjorner f01d096fb5 fix again 2021-12-20 09:51:15 -08:00
Nikolaj Bjorner ad91748b5f Merge branch 'master' of https://github.com/z3prover/z3 2021-12-20 09:21:53 -08:00
Nikolaj Bjorner 83b47f1859 fix #5726 2021-12-20 09:21:40 -08:00
Margus Veanes be38b256c8
fixed bug in is_char_const_range (#5724) 2021-12-19 17:46:42 -08:00
Margus Veanes 25d54ebb40
fixing regression of issue 1224 (#5723) 2021-12-19 14:07:53 -08:00
Nikolaj Bjorner 4b813bac1c na 2021-12-19 12:31:47 -08:00
Nikolaj Bjorner 6a039c2700 Update z3++.h 
simplify definition
 2021-12-19 11:53:01 -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
Nikolaj Bjorner bee742111a na 2021-12-19 11:05:19 -08:00
Nikolaj Bjorner 7441bd706b na 2021-12-19 10:57:42 -08:00
Nikolaj Bjorner 85e362277c Update z3++.h 
with bindings for user propagate functions
 2021-12-18 11:56:05 -08:00
Nikolaj Bjorner f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner 4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner 8ca023d541 expose propagate created 2021-12-17 16:12:47 -08:00
Nikolaj Bjorner e1ffaa7faf na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 11:34:57 -08:00
Nikolaj Bjorner 9c8800bdde adding a new toy for Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 10:45:59 -08:00
Nikolaj Bjorner 6963451704 na 2021-12-16 20:13:29 -08:00
Nikolaj Bjorner 5974200444 fixes to previous push and streamlining 2021-12-16 20:06:49 -08:00
Nikolaj Bjorner 4e82a9af5f pin expressions 2021-12-16 19:41:32 -08:00
Nikolaj Bjorner 6cc9aa3562 prepare user propagator declared functions for likely Clemens use case 2021-12-16 19:37:30 -08:00
Margus Veanes a288f9048a
Update regex union and intersection to maintain ANF (#5717) 
* added merge for unions and intersections

* added normalization rules to ensure ANF

* fixing PR comments related to merge
 2021-12-16 19:19:36 -08:00
Nikolaj Bjorner db62038845 Update nightly.yaml 
see if this gets us past the upload to GitHub issue
 2021-12-16 14:20:40 -08:00
Nikolaj Bjorner 4641a20f4f #5700 - Add download x86 as part of release NuGet 
x86 is part of nightly NuGet but was not added to the release pipeline.
 2021-12-16 13:50:31 -08:00
Nikolaj Bjorner 122b0fec0f fix #5710 2021-12-16 12:30:29 -08:00
Nikolaj Bjorner a099972354 fix #5714 
It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints.
So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense.

Just running the samples in debug mode  points to the root cause.

Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers:

- reproduce bug in debug builds to assess whether a debug assert triggers.
- minimize or keep it simpler when possible (in this case it does not apply)
- perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause.

Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see.
 2021-12-16 10:20:53 -08:00
Nikolaj Bjorner dd6a11b526 fix #5715 2021-12-16 09:35:54 -08:00
Nikolaj Bjorner 2caa7e6e45 remove EnumToNative as it drops reference counts, fixes #5713 2021-12-16 03:22:54 -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 3b58f548f7 remove dead code 2021-12-14 13:42:52 -08:00
Nikolaj Bjorner 03b5380a20 na 2021-12-14 13:39:52 -08:00
Nikolaj Bjorner b1d167de5b fix co-factoring' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:12:38 -08:00
Nikolaj Bjorner 5348af3c4c fix co-factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:05:09 -08:00
Nikolaj Bjorner f40becf099 remove case for non-emptiness to combine with standard membership 
as part of revising engine for addressing #5693
 2021-12-13 18:17:40 -08:00
Nikolaj Bjorner b2af7ea68f stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-13 15:19:29 -08:00
Nikolaj Bjorner 9ec0f94ab9 hoisting out blocker for empty 
#5693
 2021-12-13 14:25:05 -08:00