Commits

Scott West committed eced0cf

Adding else part and datatype for function models.

The new datatype rolls together the map and else part of a function model.

Comments (0)

Files changed (3)

     , getReal
 
     -- * Models
+    , FuncModel (..)
     , eval
     , evalT
     , evalFunc
 evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
 evalT c m = fmap T.sequence . T.mapM (eval c m)
 
+-- | The interpretation of a function is a mapping part (arguments to values)
+-- and an 'else' part.
+data FuncModel = FuncModel
+    { interpMap :: [([AST], AST)]
+    , interpElse :: AST
+    }
+
 -- | Evaluate a function declaration to a list of argument/value pairs.
-evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe [([AST], AST)])
+evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
 evalFunc ctx m fDecl =
     do interpMb <- getFuncInterp ctx m fDecl
        case interpMb of
          Nothing -> return Nothing
-         Just interp -> Just <$> getMapFromInterp ctx interp
+         Just interp ->
+             do funcMap  <- getMapFromInterp ctx interp
+                elsePart <- funcInterpGetElse ctx interp
+                return (Just $ FuncModel funcMap elsePart)
 
 -- | Evaluate an array as a function, if possible.
-evalArray :: Context -> Model -> AST -> IO (Maybe [([AST], AST)])
+evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
 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.
   , App
   , Pattern
   , Model
+  , FuncModel(..)
 
   -- ** Satisfiability result
   , Result(..)
   , App
   , Pattern
   , Model
+  , FuncModel(..)
   , Result(..)
   , Logic(..)
   , ASTPrintMode(..)
 evalT = liftFun2 Base.evalT
 
 -- | Get function as a list of argument/value pairs.
-evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe [([AST], AST)])
+evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
 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 :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
 evalArray = liftFun2 Base.evalArray
 
 

examples/monad/func_and_array.hs

 
 import Z3.Monad
 
-type RetType = [([Integer], Integer)]
+type RetType = ([([Integer], Integer)], Integer)
 
 toIntsPair :: ([AST], AST) -> Z3 ([Integer], Integer)
 toIntsPair (is, i) =
        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')
+
 arrayScript :: Z3 (RetType, RetType)  -- Map (Int, Int) Int)
 arrayScript =
     do intSort <- mkIntSort
        let 
            convertArr :: Model -> AST -> Z3 RetType
            convertArr model arr = 
-               do Just fs <- evalArray model arr
-                  mapM toIntsPair fs
+               do Just f <- evalArray model arr
+                  toRetType f
 
        (_res, modelMb) <- getModel
        case modelMb of
        (_res, modelMb) <- getModel
        case modelMb of
          Just model -> 
-             do Just fs <- evalFunc model fDecl
-                mapM toIntsPair fs
+             do Just f <- evalFunc model fDecl
+                toRetType f
          Nothing -> error "Couldn't construct model"
 
 main :: IO ()