mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
4548 commits 24 branches 48 tags 158 MiB
Commit graph

3702 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
6aa5ec9f77 Eliminated unused variables 2015-11-23 13:12:05 +00:00
Christoph M. Wintersteiger
59c1944f92 Bugfix for FP casts (float to float conversion). 
Fixes #331.
 2015-11-22 14:49:04 +00:00
Nuno Lopes
d9bafc3fba rewrite scoped_timer for linux 
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory

This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-22 11:40:52 +00:00
Nuno Lopes
b26735a887 fix build with gcc 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-22 11:24:30 +00:00
Nikolaj Bjorner
c1a6163bda disable aig tactic in inc_sat_solver (it can blow up the size of formulas significantly without sharing) and fix configuration update bug for optimization context exposed in example by Corina 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 14:34:31 -08:00
Nikolaj Bjorner
665af3d8b9 remove deprecated user-theory plugins and other unused functionality from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:43:27 -08:00
Nikolaj Bjorner
fd8fd40669 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:00:01 -08:00
Nikolaj Bjorner
0592e76574 Enhancement for Valentin #332 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-19 10:26:01 -08:00
Nikolaj Bjorner
9eb051593d Merge pull request #329 from NikolajBjorner/master 
Remove deprecated API functionality.
 2015-11-19 08:25:22 -08:00
Nikolaj Bjorner
5948013b1b clear label buffer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 18:56:54 -08:00
Nikolaj Bjorner
1d4b996765 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 16:39:51 -08:00
Nikolaj Bjorner
c58e640563 extract labels for optimal model. Fix to #325 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 14:53:08 -08:00
Nikolaj Bjorner
9cba63c31f remove deprecated iz3 example. Remove deprecated process control 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 12:32:15 -08:00
Nikolaj Bjorner
1575dd06a7 expose labels from optimization. Move printing of objectives to after sat/unsat. Cahnge format to something that is somewhat related to how other output is created. Issue #325. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 09:42:12 -08:00
Nikolaj Bjorner
04b0e3c2f7 add checks for cancellation inside mam to agilely not ignore Rustan's soft requests for a timeout #326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 18:48:52 -08:00
Nikolaj Bjorner
d6d301c5eb fix for mising handling of quantifiers in tactic. Bug #324 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 18:38:37 -08:00
Nikolaj Bjorner
66fc873613 Fix for #322: PDR engine cannot falls back on fixed size arithmetic for difference logic. It would eventually overflow and cause incorrect model construction. Enable only fixed-size arithmetic when configuration allows it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 09:00:16 -08:00
Nikolaj Bjorner
3b7dfda0df Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-16 22:59:17 -08:00
Nikolaj Bjorner
c8f09fa955 fix for unsound results reported in #313 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-16 22:59:07 -08:00
Yan
4e9b76365d pass the correct context into And() when doing Tactic.as_expr() 2015-11-16 15:41:12 -08:00
Christoph M. Wintersteiger
e8d37dba9c Added comments for quantifier constructors. Fixes #319. 2015-11-16 21:58:17 +01:00
Christoph M. Wintersteiger
5e6fa5ee6f Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-16 16:01:05 +01:00
Christoph M. Wintersteiger
706a037bf4 Python 3.x string decoding fix 2015-11-16 15:16:50 +01:00
Nikolaj Bjorner
7712c9f9bb Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-15 12:53:57 -08:00
Nikolaj Bjorner
b8e4871d9e disable bottom-up coi filtering when relations contain facts. bug reported by SeanMcL 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-15 10:53:00 -08:00
Nikolaj Bjorner
6ac95048e0 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 18:48:39 -08:00
Nikolaj Bjorner
ab4033133f remove solver_old 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 18:46:49 -08:00
Nikolaj Bjorner
3a3e1796e2 Fix bug #311. update tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 18:42:11 -08:00
Nikolaj Bjorner
f537167080 Fix bug #311 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 18:41:16 -08:00
Nikolaj Bjorner
cb85b60160 Fix issue #311 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 18:13:14 -08:00
Nikolaj Bjorner
bea68cd194 remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 17:05:15 -08:00
Nikolaj Bjorner
0f602d652a remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 13:47:41 -08:00
Nikolaj Bjorner
c2108f74f1 fix uninitialized variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 10:35:06 -08:00
Christoph M. Wintersteiger
6b5e49c4a1 Added checks for uint parameter values in context_params 2015-11-14 17:25:18 +00:00
Bernhard F. Brodowsky
f880433a69 Fixed typo in warning message. 2015-11-14 15:47:47 +01:00
Nikolaj Bjorner
54bb33615e Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-13 15:13:09 -05:00
Nikolaj Bjorner
0a26bcf14c ensure unique symbols when MaxSAT problems are extracted from linear objectives such that multiple objectives can be supported. Fixes issue #308 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-13 15:12:08 -05:00
Christoph M. Wintersteiger
15c48eeaf9 Fix for timeout/rlimit in deprecated solver API. 
Partially fixes #307.
 2015-11-13 16:42:46 +00:00
Christoph M. Wintersteiger
954400cfa2 whitespace 2015-11-13 16:35:08 +00:00
Christoph M. Wintersteiger
4cb96bfe76 Fixed assertion failure in fpa2bv_converter. 
Partially addresses #307
 2015-11-13 15:55:01 +00:00
Christoph M. Wintersteiger
806016c315 build fix 2015-11-13 14:11:39 +00:00
Christoph M. Wintersteiger
643dbb874b Added tactic that translates BV arrays into BV UFs. 2015-11-12 15:27:33 +00:00
Christoph M. Wintersteiger
5f8f0b1280 Added bool rewriter case. 2015-11-12 14:49:21 +00:00
Christoph M. Wintersteiger
5cf2caa7e9 Added check for QF_BV in QF_UFBV tactic. 2015-11-12 14:48:55 +00:00
Christoph M. Wintersteiger
87ae5888ee whitespace 2015-11-12 14:48:29 +00:00
Nikolaj Bjorner
2865f60f8c deal with case of unsatisfiable context and bit-vector objectives that are not normalized to maxsmt. Issue #304 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-11 11:39:34 -05:00
Nikolaj Bjorner
315dc80eb0 toggle default for bv2int decision procedure support to avoid confusing users. Issue #301 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-10 15:09:52 -05:00
Christoph M. Wintersteiger
746689904d Added elim_small_bv_tactic. 2015-11-10 16:23:05 +00:00
Christoph M. Wintersteiger
faace0e6a3 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-09 19:44:40 +00:00
Christoph M. Wintersteiger
1807acdf26 tabs, whitespace 2015-11-09 17:50:50 +00:00