{-# LANGUAGE ScopedTypeVariables #-} -- | -- Module : Z3.Lang.Pow -- 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> {-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} -- Imports deprecated modules, but it is a depcrecated module itself. -- TODO generalize for x^y module Z3.Lang.Pow2 {-# DEPRECATED "The Z3.Lang interface will be moved to a dedicated package." #-} ( declarePow2 ) where import Z3.Lang.Prelude -- | 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. declarePow2 :: IsInt a => Z3 (Expr a -> Expr a) declarePow2 = do pow2::Expr a -> Expr a <- fun1 -- invariants assert $ forall $ \x -> (x <* 0 ==> pow2 x ==* 0) `instanceWhen` [Pat $ pow2 x] assert $ forall $ \x -> (x >=* 0 ==> pow2 x >* 0) `instanceWhen` [Pat $ pow2 x] assert $ forall $ \x -> (x >=* 0 ==> pow2 x >* x) `instanceWhen` [Pat $ pow2 x] -- base cases assert $ pow2 0 ==* 1 assert $ pow2 1 ==* 2 -- recursive definition assert $ forall $ \x -> (x >* 1 ==> pow2 x ==* 2 * pow2 (x-1)) `instanceWhen` [Pat $ pow2 x] -- and that's it! return pow2