3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

263 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 237577acc8 Bumping version to 4.4
Added to release notes

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-20 15:59:54 +00:00
Christoph M. Wintersteiger a8d8e3e9e5 formatting
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 18:16:51 +00:00
Christoph M. Wintersteiger f50a8b0a59 Bumped version number.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-25 17:05:02 +01:00
Christoph M. Wintersteiger e0c42f5892 Java API bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-24 14:43:01 +01:00
Nikolaj Bjorner fe4a8b44a5 revert some changes to how 'out' parameters are annotated on API calls. Retain the 'out' annotation for so-called managed out parameters. The data-type examples in managed API fail with the out parameter annotation as no memory is allocated on instances of out parameters, other than the interpolation APIs that are new
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-16 22:40:52 -07:00
Christoph M. Wintersteiger 3e7c95db6b Interpolation API bugfixes
Added Interpolation to the Java API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-10 12:34:17 +01:00
Christoph M. Wintersteiger 9b8406c717 Resolved interpolation API issues.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-10 11:41:21 +01:00
Christoph M. Wintersteiger 503ad78bf3 Interpolation API bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-09 18:08:07 +01:00
Nikolaj Bjorner f0c63e56f3 make module parameter validation and adjustment more flexible: you can use both module qualifiers and unqualified parameters from the API at local scope
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-08 16:27:40 -07:00
Christoph M. Wintersteiger b03a9d3f0a Interpolation API: infrastructure fixes and .NET API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-08 21:01:27 +01:00
Christoph M. Wintersteiger 9949c7e31c fixed typos
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-09-18 17:09:22 +01:00
Christoph M. Wintersteiger fa24d9db6f Added multi processor compilation to VS project.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-09-01 17:27:07 +01:00
Christoph M. Wintersteiger 38ee8cb807 .NET API: bugfix. Thanks to Konrad Jamrozik for catching this one.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-08-22 12:57:33 +01:00
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
Ken McMillan c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Christoph M. Wintersteiger fb4c07a2ea FPA refactoring in preparation for FPA support in the kernel.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-23 18:36:38 +01:00
Christoph M. Wintersteiger b6c0b8c9ff Compilation fix for FreeBSD 2014-04-07 16:09:22 +01:00
Christoph M. Wintersteiger 4444eb361c bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-03 13:11:39 +01:00
Christoph M. Wintersteiger 83f88917a8 bugfix for python 2.6 2014-03-20 17:47:41 +00:00
Christoph M. Wintersteiger 07d56bdc70 Java API bugfixes for cygwin compilation
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-02-21 13:44:39 +00:00
Leonardo de Moura e077fc5cb4 fix(api/python): make sure Z3 compiles using Python3
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-20 14:09:55 -08:00
Christoph M. Wintersteiger b2be81fd4d bugfix for OSX build configuration 2014-01-22 13:41:48 +00:00
Christoph M. Wintersteiger 73a1dddc45 Bugfixes for the build on new OSX machines (XCode 5.0 on). 2014-01-21 17:06:13 +00:00
Ken McMillan a410e7f716 fussing with qe in duality 2013-12-13 12:21:54 -08:00
Ken McMillan 3a0947b3ba merged with unstable 2013-10-18 17:26:41 -07:00
Ken McMillan 2c9c5ba1f0 still working on interpolation of full z3 proofs 2013-09-15 13:33:20 -07:00
Nikolaj Bjorner 457b22b00e add TPTP example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-06 21:49:00 -07:00
Nikolaj Bjorner e4338f085b re-organization of muz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 22:11:33 -07:00
Nikolaj Bjorner 9e61820125 re-organizing muz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 21:49:53 -07:00
Nikolaj Bjorner 0d56499e2d re-organize muz_qe into separate units
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 21:20:24 -07:00
Nikolaj Bjorner 137339a2e1 split muz_qe into two directories
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 12:08:47 -07:00
Christoph M. Wintersteiger 6ce0e7cf25 .NET build changes to include /linkresource
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-07-15 12:22:01 +01:00
Leonardo de Moura efb6b2453e Move AssemblyInfo.cs AssemblyInfo. Update mk_util.py to generate AssemblyInfo.cs instead of modifying it.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-06-24 15:37:49 -07:00
Leonardo de Moura 205520ed6c Move AssemblyInfo.cs AssemblyInfo. Update mk_util.py to generate AssemblyInfo.cs instead of modifying it.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-06-24 15:34:42 -07:00
Nuno Lopes 6560fc0a2c add experimental Horn clause to AIG (AAG format) converter.
Clauses should be over booleans only (or bit-blasted with fixedpoint.bit_blast=true).
We will crash if that's not the case.
Only linear clauses supported for now

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-05-16 09:58:31 -07:00
Ken McMillan 8488ca24d2 first commit of duality 2013-04-20 18:18:45 -07:00
U-REDMOND\kenmcmil 28266786f3 porting to windows 2013-03-27 12:17:52 -07:00
Ken McMillan 78848f3ddd working on smt2 and api 2013-03-26 17:25:54 -07:00
Christoph M. Wintersteiger 21f69c2b3a Java API build bugfix. Thanks to Fabian Emmes for reporting this.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-03-12 12:27:08 +00:00
Ken McMillan 2b93537366 debugging interpolation 2013-03-06 18:26:46 -08:00
Ken McMillan ae9276ad9b more work on interpolation 2013-03-05 21:56:09 -08:00
Ken McMillan 68fb01c206 initial commit for interpolation 2013-03-03 20:45:58 -08:00
Christoph M. Wintersteiger 14f582eca5 Java API: added automatic detection of jar
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-25 16:03:57 +00:00
Christoph M. Wintersteiger f5cdc14737 Java API: build system bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-25 15:44:54 +00:00
Christoph M. Wintersteiger ffb1fc37df Java API: New JDK detection routines.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-25 15:37:33 +00:00
Christoph M. Wintersteiger 2c6c09301f Java API: build system bugfixes.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-21 16:46:18 +00:00
Christoph M. Wintersteiger 876c6a361e Java API: build system fix for OSX
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-21 16:40:10 +00:00
Christoph M. Wintersteiger 18bae81731 Java Example: build fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-19 22:48:41 +00:00
Leonardo de Moura 5e72cf0123 Compress windows distribution zip files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-14 10:55:43 -08:00
Leonardo de Moura 9d45d872a7 Compress Z3 distribution zip files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-14 10:26:15 -08:00