mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity
14151 commits 46 branches 52 tags 178 MiB
Commit graph

14151 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
4b6ca6a10c replace size by data_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-22 11:16:36 -07:00
Nikolaj Bjorner
85661c415d remove ex-act 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-22 09:08:04 -07:00
Nikolaj Bjorner
6a54c0bc04 fix issues reported in #4525 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-21 17:43:05 -07:00
Nikolaj Bjorner
02f34ea4b1 address some crashes reported by Caleb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-20 18:35:35 -07:00
Lev Nachmanson
6524a70c32 remove un unnecessary call 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
8f588a9263 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
b703d2786c fix the build cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
3bde9f54d8 add some comments cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
115ae8fe14 check for integrality when adding an equality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
c4fbe05a96 simplify cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
e3503f060f debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
42ed1e62a9 debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
2e2e98925a debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
ffaa7d0b27 debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
7a2aa28644 make the tree option in cheap_eqs the default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
525f747e3c cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
c2cead4fb6 cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
b5fc9635c4 cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
3b00b34c6f cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
80467f1400 cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
431bb36cf5 cheap_eqs tree 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
f7f9c15676 cheap_eqs tree 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Nikolaj Bjorner
274323b818 fix reset order for #4533 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-19 16:07:45 -07:00
Nikolaj Bjorner
1204671595 fix #4534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-19 14:10:49 -07:00
Arie Gurfinkel
07a1aea689 fix(spacer): bug in assign_bounds to Farkas conversion 
The fix is to remove a hack that used a theory rewriter to simplify
the conversion. Now the conversion happens less often than possible.
Will need more thinking to fix properly.

The unsoundness at this point would cause SPACER to generate lemmas
that do not block a proof obligation and then get stuck in an infinite loop
blocking and generating the same lemma.
 2020-06-18 21:19:53 -04:00