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

495 commits

Author SHA1 Message Date
Leonardo de Moura 4df172e971 Fix file name (use same naming convention) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-14 09:04:20 -08:00
Leonardo de Moura 6958b9cdb6 Fixed issues with the pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-13 15:19:37 -08:00
Leonardo de Moura c98f0c8307 fixed unused variable warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-13 14:09:52 -08:00
Leonardo de Moura e0f4d870fd Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-13 14:03:58 -08:00
Leonardo de Moura 5b6842fbc5 cleaning defined_names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-13 12:37:03 -08:00
Leonardo de Moura a934c6813a Fixed bug reported by Yan Peng from UBC 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-12 13:04:54 -08:00
Leonardo de Moura 6348dab24a removed dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-12 09:10:47 -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
Nikolaj Bjorner 89ddb5eac4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-11 20:49:49 -08:00
Leonardo de Moura 13dda76ddb Removed dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-11 18:00:09 -08:00
Leonardo de Moura bee783fdd1 merged 2012-12-11 17:56:04 -08:00
Leonardo de Moura 528f348022 Fixed bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-11 17:51:49 -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
Nikolaj Bjorner 639f902ad1 fix bug in difference logic recognizer, assert in proof_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-11 17:01:00 -08:00
Nikolaj Bjorner 299c5eb947 make qe-light routine do a little more about traversal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-11 16:41:25 -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
Nikolaj Bjorner 01826fa8c9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-10 21:21:13 -08:00
Nikolaj Bjorner 730801e2f0 fix unintialized variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-10 21:21:02 -08:00
Leonardo de Moura 0774bc4075 merged 2012-12-10 18:46:32 -08:00
Leonardo de Moura 589f2c6bb3 improved unknown parameter error msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 18:46:02 -08:00
Nikolaj Bjorner 0831e020e3 add qe-lite tatic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-10 17:25:28 -08:00
Nikolaj Bjorner 271c143de5 update unstable branch with qhc changes that don't have dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-10 11:13:04 -08:00
Leonardo de Moura 7f210d55be fixed warnings on Win64 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 07:52:33 -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 840d0aef6d fixed bug in generated code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 18:59:32 -08:00
Leonardo de Moura ed97a3a180 merged 2012-12-09 16:49:14 -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 84aeba94a5 merged 2012-12-09 15:06:50 -08:00
Leonardo de Moura 6ae6414236 avoiding clang warning messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 15:04:14 -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 33234a4162 Fixed issue http://z3.codeplex.com/workitem/10 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 12:23:35 -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 cba449b75e more parameter issues 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 15:16:46 -08:00
Leonardo de Moura a07b459fdf Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 12:53:51 -08:00
Leonardo de Moura bd0366eef7 Fixed problems in the new parameter setting. Many thanks to Nuno Lopes for sending a benchmark that exposed the problem, a noticing the discrepancy between unstable and master branches. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 11:09:14 -08:00
Leonardo de Moura e055e0b47c Fixed other parameter setting problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 10:41:50 -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 8d45de02c5 Fixed timer bug on freebsd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 06:07:57 -08:00
Leonardo de Moura 68b97024e2 added missing option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 08:54:00 -08:00
Leonardo de Moura 75739fdf7b fixed memory smash 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 08:19:42 -08:00
Leonardo de Moura 294d40889f Merge branch 'nikolaj' into unstable 2012-12-06 07:42:50 -08:00
Nikolaj Bjorner dbde71c290 fixing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-06 07:38:53 -08:00
Nikolaj Bjorner 6bdde9047a fixing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-06 07:38:50 -08: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
Josh Berdine 6a5de3384c Regenerate ml api 2012-12-06 00:42:30 +00:00
Josh Berdine 79be6ee6c2 Update build system for ml api 2012-12-06 00:39:45 +00:00
Josh Berdine c9865606e6 Fixes for error handling in ml api 2012-12-06 00:34:34 +00:00
Josh Berdine 192f51e986 Change to avoid relying on sed supporting disjunction or escaped control characters 2012-12-06 00:34:34 +00:00
Josh Berdine 8cc695eb7f Change treatment of unsigned to avoid depending on unspecified behavior of recursive macros 2012-12-06 00:34:33 +00:00
Leonardo de Moura 3a5e71afef Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-05 16:22:16 -08:00
Leonardo de Moura 1a11196211 fixing bug introduced today 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 16:21:53 -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 5e4d1151eb fixing clang compilation problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 15:20:16 -08:00
Nikolaj Bjorner 188aea3fb1 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-05 13:48:27 -08:00
Nikolaj Bjorner 53cb389398 fixing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-05 13:05:14 -08:00
Nikolaj Bjorner 3b51597dbe fixing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-05 12:05:07 -08:00
Nikolaj Bjorner 3bf86e1a49 fixing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-05 12:02:08 -08:00
Nikolaj Bjorner aeb3857391 fixing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-05 12:01:03 -08:00
Leonardo de Moura 3736c5ea3b removed template specialization overkill 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 08:56:19 -08:00
Leonardo de Moura 5379130c8c eliminated m_proof_mode from smt_params, ast_manager has this information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 08:35:03 -08:00
Leonardo de Moura f6a3ec58e5 allow --help, --version, etc as valid parameter names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 15:48:28 -08:00
Leonardo de Moura 89385b4e9a no need for / options 2012-12-04 15:38:16 -08:00
Leonardo de Moura 6f5f1b290e better error message for renamed parameter names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 15:33:21 -08:00
Leonardo de Moura 2eef4cc1e7 forgot synch 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:59:46 -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 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
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