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
Jamey Sharp
1d3ee70af4
support bit-blasting bvand ( #5458 )
2021-08-08 15:52:54 -07:00
Nikolaj Bjorner
dcfd7b76c9
more rewrites based on example in #5457
2021-08-05 11:54:13 -07:00
Nikolaj Bjorner
e10850e66a
fix #5457
2021-08-05 11:27:03 -07:00
Nikolaj Bjorner
ed3f8a52e6
#5454
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-04 14:05:29 -07:00