./math/z3, The Z3 theorem prover / SMT solver

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]


Branch: CURRENT, Version: 4.5.0nb2, Package name: z3-4.5.0nb2, Maintainer: dholland

z3 is an open source theorem prover / SMT solver from Microsoft Research.

(SMT stands for "satisfiability modulo theories".)


Required to run:
[lang/ocaml] [lang/python27] [math/ocaml-num]

Required to build:
[pkgtools/cwrappers]

Package options: ocaml

Master sites:

SHA1: 6f4e94e025fcc2fa2896524d8fbb9de0b3033854
RMD160: 81121307ac83f42989da49efda31964a94f7f5d5
Filesize: 3489.937 KB

Version history: (Expand)


CVS history: (Expand)


   2018-06-15 17:11:35 by Jonathan Perkin | Files touched by this commit (2)
Log message:
z3: Fix broken build system by pretending SunOS is Linux.
   2018-04-13 15:55:39 by Jaap Boender | Files touched by this commit (88)
Log message:
Revbump associated with the upgrade of lang/ocaml

(this is the upgrade from 4.06 to 4.06.1)
   2018-03-13 22:20:34 by Pierre Pronchery | Files touched by this commit (3) | Package updated
Log message:
Re-introduce support for NetBSD in src/util/scoped_timer.cpp

I forgot to patch this part in the latest update; sorry.
This has now been submitted upstream as well.

Originally from dholland@.

Compile-tested on NetBSD/amd64.

Bump PKGREVISION.
   2018-03-13 01:36:05 by Pierre Pronchery | Files touched by this commit (1)
Log message:
Import a package for the Python bindings for math/z3
   2018-03-13 01:34:02 by Pierre Pronchery | Files touched by this commit (2)
Log message:
Remove the references to wip
   2018-03-13 01:31:16 by Pierre Pronchery | Files touched by this commit (11) | Package updated
Log message:
Update math/z3 to version 4.5.0

From the release notes:

    New features:
    - New theories of strings and sequences.
    - Incremental consequence finder for finite domains.
    - CMake build system (thanks @delcypher).
    - Updated and improved OCaml API (thanks @martin-neuhaeusser).
    - Updated and improved Java API (thanks @cheshire).
    - New resource limit facilities to avoid non-deterministic timeout behaviour.
    - New bit-vector simplification and ackermannization tactics (thanks \ 
@MikolasJanota, @nunoplopes).
    - QSAT: a new solver for quantified arithmetic problems. See:
      Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016.

    A multitude of bugs has been fixed.

I am about to commit a separate package for the Python bindings.

Coordinated with dholland@
   2018-03-11 07:14:45 by David A. Holland | Files touched by this commit (1)
Log message:
Requires ocaml-num with ocaml 4.06
   2018-02-27 09:34:16 by Thomas Klausner | Files touched by this commit (1)
Log message:
z3: forbid python 3.x

First complains about indentation problems, then about reading
non-ASCII bytes.