mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
4927 commits 49 branches 53 tags 182 MiB
Commit graph

511 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
ecceb0accc FPA: debug output disabled. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 20:16:02 +01:00
Christoph M. Wintersteiger
92c1b25978 FPA: bugfix for float to float conversion (subnormal numbers). 
Thanks to Gabriele Paganelli for reporting this bug!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 20:14:00 +01:00
Christoph M. Wintersteiger
455618bb2b FPA: added is_nan 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:34:31 +01:00
Christoph M. Wintersteiger
d7639557d2 FPA: added rewriting and fpa2bv conversion rules for new operations. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:03:46 +01:00
Christoph M. Wintersteiger
724f2af8c7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-07 17:34:38 +01:00
Leonardo de Moura
2b59f2ecc2 Fix issue https://z3.codeplex.com/workitem/37 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 18:29:29 -07:00
Christoph M. Wintersteiger
093fe945bc FPA: min/max/fma bugfixes + partial quantifier support 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:19:45 +01:00
Christoph M. Wintersteiger
7c32df93a4 SLS tactic: compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:17:41 +01:00
Nuno Lopes
878d57d139 minor code simplification 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-15 09:23:57 -07:00
Nuno Lopes
7fc93b94f5 remove unimplemented method 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-14 08:54:04 -07:00
Christoph M. Wintersteiger
787a65be29 FPA: bugfix for QFPA -> QBV conversion. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-07 18:27:47 +01:00
Christoph M. Wintersteiger
b65adc10da FPA: bugfix for quantified FP -> quantified BV conversion. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-07 17:58:43 +01:00
Christoph M. Wintersteiger
121e83b6b7 FPA: bugfixes for UF in model converter for fpa2bv. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-03 17:54:30 +01:00
Christoph M. Wintersteiger
8f60a936d2 FPA: Added support for float-UF to BV-UF translation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-03 15:57:42 +01:00
Christoph M. Wintersteiger
00d5dea9a5 FPA: added support for rewriting quantified floats to quantified bit-vectors. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-02 15:24:07 +01:00
Nikolaj Bjorner
83add2bd9b fix bugs reported by Filip Konecny <filip.konecny@epfl.ch> in PDR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-25 13:39:11 -07:00
Nikolaj Bjorner
eead1bbc48 missing else 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 09:24:39 -07:00
Nikolaj Bjorner
e1d5f484f1 simplify result from tactics, remove unused features from difference logic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 08:46:46 -07:00
Nuno Lopes
7ce88d4da9 fix a few compilation warnings 
- remove unused variables and class fields
 - add support for gcc 4.5 & clang's __builtin_unreachable
 - fix 2 bugs related to strict aliasing
 - remove a few unused function parameters

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-21 14:36:39 -07:00
Leonardo de Moura
8627f6f1d5 Remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 18:02:28 -07:00
Leonardo de Moura
93297fa9e7 Fix bug in purify_arith reported at https://z3.codeplex.com/workitem/32 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 18:00:43 -07:00
Christoph M. Wintersteiger
5915533170 FPA: bugfix for corner-case sign of division 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-04-05 15:27:05 +01:00
Christoph M. Wintersteiger
26efb3c7f1 FPA bugfixes for denormal numbers. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-04-05 12:45:28 +01:00
Christoph M. Wintersteiger
4c353ec720 FPA: bugfix for model completion. Thanks to Levent Erkok. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-04-02 13:45:42 +01:00
Leonardo de Moura
9abcde9a35 Fix typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-25 14:42:18 -07:00
Christoph M. Wintersteiger
a9c7517275 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-08 13:22:06 +00:00
Nikolaj Bjorner
37a75622a9 LRA tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-06 08:32:21 -08:00
Nikolaj Bjorner
f9aeeeef36 LRA tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-06 08:29:29 -08:00
Christoph M. Wintersteiger
e5307300de FPA: bugfixes in mul() and abs() 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-06 15:04:58 +00:00
Christoph M. Wintersteiger
9a4331995e FPA: bugfix for bitblaster. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-05 14:11:50 +00:00
Christoph M. Wintersteiger
35906889b6 FPA: compilation bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-05 13:49:42 +00:00
Christoph M. Wintersteiger
e5f03f999a FPA: Added conversion operator float -> float. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-04 20:21:14 +00:00
Christoph M. Wintersteiger
7822b86b53 FPA: multiple bugfixes for HWF, MPF and a bugfix for FPA2BV (many thanks to Gabriele Paganelli) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-01 19:06:01 +00:00
Christoph M. Wintersteiger
6f3850bfbc FPA bug and leak fixes (thanks to Gabriele Paganelli) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-28 18:46:29 +00:00
Leonardo de Moura
4922d62311 Fix bug reported at http://z3.codeplex.com/workitem/23 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-21 11:02:13 -08:00
Leonardo de Moura
97bf9418f7 Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-20 13:41:08 -08:00
Christoph M. Wintersteiger
c051876e3f FPA bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-31 12:49:43 +00:00
Christoph M. Wintersteiger
61b686f86f FPA: fixes for sbits < ebits 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-11 11:15:18 +00:00
Leonardo de Moura
53df82c314 Add arith_decls for underspecified operators 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-26 11:35:00 -08:00
Leonardo de Moura
d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 17:14:25 -08:00
Leonardo de Moura
cec328cfdc Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 14:44:51 -08:00
Leonardo de Moura
607fab486c Fix incorrect uses of set_cancel() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 18:48:10 -08:00
Leonardo de Moura
7e66a65e98 Add blast_distinct_threshold option to rewriter. Enable blast_distinct in the QF_LIA default strategy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 10:32:00 -08:00
Leonardo de Moura
9634d66699 Fix typo in tactic selection 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-15 08:10:48 -08:00
Leonardo de Moura
4df172e971 Fix file name (use same naming convention) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-14 09:04:20 -08:00
Leonardo de Moura
e0f4d870fd Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-13 14:03:58 -08:00
Leonardo de Moura
528f348022 Fixed bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-11 17:51:49 -08:00
Leonardo de Moura
8198e62cbd solver factories, cleanup solver API, simplified strategic solver, added combined solver 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-11 17:47:27 -08:00
Leonardo de Moura
6ae6414236 avoiding clang warning messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 15:04:14 -08:00
Leonardo de Moura
a07b459fdf Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 12:53:51 -08:00