mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
16017 commits 23 branches 48 tags 157 MiB
Commit graph

16017 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f7c1ed8273 missing this 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 10:41:37 -07:00
Nikolaj Bjorner
4d39af3d7b #5507 missing init 2021-08-26 09:37:06 -07:00
Nikolaj Bjorner
07c26208fa regressions from previous push 2021-08-25 18:30:50 -07:00
Nikolaj Bjorner
2daf569da6 update Bool rewriter to pull negations up 2021-08-25 17:50:49 -07:00
Nikolaj Bjorner
e6264a80ff extend macro detection to negated equivalences #5496 2021-08-25 17:47:30 -07:00
Nikolaj Bjorner
f03d756e08 missing rewrite exposed by #5498 2021-08-25 06:34:27 -07:00
Nikolaj Bjorner
17663acf75 #5482 other relevancy tracking 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
e75b5e9513 don't copy "true" 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
037c93b258 #5482 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
7bae297297 #5482 
add unit propagation
 2021-08-24 11:24:31 -07:00
Nikolaj Bjorner
26db68bf2c #5482 2021-08-24 11:15:52 -07:00
Nikolaj Bjorner
e5b6cd36f0 use datatype name instead of instantiation for cycle detection #5482 2021-08-24 11:14:41 -07:00
Nikolaj Bjorner
e90ec457c3 #5482 
non-termination (stack overflow) bug in recursive comparison
 2021-08-24 09:49:36 -07:00
Nikolaj Bjorner
5fa1b0b09f update project description #5503 2021-08-24 09:48:33 -07:00
Nikolaj Bjorner
23b995d3b5 #5499 
throw exception when dividing by a small 0
 2021-08-24 08:52:20 -07:00
Nikolaj Bjorner
dd91cfb47e #5482 
update temp variables
 2021-08-23 22:21:52 -07:00
Nikolaj Bjorner
592c53e46d char sort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 20:45:26 -07:00
Nikolaj Bjorner
170ef1dcca add character sort to Python API and allchar function to API for ease. #5500 2021-08-23 20:02:50 -07:00
Nikolaj Bjorner
4b3b4b95d9 missing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 10:03:34 -07:00
Nikolaj Bjorner
2a682e4b13 #5482 
tricky one
 2021-08-23 10:01:53 -07:00
Nikolaj Bjorner
9c7d9f06ed #5497 2021-08-22 17:22:37 -07:00
Nikolaj Bjorner
1975e486ee finally expose some easier to use basics could be used in cases such as #5496 2021-08-21 21:22:54 -07:00
Nikolaj Bjorner
aa05298950 fix #5491 2021-08-19 21:12:27 -07:00
Nikolaj Bjorner
15e3e81cb5 remove likely culprit for #5493 
@zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in #5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes #5493
 2021-08-19 21:08:20 -07:00
Nikolaj Bjorner
d0e210849f #5454 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-19 03:06:23 -07:00
Nikolaj Bjorner
9122ec9cd6 comment out for now 2021-08-18 14:52:59 -07:00
Nikolaj Bjorner
93c3fc2bda try without semi-colon 2021-08-18 14:52:12 -07:00
Nikolaj Bjorner
adcdd11afc #5454 again 2021-08-18 13:32:51 -07:00
Nikolaj Bjorner
2492278a4b Update test for java 2021-08-18 13:32:51 -07:00
Nikolaj Bjorner
1db9f9a3b5 try vscode from github integration 2021-08-18 11:02:02 -07:00
Nikolaj Bjorner
810b9d003d move examples to python based build 2021-08-18 10:06:02 -07:00
Nikolaj Bjorner
d980ee0533 fix regression in FPNumRef sign 2021-08-18 10:00:22 -07:00
Nikolaj Bjorner
b3db9a1cd5 #5488 2021-08-18 08:30:08 -07:00
Nikolaj Bjorner
5c9f4dc4d7 #5486 - improve type elaboration by epsilon to make common cases parse without type annotation 2021-08-17 16:43:36 -07:00
Nikolaj Bjorner
7f88cfe727 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 10:10:20 -07:00
Nikolaj Bjorner
1884ad5b2f expose method for updating python model for constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 09:09:04 -07:00
Nikolaj Bjorner
34fc0276e9 Update array_axioms.cpp 2021-08-16 17:52:37 -07:00
Nikolaj Bjorner
749d1ab305 remove dependencies on stale component 2021-08-16 17:52:36 -07:00
0152la
3516c5272a
Update coverage github action (#5483) 
* Correctly emits simple and detailed coverage reports using a
  combination of `gcovr` and `llvm-cov gcov`
* Uploads the reports as associated artifacts, with 4 days of retention
* Executes on every `master` push, and daily at 11 UTC

Co-authored-by: Andrei Lascu <andrei.lascu10@imperial.ac.uk>
 2021-08-16 14:13:28 -07:00
Nikolaj Bjorner
c8a83749dd #5484 2021-08-16 11:19:22 -07:00
Nikolaj Bjorner
904c6e21b1 modify #5454 2021-08-16 03:29:40 -07:00
Nikolaj Bjorner
429e5ed0cd #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 19:07:37 -07:00
Nikolaj Bjorner
3d13c0335f #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 18:40:05 -07:00
Nikolaj Bjorner
6a3ba64afe #5454 
@wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though.
 2021-08-15 16:48:28 -07:00
Nikolaj Bjorner
fe4c48e14c reorder fields 2021-08-15 12:29:43 -07:00
Nikolaj Bjorner
bebf2d6a52 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 00:24:43 -07:00
Nikolaj Bjorner
b7d4501bc3 widen scope of der #5480 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 00:22:34 -07:00
Nikolaj Bjorner
2704fb5fd5 expose n-ary xor 2021-08-14 10:52:09 -07:00
Karlheinz Friedberger
764e033bf4
Specify and document value for environment variable for loading native library in Java bindings (#5477) 
* limit range of environment variable for loading the native library in Java to "true".

This change specifies the range of values that are allowed to set the environment
variable "z3.skipLibraryLoad".
Only the value "true" (in upper-, lower-, and mixed-case is accepted as valid value.
Other values, such as "false", "0", "1", "foo", an empty or a missing value are
evaluated to "false" and cause the default loading of the native library.

* adding documentation about environment variable for (not) loading the native library in Java.

This is a follow-up commit for #4667 to provide a publicly visible documentation.
 2021-08-13 14:54:02 -07:00
intrigus-lgtm
35698c650d
Add AssertSoft String overload for Java Api (#5475) 
This adds a String overload for AssertSoft.
Previously only integer weights could have been used,
limiting the user. With Strings the user can now use
e.g. Java's BigInteger class converted to a String instead.
 2021-08-12 09:18:18 -07:00