mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
Code Activity
15845 commits 23 branches 48 tags 156 MiB
Commit graph

15845 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner b016465ad2 #5454 2021-08-11 20:31:53 -07:00
Nikolaj Bjorner fea14245a0 #5454 2021-08-11 19:43:42 -07:00
Nikolaj Bjorner 46107022f7 #5454 2021-08-11 17:06:42 -07:00
Nikolaj Bjorner fde8808a40 #5454 2021-08-11 16:59:46 -07:00
Nikolaj Bjorner 8faad26c3c #5454 2021-08-11 09:46:35 -07:00
Nikolaj Bjorner 178262fc12 #5454 2021-08-11 09:30:03 -07:00
Nikolaj Bjorner 496ec5f2b4 #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-11 05:00:02 -07:00
Nikolaj Bjorner d1d64bbe59 #5454 2021-08-11 04:55:20 -07:00
Nikolaj Bjorner 4f2211baab fix solver-subsumption again, #5468 (negation was swapped in original wrong subsumption check, then soundness fix removed core subsumption functionality) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-11 04:36:48 -07:00
Nikolaj Bjorner 7ab7b8646b #5454 2021-08-10 14:47:26 -07:00
Nikolaj Bjorner 081cdbd762 fix #5468 2021-08-10 10:46:47 -07:00
Nikolaj Bjorner 391db898d3 lost update from August 3 #5468 2021-08-10 09:45:17 -07:00
Nikolaj Bjorner 2075cb9fa4 remove useless literal found during review #5470 2021-08-10 09:29:39 -07:00
Nikolaj Bjorner 4beb29d45e fix #5469 documentation bug 2021-08-10 09:22:24 -07:00
Margus Veanes 22bb4c2db7
more fixes related to issue #5140 (#5466) 
* instead of u in to_re(s) make u = s

* bug fix: added missing emptiness check
 2021-08-09 17:48:35 -07:00
Nikolaj Bjorner 3eb849ad9e rewrite equality too 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-09 15:32:04 -07:00
Nikolaj Bjorner aa7e9b09f3 fix equality rewrite with itos 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-09 14:22:48 -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
Nikolaj Bjorner af5fd1014f #5460 2021-08-08 17:33:49 -07:00
Nikolaj Bjorner 85da7407dc #5460 
NB @nunoplopes - the code path regarding rewrite_uncstr could use some unit tests.
 2021-08-08 17:18:31 -07:00
Nikolaj Bjorner e27a71bbcb #5460 2021-08-08 16:29:41 -07:00
Jamey Sharp 5de5f5a442
report which operator bit-blast failed on (#5459) 2021-08-08 15:53:07 -07:00