mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity
1714 commits 23 branches 48 tags 157 MiB
Commit graph

1714 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 0df0174d62 .NET API: Enabled .xml documentation generation by default. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-08 15:24:08 +01:00
Nikolaj Bjorner 3d995648ee partial fix to model generation bug for non-linear constraints: avoid epsilon refinment for non-shared variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-07 20:39:20 +09:00
Ken McMillan e17af8a5de doc fix for interpolation bindings for python 2014-08-06 15:34:58 -07:00
Ken McMillan 6880945435 added simple interpolation bindings for python 2014-08-06 15:30:24 -07:00
Ken McMillan 5a107095c9 removing python changes for interp 2014-08-06 11:32:51 -07:00
Ken McMillan b933a4da85 merged python interp changes 2014-08-06 11:26:44 -07:00
Ken McMillan 31d4e6aa00 merging with unstable 2014-08-06 11:17:44 -07:00
Ken McMillan ab13987884 working on python interp 2014-08-06 11:16:24 -07:00
Ken McMillan c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Ken McMillan 7bf87e76ea fix for tree interpolation 2014-08-05 11:11:43 -07:00
Christoph M. Wintersteiger 39646bac3e added operator[] to obj_map for convenience 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-31 16:32:25 +01:00
Christoph M. Wintersteiger 06a4a3599d Added git hashcode information to (get-info :version) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-29 18:04:54 +01:00
Christoph M. Wintersteiger e10f256100 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-07-28 19:38:53 +01:00
Christoph M. Wintersteiger b423418810 FPA fixed omissions reported by user xor88 (codeplex discussion 554193) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-28 19:37:58 +01:00
Christoph M. Wintersteiger 1944283253 FPA unified function names 2014-07-28 19:36:11 +01:00
Leonardo de Moura 24961dc5f1 feat(ast/ast_smt_pp): display quantifier QID when printing proofs, feature requested by Dan Rosen 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 14:42:00 -07:00
Christoph M. Wintersteiger 1abf3beaba bugfix for Python 3 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-24 16:52:32 +01:00
Christoph M. Wintersteiger 5b1a98a155 Bugfix for Python 3 2014-07-24 13:53:56 +01:00
Nikolaj Bjorner 44751c0ef8 Add missing .NET API functions for parsing rules into fixedpoint object 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-23 15:27:24 -07:00
Nikolaj Bjorner 4957e71408 make get_vars populate all indices with sorts even if variable does not occur in rule. This makes the use of get_vars less prone to callers having to double check for null pointers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-21 17:12:39 +02:00
Nikolaj Bjorner 72fe197bda fix model generation bug reported by Saga Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 17:06:36 +02:00
Nikolaj Bjorner 752a6b2e33 fix quantifier elimination bugs reported by Berdine and Bornat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 16:46:27 +02:00
Nikolaj Bjorner dd786bb5bf fix quantifier elimination bugs reported by Berdine and Bornat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 15:41:03 +02:00
Nikolaj Bjorner e4dedbbefc fix quantifier elimination bugs reported by Berdine and Bornat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 15:38:22 +02:00
Nikolaj Bjorner 4f7d872d59 fix model transformation bug in bit blaster rule transformer, reported by Sagar Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-08 11:21:19 +02:00
Nikolaj Bjorner d6de73a2d1 fix model converter in inliner. Bug reported by Sagar Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-06 18:11:57 +02:00
Nikolaj Bjorner 9d221c037a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-07-02 23:49:04 +02:00
Nikolaj Bjorner 3533a09010 bit2bool bug reported by Sagar Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-02 23:48:49 +02:00
Christoph M. Wintersteiger 311fed4760 Changed python distribution to include *.py files to enable use 
with Python 2.7 and 3.4 out of the box.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-01 13:12:10 +01:00
Christoph M. Wintersteiger 7158e814d1 Bugfix for quasi-macros, many thanks to Nuno Lopez finding this bug and for suggesting a fix! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-25 13:25:23 +01:00
Christoph M. Wintersteiger 3209cd2ded Disabled construction of partial model on theory failure as it caused buggy behavior. 
Thanks to parno (Codeplex Issue #117)!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-23 16:40:49 +01:00
Christoph M. Wintersteiger 000db81b4f Fixed bug where the random seed wasn't passed through to 
theory_arith. Thanks to Carsten! (Stackoverflow #24327987)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-23 15:47:47 +01:00
Leonardo de Moura 91b32206fd fix(scripts/mk_make): python3 compatibility 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 13:59:35 -07:00
Christoph M. Wintersteiger c6319a0ba3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-06-19 15:50:30 +01:00
Christoph M. Wintersteiger a26ae624e0 Fixed dependencies of install target in Makefile 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-19 15:50:18 +01:00
Nikolaj Bjorner 8b6dcd9a1b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-06-18 09:54:00 -07:00
Nikolaj Bjorner 103e49d9b4 Add option to control explosion of cofactor-term-ite following example by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-18 09:53:47 -07:00
Nikolaj Bjorner 1ed7643d32 Add option to control explosion of cofactor-term-ite following example by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-18 09:52:59 -07:00
Nikolaj Bjorner a5e3713c2c fix unmatched parenthsis and code odor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-14 05:47:42 -07:00
Nikolaj Bjorner 8ef4ec7009 fix bit-vector rotation left bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-08 12:46:23 +01:00
Nikolaj Bjorner 88bd01bc4f patching non-termination bug in datatype factory, reported by Tiago 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-03 23:03:34 +05:30
Nikolaj Bjorner a10c318e15 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-05-31 12:04:28 +05:30
Nikolaj Bjorner f76b343bfa expose parameter settings for controlling injectivity axiom. rquested by Jasmin Blanchette 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-31 11:25:54 +05:30
Christoph M. Wintersteiger 7288353575 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-05-30 18:14:46 +01:00
Christoph M. Wintersteiger bc25ea404f Fixed potential bug (warning on OSX). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-30 18:14:33 +01:00
Nikolaj Bjorner 49f9f4b3b5 fix crash in model construction from finite domain theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-30 20:52:39 +05:30
Christoph M. Wintersteiger 1e774064bc assertion bug fix in z3py 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-30 12:26:55 +01:00
Christoph M. Wintersteiger 756645326b Bugfix for And/Or operators in Python. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-29 17:33:03 +01:00
Christoph M. Wintersteiger 4da56aa4df added debug assertion 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-29 12:41:07 +01:00
Nikolaj Bjorner aba79802cf fix warning about unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-25 21:01:10 -07:00