mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity
15564 commits 23 branches 48 tags 156 MiB
Commit graph

15564 commits

This branch
This branch
All branches
Author SHA1 Message Date
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 d5c6abe14d #close 5363 
Force in-lining auxiliary functions so that model values can be used by SPACER to retrieve counter-examples. This fixes the issue of terminating without a trace. It does not address inefficiency involved with invoking satisfiability checks to retrieve models during trace construction.
 2021-06-22 16:24:00 -07:00
Nikolaj Bjorner 55daa2424c fix #5362 2021-06-22 12:26:27 -07:00
Nikolaj Bjorner f3737f6831 #5361 2021-06-21 14:58:00 -07:00
Robert Jacobson 161d38397b
In src/sat/sat_local_search.*: Changed the return type of constraint_slack to int64_t instead of uint64_t to match the m_slack member of the constraint struct, which has type int64_t. (#5360) 2021-06-21 14:40:31 -07:00
Nikolaj Bjorner 45228bf8fb #5323 heap use after free 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 09:25:19 -07:00
Nikolaj Bjorner ed9341e3b0 #5336 2021-06-19 22:22:56 -07:00
Nikolaj Bjorner 02644b5b71 #5336 2021-06-19 22:22:56 -07:00
Nikolaj Bjorner 8d37495b7c merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-19 22:22:41 -07:00