mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
6089 commits 49 branches 53 tags 182 MiB
Commit graph

6089 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
16a69e750a fix break in configure 2016-02-01 17:38:14 +00:00
Nuno Lopes
ea55bd495f add new API function Z3_get_estimated_alloc_size() that returns *estimated* allocated memory size by Z3 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-02-01 17:19:55 +00:00
Nuno Lopes
b9c0578eea fix build on C++98 compilers 2016-02-01 17:12:22 +00:00
Nikolaj Bjorner
fe6799699c Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-01 07:51:26 -08:00
Nikolaj Bjorner
995a2e1a29 perf tuning based on Chris's examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 07:51:05 -08:00
Nuno Lopes
cc6769c866 improve bit-blasting for the case (bvsrem var power-of-two) 
We will now transform bvsrem into an extract + zero extend
Gives ~40% speedup in selected benchmarks

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-02-01 13:46:55 +00:00
mikolas
de28e57dee Adding parameters to Ackermannization in qfbv_tactic. 2016-01-29 17:21:21 +00:00
mikolas
c9799b143d Adding parameters to Ackermannization in qfbv_tactic. 2016-01-29 17:18:21 +00:00
Mikolas Janota
470b5c20fe Small modifs in ackermannization. 2016-01-29 16:43:18 +00:00
mikolas
2ce7dc68ad Adding a probe for estimating the number of Ackermann congruence lemas. 2016-01-29 15:37:10 +00:00
Nikolaj Bjorner
2115111dac update display method for datalog to use predicates, throttle use of extensionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 20:23:06 -08:00
Mikolas Janota
2141a075ba Refactoring ackermannization functionality. 2016-01-28 18:24:54 +00:00
Mikolas Janota
3e94a44540 Refactoring ackermannization functionality. 2016-01-28 18:18:42 +00:00
Nikolaj Bjorner
847607bda7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-28 08:51:40 -08:00
Nikolaj Bjorner
30f8110488 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:51:04 -08:00
Nikolaj Bjorner
b352d43e50 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:50:13 -08:00
Mikolas Janota
53c187671f Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-28 11:48:20 +00:00
mikolas
acd01c7778 Adding a probe for qf_ufbv and applying it in the qfufbv_ackr_tactic. 2016-01-28 11:46:31 +00:00
Christoph M. Wintersteiger
20df9e1cd1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-28 11:14:11 +00:00
Christoph M. Wintersteiger
5f0ea74e89 Made ufbv-rewriter tactic public 2016-01-28 11:14:01 +00:00
Nikolaj Bjorner
512aa0e8d3 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-27 14:47:24 -08:00
Nikolaj Bjorner
87228b6a9d add a little more verbiage to description of simplify. Issue #424 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-27 14:47:15 -08:00
Nuno Lopes
ac2e8f8b57 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-27 18:09:36 +00:00
Nuno Lopes
ee2bae898a remove unused exceeded_memory_allocations class 2016-01-27 18:09:24 +00:00
Mikolas Janota
28a5c27e33 Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-27 16:27:35 +00:00
Mikolas Janota
e318d460d7 dbg printing 2016-01-27 16:27:31 +00:00
mikolas
956d774299 Detecting OP_BSDIV0, etc. as uninterpreted functions in ackermannization. 2016-01-27 16:22:28 +00:00
Mikolas Janota
4b37140780 small fix 2016-01-26 18:11:33 +00:00
Nikolaj Bjorner
6529d43fb1 fix bugs exposed by unit tests from Pierre 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 09:50:14 -08:00
Mikolas Janota
e7477e2f6a Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:51 +00:00
Mikolas Janota
0dc8dc4d8e Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:30 +00:00
Mikolas Janota
470f8bca73 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-26 16:51:57 +00:00
Mikolas Janota
c63f9f4912 Moving things around. Adding tactic just for ackermannization. 2016-01-26 16:50:00 +00:00
Nikolaj Bjorner
8e378062e2 add get-some-value to seq API, expose quantifier tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 08:05:44 -08:00
Nikolaj Bjorner
345f6e87bd seq bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 07:21:31 -08:00
Mikolas Janota
3978410fcb Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-26 14:23:50 +00:00
mikolas
d32c9449b2 Editing some comments and also enabling to export the ackermannized formula as a gole. 2016-01-26 11:53:47 +00:00
Mikolas Janota
c2edf2c5bf Merge remote-tracking branch 'upstream/master' into lackr 2016-01-25 13:04:46 +00:00
Nikolaj Bjorner
924f03c6de fixing bugs in seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-23 10:38:49 -05:00
Nikolaj Bjorner
993a0434b4 fix warning message for unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 23:47:35 -05:00
Nikolaj Bjorner
099e572a26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 19:10:08 +01:00
Nikolaj Bjorner
a021e51a9c make parse error a bit more informative 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 19:09:41 +01:00
Nuno Lopes
23cc8258fe remove m_ast_lim from API context since that one isn't used either 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-01-19 15:37:58 +00:00
Nuno Lopes
1f872e720d remove m_replay_stack from API context since it's never used 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-01-19 15:19:00 +00:00
Nikolaj Bjorner
d9e4648d8d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 13:57:59 +01:00
Nikolaj Bjorner
cccd502a4d bug-fixes to sequence theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 13:57:47 +01:00
Christoph M. Wintersteiger
4dba5270ad Efficiency fix for fp.div. 2016-01-18 18:09:29 +00:00
Christoph M. Wintersteiger
99176cca60 Bugfix for FP model converter. 2016-01-18 18:00:04 +00:00
Nikolaj Bjorner
c9373ebc9f fix axiomatization for at 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 12:01:15 +05:30
Nikolaj Bjorner
6aed3c3a44 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-18 11:09:52 +05:30