Nikolaj Bjorner
91ac15d716
add u256
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-04 10:32:18 -07:00
Jakob Rath
8a773d2bee
Polysat updates ( #5444 )
...
* Simplify adding lemmas
* Remove misleading constructor from tmp_assign.
The idea is that tmp_assign is only created on the stack and
short-lived. Instead of having a convenience constructor that takes a
constraint_ref, it's clearer to have an explicit .get() at the call
site.
* Remove some log messages
* bugfix
* fix
* Add stub for conflict_core
* wip
* Add example by Clemens
2021-07-30 11:14:19 -07:00
Nikolaj Bjorner
2ef8ee25f1
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-15 00:05:42 +02:00
Nikolaj Bjorner
db3c42b02d
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-15 00:05:13 +02:00
Nikolaj Bjorner
4c6e2acd45
add colors
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-15 00:03:56 +02:00
Nikolaj Bjorner
79c261736b
charsort
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 19:50:41 +02:00
Nikolaj Bjorner
97a035fd6d
add char sort to .net
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 19:43:12 +02:00
Nikolaj Bjorner
1b648437b7
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 17:42:34 +02:00
Nikolaj Bjorner
a3010c8875
version inc, bvsort->bitvecsort
2021-07-13 17:14:47 +02:00
Nikolaj Bjorner
7ae78da850
adding access to characters over API
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 15:56:08 +02:00
Nikolaj Bjorner
3a402ca2c1
Update release.yml for Azure Pipelines
2021-07-13 15:25:23 +02:00
Nikolaj Bjorner
75a5de99ca
Update release.yml for Azure Pipelines
2021-07-13 15:24:19 +02:00
Nikolaj Bjorner
82e477ac02
bounds
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 14:40:32 +02:00
Nikolaj Bjorner
0752b1385c
add length axioms
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 14:22:58 +02:00
Nikolaj Bjorner
a49a5b3a0b
add release note for 4.8.12 prepare for addressing #5406
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 09:43:00 +02:00
Nikolaj Bjorner
34677e0e7c
fix update of bb
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 09:32:05 +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
f74adb1ebd
ubv2s step3
2021-07-12 17:15:08 +02:00
Nikolaj Bjorner
b6a3891ac4
str.from_ubv step2
2021-07-12 15:00:36 +02:00
Nikolaj Bjorner
1bc10cebc5
add ubv2s step 1
2021-07-12 12:53:00 +02:00
Nikolaj Bjorner
805bb58289
fix #5404
2021-07-12 12:35:24 +02:00
Nikolaj Bjorner
de8b2041e6
make bpp work with nullptr
2021-07-12 00:03:32 +02:00
Nikolaj Bjorner
4c53655be7
add z3doc build to release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 23:26:48 +02:00
Nikolaj Bjorner
2ccfb1937d
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 23:20:19 +02:00
Nikolaj Bjorner
a4f4975092
#5336
2021-07-11 21:08:53 +02:00
Nikolaj Bjorner
cab1076514
#5336
2021-07-11 21:00:58 +02:00
Nikolaj Bjorner
18a76ab82c
#5336
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 06:42:27 +02:00
Nikolaj Bjorner
10ad5bae21
increment version
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 06:17:58 +02:00
Nikolaj Bjorner
e05f5ef6d1
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 06:15:27 +02:00
Nikolaj Bjorner
5fac396c2f
simplify some verbose trace-stream
2021-07-11 06:15:27 +02:00
Nikolaj Bjorner
bc2e6ce037
Update release.yml for Azure Pipelines
2021-07-10 22:42:02 +02:00
Nikolaj Bjorner
66fc980154
add helper axioms for int2bv #5396
2021-07-10 17:13:16 +02:00
Nikolaj Bjorner
34885562e0
try without #!/bin/env python #5397
2021-07-10 15:20:56 +02:00
Nikolaj Bjorner
0f8d2d1d51
fix #5399
2021-07-10 14:47:51 +02:00
Nikolaj Bjorner
2973d3bdc1
fix #5392
2021-07-07 23:43:30 +02:00
Nikolaj Bjorner
897cbf347b
fix #5381
2021-07-07 16:51:06 +02:00
Nikolaj Bjorner
29c6d42380
is-char is overloaded #5389
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-07 08:20:31 +02:00
Nikolaj Bjorner
4f184b6aa9
fix #5376
2021-07-06 19:20:35 +02:00
Nikolaj Bjorner
c2595b9bc8
#5379
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-06 18:58:27 +02:00
Nikolaj Bjorner
af5b2a4179
#5376
2021-07-06 16:44:44 +02:00
Nikolaj Bjorner
ca05c66847
#5376
2021-07-06 14:20:23 +02:00
Marc Mosko
8a33391708
Expose optimize.assertAndTrack to Java ( #5387 )
...
Co-authored-by: Marc Mosko <mmosko@parc.com>
2021-07-06 01:22:00 -07:00
Gabriel Radanne
0c7625cd26
Remove size argument in OCaml's Z3.mk_re_intersect ( #5383 )
...
* Remove size argument in OCaml's `Z3.mk_re_intersect`
Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.
* Enable the ocaml documentation in Seq.
Turn all the comments into proper documentation comments.
2021-07-06 01:21:04 -07:00
Nikolaj Bjorner
bdcfba1324
use sort* not ast* #5386
2021-07-06 10:19:17 +02:00
Nikolaj Bjorner
2a8d00d815
fix #5378
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-06 00:04:16 +02:00
Nikolaj Bjorner
e5aa02b8f5
fix #5382
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-05 19:30:03 +02:00
Nikolaj Bjorner
7255a2afd1
fix #5379
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-05 18:43:11 +02:00
Nikolaj Bjorner
d5ff672aaa
generalize co-factor to handle cubes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-05 14:10:09 +02:00
Nikolaj Bjorner
04ce8ca5ef
u256, separate viable_set
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-04 23:47:12 -07:00
Nikolaj Bjorner
aeec3bb6df
viable
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-04 10:20:01 -07:00
