mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
7903 commits 49 branches 53 tags 182 MiB
Commit graph

7903 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
92a29b1e43 added Z3_global_param_reset_all API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:55:12 -08:00
Christoph M. Wintersteiger
fda39bffe2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-04 19:33:11 +00:00
Christoph M. Wintersteiger
334ec57ea4 Java API: refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-04 19:33:01 +00:00
Christoph M. Wintersteiger
acd251e554 .NET API: bugfix. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-04 19:32:46 +00:00
Christoph M. Wintersteiger
4d1d784a1c Java+.Net Examples: refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-04 19:32:20 +00:00
Leonardo de Moura
7d24cd4ae3 merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:18:10 -08:00
Leonardo de Moura
ff999773b2 adjusting verbose msgs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:17:24 -08:00
Leonardo de Moura
9754ccf8a1 fixing problems with the new parameter framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:16:42 -08:00
Josh Berdine
f7528456da Fix slight inconsistencies in use of \sa 2012-12-04 03:44:00 +00:00
Leonardo de Moura
8191cc1951 fixed problems with logger and invalid assertion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 18:44:27 -08:00
Leonardo de Moura
f0f90eecaa Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 16:58:56 -08:00
Leonardo de Moura
54e452a1af chasing bug in the Java bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 16:58:44 -08:00
Nikolaj Bjorner
1cd1a42618 cleanup, fix repeated use of fmls in validator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-03 16:02:04 -08:00
Leonardo de Moura
0ec6e2f218 adjusting examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 15:19:47 -08:00
Nikolaj Bjorner
72e09759ee factor out relation context for datalog 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-03 15:13:45 -08:00
Nikolaj Bjorner
67183ea08a factor out relation context for datalog 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-03 15:05:43 -08:00
Leonardo de Moura
6d7d205e13 fixed more problems in the new param framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 15:02:34 -08:00
Leonardo de Moura
d634c945bf renamed validate_model --> model_validate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 13:44:39 -08:00
Leonardo de Moura
847c5f9691 fixing problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 11:55:24 -08:00
Nikolaj Bjorner
8425685ea3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 11:02:08 -08:00
Nikolaj Bjorner
5c11f394cd port to new parameter infrastructure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-03 11:01:33 -08:00
Christoph M. Wintersteiger
006822a931 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 17:57:38 +00:00
Christoph M. Wintersteiger
eb3fa254d8 Java API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-03 17:56:42 +00:00
Leonardo de Moura
8744b26d06 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 09:37:57 -08:00
Leonardo de Moura
b219b875b1 fixed bug in using-params combinator in the SMT 2.0 front-end 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 09:37:15 -08:00
Nikolaj Bjorner
67485b8af7 fixing handling of arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-03 08:29:28 -08:00
Nikolaj Bjorner
361e9039bb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 08:14:54 -08:00
Christoph M. Wintersteiger
42f06b1012 FPA bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-03 15:13:11 +00:00
Leonardo de Moura
a99b8fe797 exposed rewriter parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 22:03:30 -08:00
ThanhVu (Vu) Nguyen
f533e5cfd7 added is_expr_var and is_expr_val to check if a given expression is a value or a variable 2012-12-02 23:42:16 -05:00
ThanhVu (Vu) Nguyen
a37fd146b0 added is_expr_var and is_expr_val to check if a given expression is a value or a variable 2012-12-02 23:41:31 -05:00
Leonardo de Moura
91096b638a better help 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 17:18:25 -08:00
Leonardo de Moura
0934cb06d8 exposed sat params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 16:38:33 -08:00
Nikolaj Bjorner
6a3e2d0f00 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-02 15:33:24 -08:00
Nikolaj Bjorner
a813c384a6 fix bug in proof generation for PDR, add more features for handling quantifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-02 15:33:18 -08:00
Leonardo de Moura
773f82a44c connected smt_params with new parameter infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 14:47:34 -08:00
Leonardo de Moura
5057257e40 removed unnecessary README 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 13:18:33 -08:00
Leonardo de Moura
fa53b1eb92 added module descriptions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 13:15:56 -08:00
Leonardo de Moura
1871bef6e1 cleaned algebraic params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 12:47:20 -08:00
Leonardo de Moura
b7f636984e merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 12:24:45 -08:00
Leonardo de Moura
624115ea6d exposed pattern inference params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 12:24:27 -08:00
Leonardo de Moura
32854c677c exposed old simplifier parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 12:10:06 -08:00
Leonardo de Moura
c82b8174d8 fixed win compilation bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 12:08:58 -08:00
Leonardo de Moura
8d62c95a54 fixed mk_make 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 11:31:38 -08:00
Leonardo de Moura
6a220c8b58 moved old params files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 11:27:39 -08:00
Leonardo de Moura
6107e8d9ce moved old params files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 10:47:04 -08:00
Leonardo de Moura
ffb7e26c75 removed front-end-params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 10:05:29 -08:00
Leonardo de Moura
288a96610f ported VCC trace streams 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 09:08:47 -08:00
Leonardo de Moura
80405dbd62 added context_params to API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 08:12:15 -08:00
Leonardo de Moura
1c15e078a4 cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 23:00:06 -08:00