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

1216 commits

Author SHA1 Message Date
Nikolaj Bjorner
4675643271 fixes to githup issue #133 and stackoverflow reported bug on assertion violation in poly_simplifier_plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 13:49:15 -07:00
Christoph M. Wintersteiger
6980fb3035 Bugfix for distinct of floats. 2015-06-12 12:58:19 +01:00
Nikolaj Bjorner
94f8ecb06d Merge pull request #126 from ahorn/minimum 
Basic infrastructure for minimum aggregation function
 2015-06-11 09:38:39 -07:00
Christoph M. Wintersteiger
31cb81111d Bugfix for fp.roundToIntegral 2015-06-11 16:56:36 +01:00
Alex Horn
bd57994f78 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into minimum 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>

Conflicts:
	src/test/dl_table.cpp
 2015-06-10 20:35:28 +01:00
Nikolaj Bjorner
b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
Alex Horn
140fb7942d Add datalog infrastructure for min aggregation function 
This patch adds an instruction to the datalog interpreter and
constructs a new AST node for min aggregation functions.

The compiler is currently still work in progress and depends on
changes made to the handling of simple joins and the preprocessor.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 18:14:14 +01:00
Nuno Lopes
b65d5797f8 optimize expr_safe_replace for when a subexpression has no substitutions 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-03 17:21:01 +01:00
Christoph M. Wintersteiger
81218c0983 Bugfix for fp.fma 2015-06-02 18:36:19 +01:00
Christoph M. Wintersteiger
a7b12e6321 Bugfix for fp.fma with sbits <= 3 2015-06-02 18:31:09 +01:00
Christoph M. Wintersteiger
17c06199a8 Relaxed BV type checking, follow up to issue #116 2015-06-02 12:46:30 +01:00
Nikolaj Bjorner
d4dd608bad improve type checking and reporting, fixes issue #116 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-01 14:11:31 -07:00
Nikolaj Bjorner
46a5aeaef1 improve type checking and reporting, fixes issue #116 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-01 14:10:22 -07:00
Christoph M. Wintersteiger
8d55159dc8 Proper declaration of locals to make clang happy. 2015-05-30 15:23:30 +01:00
Christoph M. Wintersteiger
fde873ac09 Bugfix for rounding in FP to_sbv. 
Fixes #113
 2015-05-30 14:50:15 +01:00
Christoph M. Wintersteiger
e240e6c430 Bugfix for variable renamings (fec815b41e) 2015-05-30 12:12:23 +01:00
Christoph M. Wintersteiger
fec815b41e Various variable renamings to avoid conflicts with previously defined local variables, function parameters, or members (Visual Studio 2015 warnings). 2015-05-29 18:13:39 +01:00
Christoph M. Wintersteiger
d35ebd6e57 Bugfix for FP to_fp from non-numeral reals. 2015-05-29 14:49:26 +01:00
Christoph M. Wintersteiger
9428acd578 Bugfix for FPA rewriter. 2015-05-29 13:58:33 +01:00
Christoph M. Wintersteiger
7619d609f9 FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. 
Fixes #68
 2015-05-28 12:20:48 +01:00
Nuno Lopes
c577ab361b fix assorted undefined behaviors caught by clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 11:45:12 +01:00
Christoph M. Wintersteiger
6f6cd61817 Bugfix for float-to-float conversion. 
Fixes #77
 2015-05-22 20:30:12 +01:00
Christoph M. Wintersteiger
8fc0ba0ab5 Moved auxiliary fp.isNaN lemma injection to the right place. 
Fixes #102
 2015-05-22 12:33:53 +01:00
Nikolaj Bjorner
8a34bd2bf1 fixes issue #88 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-21 15:08:39 -07:00
Nikolaj Bjorner
a3c5207f91 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-21 15:07:24 -07:00
Nikolaj Bjorner
c969d78042 throw exception instead of debug mode assertion in ast_manager on malformed input 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-21 15:07:01 -07:00
Christoph M. Wintersteiger
6f575689b1 Added injection of auxiliary lemmas for fp.isNaN, so that the value propagation can pick up these values and propagate them. 
Fixes #96.
 2015-05-21 19:02:09 +01:00
Christoph M. Wintersteiger
eee076b9f8 Bugfixes for fp.min, fp.max. 
Fixes the fix for #68
 2015-05-21 18:16:02 +01:00
Christoph M. Wintersteiger
8c18bdcca9 Bugfix for fp.roundToIntegral. 
Fixes #69
 2015-05-21 18:12:14 +01:00
Nikolaj Bjorner
cd8f82ebc2 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-20 10:41:50 -07:00
Nikolaj Bjorner
9d0e3abd24 use static features to set hidden configuration parameters on small integers and int vs. real 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-20 10:41:41 -07:00
Christoph M. Wintersteiger
51040d3e19 Bugfix for fp.isNormal 2015-05-20 18:32:40 +01:00
Christoph M. Wintersteiger
1e3952406c disabled debug output 2015-05-20 18:14:38 +01:00
Christoph M. Wintersteiger
c377fec7a4 Made fp.* comparison chainable. 2015-05-20 17:57:27 +01:00
Christoph M. Wintersteiger
0197f6e010 Bugfix for fp.rem when the result is zero. 
Fixes #91
 2015-05-19 16:51:56 +01:00
Christoph M. Wintersteiger
32fb679066 tabs 2015-05-19 11:01:15 +01:00
Nuno Lopes
d8dc86f558 Merge branch 'unstable' of https://github.com/mschlaipfer/z3 into unstable 2015-05-18 16:38:19 +01:00
Nikolaj Bjorner
afea50e631 remove assertion from integer constructor, rely on exceptions for API abuse 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-17 22:49:59 +01:00
Matthias Schlaipfer
c82319b358 Refactor count_vars and count_rule_vars 
ast_manager m was not used
 2015-05-14 17:04:38 +01:00
Nikolaj Bjorner
ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Christoph M. Wintersteiger
a63481de85 New implementations of fp.roundToIntegral in mpf and fpa2bv. 
Partially fixes #69
 2015-05-06 19:19:03 +01:00
Christoph M. Wintersteiger
53b479e1c3 Bugfix for fp.rem(0, 0). 
Fixes #70.
 2015-05-06 12:24:18 +01:00
Christoph M. Wintersteiger
73eb7cbf5c Bugfix for mpf roundToIntegral. 
Partially fixes #69
 2015-05-05 23:53:33 +01:00
Christoph M. Wintersteiger
57af3a4c6e FPA min/max refactoring and fixes. 
Fixes #68

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-05-04 13:47:04 +01:00
Nikolaj Bjorner
9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Christoph M. Wintersteiger
1d49f61b9a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into contrib 
Conflicts:
	README
	src/api/ml/build-lib.sh
	src/api/ml/z3.ml
	src/api/ml/z3.mli
	src/api/ml/z3_stubs.c
 2015-04-28 15:19:08 +01:00
Nikolaj Bjorner
620c11932b type check distinct operator. fixes #62 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-27 11:10:37 -07:00
Christoph M. Wintersteiger
abe73db702 FP: bugfix for get_some_value which couldn't produce rounding-mode values. 2015-04-25 15:19:48 +01:00
Christoph M. Wintersteiger
4768a360f8 FP: Fix for conversion functions from non-FP 0 to +0.0 even when the rounding mode is ToNegative. 2015-04-25 15:01:20 +01:00
Nikolaj Bjorner
6c1a5390ef fix big-int bug for shift amounts, github issue 44, reported by Dejan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-20 10:20:06 +02:00