| 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 |
Z3.Lang.Lg2
Description
Deprecated: The Z3.Lang interface will be moved to a dedicated package.
- declareLg2 :: IsInt a => Z3 (Expr a -> Expr a)
Documentation
declareLg2 :: IsInt a => Z3 (Expr a -> Expr a) Source
Ceiling logarithm base two. Axiomatization of the lg2 function. Most likely Z3 is going to diverge if you use lg2 to specify a satisfiable problem since it cannot construct a recursive definition for lg2, but it should work fine for unsatisfiable instances.