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

4127 commits

Author SHA1 Message Date
Nikolaj Bjorner
29845d037b fix build break on seq evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:48:42 -07:00
Nikolaj Bjorner
89fad8913f fix issue #535 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:16:54 -07:00
Nikolaj Bjorner
05a784fa9e fix issue #535 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:16:19 -07:00
Nikolaj Bjorner
fe4f3e7772 fix regressions exposed in QF_LIA: manager got initialized early and Euclidean solver is not safe even with some throttle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 20:38:18 -07:00
Nikolaj Bjorner
87989dd93e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-23 17:25:23 -07:00
Nikolaj Bjorner
45fdb95f53 fix performance for model construction, recognize concats of values as a value for pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 17:23:57 -07:00
Arie Gurfinkel
4e7b6b6586 proposed fix to compare 2016-03-23 19:20:57 -04:00
Arie Gurfinkel
ee125b4fe3 extend model with the value of a fresh variable 2016-03-23 19:07:50 -04:00
Nikolaj Bjorner
ec681d7565 some of Arie's fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 10:19:16 -07:00
Nikolaj Bjorner
fd6fe87c5d enable qe-lite for UFNIA benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-22 15:41:21 -07:00
Nikolaj Bjorner
72ec6dc8e1 remove debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 16:58:48 -07:00
Nikolaj Bjorner
5e737641b7 remove qe-lite pass in quant_tatics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 16:57:30 -07:00
Nikolaj Bjorner
701f32471e hardening model checker code against cancellations' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 15:04:20 -07:00
Nikolaj Bjorner
3dc2028925 adding min/max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 09:20:57 -07:00
Nikolaj Bjorner
680c28d083 remove nnf conversion which breaks NRA property 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 16:34:04 -07:00
Nikolaj Bjorner
1a5449c3d4 enable new NRA solver for nra benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 12:35:29 -07:00
Nikolaj Bjorner
73e29c6ee6 fix regression warning on invalid case split strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 10:20:43 -07:00
Nikolaj Bjorner
92b5aac12a adjusting new tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 10:13:23 -07:00
Dan Liew
971fd59fbb Fix gcc build broken by f175f864ec. 
C++ enums (unless they are class enums) don't define their own
namespace.
 2016-03-20 10:18:59 +00:00
Nikolaj Bjorner
f0bdcbb3db expose qsat tactic to default tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 18:40:59 -07:00
Nikolaj Bjorner
20bbdfe31a moving remaining qsat functionality over 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:35:26 -07:00
Nikolaj Bjorner
d614fedde2 more merges with qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:41:41 -07:00
Nikolaj Bjorner
76d637626a include more qsat features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:30:24 -07:00
Nikolaj Bjorner
c4472ce717 include more qsat features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:29:23 -07:00
Nikolaj Bjorner
f175f864ec merge useful utilities from qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:01:44 -07:00
Nikolaj Bjorner
f951372f03 fix regression in internalizing bit-vectors, reported by Mikolas Janota 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-18 13:54:42 -07:00
Nikolaj Bjorner
b0f65335ab update copyright year 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-17 13:07:40 -07:00
Nikolaj Bjorner
ab82fee398 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-17 13:06:21 -07:00
Christoph M. Wintersteiger
94054593a4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-17 17:52:32 +00:00
Christoph M. Wintersteiger
cc04fdbd70 Added eager ackermannization to QF_FP, so that small numbers of unspecified operators are eliminated upfront. 2016-03-17 17:52:26 +00:00
Nuno Lopes
f5c4800eec reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs 2016-03-17 15:29:48 +00:00
Nuno Lopes
facb421398 reduce-args: fix unsoundness 2: f(v + 2), where b is quantified 2016-03-17 13:27:07 +00:00
Nuno Lopes
aed4619066 reduce-args: fixed unsoundness introduced in my previous commit 
skip an UF arg if it's quantified
e.g. forall a . f(a, b) -> f(b) (but not f)
 2016-03-17 13:14:43 +00:00
Christoph M. Wintersteiger
c8af48d7ef Bugfix for bvurem0 model evaluation (+1 rewriting step) 2016-03-17 13:09:52 +00:00
Nikolaj Bjorner
22cae143b1 Merge pull request #517 from yaqwsx/expr_values_to_int 
Add methods for obtaining numeral values in C++ API
 2016-03-16 20:43:39 -04:00
Andres Nötzli
34da0a32b9 [Z3py] Fix error in FPRef.__neg__() 
`FPRef.__neg__()` did not work previously because it tried to construct an FPRef from an FPRef (`fpNeg()` already returns an FPRef).
 2016-03-16 17:12:45 -07:00
Christoph M. Wintersteiger
6b2d84b2be Fixed model evaluation/simplification for to_ieee_bv. 2016-03-16 17:46:52 +00:00
Christoph M. Wintersteiger
7ec70c1686 bug fixes for unspecified FP results 2016-03-16 16:57:20 +00:00
Christoph M. Wintersteiger
db6b9faabc Bugfix for FPA rewriter. 2016-03-16 16:35:45 +00:00
Christoph M. Wintersteiger
778c7fcc64 Bugfix for model evaluator and internal, uninterpreted FPA functions. 
Fixes #518
 2016-03-16 16:17:08 +00:00
Christoph M. Wintersteiger
cdc8e1303a Bugfix for fp.to_*_unspecified. 
Fixes #507
 2016-03-16 16:16:29 +00:00
Jan Mrázek
57265f6eb1 Add methods for obtaining numeral values in C++ API 2016-03-16 00:18:49 +01:00
Christoph M. Wintersteiger
99d7a47f82 Bugfixes for unspecified results from fp.to_* (models are still incomplete). 
Relates to #507
 2016-03-15 21:45:54 +00:00
Christoph M. Wintersteiger
3101d281e4 Removed unused variable 2016-03-15 15:12:54 +00:00
Christoph M. Wintersteiger
371573cbff More implementation of fp.to_ieee_bv for unspecified input/output 
Relates to #507
 2016-03-15 15:11:37 +00:00
Christoph M. Wintersteiger
a9df4a208f More bugfixes for fp.to_ieee_bv for unspecified input/output. 
Relates to #507
 2016-03-15 14:58:55 +00:00
Christoph M. Wintersteiger
ce64999ee2 More bugfixes for fp.to_ieee_bv for unspecified input/output 2016-03-15 14:50:59 +00:00
Christoph M. Wintersteiger
176782d62b Bugfix for fp.to_ieee_bv for unspecified input/output. 2016-03-15 14:38:11 +00:00
Christoph M. Wintersteiger
5463167a84 Bugfix for fp.rem (denormal numbers) 
Fixes #508.
 2016-03-14 15:52:09 +00:00
Nikolaj Bjorner
55956df8d8 remove critical sections that are now redundant due to different cancellation model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-13 12:10:14 -04:00