z3-0.3.2: Bindings for the Z3 Theorem Prover

Copyright(c) Iago Abal, 2012 (c) David Castro, 2012
LicenseBSD3
MaintainerIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>
Safe HaskellNone
LanguageHaskell98

Z3.Lang.Pow2

Description

Deprecated: The Z3.Lang interface will be moved to a dedicated package.

Synopsis

Documentation

declarePow2 :: IsInt a => Z3 (Expr a -> Expr a) Source

Raise to the power of 2. Axiomatization of the 2^n function. Most likely Z3 is going to diverge if you use 2^n to specify a satisfiable problem, since it cannot construct a recursive definition for 2^n, but it should work fine for unsatisfiable instances.