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

14602 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 41cc037204 change manylinux to ubuntu-latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-10 16:17:35 -08:00
Lev Nachmanson 4810b4cac2 add a comment in nla_order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-11-10 11:12:28 -08:00
Lev Nachmanson fc5e5a2098 add a comment in nla_order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-11-10 11:11:42 -08:00
Nikolaj Bjorner fdedeed7ae additional sign related fix for #4740 https://github.com/Z3Prover/z3/issues/4740#issuecomment-721508240 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-10 10:50:13 -08:00
Nikolaj Bjorner 5ace60c812 enforce guard option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-10 09:22:32 -08:00
Nikolaj Bjorner 672e392386 guard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-10 08:01:29 -08:00
Nikolaj Bjorner be50f38903 enforce sign coherence #4740 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 14:30:00 -08:00
Nikolaj Bjorner 638ef9ed03 enforce sign coherence #4740 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 14:28:49 -08:00
Nikolaj Bjorner e955bd09e5 push equality for #4740 
https://github.com/Z3Prover/z3/issues/4740#issuecomment-711460353
 2020-11-09 13:08:46 -08:00
Nikolaj Bjorner 3c9ada54b6 tune hoist-rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 11:25:18 -08:00
Nikolaj Bjorner 768e2c1d0d tune hoist-rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 11:25:17 -08:00
Nikolaj Bjorner 4d26aabd83 fix bug in rewriting of power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-09 07:12:37 -08:00
Nikolaj Bjorner f78980c81c fix rewriting of power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 20:58:16 -08:00
Johannes Kanig 7d205f1cf0
TB08-009 fix z3 build on windows (#4782) 
It seems that VS 15.0 doesn't like this usage of "enum"

Change-Id: Ie7eba81ad9fd990aa436d323dc848d1b0f2c4370
 2020-11-08 20:47:25 -08:00
Nikolaj Bjorner 864eaf8bf8 remove unsound rewrite #4778 2020-11-08 17:48:51 -08:00
Nikolaj Bjorner e2c1436cc8 fix #4775 2020-11-08 17:18:18 -08:00
Nikolaj Bjorner 89ffb45c4f fixes to bv/dual-solver, 2020-11-08 17:18:18 -08:00
Nikolaj Bjorner a4354c960c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 17:18:17 -08:00
Nikolaj Bjorner 752f08c9d6 check_feasible is called after column is added for fixed variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 17:18:17 -08:00
Nikolaj Bjorner 2ead7c77ee use value function in lar_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 17:18:16 -08:00
Christoph M. Wintersteiger eadf755628
Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381. 2020-11-06 20:54:10 +00:00
Christoph M. Wintersteiger 372bb4b25a
Fix reference counting in Z3_mk_fpa_to_ieee_bv 2020-11-06 12:16:09 +00:00
Nuno Lopes 30fd01b526 api: avoid copying param_refs whenever possible 2020-11-06 10:51:51 +00:00
Nikolaj Bjorner d0d06c288a rename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-03 12:13:23 -08:00
Nikolaj Bjorner 620204bbb4
use value function in lar_solver (#4771) 
* use value function in lar_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add missing return

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* check_feasible is called after column is added for fixed variable

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na
 2020-11-03 01:08:24 -08:00
Nikolaj Bjorner 5335097768 use get_value/get_ivalue API instead of self-rolled from arith_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 19:38:13 -08:00
Nikolaj Bjorner ee12e3fb52 add init_model, global m_delta, get_value, get_ivalue to push model maintainance into lar_solver #4740 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 19:21:15 -08:00
Nikolaj Bjorner ab199dedf9 debug arith/mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 12:13:19 -08:00
Nikolaj Bjorner fb6e7e146b test mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 17:03:04 -07:00
Nikolaj Bjorner a764d528a1 'clean 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 13:14:48 -07:00
Nikolaj Bjorner d64bc795f0 wrong assert, compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 10:10:59 -07:00
Christoph M. Wintersteiger c03c395267
Add missing assertion. Fixes #4642. 2020-10-30 14:09:51 +00:00
Nuno Lopes 1730bc7c7f fix #4763: shell not finishing before hard timeout 
The timer thread for the hard timeout was leaking and thus the thread only exited on timeout
 2020-10-30 10:01:09 +00:00
Nikolaj Bjorner 0e1def5bd6 fix #4736 2020-10-30 01:54:42 -07:00
Nikolaj Bjorner f354671465 add parameter for scenario from #4743 2020-10-30 01:14:34 -07:00
Nikolaj Bjorner ceedd7e84d #4721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-29 16:55:30 -07:00
Nikolaj Bjorner c07cfc0e69 include path to thread and guard by SINGLE_THREAD 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-29 16:43:15 -07:00
Nikolaj Bjorner ac4bcb9034 update logging for lemmas 2020-10-29 15:09:23 -07:00
Nikolaj Bjorner 91511f73a0 fix #4744 2020-10-29 15:09:13 -07:00
Nikolaj Bjorner 9026ff28bc #4762 2020-10-29 12:57:13 -07:00
Nikolaj Bjorner 601ba2a361 #4765 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-29 12:10:00 -07:00
Nikolaj Bjorner 0de3149634 fix #4763 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-29 11:15:53 -07:00
Nikolaj Bjorner 2e684d58d2 redo purification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-29 11:06:31 -07:00
Ding Fei da0e140e1c
fix git dir for git-dependency in cmake (#4759) 
This is not fixed as #1993 stated.

Co-authored-by: Ding Fei <fei.ding@ustchcs.com>
 2020-10-28 10:08:13 -07:00
Ding Fei c40a67da7d
avoid use of uninit member (m) (#4761) 
Co-authored-by: Ding Fei <fei.ding@ustchcs.com>
 2020-10-28 10:06:50 -07:00
Nikolaj Bjorner 07680408a6 add flag to control whether ite-lifting under quantifiers is conservative or full for #4746, use smt.q.lift_ite=2 to obtain legacy behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-27 16:27:24 -07:00
Nikolaj Bjorner e2fbd05fe7 adding argument restriction to mbqi, fix tracking of m_src/m_dst for expr_safe_replace and avoid resetting the cache. 2020-10-27 11:41:52 -07:00
Pierre Bouvier 24321e311b
Add support of the SunOS platform (Solaris, OpenSolaris, OpenIndiana) (#4757) 
* Add support of the SunOS plateform (OpenSolaris, OpenIndiana) in scripts/mk_util.py

* Add missing casts for the SunOS plateform (OpenSolaris, OpenIndiana) for the pow function
 2020-10-27 11:39:21 -07:00
Nikolaj Bjorner 9e9963d765 remove also second hash-table for ALIVE_OPT #4747 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-27 00:12:34 -07:00
Nikolaj Bjorner e962deb557 remove also second hash-table for ALIVE_OPT #4747 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-27 00:12:34 -07:00