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

14137 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nuno Lopes 38d4418f94 simplify string_buffer::append 2020-06-18 19:55:34 +01:00
Nuno Lopes fdeba2102c fix deref of free'd memory in mk_fresh_const 2020-06-18 19:25:32 +01:00
Nikolaj Bjorner 3b1149330d enable theory propagation of regex accept condition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-17 13:42:40 -07:00
Nikolaj Bjorner be36a8fd80 fix for SPACER models using bit2bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-16 10:45:11 -07:00
Nikolaj Bjorner 48d4d8d7af fix tracking of bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-15 17:36:20 -07:00
Lev Nachmanson f882219081 fix a bug in cheap_eqs with table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Lev Nachmanson 09516d74f6 change the default for cheap eqs to table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Lev Nachmanson d13e584706 simplify the fixed var table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Nikolaj Bjorner d09e6eccf0 re-enable proofs for qe-lite #3153 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-15 12:03:15 -07:00
Nikolaj Bjorner 395a304262 add optional feature to bound search within ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 21:34:54 -07:00
Nikolaj Bjorner 180fb3abf6 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 11:36:09 -07:00
Nikolaj Bjorner 7387fc9dec avoid some bignum overhead in addmul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 11:20:05 -07:00
Nikolaj Bjorner 53e49eb428 neatify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-13 15:20:21 -07:00
Nikolaj Bjorner 5ee9edf46b fix incorrect bound in order-lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-13 14:28:42 -07:00