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

4460 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger db2f973e3e Fixed initialization order in bvarray2uf_tactic 2015-11-27 15:34:06 +00:00
Nuno Lopes 2739930900 fix build with clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-27 12:13:44 +00:00
Christoph M. Wintersteiger 8eea6fd775 Bugfix for FPA float to float conversion. 
Fixes #337
 2015-11-24 17:21:40 +00:00
Christoph M. Wintersteiger 5e37cf9bbf Removed potentially unnecessary string decoding in Python API. 2015-11-23 18:41:31 +00:00
Christoph M. Wintersteiger 6aa5ec9f77 Eliminated unused variables 2015-11-23 13:12:05 +00:00
Nikolaj Bjorner 436a51d8f0 fix build of maxsat.c 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-22 22:10:22 -08: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 3be279dc29 fix build break on maxsat.c example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-21 10:36:24 -08: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 95fe9a3a68 Merge pull request #334 from NikolajBjorner/master 
remove deprecated user-theory plugins and other unused functionality …
 2015-11-20 11:47:05 -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 e96d93ee42 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-20 08:02:08 -08:00
Nikolaj Bjorner 995e112a18 fix examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:01:59 -08:00
Nikolaj Bjorner fd8fd40669 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:00:01 -08:00
Christoph M. Wintersteiger d9beb9e15a Windows build fix 2015-11-20 09:57:05 +01:00
Christoph M. Wintersteiger 9175cf195d Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-19 23:27:24 +01:00
Christoph M. Wintersteiger 3ed5945cb2 Fixed Python 2.x vs 3.x issues. 
Fixes Z3Prover/bin#2.
 2015-11-19 23:27:12 +01:00
Christoph M. Wintersteiger 0881c96b2e Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-19 23:24:34 +01:00
Christoph M. Wintersteiger b2281f956b Fixed Python 2.x vs 3.x issues. 
Fixes Z3Prover/bin/#2.
 2015-11-19 23:24:04 +01: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 2122fdee45 fix build script for update to name of get_error_msg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-19 08:33:27 -08:00
Nikolaj Bjorner f859689835 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-19 08:25:35 -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 56c56e277b Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-19 08:04:26 -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 d7c3e77b66 port test_capi.c to use mostly essentially non-deprecated APIs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 18:59:43 -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 86f1753ebf Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-17 09:58:50 -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
Christoph M. Wintersteiger 17a6693db7 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-17 13:55:29 +00:00
Christoph M. Wintersteiger fc05eb65bd Fixed regular expressions in build scripts to expect cross-platform newlines. 2015-11-17 13:55:16 +00:00
Christoph M. Wintersteiger 70069e0ae1 Fixed regular expressions in to expect cross-platform newlines. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-11-17 13:50:11 +00:00
Nikolaj Bjorner 6e1c246454 avoid exception in Ratul's environment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-16 23:06:04 -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
Nikolaj Bjorner 86c43d1d3a Merge pull request #321 from angr/fix/and_context 
pass the correct context into And() when doing Tactic.as_expr()
 2015-11-16 15:55:13 -08:00
Yan 4e9b76365d pass the correct context into And() when doing Tactic.as_expr() 2015-11-16 15:41:12 -08:00
Nikolaj Bjorner 90400ec914 update C example to use new API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-16 15:03:58 -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