mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 17:59:24 +00:00
Code Activity
5757 commits 44 branches 52 tags 177 MiB
Commit graph

5757 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
bd73bd9177 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-03 17:11:58 +00:00
Nikolaj Bjorner
6fef24edb4 recursive function definitions; combine model-building functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-03 08:07:06 -08:00
Nikolaj Bjorner
50b2389e7f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-03 07:59:13 -08:00
Nikolaj Bjorner
7c6540e18f recursive function definitions; combine model-building functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-03 07:59:03 -08:00
Christoph M. Wintersteiger
1aeea763ff Assertion fix in inc_sat_solver 2016-03-02 18:39:28 +00:00
Christoph M. Wintersteiger
e79960b253 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-02 18:27:30 +00:00
Christoph M. Wintersteiger
bf40bb8005 Bugfix for inc_sat_solver 2016-03-02 18:27:01 +00:00
Christoph M. Wintersteiger
68416bf6bc whitespace 2016-03-02 18:25:56 +00:00
Christoph M. Wintersteiger
bddf416064 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-02 18:06:22 +00:00
Christoph M. Wintersteiger
dbf9609b4c added assertion 2016-03-02 18:06:14 +00:00
Christoph M. Wintersteiger
f128c76f23 whitespace 2016-03-02 18:05:14 +00:00
Christoph M. Wintersteiger
b27977ea90 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-02 15:14:12 +00:00
Christoph M. Wintersteiger
6fa2338edc Merge pull request #471 from 4tXJ7f/patch-1 
[Z3py] Fix documentation in FPSortRef
 2016-03-02 14:14:54 +00:00
Nikolaj Bjorner
1a081936ac Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 22:31:53 -08:00
Nikolaj Bjorner
a25336a899 fix test build, working on rec-functions and automata complementation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 22:31:44 -08:00
Andres Nötzli
18b9cd1948 [Z3py] Fix documentation in FPSortRef 2016-03-01 18:56:20 -08:00
Christoph M. Wintersteiger
1e86175c03 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 21:21:32 +00:00
Christoph M. Wintersteiger
59e695f2be Bugfixes for FP numerals in Python 
Relates to #464, #470
 2016-03-01 21:21:25 +00:00
Nikolaj Bjorner
9b6963d112 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 09:48:53 -08:00
Nikolaj Bjorner
67397bf71e enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:48:24 -08:00
Christoph M. Wintersteiger
0cb8193cdd logic fix 2016-03-01 17:42:33 +00:00
Christoph M. Wintersteiger
4fe4db6657 build fix for static libray on Windows 2016-03-01 17:34:45 +00:00
Nikolaj Bjorner
7f51ecab37 enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:26:14 -08:00
Nikolaj Bjorner
31c58b0999 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 08:46:51 -08:00
Nikolaj Bjorner
908f09a9df update logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 08:46:43 -08:00
Christoph M. Wintersteiger
c171170bed Fixed FP string input conversions. 
Fixes #464
 2016-03-01 15:31:33 +00:00
Christoph M. Wintersteiger
b6e43b6d7b Merge pull request #468 from 4tXJ7f/fix_fp_neq 
[Z3py] Consistent behavior of eq and ne for FP
 2016-03-01 14:07:28 +00:00
Christoph M. Wintersteiger
ad9127690d Merge branch '4tXJ7f-fix_build' 2016-03-01 14:05:30 +00:00
Christoph M. Wintersteiger
5c35a07a46 Merge branch 'master' of https://github.com/Z3Prover/z3 into 4tXJ7f-fix_build 
# Conflicts:
#	src/math/automata/symbolic_automata_def.h
 2016-03-01 14:05:19 +00:00
Nuno Lopes
62e46aacd9 bv_bounds: make may_simplify more precise to skip exprs with just 1 bound expr 
speedups up to 3x in selected benchmarks
 2016-03-01 11:31:08 +00:00
Nuno Lopes
33431ef922 fix build with gcc 2016-03-01 10:02:24 +00:00
Nuno Lopes
10ea36bfed fix build with gcc 2016-03-01 10:00:58 +00:00
Andres Notzli
91d6b2cbbb [Z3py] Consistent behavior of eq and ne for FP 
Before, x == y and x != y were returning inconsistent expressions (i.e.
`Not(x == y)` was not the same as `x != y`):

>>> x = FP('x', Float32())
>>> y = FP('y', Float32())
>>> (x == y).sexpr()
'(= x y)'
>>> (x != y).sexpr()
'(not (fp.eq x y))'

`=` does not have the same semantics as `fp.eq` (e.g. `fp.eq` of +0.0
and -0.0 is true while it is false for `=`).
This patch removes the __ne__ method from FPRef, so `x == y` and `x !=
y` use the inherited operations while fpEQ and fpNEQ can be used to
refer to `fp.eq(..)`/`Not(fp.eq(..))`.
 2016-03-01 00:21:10 -08:00
Nikolaj Bjorner
830a99aab4 finish minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 00:04:03 -08:00
Andres Notzli
570bc3c9c1 Fix build 
Previous commits seem to have removed some variable declarations, so the
build did not work. This patch reintroduces the variables.
 2016-02-29 23:41:33 -08:00
Nikolaj Bjorner
4a15d756d7 uint64_t -> uint64 for cross platform 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 22:16:03 -08:00
Nikolaj Bjorner
b90bc4e685 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 21:15:44 -08:00
Nikolaj Bjorner
3b6eef05c9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-29 20:23:29 -08:00
Nikolaj Bjorner
6cf76f2113 remove references to _DEBUG use Z3DEBUG instead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 20:23:20 -08:00
Nikolaj Bjorner
6f45970b6e Merge pull request #466 from 4tXJ7f/patch-1 
Fix documentation for floating-point comparisons
 2016-02-29 20:22:57 -08:00
Andres Nötzli
c9269c1983 Fix documentation for floating-point comparisons 2016-02-29 19:12:14 -08:00
Nikolaj Bjorner
7ac5e67538 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-29 17:04:32 -08:00
Nikolaj Bjorner
c6c84dd59a update documentation help to be inline with fpLT. Issue #465 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 17:04:26 -08:00
Nuno Lopes
43202572ee bv_bounds: switch from rational to uint64 
this limits the analysis to 64-bit BVs, but gives a speedup of up to one order of magnitude
 2016-02-29 17:23:54 +00:00
Nikolaj Bjorner
9efc7f4aea turn on model completion in validation code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 09:06:20 -08:00
Nikolaj Bjorner
d89c39cbe2 apply t() 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 08:36:25 -08:00
Nuno Lopes
006dc147a8 fix build with gcc 5 2016-02-29 14:34:48 +00:00
Nikolaj Bjorner
7656adc483 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-28 17:05:52 -08:00
Nikolaj Bjorner
df2d7e7628 add intersection using symbolic automata facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-28 17:05:12 -08:00
Nuno Lopes
c1eb1cc3f2 bv_bounds: improve perf of push/pop 2016-02-28 20:07:39 +00:00