3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-07 03:35:47 +00:00

Commit graph

  • 8515044f8b Add option bvnot2arith Leonardo de Moura 2012-12-27 20:28:42 -08:00
  • 1a09523c99 Fix mk_make bug introduced yesterday Leonardo de Moura 2012-12-27 09:10:13 -08:00
  • 6e468e84e7 Update installation instructions in the README file Leonardo de Moura 2012-12-26 17:37:18 -08:00
  • 1b35668eb7 Improve Z3Py installation in non-standard prefix. Leonardo de Moura 2012-12-26 17:24:26 -08:00
  • 7c886fb7dd Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2012-12-26 15:50:54 -08:00
  • 71aec11a04 Ignore callgrind files and Python pyo files Leonardo de Moura 2012-12-26 15:50:09 -08:00
  • 00b5d9e014 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-12-26 15:45:11 -08:00
  • c513f7e9c2 fixed slicing Nikolaj Bjorner 2012-12-26 15:44:54 -08:00
  • 53df82c314 Add arith_decls for underspecified operators Leonardo de Moura 2012-12-26 11:35:00 -08:00
  • 8b8fb74fd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-12-26 11:31:09 -08:00
  • bc77a97e92 qe lite checks Nikolaj Bjorner 2012-12-26 11:28:05 -08:00
  • 2a286541e0 Fix crash reported at http://z3.codeplex.com/workitem/11. Fix array rewriter bug, rewriter was producing sort incorrect expression. Leonardo de Moura 2012-12-26 08:36:25 -08:00
  • fbce816025 Merge branch 'unstable' into contrib Leonardo de Moura 2012-12-22 14:36:30 -08:00
  • 3cc9d57438 Fix pytest, it should work with Python 2.7.x and 3.x Leonardo de Moura 2012-12-21 16:58:10 -08:00
  • a0a505e1b8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2012-12-20 17:48:30 -08:00
  • 6602803850 Add Python 3.x support Leonardo de Moura 2012-12-20 17:47:38 -08:00
  • 7d97f407c2 Remove non-ascii characters Leonardo de Moura 2012-12-20 10:40:14 -08:00
  • d7b8110cc8 Regenerate ml api Josh Berdine 2012-12-20 12:58:21 +00:00
  • a7f89dcdd2 Move Z3_get_implied_equalities from v3 to v4 ml api as it now needs Z3_solver type Josh Berdine 2012-12-20 12:54:44 +00:00
  • fd5372d7a2 Z3_search_failure type not needed in v4 ml api Josh Berdine 2012-12-08 18:05:26 +00:00
  • 32896a15e6 Fix for compiling ml api Josh Berdine 2012-12-12 02:02:08 +00:00
  • 27438b0fc9 Fix newlines Josh Berdine 2012-12-13 11:33:38 +00:00
  • 7b1fac11e6 Add new C++ examples Leonardo de Moura 2012-12-19 12:33:14 -08:00
  • d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id Leonardo de Moura 2012-12-18 17:14:25 -08:00
  • 3ddb1a85f1 Add basic_recognizers and array_recognizers Leonardo de Moura 2012-12-18 15:00:16 -08:00
  • cec328cfdc Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util. Leonardo de Moura 2012-12-18 14:44:51 -08:00
  • 4f0d5a5756 Add thanks to Etienne Kneuss Leonardo de Moura 2012-12-18 07:27:20 -08:00
  • 83f7b294cc Update RELEASE_NOTES with latest bug fix Leonardo de Moura 2012-12-17 21:05:04 -08:00
  • 08789b69d4 Fix warning on FreeBSD Leonardo de Moura 2012-12-17 20:56:20 -08:00
  • 9674f511b3 Fix scoped_timer for Linux. Nested timers were misbehaving, and it was not possible to create timers in more than one thread Leonardo de Moura 2012-12-17 20:46:04 -08:00
  • 607fab486c Fix incorrect uses of set_cancel() Leonardo de Moura 2012-12-17 18:35:50 -08:00
  • f8014f54c1 Fix bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model Leonardo de Moura 2012-12-17 15:12:36 -08:00
  • 8c211dd4fc Fix bug reported by Philippe Suter, see RELEASE_NOTES Leonardo de Moura 2012-12-17 14:07:21 -08:00
  • 143b829488 Fix literal duplication bug that was introduced after v4.3.1 release Leonardo de Moura 2012-12-17 13:42:01 -08:00
  • 7e66a65e98 Add blast_distinct_threshold option to rewriter. Enable blast_distinct in the QF_LIA default strategy Leonardo de Moura 2012-12-17 10:32:00 -08:00
  • 050ec0b760 Fix memout detected in nightly regressions Leonardo de Moura 2012-12-15 13:26:11 -08:00
  • 9634d66699 Fix typo in tactic selection Leonardo de Moura 2012-12-15 08:10:48 -08:00
  • 1dfea1324e Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-12-14 16:55:04 -08:00
  • 0a3f95bdaa quantifiers Nikolaj Bjorner 2012-12-14 16:54:59 -08:00
  • 4df172e971 Fix file name (use same naming convention) Leonardo de Moura 2012-12-14 08:14:44 -08:00
  • 6958b9cdb6 Fixed issues with the pretty printer Leonardo de Moura 2012-12-13 15:19:37 -08:00
  • c98f0c8307 fixed unused variable warning Leonardo de Moura 2012-12-13 14:09:52 -08:00
  • e0f4d870fd Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem. Leonardo de Moura 2012-12-13 14:03:58 -08:00
  • 5b6842fbc5 cleaning defined_names Leonardo de Moura 2012-12-13 12:37:03 -08:00
  • 0cf7396707 merged Leonardo de Moura 2012-12-13 07:23:48 -08:00
  • 85ac2f558c marked script as executable Leonardo de Moura 2012-12-13 07:23:09 -08:00
  • dfcfd3f014 C:/Program Files (x86)/Git/Gm and /MP are incompatible Leonardo de Moura 2012-12-12 18:16:59 -08:00
  • 75f96f0b9b added hack for nmake limitation Leonardo de Moura 2012-12-12 18:12:04 -08:00
  • a934c6813a Fixed bug reported by Yan Peng from UBC Leonardo de Moura 2012-12-12 13:04:54 -08:00
  • ed1f67f1f1 merged Leonardo de Moura 2012-12-12 09:11:14 -08:00
  • 6348dab24a removed dead code Leonardo de Moura 2012-12-12 09:10:47 -08:00
  • 3fa05d8131 Added script for tracking all remote branches Leonardo de Moura 2012-12-12 08:58:10 -08:00
  • 512cdc182a include Java bindinings in the binary distribution Leonardo de Moura 2012-12-12 07:29:04 -08:00
  • f02d2ee0e3 fixed missing libz3.lib file in the z3 binary distribution for windows (thanks to GManNickG) Leonardo de Moura 2012-12-12 07:09:26 -08:00
  • e13e12636a fixed mk_win_dist.py Leonardo de Moura 2012-12-12 07:07:52 -08:00
  • 635aabf2d5 fix get_implied equalities and the unit test Nikolaj Bjorner 2012-12-11 21:39:31 -08:00
  • 89ddb5eac4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-12-11 20:49:49 -08:00
  • 13dda76ddb Removed dead code Leonardo de Moura 2012-12-11 18:00:09 -08:00
  • bee783fdd1 merged Leonardo de Moura 2012-12-11 17:56:04 -08:00
  • 528f348022 Fixed bug Leonardo de Moura 2012-12-11 17:51:49 -08:00
  • 8198e62cbd solver factories, cleanup solver API, simplified strategic solver, added combined solver Leonardo de Moura 2012-12-11 17:47:27 -08:00
  • 639f902ad1 fix bug in difference logic recognizer, assert in proof_util Nikolaj Bjorner 2012-12-11 17:01:00 -08:00
  • 299c5eb947 make qe-light routine do a little more about traversal Nikolaj Bjorner 2012-12-11 16:41:25 -08:00
  • bfe6678ad2 merged Leonardo de Moura 2012-12-11 11:40:43 -08:00
  • 2c9b14ada8 removed private API based on deprecated features Leonardo de Moura 2012-12-11 11:37:29 -08:00
  • b6459a8a92 add solver object to get_implied_equalities Nikolaj Bjorner 2012-12-11 10:53:21 -08:00
  • 01826fa8c9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-12-10 21:21:13 -08:00
  • 730801e2f0 fix unintialized variable Nikolaj Bjorner 2012-12-10 21:21:02 -08:00
  • 0774bc4075 merged Leonardo de Moura 2012-12-10 18:46:32 -08:00
  • 589f2c6bb3 improved unknown parameter error msg Leonardo de Moura 2012-12-10 18:46:02 -08:00
  • 0831e020e3 add qe-lite tatic Nikolaj Bjorner 2012-12-10 17:25:28 -08:00
  • 265bdbe757 merged Leonardo de Moura 2012-12-10 14:07:59 -08:00
  • eaf448b664 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-12-10 11:13:29 -08:00
  • 271c143de5 update unstable branch with qhc changes that don't have dependencies Nikolaj Bjorner 2012-12-10 11:13:04 -08:00
  • 8bfbdf1e68 fixing clang warnings on OSX Leonardo de Moura 2012-12-10 19:04:21 +00:00
  • 7f210d55be fixed warnings on Win64 Leonardo de Moura 2012-12-10 07:52:33 -08:00
  • 8015d8b79a Updated Java README Leonardo de Moura 2012-12-10 07:52:14 -08:00
  • 99d0449272 added Java docs Leonardo de Moura 2012-12-10 07:51:45 -08:00
  • 4981134fd7 Fixing VS warning Leonardo de Moura 2012-12-10 06:52:56 -08:00
  • 1fb0fec7d1 improved jni.h detection Leonardo de Moura 2012-12-10 06:43:57 -08:00
  • af37aa2743 improving java bindings build Leonardo de Moura 2012-12-10 06:30:26 -08:00
  • 840d0aef6d fixed bug in generated code Leonardo de Moura 2012-12-09 18:59:32 -08:00
  • ed97a3a180 merged Leonardo de Moura 2012-12-09 16:49:14 -08:00
  • d6a1ea82e1 exposed subresultants aka psc-chain procedure Leonardo de Moura 2012-12-09 16:47:37 -08:00
  • 84aeba94a5 merged Leonardo de Moura 2012-12-09 15:06:50 -08:00
  • 6ae6414236 avoiding clang warning messages Leonardo de Moura 2012-12-09 15:04:14 -08:00
  • 9b7946e52d added method for creating ast_manager based on context_params configuration Leonardo de Moura 2012-12-09 14:24:37 -08:00
  • 84e79035cb Updated release notes Leonardo de Moura 2012-12-09 12:24:14 -08:00
  • 33234a4162 Fixed issue http://z3.codeplex.com/workitem/10 Leonardo de Moura 2012-12-09 12:23:35 -08:00
  • 7ffba3ebf4 more examples Leonardo de Moura 2012-12-09 08:02:12 -08:00
  • 7a31c6bc74 exposed root isolation algorithm in the API Leonardo de Moura 2012-12-08 21:07:17 -08:00
  • 0d230375be added polynomial evaluation at algebraic point Leonardo de Moura 2012-12-08 20:39:16 -08:00
  • bf2340850a minor change Leonardo de Moura 2012-12-08 11:11:53 -08:00
  • 277244098c Adding python interface for computing with algebraic numbers Leonardo de Moura 2012-12-08 10:57:05 -08:00
  • 47edff2076 fixed bugs Leonardo de Moura 2012-12-08 08:32:06 -08:00
  • 189fc46b6d working on api for algebraic numbers Leonardo de Moura 2012-12-07 19:06:48 -08:00
  • 4e2a9e7caf working on api Leonardo de Moura 2012-12-07 18:44:03 -08:00
  • c011b05b61 exposing algebraic numbers in the API (working in progress) Leonardo de Moura 2012-12-07 17:48:57 -08:00
  • c350943c78 fixed bug introduced today Leonardo de Moura 2012-12-07 15:59:54 -08:00
  • cba449b75e more parameter issues Leonardo de Moura 2012-12-07 15:16:46 -08:00