mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
10524 commits 49 branches 53 tags 182 MiB
Commit graph

10524 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Leonardo de Moura
722cce0cff checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 17:52:07 -08:00
Leonardo de Moura
cf28cbab0a saved params work 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 17:19:12 -08:00
Nikolaj Bjorner
646ace6842 fix bugs uncovered from running non-Horn SDV samples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-29 14:56:09 -08:00