mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
5610 commits 46 branches 52 tags 178 MiB
Commit graph

5610 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
0254b1f7ff ML API bug fixes 2016-02-15 13:28:22 +00:00
Christoph M. Wintersteiger
0dc85620aa ML API bug fix 2016-02-15 13:01:00 +00:00
Christoph M. Wintersteiger
733c115722 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-02-15 12:54:11 +00:00
Christoph M. Wintersteiger
62cae4186b ML API bug fixes 2016-02-15 12:54:05 +00:00
Nuno Lopes
96f6bf7028 ctx_simplify: simplify ite if then/else values become equal 2016-02-15 12:06:20 +00:00
Christoph M. Wintersteiger
18c0a3bfaf removed comments 2016-02-14 19:57:21 +00:00
Christoph M. Wintersteiger
b99fcb9c8a More new OCaml API 2016-02-14 19:56:22 +00:00
Christoph M. Wintersteiger
824169da0a New OCaml API 2016-02-13 22:09:45 +00:00
Nikolaj Bjorner
8fc58e1ace propagate bounds implementation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-13 02:07:41 +00:00
Nikolaj Bjorner
d7186eede8 bv bounds tactic for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-13 00:13:16 +00:00
Nikolaj Bjorner
e484fc365d add outline of bv bounds tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 22:57:47 +00:00
Nikolaj Bjorner
94be6fc776 remove passing suffixes into pdr_sym_mux, trying to isolate cause of issue #420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 19:25:52 +00:00
Nikolaj Bjorner
660eff0b9e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-12 18:59:05 +00:00
Nikolaj Bjorner
45999b254c hoist simplifier functionality out of context loop to allow plugging in other contextual simplification methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 18:58:37 +00:00
Christoph M. Wintersteiger
6319861e26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-12 18:32:46 +00:00
Christoph M. Wintersteiger
da502a79dc Merge branch 'cheshire-codesmells' 2016-02-12 18:32:25 +00:00
Christoph M. Wintersteiger
f399fe5e1d resolved conflicts 2016-02-12 18:29:46 +00:00
Christoph M. Wintersteiger
3356f36b8f Merge pull request #446 from msullivan/arm-build 
Fix gcc build failure on ARM caused by including <emmintrin.h>
 2016-02-12 18:27:14 +00:00
Nikolaj Bjorner
e2dc7c6f64 add note that current re.complement is non-standard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 17:12:43 +00:00
Nikolaj Bjorner
94453033b6 add partial support for complementation of regular expressions. Handles case of complementing character ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 15:59:33 +00:00
Christoph M. Wintersteiger
9dbb8057ca Merge pull request #449 from kenmcmil/issue243 
fixed logging on return of Z3_compute_interpolant...
 2016-02-12 12:40:01 +00:00
Nikolaj Bjorner
8d61d36c3f add documentation methods to param_descrs, add C++ API and example for param_descrs. Issue #443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 11:45:00 +00:00
Ken McMillan
8b90bc9e91 fixed logginf on return of Z3_compute_interpolant and added interpolation example to test_capi.c 2016-02-11 16:09:54 -08:00
Michael Sullivan
fa598edf43 Fix gcc build failure on ARM caused by including <emmintrin.h> 
src/util/hwf.cpp tries to use <emmintrin.h> to directly use SSE
intrinsics. Make sure to only use those when actually on x86 or
x86_64.
 2016-02-10 20:47:08 +00:00
Nikolaj Bjorner
9ed7dadc02 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-10 15:02:28 +00:00
Nikolaj Bjorner
a6e1c70eab fix documentation/default bug. #445 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 15:02:22 +00:00
Christoph M. Wintersteiger
fa68b00563 Cleanliness 2016-02-10 14:39:33 +00:00
Christoph M. Wintersteiger
8c80ed33fa Merge branch 'MikolasJanota-lackr' 2016-02-10 14:26:20 +00:00
Christoph M. Wintersteiger
c01f0323c3 Merge branch 'lackr' of https://github.com/MikolasJanota/z3 into MikolasJanota-lackr 2016-02-10 14:26:04 +00:00
Nikolaj Bjorner
84cf208d5f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-10 12:02:51 +00:00
Nikolaj Bjorner
535fb39313 add documentation comments as raised in #443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 12:02:40 +00:00
Nikolaj Bjorner
56f15e98b5 Merge pull request #444 from delcypher/explicit_solver_timeout_units 
Explicitly state what the units of the timeout parameter for the "smt" module are.
 2016-02-10 11:43:31 +00:00
Dan Liew
ea900db337 Explicitly state what the units of the timeout parameter for the "smt" 
module are.
 2016-02-10 11:35:15 +00:00
Nikolaj Bjorner
5285a795ac handle configuration passed in as null, deal with crash in logs attached to issue #243 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 01:20:16 +00:00
Nikolaj Bjorner
cacfa0cb98 fix build, likely addressing issue #420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:58:08 +00:00
Nikolaj Bjorner
a0503ba6a1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 22:24:48 +00:00
Nikolaj Bjorner
6c6da44f8f removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:24:37 +00:00
Nikolaj Bjorner
5ce85aba40 removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:23:37 +00:00
Christoph M. Wintersteiger
a16f524eae Install target fix for ocamlfind_install on Windows. 
Relates to #409
 2016-02-09 19:58:52 +00:00
Mikolas Janota
73ef125171 Merge remote-tracking branch 'upstream/master' into lackr 2016-02-09 17:28:24 +00:00
Christoph M. Wintersteiger
4ba744987d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 16:38:42 +00:00
Christoph M. Wintersteiger
3df9fea54c removed unused variables 2016-02-09 16:38:35 +00:00
Nuno Lopes
564343c39c remove unused methods in ast.cpp 2016-02-09 15:30:05 +00:00
Nikolaj Bjorner
60c0e73b2f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 11:08:52 +00:00
Nikolaj Bjorner
133e3693de fix bug in replace built-in and move length-equality propagation to branch final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 11:08:33 +00:00
Christoph M. Wintersteiger
a2f376f9d6 Fixed memory leak in theory_fpa. Relates to #436 2016-02-08 17:17:49 +00:00
Christoph M. Wintersteiger
7e2783c6a2 Fixed javadoc links in comments. 
Relates to #401.
 2016-02-08 15:25:53 +00:00
Mikolas Janota
b614e7732b Merge remote-tracking branch 'upstream/master' into lackr 2016-02-08 12:54:22 +00:00
Christoph M. Wintersteiger
92b6a3e134 Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits). 
Fixes #439.
 2016-02-07 17:33:33 +00:00
Christoph M. Wintersteiger
e9d94e53f6 Improved FPA simplifier plugin 2016-02-07 15:01:22 +00:00