mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity
14593 commits 23 branches 48 tags 157 MiB
Commit graph

12360 commits

Author SHA1 Message Date
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
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
Pierre Bouvier
f3147d6e22
Fix: QF_UFDT has UF (#4755) 2020-10-26 12:01:21 -07:00
Nikolaj Bjorner
3ba857fb04 add alternate caching mechanism to allow experimenting for #4747 
@nunoplopes @aqjune you can experiment by setting ALIVE_OPT to 1 and see if this helps.
A further possible optimization is to persist the "subst" object on the api_context object.
Then in Z3_substitute in api_ast.cpp, instead of declaring locally
        expr_safe_replace subst(m);
you can use an attribute on the context to retrieve the same substitution object.

It is not easy to figure out if this matters without having some profiling information so I hope you can determine on your side whether this is useful.
 2020-10-26 11:49:24 -07:00
Nikolaj Bjorner
8d76470a8a fixes to mostly solver arith/euf and backtracking scopes 2020-10-26 11:06:41 -07:00
Nikolaj Bjorner
1ee2ba2a9b mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-26 11:06:40 -07:00
Andy Wright
34e0e26e3d
Fixed model translate method in Python API (#4753) 2020-10-25 15:42:17 -07:00
Nuno Lopes
aaa1af5b28 fix debug build 2020-10-24 13:05:25 +01:00
Nuno Lopes
4e9035d4b9 cleanup thread pool of scoped_timer on memory finalize 
but keep it alive on Z3_memory_reset()
 2020-10-24 12:46:50 +01:00
Nuno Lopes
0213af3c61 replace remaining volatiles with atomic<> 
volatiles are now deprecated in recent C++
 2020-10-24 11:47:45 +01:00
Nikolaj Bjorner
a4aa87b6c9 revert to STL allocated memory to be orthogonal to memory manager behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-22 12:12:32 -07:00
Nikolaj Bjorner
a083633ab4 fix #4749 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-22 12:01:40 -07:00