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

1097 commits

Author SHA1 Message Date
Leonardo de Moura
f8014f54c1 Fix bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 15:13:05 -08:00
Nikolaj Bjorner
635aabf2d5 fix get_implied equalities and the unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-11 21:39:31 -08:00
Leonardo de Moura
8198e62cbd solver factories, cleanup solver API, simplified strategic solver, added combined solver 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-11 17:47:27 -08:00
Leonardo de Moura
bfe6678ad2 merged 2012-12-11 11:40:43 -08:00
Leonardo de Moura
2c9b14ada8 removed private API based on deprecated features 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-11 11:37:29 -08:00
Nikolaj Bjorner
b6459a8a92 add solver object to get_implied_equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-11 10:53:21 -08:00
Leonardo de Moura
265bdbe757 merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 14:07:59 -08:00
Leonardo de Moura
8015d8b79a Updated Java README 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 07:52:14 -08:00
Leonardo de Moura
4981134fd7 Fixing VS warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 06:52:56 -08:00
Leonardo de Moura
d6a1ea82e1 exposed subresultants aka psc-chain procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 16:47:37 -08:00
Leonardo de Moura
9b7946e52d added method for creating ast_manager based on context_params configuration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 14:24:37 -08:00
Leonardo de Moura
7ffba3ebf4 more examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 08:02:12 -08:00
Leonardo de Moura
7a31c6bc74 exposed root isolation algorithm in the API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 21:07:17 -08:00
Leonardo de Moura
0d230375be added polynomial evaluation at algebraic point 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 20:39:16 -08:00
Leonardo de Moura
bf2340850a minor change 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 11:11:53 -08:00
Leonardo de Moura
277244098c Adding python interface for computing with algebraic numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 10:57:05 -08:00
Leonardo de Moura
47edff2076 fixed bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 08:32:06 -08:00
Leonardo de Moura
189fc46b6d working on api for algebraic numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 19:06:48 -08:00
Leonardo de Moura
4e2a9e7caf working on api 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 18:44:03 -08:00
Leonardo de Moura
c011b05b61 exposing algebraic numbers in the API (working in progress) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 17:48:57 -08:00
Leonardo de Moura
c350943c78 fixed bug introduced today 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 15:59:54 -08:00
Leonardo de Moura
ac03c9eff7 chasing parameter setting bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 08:27:17 -08:00
Leonardo de Moura
bca0c0bb5f Merge branch 'contrib' of https://git01.codeplex.com/forks/nguyenthanhvuh/vuz3 into vu 2012-12-06 12:00:50 -08:00
Leonardo de Moura
9ab1210cc2 merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 11:05:49 -08:00
ThanhVu (Vu) Nguyen
72a250c01a moving my common z3 stuff to z3util.py … note the vset() call essentially returns a list with no duplicate elements, it's like set but allows the user to add in a function to compute the representation of the list elements. 2012-12-06 13:54:57 -05:00
Leonardo de Moura
3cefa0a1f7 making tests deterministic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 19:20:48 -08:00
Josh Berdine
2f3daf14b5 Regenerate ml api 2012-12-05 19:20:48 -08:00
Josh Berdine
6fad07e6e1 Update build system for ml api 2012-12-05 19:20:47 -08:00
Josh Berdine
949317ccfc Fixes for error handling in ml api 2012-12-05 19:20:47 -08:00
Josh Berdine
ae5f96895d Change to avoid relying on sed supporting disjunction or escaped control characters 2012-12-05 19:20:47 -08:00
Josh Berdine
4ec4151e82 Change treatment of unsigned to avoid depending on unspecified behavior of recursive macros 2012-12-05 19:20:47 -08:00
Leonardo de Moura
2b66b50c75 making tests deterministic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 16:21:38 -08:00
Leonardo de Moura
bce9d1440b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-04 11:57:00 -08:00
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
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
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
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
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
Christoph M. Wintersteiger
eb3fa254d8 Java API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-03 17:56:42 +00: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
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
ffb7e26c75 removed front-end-params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 10:05:29 -08:00