mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-24 16:34:36 +00:00
Code Activity
16176 commits 43 branches 52 tags 176 MiB
Commit graph

16176 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
4a8533e41f enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:17:54 -07:00
Nikolaj Bjorner
2d358a9a50 fix #4565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-06 17:07:37 -07:00
Nuno Lopes
ca97bfb4b8 fix build 2020-07-05 11:44:12 +01:00
Nikolaj Bjorner
006418e027 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 23:34:21 -07:00
Nikolaj Bjorner
f380d4cf83 mpfx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:25:32 -07:00
Nikolaj Bjorner
74eb401c3b addrecdef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:18:25 -07:00
Nikolaj Bjorner
51d43c04ea st 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:13:04 -07:00
Nikolaj Bjorner
2bb712c9da ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:09:08 -07:00
Nikolaj Bjorner
5ea145ce26 ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:08:22 -07:00
Nikolaj Bjorner
bf14444f7d st 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:07:07 -07:00
Nikolaj Bjorner
f3b51db891 ml build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 16:22:01 -07:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
10d0404175 add rec decl/def to ML #4563 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:38:32 -07:00
Lev Nachmanson
62b9630c4b remove unicode from hnf_cutter.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
7a4eed0216 add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
49e49d6bb6 add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
80a4da9b1d add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
fff6a94de4 cheap_eqs - fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
61da368ee3 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
f4502ff952 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
1695379dc9 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
a1c5cff541 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
29b3f438bc cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
cb3ebac3dd cleanup lp_bound_propagator.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
b996bc1f02 remove cheap equalities with the table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Murphy Berzish
e8690d28f8
z3str3: continue instead of incorrectly giving up in solve_regex_automata (#4556) 2020-07-03 17:13:27 -05:00
Nikolaj Bjorner
8d3caa00fe do as Lev does 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-03 13:21:43 -07:00
Nikolaj Bjorner
7802e33f37 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-03 12:22:13 -07:00
Nikolaj Bjorner
5e768c9697 move unused literals under if0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-03 12:21:20 -07:00
Nikolaj Bjorner
5987d9ae20 cache computing strings and regexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-02 11:14:29 -07:00
Nikolaj Bjorner
655166b867 randomize generation of 'some value' for user sorts. #4557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-01 16:34:09 -07:00
Nikolaj Bjorner
d91ca423ab enforce reference count ownership in context of mk_derivative calls. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-01 13:13:17 -07:00
Nikolaj Bjorner
d75ce38016 fix #4552 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-30 19:14:55 -07:00
Murphy Berzish
fce1252145
Z3str3: Add consistency checks for string-integer conversion terms in model construction (#4551) 
* z3str3: check consistency of str.to_int in fixed length solver

* z3str3: add similar check for int.to_str as well

* z3str3: refactor string-integer conversion check and add post checks for model construction
 2020-06-30 11:20:44 -05:00
Nuno Lopes
8fda4f904d API: dont deref already free'd memory on error 2020-06-30 15:04:40 +01:00
Nuno Lopes
64f1a759a7 inline api_context::reset_error_code() 2020-06-29 19:14:17 +01:00
pinzaghi
aec8000bda
in check method, as_ast() call fails when True passed as assumption (#4550) 2020-06-29 09:59:10 -07:00
Nikolaj Bjorner
eaffe46468 revert debug changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-28 10:27:47 -07:00
Nikolaj Bjorner
9a642215eb avoid infinite loop between is-nullable and mk-bool-app 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-28 10:27:47 -07:00
Jacob Lifshay
4dc7089cc4
add android support (#4545) 
built successfully in termux on aarch64 android 10 using:
cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/data/data/com.termux/files/usr/ -DCMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR=/data/data/com.termux/files/usr/lib/cmake/z3 <path/to/z3>
 2020-06-26 14:58:01 -07:00
Nikolaj Bjorner
9bc5552ca2 add vcrunime pattern to distribution directive #4542 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-25 08:56:13 -07:00
Nikolaj Bjorner
85cb0293f5 fix #4541 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-24 20:26:59 -07:00
Federico Mora Rocha
8d16a9a034
z3str3: fix Issues 4349, 4354, and 4310 (#4529) 
* regex needs lesson; m.mk_eq not ctx.mk_eq

* when unsat core is of size 0, then do naive learning

* remove two extra comments, and correct positive regex learning

* replace magic numbers for fixed-length lessons with constants
 2020-06-24 15:46:32 -05:00
Nikolaj Bjorner
c0fbb31379 use nonse based seed for transition characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-24 12:07:37 -07:00
Murphy Berzish
b0633ecc86
Z3str3: safety checks for substr and propagate (#4528) 
* z3str3: handle str.substr arguments missing arith values in model construction safely

* z3str3: reset propagation vectors on scope pop
 2020-06-24 12:14:03 -05:00
Nikolaj Bjorner
7f3bdea0d5 unused methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-23 19:28:07 -07:00
Nikolaj Bjorner
5d36578684 some unused variables reported by Caleb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-22 19:04:10 -07:00
Nikolaj Bjorner
8758baf24e perf and div/mod axioms #4532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-22 14:51:58 -07:00
Nikolaj Bjorner
38d6771a5e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-22 12:23:42 -07:00
Lev Nachmanson
6ced6995d0 check for m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner()) in equality propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-22 11:48:46 -07:00