mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity
14477 commits 23 branches 48 tags 156 MiB
Commit graph

14477 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 4b346ef693 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:58:42 -07:00
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