mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity
4827 commits 24 branches 48 tags 158 MiB
Commit graph

4827 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
3b92128ed8 Fixed old-style C variable declaration problem in interpolation C example. 2016-02-16 12:12:59 +00:00
Nuno Lopes
96f6bf7028 ctx_simplify: simplify ite if then/else values become equal 2016-02-15 12:06:20 +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
Christoph M. Wintersteiger
37b11cdc74 Comments, whitespace. 2016-02-07 15:01:09 +00:00
Nikolaj Bjorner
3ef6d91038 fix #434: repeat documentation remarks about reference counting for disambiguation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:46:53 +00:00
Nikolaj Bjorner
677b4bf4fe fix #436, adding more length-based propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:43:53 +00:00
Nikolaj Bjorner
fc1f37efc9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-06 16:14:07 +00:00
Nikolaj Bjorner
5b50d98b89 ensure that seq rewriter gets invoked during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-06 16:13:31 +00:00
Christoph M. Wintersteiger
b61376e8c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-05 15:22:42 +00:00