Copyright | (c) Iago Abal, 2012 (c) David Castro, 2012 |
---|---|
License | BSD3 |
Maintainer | Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> |
Safe Haskell | None |
Language | Haskell98 |
Deprecated: The Z3.Lang interface will be moved to a dedicated package.
- declarePow2 :: IsInt a => Z3 (Expr a -> Expr a)
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.