Commits

Scott West committed 078bb08

Adding array evaluation.

Evaluation of the array is done by converting an evaluated array
into a function interpretation, then using the function interpretation
extraction mechanism.

The example has been updated to contain a small use of each. Although
not a full practical example, it can serve as a simple test and showing
how they can be used.

Comments (0)

Files changed (5)

     , eval
     , evalT
     , evalFunc
+    , evalArray
     , showModel
     , showContext
 
 evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
 evalT c m = fmap T.sequence . T.mapM (eval c m)
 
+-- | Evaluate a function declaration to a list of argument/value pairs.
+evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe [([AST], AST)])
+evalFunc ctx m fDecl =
+    do interpMb <- getFuncInterp ctx m fDecl
+       case interpMb of
+         Nothing -> return Nothing
+         Just interp -> Just <$> getMapFromInterp ctx interp
 
-evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe [([AST], AST)])
-evalFunc ctx m fDecl
-    = do interpMb <- getFuncInterp ctx m fDecl
-         case interpMb of
-           Nothing -> return Nothing
-           Just interp -> Just <$> getMapFromInterp ctx interp
+-- | Evaluate an array as a function, if possible.
+evalArray :: Context -> Model -> AST -> IO (Maybe [([AST], AST)])
+evalArray ctx model array =
+    do -- The array must first be evaluated normally, to get it into 
+       -- 'as-array' form, which is required to acquire the FuncDecl.
+       evaldArrayMb <- eval ctx model array
+       case evaldArrayMb of
+         Nothing -> return Nothing
+         Just evaldArray ->
+             do canConvert <- isAsArray ctx evaldArray
+                if canConvert
+                  then 
+                    do arrayDecl <- getAsArrayFuncDecl ctx evaldArray
+                       evalFunc ctx model arrayDecl
+                  else return Nothing
+       
+
+-- | Return the function declaration f associated with a (_ as_array f) node.
+-- 
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>
+getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
+getAsArrayFuncDecl ctx a =
+    FuncDecl <$> z3_get_as_array_func_decl (unContext ctx) (unAST a)
+
+-- | The (_ as-array f) AST node is a construct for assigning interpretations for 
+-- arrays in Z3. It is the array such that forall indices i we have that 
+-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE if 
+-- the a is an as-array AST node.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>
+isAsArray :: Context -> AST -> IO Bool
+isAsArray ctx a = toBool <$> z3_is_as_array (unContext ctx) (unAST a)
+    
 
 getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)]
 getMapFromInterp ctx interp =
             -> Ptr (Ptr Z3_ast)
             -> IO Z3_bool
 
+-- | The (_ as-array f) AST node is a construct for assigning interpretations for 
+-- arrays in Z3. It is the array such that forall indices i we have that 
+-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE if 
+-- the a is an as-array AST node.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>
+foreign import ccall unsafe "Z3_is_as_array"
+    z3_is_as_array :: Ptr Z3_context
+                   -> Ptr Z3_ast
+                   -> IO Z3_bool
+ 	
+-- | Return the function declaration f associated with a (_ as_array f) node.
+-- 
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>
+foreign import ccall unsafe "Z3_get_as_array_func_decl"
+    z3_get_as_array_func_decl :: Ptr Z3_context
+                              -> Ptr Z3_ast
+                              -> IO (Ptr Z3_func_decl)
+
 -- | Return the interpretation of the function f in the model m. 
 -- Return NULL, if the model does not assign an interpretation for f. 
 -- That should be interpreted as: the f does not matter.
   , eval
   , evalT
   , evalFunc
+  , evalArray
   , showModel
   , showContext
 
 evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe [([AST], AST)])
 evalFunc = liftFun2 Base.evalFunc
 
+-- | Get array as a list of argument/value pairs, if it is
+-- represented as a function (ie, using as-array).
+evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe [([AST], AST)])
+evalArray = liftFun2 Base.evalArray
+
+
 ---------------------------------------------------------------------
 -- Constraints
 

examples/monad/func_and_array.hs

+module Main where
+
+import Z3.Monad
+
+type RetType = [([Integer], Integer)]
+
+toIntsPair :: ([AST], AST) -> Z3 ([Integer], Integer)
+toIntsPair (is, i) =
+    do is' <- mapM getInt is
+       i' <- getInt i
+       return (is', i')
+
+arrayScript :: Z3 (RetType, RetType)  -- Map (Int, Int) Int)
+arrayScript =
+    do intSort <- mkIntSort
+       arrSort <- mkArraySort intSort intSort
+
+       a1Sym   <- mkStringSymbol "a1"
+       a2Sym   <- mkStringSymbol "a2"
+
+       a1      <- mkConst a1Sym arrSort
+       a2      <- mkConst a2Sym arrSort
+
+       
+       i1      <- mkInt (5 :: Int)
+       i2      <- mkInt (10 :: Int)
+       a1Val1  <- mkSelect a1 i1
+       mkGt a1Val1 i2 >>= assertCnstr
+
+       i3      <- mkInt (42 :: Int)
+       i4      <- mkInt (81 :: Int)
+       a3      <- mkStore a1 i3 i4
+       mkEq a2 a3 >>= assertCnstr
+
+       let 
+           convertArr :: Model -> AST -> Z3 RetType
+           convertArr model arr = 
+               do Just fs <- evalArray model arr
+                  mapM toIntsPair fs
+
+       (_res, modelMb) <- getModel
+       case modelMb of
+         Just model -> 
+             do a1' <- convertArr model a1
+                a2' <- convertArr model a2
+                return (a1', a2')
+         Nothing -> error "Couldn't construct model"
+
+
+
+funcScript :: Z3 RetType
+funcScript =
+    do intSort <- mkIntSort
+       fSym    <- mkStringSymbol "f"
+       fDecl   <- mkFuncDecl fSym [intSort, intSort] intSort
+
+       i1      <- mkInt (5 :: Int)
+       i2      <- mkInt (10 :: Int)
+       i3      <- mkInt (42 :: Int)
+
+       v       <- mkApp fDecl [i1, i2]
+
+       mkGt v i3 >>= assertCnstr
+       (_res, modelMb) <- getModel
+       case modelMb of
+         Just model -> 
+             do Just fs <- evalFunc model fDecl
+                mapM toIntsPair fs
+         Nothing -> error "Couldn't construct model"
+
+main :: IO ()
+main = 
+    do evalZ3 arrayScript >>= print
+       evalZ3 funcScript >>= print

examples/monad/funcinterp.hs

-module Main where
-
-import Control.Applicative
-import Control.Monad ( join )
-import Control.Monad.Trans
-
-import Data.Maybe
-
-import Z3.Monad
-
-
-script :: Z3 [([Integer], Integer)] -- Map (Int, Int) Int)
-script =
-    do intSort <- mkIntSort
-       fSym    <- mkStringSymbol "f"
-       fDecl   <- mkFuncDecl fSym [intSort, intSort] intSort
-
-       i1      <- mkInt 5
-       i2      <- mkInt 10
-       i3      <- mkInt 42
-
-       v       <- mkApp fDecl [i1, i2]
-
-       mkGt v i3 >>= assertCnstr
-       (_res, modelMb) <- getModel
-       case modelMb of
-         Just model -> 
-             do Just fs <- evalFunc model fDecl
-                let toIntsPair (is, i) =
-                        do is' <- mapM getInt is
-                           i' <- getInt i
-                           return (is', i')
-                mapM toIntsPair fs
-         Nothing -> error "Couldn't construct model"
-
-main = evalZ3 script >>= print