mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
17477 commits 23 branches 48 tags 157 MiB
Commit graph

17477 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Leonardo de Moura
f15de18c4a context params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 22:53:55 -08:00
Leonardo de Moura
02e763bb6b env params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 20:56:40 -08:00
Leonardo de Moura
9bd4fd969a cleanning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 18:50:26 -08:00
Leonardo de Moura
29ec68284b Added better error message when old parameter name is used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 18:34:53 -08:00
Leonardo de Moura
92acd6d4ee removed front_end_params from cmd_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 18:19:02 -08:00
Leonardo de Moura
29cf179364 more reorg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 17:03:14 -08:00
Leonardo de Moura
32791204e7 merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 16:36:24 -08:00
Leonardo de Moura
9374a4e20a removed ini_file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 16:30:39 -08:00
Leonardo de Moura
823dd6ca47 missing file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 15:54:53 -08:00
Leonardo de Moura
589f096e6e working on new parameter framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 15:54:34 -08:00
Christoph M. Wintersteiger
f78e595b56 Added QF_FPABV logic, default tactic, and the asIEEEBV conversion function. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-01 15:51:33 +00:00
Leonardo de Moura
be5f933201 removed dead module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 18:20:07 -08:00
Leonardo de Moura
6195ed7c66 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 18:16:02 -08:00
Leonardo de Moura
3e6bddbad1 converted pp_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 17:20:45 -08:00
Nikolaj Bjorner
2d1a6bf270 fix regression for simplifying tails with quantifiers, add some more handling for quantified tails 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-30 15:58:06 -08:00
Leonardo de Moura
4f9442864a auto generation of parameter helper 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 15:31:40 -08:00
Christoph M. Wintersteiger
692593baaa Java API: 32-bit issues and bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 22:31:07 +00:00
Leonardo de Moura
124c0339c1 merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 13:17:41 -08:00
Leonardo de Moura
9246a7a673 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 13:14:42 -08:00
Christoph M. Wintersteiger
9b2236361c Java API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 19:50:57 +00:00
Christoph M. Wintersteiger
d13d6fecbf Java API: added correct error handling. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 19:43:34 +00:00
Leonardo de Moura
caf14b96d4 moving to gparams... 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 11:30:20 -08:00
Christoph M. Wintersteiger
e87e0991f3 Java API: multi-platform fixes 2012-11-30 19:17:05 +00:00
Christoph M. Wintersteiger
3544379f53 Java API: removed platform-dependency of Native.cpp 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 19:10:59 +00:00
Christoph M. Wintersteiger
0c1f2a8281 Java API: Added exception wrappers and build dependencies. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 15:39:25 +00:00
Nikolaj Bjorner
654c02701c pretty print rules with quoted symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-29 19:17:01 -08:00