Nikolaj Bjorner
|
ff5d210e81
|
na
|
2022-02-20 10:33:15 +02:00 |
|
Nikolaj Bjorner
|
c25d710958
|
try out arch arm64 on the mac
|
2022-02-20 10:31:29 +02:00 |
|
Nikolaj Bjorner
|
4d184fe65d
|
skip expensive equality rewriting of Booleans
|
2022-02-20 10:31:10 +02:00 |
|
Nikolaj Bjorner
|
10b611b3ba
|
fix #5850
|
2022-02-20 10:30:52 +02:00 |
|
Nikolaj Bjorner
|
91045d3e4a
|
two words
|
2022-02-20 10:29:57 +02:00 |
|
Nikolaj Bjorner
|
9a1a72867c
|
Add str.<= and str.< to Java API
|
2022-02-20 10:29:38 +02:00 |
|
Nikolaj Bjorner
|
7091b1c856
|
add additional regex operators to API
|
2022-02-20 10:29:18 +02:00 |
|
Nikolaj Bjorner
|
2e00f2f32d
|
Propagator (#5845)
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix signature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* references #5818
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix c++ build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update propagator example (I) (#5835)
* fix #5829
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Adapted the example to the changes in the propagator
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* context goes out of scope in stack allocation, so can't used scoped context when passing objects around
* parameter check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Fixed bug in user-propagator "created" (#5843)
Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
|
2022-02-17 09:21:41 +02:00 |
|
mbergen
|
2e15e2aa4d
|
Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (#5832)
* Add mkLinearOrder
* reorder arguments to match definition, add short comment
* add partial order
* add comments
|
2022-02-16 23:37:20 +02:00 |
|
Qix
|
9cf50766a6
|
fix compiler warnings under clang (#5839)
|
2022-02-16 23:36:34 +02:00 |
|
Valentine Sobol
|
09da87dc85
|
use horn_subsume_model_converter in coi filter (#5844)
|
2022-02-16 23:35:58 +02:00 |
|
Nikolaj Bjorner
|
5bbb8fb807
|
add bail #5825
|
2022-02-16 23:30:12 +02:00 |
|
Nikolaj Bjorner
|
33985ebcf5
|
update expected
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-16 19:14:54 +02:00 |
|
Nikolaj Bjorner
|
6202cd5394
|
fix #5842
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-16 17:38:19 +02:00 |
|
Nikolaj Bjorner
|
aa6ec418e3
|
move idiv test to after cuts/branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-14 19:50:49 +02:00 |
|
Nikolaj Bjorner
|
9a4d6cee6c
|
overhead with push-ite on shared terms
|
2022-02-14 19:36:14 +02:00 |
|
Nikolaj Bjorner
|
3d26b501e7
|
fix #5827 #5828
|
2022-02-14 10:31:04 +02:00 |
|
Nikolaj Bjorner
|
d745d03afd
|
switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-10 08:55:43 +02:00 |
|
Nikolaj Bjorner
|
81e94b2154
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-09 12:10:01 +02:00 |
|
Nikolaj Bjorner
|
07d02ea415
|
fix #5829
|
2022-02-09 12:08:36 +02:00 |
|
Nikolaj Bjorner
|
4f6fcf8ea7
|
fix #5814
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-08 10:20:19 +02:00 |
|
Nikolaj Bjorner
|
0059e88036
|
fix #5808
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-07 20:10:32 +02:00 |
|
Nikolaj Bjorner
|
9958cab5cc
|
fix #5808
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-07 07:43:30 +02:00 |
|
Nikolaj Bjorner
|
3f3d058567
|
extract also units from search state
|
2022-02-07 06:16:22 +02:00 |
|
Kaleb Crans
|
d4ea67a6e7
|
Fix a few typos in README (#5782)
|
2022-02-06 19:47:47 +02:00 |
|
Nikolaj Bjorner
|
03ff3201b9
|
block recursive definitions with lambdas until they are properly supported #5813
|
2022-02-06 08:57:58 +02:00 |
|
Nikolaj Bjorner
|
1c10ce4070
|
#5815 - surface multi-arity arrays over python API
|
2022-02-06 08:40:56 +02:00 |
|
Nikolaj Bjorner
|
8a84cacfea
|
add tuple support for __getitem__ #5815
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-06 04:02:12 +02:00 |
|
Nikolaj Bjorner
|
e9dad84b85
|
update documentation comments
|
2022-02-06 03:35:32 +02:00 |
|
Nikolaj Bjorner
|
9d655cc658
|
track all unhandled operators instead of latest
|
2022-02-04 22:07:29 -08:00 |
|
Nikolaj Bjorner
|
474949542e
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2022-02-04 13:08:59 -08:00 |
|
Nikolaj Bjorner
|
05e28e4344
|
fix #5812
|
2022-02-04 13:08:52 -08:00 |
|
Nikolaj Bjorner
|
6a412f7f04
|
allow to pass Booleans as arguments to arithmetic expressions
|
2022-01-31 12:00:54 -08:00 |
|
Nikolaj Bjorner
|
994c7ef52d
|
format
|
2022-01-31 12:00:26 -08:00 |
|
Nikolaj Bjorner
|
1e0d49512b
|
call mux finder
|
2022-01-31 12:00:16 -08:00 |
|
Nikolaj Bjorner
|
4392b88718
|
return negated literal when expression is "not"
|
2022-01-31 12:00:00 -08:00 |
|
Nikolaj Bjorner
|
7ddfc54250
|
shortcut negation
|
2022-01-31 11:58:02 -08:00 |
|
Nikolaj Bjorner
|
f3fc6a50f3
|
formatting
|
2022-01-31 11:57:42 -08:00 |
|
Nikolaj Bjorner
|
6422b783b2
|
fix mux extraction to check for top-level assertion
|
2022-01-31 11:57:16 -08:00 |
|
Nikolaj Bjorner
|
62bb234251
|
expose extract roots as separate
|
2022-01-31 11:56:44 -08:00 |
|
Nikolaj Bjorner
|
a326ad4cd9
|
flag incomplete on lambdas #5803
|
2022-01-31 11:54:06 -08:00 |
|
Nikolaj Bjorner
|
a189ca8b60
|
truncation directive #5805
|
2022-01-31 10:50:46 -08:00 |
|
Nikolaj Bjorner
|
773e829c58
|
#5804
|
2022-01-31 10:16:09 -08:00 |
|
Nikolaj Bjorner
|
913b90f7aa
|
fix #5802
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-30 10:42:34 -08:00 |
|
Nikolaj Bjorner
|
2551631957
|
mul overflow #5797
|
2022-01-29 09:15:38 -08:00 |
|
Nikolaj Bjorner
|
5e81c1220c
|
#5797 probably still wrong wrt underflow.
|
2022-01-27 12:48:15 -08:00 |
|
Nikolaj Bjorner
|
9e5b6e0c9c
|
#5778
|
2022-01-27 12:12:58 -08:00 |
|
Nikolaj Bjorner
|
4da930b490
|
#5794
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-27 10:50:48 -08:00 |
|
Nikolaj Bjorner
|
a621041308
|
fix #5795
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-27 10:45:38 -08:00 |
|
Nikolaj Bjorner
|
461e71017d
|
fix #5792 again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-26 15:54:44 -08:00 |
|