packages feed

z3 (empty) → 0.1.1

raw patch · 9 files changed

+2106/−0 lines, 9 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl

Files

+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c)2012, Iago Abal, David Castro++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the names of Iago Abal and David Castro nor the names of+      other contributors may be used to endorse or promote products+      derived from this software without specific prior written+      permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Z3/Base.hs view
@@ -0,0 +1,827 @@+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}++-- |+-- Module    : Z3.Base+-- 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>+--+-- Medium-level bindings, highly inspired by yices-painless.+--++module Z3.Base (++    -- * Types+      Config+    , Context+    , Symbol+    , AST+    , Sort+    , App+    , Pattern+    , Model++    , castAST+    +    -- ** Satisfiability result+    , Result(..)++    -- ** Z3 types+    , Z3Type(..)+    , Z3Scalar(..)+    , Z3Num++    -- * Configuration+    , mkConfig+    , setParamValue+    , set_MODEL+    , set_MODEL_PARTIAL+    , set_WELL_SORTED_CHECK++    -- * Context+    , mkContext++    -- * Symbols+    , mkStringSymbol++    -- * Sorts+    , mkBoolSort+    , mkIntSort+    , mkRealSort++    -- * Constants and Applications+    , mkConst+    , mkTrue+    , mkFalse+    , mkEq+    , mkNot+    , mkIte+    , mkIff+    , mkImplies+    , mkXor+    , mkAnd+    , mkOr+    , mkAdd+    , mkMul+    , mkSub+    , mkUnaryMinus+    , mkDiv+    , mkMod+    , mkRem+    , mkLt+    , mkLe+    , mkGt+    , mkGe+    , mkInt2Real+    , mkReal2Int+    , mkIsInt++    -- * Numerals+    , mkNumeral+    , mkInt+    , mkReal++    -- * Accessors+    , getBool+    , getInt+    , getReal++    -- * Models+    , eval++    -- * Constraints+    , assertCnstr+    , check+    , getModel++    ) where++import Z3.Base.C+import Z3.Types.TY++import Control.Applicative ( (<$>) )+import Control.Monad ( liftM2 )+import Data.Typeable ( Typeable )+import Data.Int+import Data.Ratio ( Ratio, numerator, denominator, (%) )+import Data.Word+import Data.Typeable ( Typeable, typeOf )+import Foreign hiding ( newForeignPtr, toBool )+import Foreign.C+  ( CInt, CUInt, CLLong, CULLong+  , peekCString+  , withCString )+import Foreign.Concurrent ( newForeignPtr )++---------------------------------------------------------------------+-- Types+--++-- | A Z3 /configuration object/.+-- +--+-- /Notes:/+--+-- * The resource is automatically managed by the Haskell garbage+-- collector, and the structure is automatically deleted once it is out+-- of scope (no need to call 'z3_del_config').+--+newtype Config = Config { unConfig :: ForeignPtr Z3_config }+    deriving Eq++-- | A Z3 /logical context/.+-- +--+-- /Notes:/+--+-- * The resource is automatically managed by the Haskell garbage+-- collector, and the structure is automatically deleted once it is out+-- of scope (no need to call 'z3_del_context').+--+newtype Context = Context { unContext :: ForeignPtr Z3_context }+    deriving Eq++-- | A Z3 /Lisp-link symbol/.+-- +newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol }+    deriving (Eq, Ord, Show, Storable)++-- | A Z3 /AST node/.+-- +-- TODO: Does the extra type safety provided by the phantom type worth+--       complicating the higher-level layers such as 'Z3.Monad' ?+--+newtype AST a = AST { unAST :: Ptr Z3_ast }+    deriving (Eq, Ord, Show, Storable)++-- | Cast an 'AST a' to 'AST b' when 'a' and 'b' are the same type.+--+-- This is useful when unpacking an existentially quantified AST.+--+castAST :: forall a b. (Z3Type a, Z3Type b) => AST a -> Maybe (AST b)+castAST (AST a) +    | typeOf (TY::TY a) == typeOf (TY::TY b) = Just (AST a)+    | otherwise                              = Nothing++-- | Kind of Z3 AST representing /types/.+--+newtype Sort a = Sort { unSort :: Ptr Z3_sort }+    deriving (Eq, Ord, Show, Storable)++-- | A kind of Z3 AST used to represent constant and function declarations.+--+newtype App a = App { _unApp :: Ptr Z3_app }+    deriving (Eq, Ord, Show, Storable)++-- | A kind of AST used to represent pattern and multi-patterns used to +--   guide quantifier instantiation.+--+newtype Pattern = Pattern { _unPattern :: Ptr Z3_pattern }+    deriving (Eq, Ord, Show, Storable)++-- | A model for the constraints asserted into the logical context.+--+data Model+    = Model {+        modelContext :: Context+      , unModel      :: ForeignPtr Z3_model+      }+    deriving Eq++-- | Result of a satisfiability check.+--+data Result+    = Sat+    | Unsat+    | Undef+    deriving (Eq, Ord, Enum, Bounded, Read, Show)++-- | Convert 'Z3_lbool' from Z3.Base.C to 'Result'+--+toResult :: Z3_lbool -> Result+toResult lb+    | lb == z3_l_true  = Sat+    | lb == z3_l_false = Unsat+    | lb == z3_l_undef = Undef+    | otherwise        = error "Z3.Base.toResult: illegal `Z3_lbool' value"++-- | Convert 'Z3_bool' to 'Bool'.+--+-- 'Foreign.toBool' should be OK but this is convenient.+--+toBool :: Z3_bool -> Bool+toBool b+    | b == z3_true  = True+    | b == z3_false = False+    | otherwise     = error "Z3.Base.toBool: illegal `Z3_bool' value"++-----------------------------------------------------------+-- Z3 types+--++-- | A Z3 type+--+class Typeable a => Z3Type a where+  mkSort :: Context -> IO (Sort a)++instance Z3Type Bool where+  mkSort = mkBoolSort++instance Z3Type Integer where+  mkSort = mkIntSort++instance Z3Type Rational where+  mkSort = mkRealSort++-- | A Z3 scalar type+--+class (Eq a, Show a, Z3Type a) => Z3Scalar a where+  mkValue :: Context -> a -> IO (AST a)+  getValue :: Context -> AST a -> IO (Maybe a)++instance Z3Scalar Bool where+  mkValue ctx True = mkTrue ctx+  mkValue ctx False = mkFalse ctx+  getValue = getBool++instance Z3Scalar Integer where+  mkValue ctx = mkInt ctx+  getValue ctx ast = Just <$> getInt ctx ast++instance Z3Scalar Rational where+  mkValue ctx = mkReal ctx+  getValue ctx ast = Just <$> getReal ctx ast++-- | A Z3 numeric type+--+class (Z3Scalar a, Num a) => Z3Num a where+instance Z3Num Integer where+instance Z3Num Rational where++---------------------------------------------------------------------+-- Configuration++-- | Create a configuration.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>+--+mkConfig :: IO Config+mkConfig = do+  ptr <- z3_mk_config+  fptr <- newForeignPtr ptr (z3_del_config ptr)+  return $! Config fptr++-- | Set a configuration parameter.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3>+--+-- See: <http://research.microsoft.com/en-us/um/redmond/projects/z3/config.html>+--+setParamValue :: Config -> String -> String -> IO ()+setParamValue cfg s1 s2 =+    withForeignPtr (unConfig cfg) $ \cfgPtr ->+    withCString s1                $ \cs1 ->+    withCString s2                $ \cs2 ->+        z3_set_param_value cfgPtr cs1 cs2++-- | Set the /MODEL/ configuration parameter.+--+-- default: 'True', enable/disable model construction.+--+set_MODEL :: Config -> Bool -> IO ()+set_MODEL cfg True  = setParamValue cfg "MODEL" "true"+set_MODEL cfg False = setParamValue cfg "MODEL" "false"++-- | Set the /MODEL_PARTIAL/ configuration parameter.+--+-- default: 'False', enable/disable partial function interpretations.+--+set_MODEL_PARTIAL :: Config -> Bool -> IO ()+set_MODEL_PARTIAL cfg True  = setParamValue cfg "MODEL_PARTIAL" "true"+set_MODEL_PARTIAL cfg False = setParamValue cfg "MODEL_PARTIAL" "false"++-- | Set the /WELL_SORTED_CHECK/ configuration parameter.+--+-- default: 'True', enable/disable type checker.+--+set_WELL_SORTED_CHECK :: Config -> Bool -> IO ()+set_WELL_SORTED_CHECK cfg True  = setParamValue cfg "MWELL_SORTED_CHECK" "true"+set_WELL_SORTED_CHECK cfg False = setParamValue cfg "WELL_SORTED_CHECK" "false"++---------------------------------------------------------------------+-- Context++-- | Create a context using the given configuration.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46>+--+mkContext :: Config -> IO Context+mkContext cfg = withForeignPtr (unConfig cfg) $ \cfgPtr -> do+  ptr <- z3_mk_context cfgPtr+  fptr <- newForeignPtr ptr (z3_del_context ptr)+  return $! Context fptr++---------------------------------------------------------------------+-- Symbols++-- | Create a Z3 symbol using a string.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>+--+mkStringSymbol :: Context -> String -> IO Symbol+mkStringSymbol ctx s =+    withForeignPtr (unContext ctx) $ \ctxPtr ->+    withCString s                  $ \cs     ->+        Symbol <$> z3_mk_string_symbol ctxPtr cs++---------------------------------------------------------------------+-- Sorts++-- TODO Sorts: Z3_is_eq_sort+-- TODO Sorts: Z3_mk_uninterpreted_sort++-- | Create the Boolean type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>+--+mkBoolSort :: Context -> IO (Sort Bool)+mkBoolSort c = withForeignPtr (unContext c) $ \cptr ->+  Sort <$> z3_mk_bool_sort cptr++-- | Create an integer type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>+--+mkIntSort :: Context -> IO (Sort Integer)+mkIntSort c = withForeignPtr (unContext c) $ \cptr ->+  Sort <$> z3_mk_int_sort cptr++-- | Create a real type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>+--+mkRealSort :: Context -> IO (Sort Rational)+mkRealSort c = withForeignPtr (unContext c) $ \cptr ->+  Sort <$> z3_mk_real_sort cptr++-- TODO Sorts: from Z3_mk_real_sort on++---------------------------------------------------------------------+-- Constants and Applications++-- TODO Constants and Applications: Z3_mk_func_decl+-- TODO Constants and Applications: Z3_mk_app++-- | Declare and create a constant.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>+--+mkConst :: Context -> Symbol -> Sort a -> IO (AST a)+mkConst c x s = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_const cptr (unSymbol x) (unSort s)++-- TODO Constants and Applications: Z3_mk_fresh_func_decl+-- TODO Constants and Applications: Z3_mk_fresh_const++-- | Create an AST node representing /true/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>+--+mkTrue :: Context -> IO (AST Bool)+mkTrue c = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_true cptr++-- | Create an AST node representing /false/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>+--+mkFalse :: Context -> IO (AST Bool)+mkFalse c = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_false cptr++-- | Create an AST node representing l = r.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>+--+mkEq :: Z3Scalar a => Context -> AST a -> AST a -> IO (AST Bool)+mkEq c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_eq cptr (unAST e1) (unAST e2)++-- | Create an AST node representing not(a).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>+--+mkNot :: Context -> AST Bool -> IO (AST Bool)+mkNot c e = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_not cptr (unAST e)++-- | Create an AST node representing an if-then-else: ite(t1, t2, t3).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>+--+mkIte :: Context -> AST Bool -> AST a -> AST a -> IO (AST a)+mkIte c g e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_ite cptr (unAST g) (unAST e1) (unAST e2)++-- | Create an AST node representing t1 iff t2. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>+--+mkIff :: Context -> AST Bool -> AST Bool -> IO (AST Bool)+mkIff c p q = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_iff cptr (unAST p) (unAST q)++-- | Create an AST node representing t1 implies t2. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>+--+mkImplies :: Context -> AST Bool -> AST Bool -> IO (AST Bool)+mkImplies c p q = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_implies cptr (unAST p) (unAST q)++-- | Create an AST node representing t1 xor t2. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>+--+mkXor :: Context -> AST Bool -> AST Bool -> IO (AST Bool)+mkXor c p q = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_xor cptr (unAST p) (unAST q)++-- | Create an AST node representing args[0] and ... and args[num_args-1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>+--+mkAnd :: Context -> [AST Bool] -> IO (AST Bool)+mkAnd _ [] = error "Z3.Base.mkAnd: empty list of expressions"+mkAnd c es +  = withArray es $ \aptr -> +    withForeignPtr (unContext c) $ \cptr ->+      AST <$> z3_mk_and cptr n (castPtr aptr) +  where n = fromIntegral $ length es++-- | Create an AST node representing args[0] or ... or args[num_args-1]. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>+--+mkOr :: Context -> [AST Bool] -> IO (AST Bool)+mkOr _ [] = error "Z3.Base.mkOr: empty list of expressions"+mkOr c es +  = withArray es $ \aptr -> +    withForeignPtr (unContext c) $ \cptr ->+      AST <$> z3_mk_or cptr n (castPtr aptr) +  where n = fromIntegral $ length es++-- | Create an AST node representing args[0] + ... + args[num_args-1].  +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>+--+mkAdd :: Z3Num a => Context -> [AST a] -> IO (AST a)+mkAdd _ [] = error "Z3.Base.mkAdd: empty list of expressions"+mkAdd c es +  = withArray es $ \aptr -> +    withForeignPtr (unContext c) $ \cptr ->+      AST <$> z3_mk_add cptr n (castPtr aptr) +  where n = fromIntegral $ length es++-- | Create an AST node representing args[0] * ... * args[num_args-1].  +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>+--+mkMul :: Z3Num a => Context -> [AST a] -> IO (AST a)+mkMul _ [] = error "Z3.Base.mkMul: empty list of expressions"+mkMul c es +  = withArray es $ \aptr -> +    withForeignPtr (unContext c) $ \cptr ->+      AST <$> z3_mk_mul cptr n (castPtr aptr) +  where n = fromIntegral $ length es++-- | Create an AST node representing args[0] - ... - args[num_args - 1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>+--+mkSub ::Z3Num a => Context -> [AST a] -> IO (AST a)+mkSub _ [] = error "Z3.Base.mkSub: empty list of expressions"+mkSub c es +  = withArray es $ \aptr -> +    withForeignPtr (unContext c) $ \cptr ->+      AST <$> z3_mk_sub cptr n (castPtr aptr) +  where n = fromIntegral $ length es++-- | Create an AST node representing -arg.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>+--+mkUnaryMinus :: Z3Num a => Context -> AST a -> IO (AST a)+mkUnaryMinus c e = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_unary_minus cptr (unAST e)++-- | Create an AST node representing arg1 div arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>+--+mkDiv :: Z3Num a => Context -> AST a -> AST a -> IO (AST a)+mkDiv c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_div cptr (unAST e1) (unAST e2)++-- | Create an AST node representing arg1 mod arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>+--+mkMod :: Context -> AST Integer -> AST Integer -> IO (AST Integer)+mkMod c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_mod cptr (unAST e1) (unAST e2)++-- | Create an AST node representing arg1 rem arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>+--+mkRem :: Context -> AST Integer -> AST Integer -> IO (AST Integer)+mkRem c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_rem cptr (unAST e1) (unAST e2)++-- | Create less than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>+--+mkLt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)+mkLt c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_lt cptr (unAST e1) (unAST e2)++-- | Create less than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>+--+mkLe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)+mkLe c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_le cptr (unAST e1) (unAST e2)++-- | Create greater than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>+--+mkGt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)+mkGt c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_gt cptr (unAST e1) (unAST e2)++-- | Create greater than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>+--+mkGe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)+mkGe c e1 e2 = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_ge cptr (unAST e1) (unAST e2)++-- | Coerce an integer to a real.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>+--+mkInt2Real :: Context -> AST Integer -> IO (AST Rational)+mkInt2Real c e = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_int2real cptr (unAST e)++-- | Coerce a real to an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>+--+mkReal2Int :: Context -> AST Rational -> IO (AST Integer)+mkReal2Int c e = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_real2int cptr (unAST e)++-- | Check if a real number is an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>+--+mkIsInt :: Context -> AST Rational -> IO (AST Bool)+mkIsInt c e = withForeignPtr (unContext c) $ \cptr ->+  AST <$> z3_mk_is_int cptr (unAST e)++-- TODO Bit-vector, Arrays, Sets+++---------------------------------------------------------------------+-- Numerals++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>+--+mkNumeral :: Z3Num a => Context -> String -> Sort a -> IO (AST a)+mkNumeral c str s =+    withForeignPtr (unContext c) $ \cptr ->+    withCString str              $ \cstr->+        AST <$> z3_mk_numeral cptr cstr (unSort s)++-------------------------------------------------+-- Numerals / Integers++-- | Create a numeral of sort /int/.+mkInt :: Integral a => Context -> a -> IO (AST Integer)+mkInt c n = mkIntSort c >>= mkNumeral c n_str+    where n_str = show $ toInteger n++{-# INLINE mkIntZ3 #-}+mkIntZ3 :: Z3Num a => Context -> Int32 -> Sort a -> IO (AST a)+mkIntZ3 c n s =+    withForeignPtr (unContext c) $ \ctxPtr ->+        AST <$> z3_mk_int ctxPtr cn (unSort s)+    where cn = fromIntegral n :: CInt++{-# INLINE mkUnsignedIntZ3 #-}+mkUnsignedIntZ3 :: Z3Num a => Context -> Word32 -> Sort a -> IO (AST a)+mkUnsignedIntZ3 c n s =+    withForeignPtr (unContext c) $ \ctxPtr ->+        AST <$> z3_mk_unsigned_int ctxPtr cn (unSort s)+    where cn = fromIntegral n :: CUInt++{-# INLINE mkInt64Z3 #-}+mkInt64Z3 :: Z3Num a => Context -> Int64 -> Sort a -> IO (AST a)+mkInt64Z3 c n s =+    withForeignPtr (unContext c) $ \ctxPtr ->+        AST <$> z3_mk_int64 ctxPtr cn (unSort s)+    where cn = fromIntegral n :: CLLong++{-# INLINE mkUnsignedInt64Z3 #-}+mkUnsignedInt64Z3 :: Z3Num a => Context -> Word64 -> Sort a -> IO (AST a)+mkUnsignedInt64Z3 c n s =+    withForeignPtr (unContext c) $ \ctxPtr ->+        AST <$> z3_mk_unsigned_int64 ctxPtr cn (unSort s)+    where cn = fromIntegral n :: CULLong++{-# RULES "mkInt/mkInt_IntZ3" mkInt = mkInt_IntZ3 #-}+mkInt_IntZ3 :: Context -> Int32 -> IO (AST Integer)+mkInt_IntZ3 c n = mkIntSort c >>= mkIntZ3 c n++{-# RULES "mkInt/mkInt_UnsignedIntZ3" mkInt = mkInt_UnsignedIntZ3 #-}+mkInt_UnsignedIntZ3 :: Context -> Word32 -> IO (AST Integer)+mkInt_UnsignedIntZ3 c n = mkIntSort c >>= mkUnsignedIntZ3 c n++{-# RULES "mkInt/mkInt_Int64Z3" mkInt = mkInt_Int64Z3 #-}+mkInt_Int64Z3 :: Context -> Int64 -> IO (AST Integer)+mkInt_Int64Z3 c n = mkIntSort c >>= mkInt64Z3 c n++{-# RULES "mkInt/mkInt_UnsignedInt64Z3" mkInt = mkInt_UnsignedInt64Z3 #-}+mkInt_UnsignedInt64Z3 :: Context -> Word64 -> IO (AST Integer)+mkInt_UnsignedInt64Z3 c n = mkIntSort c >>= mkUnsignedInt64Z3 c n++-------------------------------------------------+-- Numerals / Reals++-- | Create a numeral of sort /real/.+mkReal :: Real r => Context -> r -> IO (AST Rational)+mkReal c n = mkRealSort c >>= mkNumeral c n_str+    where r = toRational n+          r_n = toInteger $ numerator r+          r_d = toInteger $ denominator r+          n_str = show r_n ++ " / " ++ show r_d++{-# RULES "mkReal/mkRealZ3" mkReal = mkRealZ3 #-}+mkRealZ3 :: Context -> Ratio Int32 -> IO (AST Rational)+mkRealZ3 c r =+    withForeignPtr (unContext c) $ \ctxPtr ->+        AST <$> z3_mk_real ctxPtr n d+    where n = (fromIntegral $ numerator r)   :: CInt+          d = (fromIntegral $ denominator r) :: CInt++{-# RULES "mkReal/mkReal_IntZ3" mkReal = mkReal_IntZ3 #-}+mkReal_IntZ3 :: Context -> Int32 -> IO (AST Rational)+mkReal_IntZ3 c n = mkRealSort c >>= mkIntZ3 c n++{-# RULES "mkReal/mkReal_UnsignedIntZ3" mkReal = mkReal_UnsignedIntZ3 #-}+mkReal_UnsignedIntZ3 :: Context -> Word32 -> IO (AST Rational)+mkReal_UnsignedIntZ3 c n = mkRealSort c >>= mkUnsignedIntZ3 c n++{-# RULES "mkReal/mkReal_Int64Z3" mkReal = mkReal_Int64Z3 #-}+mkReal_Int64Z3 :: Context -> Int64 -> IO (AST Rational)+mkReal_Int64Z3 c n = mkRealSort c >>= mkInt64Z3 c n++{-# RULES "mkReal/mkReal_UnsignedInt64Z3" mkReal = mkReal_UnsignedInt64Z3 #-}+mkReal_UnsignedInt64Z3 :: Context -> Word64 -> IO (AST Rational)+mkReal_UnsignedInt64Z3 c n = mkRealSort c >>= mkUnsignedInt64Z3 c n++-- TODO Quantifiers++---------------------------------------------------------------------+-- Accessors++-- | Cast a 'Z3_lbool' from Z3.Base.C to @Bool@.+castLBool :: Z3_lbool -> Maybe Bool+castLBool lb+    | lb == z3_l_true  = Just True+    | lb == z3_l_false = Just False+    | lb == z3_l_undef = Nothing+    | otherwise        = error "Z3.Base.castLBool: illegal `Z3_lbool' value"++-- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF+-- otherwise.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>+--+getBool :: Context -> AST Bool -> IO (Maybe Bool)+getBool c a = withForeignPtr (unContext c) $ \ctxPtr ->+  castLBool <$> z3_get_bool_value ctxPtr (unAST a)++-- | Return numeral value, as a string of a numeric constant term.  +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>+--+getNumeralString :: Z3Num a => Context -> AST a -> IO String+getNumeralString c a = withForeignPtr (unContext c) $ \ctxPtr ->+  peekCString =<< z3_get_numeral_string ctxPtr (unAST a)++-- | Return 'Z3Int' value+--+getInt :: Num a => Context -> AST Integer -> IO a+getInt c a = fromInteger . read <$> getNumeralString c a++-- | Return the numerator (as a numeral AST) of a numeral AST of sort /real/. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga69564aaa9f2a76556b54f5bbff8e7175>+--+getNumerator :: Context -> AST Rational -> IO Integer+getNumerator c a = withForeignPtr (unContext c) $ \ctxPtr ->+  z3_get_numerator ctxPtr (unAST a) >>= getInt c . AST++-- | Return the denominator (as a numeral AST) of a numeral AST of sort /real/. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga25e5269d6845bb8ae03b551f09f5d46d>+--+getDenominator :: Context -> AST Rational -> IO Integer+getDenominator c a = withForeignPtr (unContext c) $ \ctxPtr ->+  z3_get_denominator ctxPtr (unAST a) >>= getInt c . AST++-- | Return 'Z3Real' value+--+getReal :: Fractional a => Context -> AST Rational -> IO a+getReal c a = fromRational <$>+  liftM2 (%) (getNumerator c a) (getDenominator c a)++-- TODO Modifiers++---------------------------------------------------------------------+-- Models++mkModel :: Context -> Ptr Z3_model -> IO Model+mkModel ctx ptr = withForeignPtr (unContext ctx) $ \ctxPtr ->+    Model ctx <$> newForeignPtr ptr (z3_del_model ctxPtr ptr)++-- | Evaluate an AST node in the given model.+eval :: Model -> AST a -> IO (Maybe (AST a))+eval m a+  = withForeignPtr (unContext $ modelContext m) $ \ctxPtr ->+    withForeignPtr (unModel m) $ \mdlPtr ->+      alloca $ \aptr2 ->+        z3_eval ctxPtr mdlPtr (unAST a) aptr2 >>= peekAST aptr2 . toBool+  where peekAST :: Ptr (Ptr Z3_ast) -> Bool -> IO (Maybe (AST a))+        peekAST _p False = return Nothing+        peekAST  p True  = Just . AST <$> peek p++---------------------------------------------------------------------+-- Constraints++-- TODO Constraints: Z3_push+-- TODO Constraints: Z3_pop+-- TODO Constraints: Z3_get_num_scopes+-- TODO Constraints: Z3_persist_ast++-- | Assert a constraing into the logical context.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>+--+assertCnstr :: Context -> AST Bool -> IO ()+assertCnstr ctx ast =+    withForeignPtr (unContext ctx) $ \ctxPtr ->+        z3_assert_cnstr ctxPtr (unAST ast)++-- | Get model (logical context is consistent)+--+-- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>+--+getModel :: Context -> IO (Result, Maybe Model)+getModel c = withForeignPtr (unContext c) $ \ctxPtr ->+  alloca $ \mptr ->+    z3_check_and_get_model ctxPtr mptr >>= peekModel mptr . toResult+  where peekModel :: Ptr (Ptr Z3_model)+                  -> Result+                  -> IO (Result, Maybe Model)+        peekModel p r | p == nullPtr = return (r, Nothing)+                      | otherwise    = do z3m <- peek p+                                          m   <- mkModel c z3m+                                          return (r, Just m)++-- | Check whether the given logical context is consistent or not. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>+--+check :: Context -> IO Result+check ctx = toResult <$> withForeignPtr (unContext ctx) z3_check++-- TODO Constraints: Z3_check_assumptions+-- TODO Constraints: Z3_get_implied_equalities++-- TODO From section 'Constraints' on.
+ Z3/Base/C.hsc view
@@ -0,0 +1,489 @@+{-# LANGUAGE EmptyDataDecls             #-}+{-# LANGUAGE ForeignFunctionInterface   #-}++-- |+-- Module    : Z3.Base.C+-- 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>+--+-- Low-level bindings, highly inspired by yices-painless.+--+++module Z3.Base.C where++import Foreign+import Foreign.C.Types+import Foreign.C.String++#include <z3.h>+++---------------------------------------------------------------------+-- * Types++-- | A configuration object used to initialize logical contexts.+data Z3_config++-- | Logical context. This is the main Z3 data-structure.+data Z3_context++-- | A Lisp-link symbol. It is used to name types, constants, and functions.+-- A symbol can be created using string or integers.+data Z3_symbol++-- | Abstract syntax tree node. That is, the data-structure used in Z3 to+-- represent terms, formulas and types.+data Z3_ast++-- | A kind of AST used to represent types.+data Z3_sort++-- | A kind of AST used to represent constant and function declarations.+data Z3_app++-- | A kind of AST used to represent pattern and multi-patterns used to +-- guide quantifier instantiation.+data Z3_pattern ++-- | A model for the constraints asserted into the logical context.+data Z3_model++-- | Lifted Boolean type: false, undefined, true.+type Z3_lbool = CInt++-- | Values of lifted boolean type+z3_l_true, z3_l_false, z3_l_undef :: Z3_lbool+z3_l_true  = #const Z3_L_TRUE+z3_l_false = #const Z3_L_FALSE+z3_l_undef = #const Z3_L_UNDEF++-- | Boolean type. It is just an alias for int.+type Z3_bool = CInt++-- | Z3_bool values+z3_true, z3_false :: Z3_lbool+z3_true  = #const Z3_TRUE+z3_false = #const Z3_FALSE++-- | Z3 String type+type Z3_string = CString++---------------------------------------------------------------------+-- * Create configuration++-- | Create a configuration.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>+--+foreign import ccall unsafe "Z3_mk_config"+    z3_mk_config :: IO (Ptr Z3_config)++-- | Delete the given configuration object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774>+--+foreign import ccall unsafe "Z3_del_config"+    z3_del_config :: Ptr Z3_config -> IO ()++-- | Set a configuration parameter.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3>+--+foreign import ccall unsafe "Z3_set_param_value"+    z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO ()+++---------------------------------------------------------------------+-- * Create context++-- | Create a context using the given configuration.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46>+--+foreign import ccall unsafe "Z3_mk_context"+    z3_mk_context :: Ptr Z3_config -> IO (Ptr Z3_context)++-- | Delete the given logical context.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200>+--+foreign import ccall unsafe "Z3_del_context"+    z3_del_context :: Ptr Z3_context -> IO ()+++---------------------------------------------------------------------+-- * Symbols++-- | Create a Z3 symbol using a C string.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>+--+foreign import ccall unsafe "Z3_mk_string_symbol"+    z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol)+++---------------------------------------------------------------------+-- * Sorts++-- TODO Sorts: Z3_is_eq_sort+-- TODO Sorts: Z3_mk_uninterpreted_sort++-- | Create the Boolean type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>+--+foreign import ccall unsafe "Z3_mk_bool_sort"+    z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)++-- | Create an integer type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>+--+foreign import ccall unsafe "Z3_mk_int_sort"+    z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)++-- | Create a real type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>+--+foreign import ccall unsafe "Z3_mk_real_sort"+    z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)++-- TODO Sorts: from Z3_mk_real_sort on+++---------------------------------------------------------------------+-- * Constants and Applications++-- TODO Constants and Applications: Z3_mk_func_decl+-- TODO Constants and Applications: Z3_mk_app++-- | Declare and create a constant.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>+--+foreign import ccall unsafe "Z3_mk_const"+    z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast)++-- TODO Constants and Applications: Z3_mk_fresh_func_decl+-- TODO Constants and Applications: Z3_mk_fresh_const++---------------------------------------------------------------------+-- * Propositional Logic and Equality++-- | Create an AST node representing /true/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>+--+foreign import ccall unsafe "Z3_mk_true"+    z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast)++-- | Create an AST node representing /false/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>+--+foreign import ccall unsafe "Z3_mk_false"+    z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast)++-- | Create an AST node representing l = r.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>+--+foreign import ccall unsafe "Z3_mk_eq"+    z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- TODO: Z3_mk_distinct++-- | Create an AST node representing not(a).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>+--+foreign import ccall unsafe "Z3_mk_not"+    z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Create an AST node representing an if-then-else: ite(t1, t2, t3).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>+--+foreign import ccall unsafe "Z3_mk_ite"+    z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Create an AST node representing t1 iff t2. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>+--+foreign import ccall unsafe "Z3_mk_iff"+    z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Create an AST node representing t1 implies t2. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>+--+foreign import ccall unsafe "Z3_mk_implies"+    z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Create an AST node representing t1 xor t2. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>+--+foreign import ccall unsafe "Z3_mk_xor"+    z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Create an AST node representing args[0] and ... and args[num_args-1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>+--+foreign import ccall unsafe "Z3_mk_and"+    z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++-- | Create an AST node representing args[0] or ... or args[num_args-1]. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>+--+foreign import ccall unsafe "Z3_mk_or"+    z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++---------------------------------------------------------------------+-- * Arithmetic: Integers and Reals++-- | Create an AST node representing args[0] + ... + args[num_args-1].  +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>+--+foreign import ccall unsafe "Z3_mk_add"+    z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++-- | Create an AST node representing args[0] * ... * args[num_args-1].  +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>+--+foreign import ccall unsafe "Z3_mk_mul"+    z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++-- | Create an AST node representing args[0] - ... - args[num_args - 1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>+--+foreign import ccall unsafe "Z3_mk_sub"+    z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++-- | Create an AST node representing -arg.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>+--+foreign import ccall unsafe "Z3_mk_unary_minus"+    z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Create an AST node representing arg1 div arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>+--+foreign import ccall unsafe "Z3_mk_div"+    z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Create an AST node representing arg1 mod arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>+--+foreign import ccall unsafe "Z3_mk_mod"+    z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Create an AST node representing arg1 rem arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>+--+foreign import ccall unsafe "Z3_mk_rem"+    z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Create less than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>+--+foreign import ccall unsafe "Z3_mk_lt"+    z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Create less than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>+--+foreign import ccall unsafe "Z3_mk_le"+    z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Create greater than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>+--+foreign import ccall unsafe "Z3_mk_gt"+    z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Create greater than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>+--+foreign import ccall unsafe "Z3_mk_ge"+    z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast ->  IO (Ptr Z3_ast)++-- | Coerce an integer to a real.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>+--+foreign import ccall unsafe "Z3_mk_int2real"+    z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Coerce a real to an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>+--+foreign import ccall unsafe "Z3_mk_real2int"+    z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Check if a real number is an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>+--+foreign import ccall unsafe "Z3_mk_is_int"+    z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- TODO Bit-vectors, Arrays, Sets++---------------------------------------------------------------------+-- * Numerals++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>+--+foreign import ccall unsafe "Z3_mk_numeral"+    z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort ->  IO (Ptr Z3_ast)++-- | Create a real from a fraction.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabe0bbc1e01a084a75506a62e5e6900b3>+--+foreign import ccall unsafe "Z3_mk_real"+    z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast)++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8779204998136569c3e166c34cfd3e2c>+--+foreign import ccall unsafe "Z3_mk_int"+    z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort ->  IO (Ptr Z3_ast)++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7201b6231b61421c005457206760a121>+--+foreign import ccall unsafe "Z3_mk_unsigned_int"+    z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort ->  IO (Ptr Z3_ast)++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga42cc319787d485d9cb665d80e02d206f>+--+foreign import ccall unsafe "Z3_mk_int64"+    z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort ->  IO (Ptr Z3_ast)++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88a165138162a8bac401672f0a1b7891>+--+foreign import ccall unsafe "Z3_mk_unsigned_int64"+    z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort ->  IO (Ptr Z3_ast)++-- TODO Quantifiers++---------------------------------------------------------------------+-- * Accessors++-- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF+-- otherwise.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>+--+foreign import ccall unsafe "Z3_get_bool_value"+    z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool++-- | Return numeral value, as a string of a numeric constant term.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>+--+foreign import ccall unsafe "Z3_get_numeral_string"+    z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string++-- | Return the numerator (as a numeral AST) of a numeral AST of sort Int.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga69564aaa9f2a76556b54f5bbff8e7175>+--+foreign import ccall unsafe "Z3_get_numerator"+    z3_get_numerator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Return the denominator (as a numeral AST) of a numeral AST of sort Real.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga25e5269d6845bb8ae03b551f09f5d46d>+--+foreign import ccall unsafe "Z3_get_denominator"+    z3_get_denominator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- TODO Modifiers++---------------------------------------------------------------------+-- * Models++-- | Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded,+-- and store the result in v.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga47d3655283564918c85bda0b423b7f67>+--+foreign import ccall unsafe "Z3_eval"+    z3_eval :: Ptr Z3_context+            -> Ptr Z3_model+            -> Ptr Z3_ast+            -> Ptr (Ptr Z3_ast)+            -> IO Z3_bool++---------------------------------------------------------------------+-- * Constraints++-- TODO Constraints: Z3_push+-- TODO Constraints: Z3_pop+-- TODO Constraints: Z3_get_num_scopes+-- TODO Constraints: Z3_persist_ast++-- | Assert a constraing into the logical context.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>+--+foreign import ccall unsafe "Z3_assert_cnstr"+    z3_assert_cnstr :: Ptr Z3_context -> Ptr Z3_ast ->  IO ()++-- | Check whether the given logical context is consistent or not.+--+-- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>+--+foreign import ccall unsafe "Z3_check_and_get_model"+    z3_check_and_get_model :: Ptr Z3_context -> Ptr (Ptr Z3_model) -> IO Z3_lbool++-- | Check whether the given logical context is consistent or not. +--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>+--+foreign import ccall unsafe "Z3_check"+    z3_check :: Ptr Z3_context ->  IO Z3_lbool++-- TODO Constraints: Z3_check_assumptions+-- TODO Constraints: Z3_get_implied_equalities++-- | Delete a model object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee>+--+foreign import ccall unsafe "Z3_del_model"+    z3_del_model :: Ptr Z3_context -> Ptr Z3_model -> IO ()+++-- TODO From section 'Constraints' on.
+ Z3/Exprs.hs view
@@ -0,0 +1,211 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}++{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs              #-}+{-# LANGUAGE StandaloneDeriving #-}++-- |+-- Module    : Z3.Exprs+-- 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>+-- Stability : experimental++-- TODO: Pretty-printing of expressions++module Z3.Exprs (++    module Z3.Types+    +    -- * Abstract syntax+    , Expr++    -- * Constructing expressions+    , true+    , false+    , not_+    , and_, (&&*)+    , or_, (||*)+    , xor+    , implies, (==>)+    , iff, (<=>)+    , (//), (%*), (%%)+    , (==*), (/=*)+    , (<=*), (<*)+    , (>=*), (>*) +    , ite++    ) where+++import Z3.Exprs.Internal+import Z3.Types++import Data.Typeable ( Typeable1(..), typeOf )+import Unsafe.Coerce ( unsafeCoerce )+++deriving instance Show (Expr a)+deriving instance Typeable1 Expr++instance Eq (Expr a) where+  (Lit l1) == (Lit l2) = l1 == l2+  (Const a) == (Const b) = a == b+  (Not e1) == (Not e2) = e1 == e2+  (BoolBin op1 p1 q1) == (BoolBin op2 p2 q2)+    = op1 == op2 && p1 == p2 && q1 == q2+  (BoolMulti op1 ps) == (BoolMulti op2 qs)+    | length ps == length qs = op1 == op2 && and (zipWith (==) ps qs)+  (Neg e1) == (Neg e2) = e1 == e2+  (CRingArith op1 as) == (CRingArith op2 bs)+    | length as == length bs = op1 == op2 && and (zipWith (==) as bs)+  (IntArith op1 a1 b1) == (IntArith op2 a2 b2)+    = op1 == op2 && a1 == a2 && b1 == b2+  (RealArith op1 a1 b1) == (RealArith op2 a2 b2)+    = op1 == op2 && a1 == a2 && b1 == b2+  (CmpE op1 a1 b1) == (CmpE op2 a2 b2)+    | op1 == op2 && typeOf a1 == typeOf a2+    = a1 == unsafeCoerce a2 && b1 == unsafeCoerce b2+  (CmpI op1 a1 b1) == (CmpI op2 a2 b2)+    | op1 == op2 && typeOf a1 == typeOf a2+    = a1 == unsafeCoerce a2 && b1 == unsafeCoerce b2+  (Ite g1 a1 b1) == (Ite g2 a2 b2) = g1 == g2 && a1 == a2 && b1 == b2+  _e1 == _e2 = False+++-- * Constructing expressions++instance IsNum a => Num (Expr a) where+  (CRingArith Add as) + (CRingArith Add bs) = CRingArith Add (as ++ bs)+  (CRingArith Add as) + b = CRingArith Add (b:as)+  a + (CRingArith Add bs) = CRingArith Add (a:bs)+  a + b = CRingArith Add [a,b]+  (CRingArith Mul as) * (CRingArith Mul bs) = CRingArith Mul (as ++ bs)+  (CRingArith Mul as) * b = CRingArith Mul (b:as)+  a * (CRingArith Mul bs) = CRingArith Mul (a:bs)+  a * b = CRingArith Mul [a,b]+  (CRingArith Sub as) - b = CRingArith Sub (as ++ [b])+  a - b = CRingArith Sub [a,b]+  negate = Neg+  abs e = ite (e >=* 0) e (-e)+  signum e = ite (e >* 0) 1 (ite (e ==* 0) 0 (-1))+  fromInteger = literal . fromInteger++instance IsReal a => Fractional (Expr a) where+  (/) = RealArith Div+  fromRational = literal . fromRational++infixl 7  //, %*, %%+infix  4  ==*, /=*, <*, <=*, >=*, >*+infixr 3  &&*, ||*, `xor`+infixr 2  `implies`, `iff`, ==>, <=>++-- | /literal/ constructor.+--+literal :: IsScalar a => a -> Expr a+literal = Lit++-- | Boolean literals.+--+true, false :: Expr Bool+true  = Lit True+false = Lit False++-- | Boolean negation+--+not_ :: Expr Bool -> Expr Bool+not_ = Not++-- | Boolean binary /xor/.+--+xor :: Expr Bool -> Expr Bool -> Expr Bool+xor = BoolBin Xor+-- | Boolean implication+--+implies :: Expr Bool -> Expr Bool -> Expr Bool+implies = BoolBin Implies+-- | An alias for 'implies'.+--+(==>) :: Expr Bool -> Expr Bool -> Expr Bool+(==>) = implies+-- | Boolean /if and only if/.+--+iff :: Expr Bool -> Expr Bool -> Expr Bool+iff = BoolBin Iff+-- | An alias for 'iff'.+--+(<=>) :: Expr Bool -> Expr Bool -> Expr Bool+(<=>) = iff++-- | Boolean variadic /and/.+--+and_ :: [Expr Bool] -> Expr Bool+and_ = BoolMulti And+-- | Boolean variadic /or/.+--+or_ :: [Expr Bool] -> Expr Bool+or_  = BoolMulti Or++-- | Boolean binary /and/.+--+(&&*) :: Expr Bool -> Expr Bool -> Expr Bool+(BoolMulti And ps) &&* (BoolMulti And qs) = and_ (ps ++ qs)+(BoolMulti And ps) &&* q = and_ (q:ps)+p &&* (BoolMulti And qs) = and_ (p:qs)+p &&* q = and_ [p,q]+-- | Boolean binary /or/.+--+(||*) :: Expr Bool -> Expr Bool -> Expr Bool+(BoolMulti Or ps) ||* (BoolMulti Or qs) = or_ (ps ++ qs)+(BoolMulti Or ps) ||* q = or_ (q:ps)+p ||* (BoolMulti Or qs) = or_ (p:qs)+p ||* q = or_ [p,q]++-- | Integer division.+--+(//) :: IsInt a => Expr a -> Expr a -> Expr a+(//) = IntArith Quot+-- | Integer modulo.+--+(%*) :: IsInt a => Expr a -> Expr a -> Expr a+(%*) = IntArith Mod+-- | Integer remainder.+--+(%%) :: IsInt a => Expr a -> Expr a -> Expr a+(%%) = IntArith Rem+++-- | Equals.+--+(==*) :: IsScalar a => Expr a -> Expr a -> Expr Bool+(==*) = CmpE Eq+-- | Not equals.+--+(/=*) :: IsScalar a => Expr a -> Expr a -> Expr Bool+(/=*) = CmpE Neq+++-- | Less or equals than.+--+(<=*) :: IsNum a => Expr a -> Expr a -> Expr Bool+(<=*) = CmpI Le+-- | Less than.+--+(<*) :: IsNum a => Expr a -> Expr a -> Expr Bool+(<*) = CmpI Lt+-- | Greater or equals than.+--+(>=*) :: IsNum a => Expr a -> Expr a -> Expr Bool+(>=*) = CmpI Ge+-- | Greater than.+--+(>*) :: IsNum a => Expr a -> Expr a -> Expr Bool+(>*) = CmpI Gt++-- | /if-then-else/.+--+ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a+ite = Ite
+ Z3/Exprs/Internal.hs view
@@ -0,0 +1,109 @@++{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE StandaloneDeriving #-}++-- |+-- Module    : Z3.Exprs.Internal+-- 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>+-- Stability : experimental++module Z3.Exprs.Internal where+++import Z3.Types++import Data.Typeable ( Typeable )+++-- | Unique identifiers+--+type Uniq = Int++{-# WARNING Lit+          , Const+          , Not+          , BoolBin+          , BoolMulti+          , Neg+          , CRingArith+          , IntArith+          , RealArith+          , CmpE+          , CmpI+          , Ite+          "You are using a constructor of type Expr, \+          \which you should NOT be using! \+          \In fact, you should not be importing this \+          \module at all! Import Z3.Exprs instead!" #-}++-- | Abstract syntax.+--+data Expr :: * -> * where+  --  | Literals+  Lit :: IsScalar a => a -> Expr a+  --  | Constants+  Const :: !Uniq -> Expr a+  --  | Logical negation+  Not :: Expr Bool -> Expr Bool+  --  | Binary boolean expressions+  BoolBin :: BoolBinOp -> Expr Bool -> Expr Bool -> Expr Bool+  --  | Variadic boolean expressions+  BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool+  --  | Arithmetic negation+  Neg :: IsNum a => Expr a -> Expr a+  --  | Arithmetic expressions for commutative rings+  CRingArith :: IsNum a => CRingOp -> [Expr a] -> Expr a+  --  | Integer arithmetic+  IntArith :: IsInt a => IntOp -> Expr a -> Expr a -> Expr a+  --  | Real arithmetic+  RealArith :: IsReal a => RealOp -> Expr a -> Expr a -> Expr a+  --  | Comparison expressions+  CmpE :: IsScalar a => CmpOpE -> Expr a -> Expr a -> Expr Bool+  CmpI :: IsNum a => CmpOpI -> Expr a -> Expr a -> Expr Bool+  --  | if-then-else expressions+  Ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a++{-# WARNING BoolBinOp+          , BoolMultiOp+          , CRingOp+          , IntOp+          , RealOp+          , CmpOpE+          , CmpOpI+          "You should NOT be using this type or data constructor! \+          \In fact, you should not be importing this \+          \module at all! Import Z3.Exprs instead!" #-}++-- | Boolean binary operations.+data BoolBinOp = Xor | Implies | Iff+    deriving (Eq,Show)++-- | Boolean variadic operations.+data BoolMultiOp = And | Or+    deriving (Eq,Show)++-- | Commutative ring operations.+data CRingOp = Add | Mul | Sub+    deriving (Eq,Show)++-- | Operations for sort /int/.+data IntOp = Quot | Mod | Rem+    deriving (Eq,Show)++-- | Operations for sort /real/.+data RealOp = Div+    deriving (Eq,Show)++-- | Equality testing.+data CmpOpE = Eq | Neq+    deriving (Eq, Show, Typeable)++-- | Inequality comparisons.+data CmpOpI = Le | Lt | Ge | Gt+    deriving (Eq, Show, Typeable)
+ Z3/Monad.hs view
@@ -0,0 +1,284 @@+{-# OPTIONS_GHC -funbox-strict-fields #-}+{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}++{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE PatternGuards              #-}+{-# LANGUAGE ScopedTypeVariables        #-}++-- |+-- Module    : Z3.Monad+-- 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>+-- Stability : experimental+++module Z3.Monad (+    -- * Z3 Monad+      Z3+    , evalZ3++    -- * Satisfiability result+    , Base.Result(..)++    -- * Z3 actions+    , var+    , assert+    , let_+    , check++    , module Z3.Exprs++    ) where++import qualified Z3.Base as Base+import Z3.Exprs+import Z3.Exprs.Internal++import Control.Monad+import Control.Monad.State.Strict+import Data.Maybe ( fromMaybe )+import qualified Data.IntMap as Map++---------------------------------------------------------------------+-- The Z3 Monad++-- | Z3 monad.+--+newtype Z3 a = Z3 (StateT Z3State IO a)+    deriving (Functor, Monad)++instance MonadState Z3State Z3 where+    get = Z3 $ StateT $ \s -> return (s,s)+    put st = Z3 $ StateT $ \_ -> return ((), st)++-- | Existential type. Used to store constants keeping sort info.+--+data AnyAST = forall a. Base.Z3Type a => AnyAST (Base.AST a)++-- | Internal state of Z3 monad.+--+data Z3State+    = Z3State { uniqVal   :: !Uniq+              , context   :: Base.Context+              , consts    :: Map.IntMap AnyAST+              }++-- | Eval a Z3 script.+--+evalZ3 :: Z3 a -> IO a+evalZ3 (Z3 s) = do+    cfg  <- Base.mkConfig+    Base.set_MODEL cfg True+    Base.set_MODEL_PARTIAL cfg False+    ctx  <- Base.mkContext cfg+    evalStateT s Z3State { uniqVal   = 0+                         , context   = ctx+                         , consts    = Map.empty+                         }++-- | Fresh symbol name.+--+fresh :: Z3 (Uniq, String)+fresh = do+    st <- get+    let i = uniqVal st+    put st { uniqVal = i + 1 }+    return (uniqVal st, 'v':show i)++-- | Add a constant of type @Base.AST a@ to the state.+--+addConst :: Base.Z3Type a => Uniq -> Base.AST a -> Z3 ()+addConst u ast = do+    st <- get+    put st { consts = Map.insert u (AnyAST ast) (consts st) }++-- | Get a 'Base.AST' stored in the Z3State.+--+{- TODO: I believe that getConst return type should be Z3 (Base.AST a)+         instead. If Map.lookup returns nothing then we "panic" because+         an undefined constant, if Base.castAST returns nothing then we+         panic because of type mismatch. We have the duty to guarantee+         that none of these errors would ever happen.+          - Iago+-}+getConst :: forall a. Base.Z3Type a => Uniq -> Z3 (Maybe (Base.AST a))+getConst u = liftM mlookup (gets consts)+    where mlookup :: Map.IntMap AnyAST -> Maybe (Base.AST a)+          mlookup m = Map.lookup u m >>= \(AnyAST e) -> Base.castAST e++---------------------------------------------------------------------+-- Constructing expressions++-- | Declare skolem variables.+--+var :: forall a. IsTy a => Z3 (Expr a)+var = do+    ctx <- gets context+    (u, str) <- fresh+    smb <- mkStringSymbol_ ctx str+    (srt :: Base.Sort (TypeZ3 a)) <- Z3 . lift $ Base.mkSort ctx+    addConst u =<< mkConst_ ctx smb srt+    return $ Const u++-- | Make assertion in current context.+--+assert :: Expr Bool -> Z3 ()+assert = join . liftM2 assertCnstr_ (gets context) . compile++-- | Introduce an auxiliary declaration to name a given expression.+--+-- If you really want sharing use this instead of Haskell's /let/.+--+let_ :: IsScalar a => Expr a -> Z3 (Expr a)+let_ e = do+  aux <- var+  assert (aux ==* e)+  return aux++-- | Check current context.+--+check :: Z3 Base.Result+check = check_ =<< gets context++-- | Create a 'Base.AST' from a 'Expr'.+--+compile :: IsTy a => Expr a -> Z3 (Base.AST (TypeZ3 a))+compile (Lit a)+    = flip mkLiteral_ (toZ3Type a) =<< gets context+compile (Const u)+    = liftM (fromMaybe $ error uNDEFINED_CONST) $ getConst u+compile (Not b)+    = do ctx <- gets context+         b'  <- compile b+         mkNot_ ctx b'+compile (BoolBin op e1 e2)+    = do ctx <- gets context+         e1' <- compile e1+         e2' <- compile e2+         mkBoolBin_ ctx op e1' e2'+compile (BoolMulti op es)+    = do ctx <- gets context+         es' <- mapM compile es+         mkBoolMulti_ ctx op es'+compile (Neg e)+    = do ctx <- gets context+         e'  <- compile e+         mkUnaryMinus_ ctx e'+compile (CRingArith op es)+    = do ctx <- gets context+         es' <- mapM compile es+         mkCRingArith_ ctx op es'+compile (IntArith op e1 e2)+    = do ctx <- gets context+         e1' <- compile e1+         e2' <- compile e2+         mkIntArith_ ctx op e1' e2'+compile (RealArith op e1 e2)+    = do ctx <- gets context+         e1' <- compile e1+         e2' <- compile e2+         mkRealArith_ ctx op e1' e2'+compile (CmpE op e1 e2)+    = do ctx <- gets context+         e1' <- compile e1+         e2' <- compile e2+         mkEq_ ctx op e1' e2'+compile (CmpI op e1 e2)+    = do ctx <- gets context+         e1' <- compile e1+         e2' <- compile e2+         mkCmp_ ctx op e1' e2'+compile (Ite b e1 e2)+    = do ctx <- gets context+         b'  <- compile b+         e1' <- compile e1+         e2' <- compile e2+         mkIte_ ctx b' e1' e2'++---------------------------------------------------------------------+-- Internal lifted Base functions++assertCnstr_ :: Base.Context -> Base.AST Bool -> Z3 ()+assertCnstr_ ctx = Z3 . lift . Base.assertCnstr ctx++check_ :: Base.Context -> Z3 Base.Result+check_ = Z3 . lift . Base.check++mkStringSymbol_ :: Base.Context -> String -> Z3 Base.Symbol+mkStringSymbol_ ctx = Z3 . lift . Base.mkStringSymbol ctx++mkLiteral_ :: forall a. Base.Z3Scalar a => Base.Context -> a -> Z3 (Base.AST a)+mkLiteral_ ctx = Z3 . lift . Base.mkValue ctx++mkNot_ :: Base.Context -> Base.AST Bool -> Z3 (Base.AST Bool)+mkNot_ ctx = Z3 . lift . Base.mkNot ctx++mkBoolBin_ :: Base.Context -> BoolBinOp ->+    Base.AST Bool -> Base.AST Bool -> Z3 (Base.AST Bool)+mkBoolBin_ ctx Xor     b1 = Z3 . lift . Base.mkXor ctx b1+mkBoolBin_ ctx Implies b1 = Z3 . lift . Base.mkImplies ctx b1+mkBoolBin_ ctx Iff     b1 = Z3 . lift . Base.mkIff ctx b1++mkBoolMulti_ :: Base.Context -> BoolMultiOp ->+    [Base.AST Bool] -> Z3 (Base.AST Bool)+mkBoolMulti_ ctx And = Z3 . lift . Base.mkAnd ctx+mkBoolMulti_ ctx Or  = Z3 . lift . Base.mkAnd ctx++mkEq_ :: Base.Z3Scalar a => Base.Context -> CmpOpE ->+    Base.AST a -> Base.AST a -> Z3 (Base.AST Bool)+mkEq_ ctx Eq  e1 = Z3 . lift . Base.mkEq ctx e1+mkEq_ ctx Neq e1 = Z3 . lift . (Base.mkNot ctx <=< Base.mkEq ctx e1)++mkCmp_ :: Base.Z3Num a => Base.Context -> CmpOpI ->+    Base.AST a -> Base.AST a -> Z3 (Base.AST Bool)+mkCmp_ ctx Le e1 = Z3 . lift . Base.mkLe ctx e1+mkCmp_ ctx Lt e1 = Z3 . lift . Base.mkLt ctx e1+mkCmp_ ctx Ge e1 = Z3 . lift . Base.mkGe ctx e1+mkCmp_ ctx Gt e1 = Z3 . lift . Base.mkGt ctx e1++mkConst_ :: Base.Z3Type a => Base.Context+              -> Base.Symbol -> Base.Sort a -> Z3 (Base.AST a)+mkConst_ ctx smb = Z3 . lift . Base.mkConst ctx smb++mkUnaryMinus_ :: Base.Z3Num a => Base.Context -> Base.AST a -> Z3 (Base.AST a)+mkUnaryMinus_ ctx = Z3 . lift . Base.mkUnaryMinus ctx++mkCRingArith_ :: Base.Z3Num a => Base.Context+                    -> CRingOp -> [Base.AST a] -> Z3 (Base.AST a)+mkCRingArith_ ctx Add = Z3 . lift . Base.mkAdd ctx+mkCRingArith_ ctx Mul = Z3 . lift . Base.mkMul ctx+mkCRingArith_ ctx Sub = Z3 . lift . Base.mkSub ctx++mkIntArith_ :: Base.Context+                -> IntOp+                -> Base.AST Integer -> Base.AST Integer+                -> Z3 (Base.AST Integer)+mkIntArith_ ctx Quot e1 = Z3 . lift . Base.mkDiv ctx e1+mkIntArith_ ctx Mod  e1 = Z3 . lift . Base.mkMod ctx e1+mkIntArith_ ctx Rem  e1 = Z3 . lift . Base.mkRem ctx e1++mkRealArith_ :: Base.Context+                  -> RealOp+                  -> Base.AST Rational -> Base.AST Rational+                  -> Z3 (Base.AST Rational)+mkRealArith_ ctx Div e1 = Z3 . lift . Base.mkDiv ctx e1++mkIte_ :: Base.Context+            -> Base.AST Bool+            -> Base.AST a -> Base.AST a+            -> Z3 (Base.AST a)+mkIte_ ctx b e1 = Z3 . lift . Base.mkIte ctx b e1++---------------------------------------------------------------------+-- Error messages++uNDEFINED_CONST :: String+uNDEFINED_CONST = "Panic! Undefined constant or unexpected\+    \constant sort."
+ Z3/Types.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-}+++-- |+-- Module    : Z3.Types+-- 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>+++module Z3.Types (+    +    -- * Types+      TypeZ3+    , IsTy+    , IsScalar(..)++    -- ** Numeric types+    , IsNum+    , IsInt+    , IsReal++    ) where++import Z3.Base ( Z3Type, Z3Scalar, Z3Num )++import Data.Typeable ( Typeable )++----------------------------------------------------------------------+-- Types ++-- | Maps a type to the underlying Z3 type.+--+type family TypeZ3 a++type instance TypeZ3 Bool = Bool+type instance TypeZ3 Integer = Integer+type instance TypeZ3 Rational = Rational++-- | Types for expressions.+--+class (Typeable a, Z3Type (TypeZ3 a)) => IsTy a where++instance IsTy Bool where+instance IsTy Integer where+instance IsTy Rational where++-- | Scalar types.+--+class (Eq a, Show a, IsTy a, Z3Scalar(TypeZ3 a)) => IsScalar a where+  fromZ3Type :: TypeZ3 a -> a+  toZ3Type   :: a -> TypeZ3 a++instance IsScalar Bool where+  fromZ3Type = id+  toZ3Type = id++instance IsScalar Integer where+  fromZ3Type = id+  toZ3Type = id++instance IsScalar Rational where+  fromZ3Type = id+  toZ3Type = id++------------------------------------------------------------+-- Numeric types+--+-- Future Work: We would like to instance 'IsInt' with 'Int32' to provide+-- support for reasoning about 32-bit integer arithmetic with overflow.+-- It would be also interesting (but perhaps more tricky) to support+-- floating point arithmetic by creating an instance of 'IsReal' for+-- 'Double'.+--++-- | Numeric types.+--+class (IsScalar a, Num a, Z3Num (TypeZ3 a)) => IsNum a where+instance IsNum Integer where+instance IsNum Rational where++-- | Typeclass for Haskell Z3 numbers of /int/ sort in Z3.+--+class (IsNum a, Integral a, TypeZ3 a ~ Integer) => IsInt a where+instance IsInt Integer where++-- | Typeclass for Haskell Z3 numbers of /real/ sort in Z3.+--+class (IsNum a, Fractional a, Real a, TypeZ3 a ~ Rational) => IsReal a where+instance IsReal Rational where
+ z3.cabal view
@@ -0,0 +1,54 @@+Name:                z3+Version:             0.1.1+Synopsis:            Bindings for the Z3 Theorem Prover+Description:         +    Bindings for the Z3 Theorem Prover.+    .+    This package is still a work in progress. Low and medium-level bindings+    to the Z3 API are provided ("Z3.Base.C" and "Z3.Base") in the spirit+    of yices-painless. These APIs are still incomplete but usable.+    The high-level API ("Z3.Monad") is still very experimental.+    .+    More information about Z3:+    .+    * <http://research.microsoft.com/en-us/um/redmond/projects/z3/>+Homepage:            http://bitbucket.org/iago/z3-haskell+License:             BSD3+License-file:        LICENSE+Author:              Iago Abal <iago.abal@gmail.com>,+                     David Castro <david.castro.dcp@gmail.com>+Maintainer:          Iago Abal <iago.abal@gmail.com>,+                     David Castro <david.castro.dcp@gmail.com>+Copyright:           2012, Iago Abal, David Castro+Category:            Math, Theorem Provers, Formal Methods+Build-type:          Simple+Cabal-version:       >= 1.6++source-repository head+  type:     mercurial+  location: https://bitbucket.org/iago/z3-haskell++Library+    Exposed-modules: ++        Z3.Base+        Z3.Base.C ++        Z3.Exprs++        Z3.Monad++        Z3.Types++    Other-modules:+        +        Z3.Exprs.Internal++    ghc-options: -Wall++    Build-depends:       base > 3 && < 5, containers, mtl++    Build-tools:         hsc2hs+    Extensions:          ForeignFunctionInterface+    includes:            z3.h+    extra-libraries:     gomp z3 gomp