Skip to content
FFI Bindings for the Z3 C API using FFI::Platypus
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
lib/Z3
t
.gitignore
Changes
README.md
api.code
api.lst
dist.ini
perlcritic.rc

README.md

NAME

Z3::FFI - Low level FFI interfaces to the Z3 solver/prover

VERSION

This is built for Z3 version 4.8.4

DESCRIPTION

This is a direct translation of the Z3 C API to a Perl API. It's most likely not the level for working with Z3 from perl.

This is a mostly functional implementation right now. A few functions are not implemented, Z3_set_error_handler in particular. This early release is also missing support for any Z3_...[] array types and the few pointer types that get used. These will be implemented in future versions

USE

You're going to want to refer to the C API documentation for Z3, http://z3prover.github.io/api/html/group__capi.html.
All functions have the Z3_ stripped from their name and are declared as part of this module.

use Z3::FFI;

my $config = Z3::FFI::mk_config(); # Create a Z3 config object
my $context = Z3::FFI::mk_context($config); # Create the Z3 Context object
... # work with the Z3 context

TODO

  • Finish the array types to allow more functions to be called.
  • Finish the pointer types to allow the rest of the functions to be called.
  • Figure out if there's a way to handle the Z3_set_error_handler function

SEE ALSO

Alien::Z3

AUTHOR

Ryan Voots simcop@cpan.org

You can’t perform that action at this time.