FuncModel.hs

-- | Extracting function and array interpretations.
module Example.Monad.FuncModel
  ( run )
  where

import Z3.Monad

run :: IO ()
run =
    do evalZ3 arrayScript >>= print
       evalZ3 funcScript >>= print

type RetType = ([([Integer], Integer)], Integer)

toIntsPair :: ([AST], AST) -> Z3 ([Integer], Integer)
toIntsPair (is, i) =
    do is' <- mapM getInt is
       i' <- getInt i
       return (is', i')

toRetType :: FuncModel -> Z3 RetType
toRetType (FuncModel fs elsePart) =
    do fs' <- mapM toIntsPair fs
       elsePart' <- getInt elsePart
       return (fs', elsePart')

-- * Arrays

-- FIXME: This script crashes when calling 'convertArr', which mysteriously now
-- returns 'Nothing'. It seems that 'isAsArray' is returning 'False' for 'a1'.
arrayScript :: Z3 (RetType, RetType)
arrayScript =
    do intSort <- mkIntSort
       arrSort <- mkArraySort intSort intSort

       a1Sym   <- mkStringSymbol "a1"
       a2Sym   <- mkStringSymbol "a2"

       a1      <- mkConst a1Sym arrSort
       a2      <- mkConst a2Sym arrSort


       i1      <- mkIntNum (5 :: Int)
       i2      <- mkIntNum (10 :: Int)
       a1Val1  <- mkSelect a1 i1
       mkGt a1Val1 i2 >>= assert

       i3      <- mkIntNum (42 :: Int)
       i4      <- mkIntNum (81 :: Int)
       a3      <- mkStore a1 i3 i4
       mkEq a2 a3 >>= assert

       let
           convertArr :: Model -> AST -> Z3 RetType
           convertArr model arr =
               do Just f <- evalArray model arr
                  toRetType f

       (_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"

-- * Functions

funcScript :: Z3 RetType
funcScript = do
  -- f :: (Integer,Integer) -> Integer
  intSort <- mkIntSort
  fDecl   <- mkFreshFuncDecl "f" [intSort, intSort] intSort

  -- f(5,10) > 42
  i5      <- mkIntNum (5 :: Integer)
  i10     <- mkIntNum (10 :: Integer)
  i42     <- mkIntNum (42 :: Integer)
  r       <- mkApp fDecl [i5, i10]
  assert =<< mkGt r i42

  -- check satisfiability and obtain model
  (res, mbModel) <- getModel
  case mbModel of
       Just model -> do
         Just f <- evalFunc model fDecl
         toRetType f
       Nothing -> error ("Couldn't construct model: " ++ show res)