Commits

Iago Abal committed 90e8595

Lifted function/array interpretations into Z3.Monad

Comments (0)

Files changed (1)

   , App
   , Pattern
   , Model
+  , FuncInterp
+  , FuncEntry
   , FuncModel(..)
 
   -- ** Satisfiability result
   , evalArray
   , showModel
   , showContext
+  , getFuncInterp
+  , isAsArray
+  , getAsArrayFuncDecl
+  , funcInterpGetNumEntries
+  , funcInterpGetEntry
+  , funcInterpGetElse
+  , funcInterpGetArity
+  , funcEntryGetValue
+  , funcEntryGetNumArgs
+  , funcEntryGetArg
 
   -- * Constraints
   , assertCnstr
   , App
   , Pattern
   , Model
+  , FuncInterp
+  , FuncEntry
   , FuncModel(..)
   , Result(..)
   , Logic(..)
 evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
 evalArray = liftFun2 Base.evalArray
 
+-- | 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.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>
+getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
+getFuncInterp = liftFun2 Base.getFuncInterp
+
+-- | 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 :: MonadZ3 z3 => AST -> z3 Bool
+isAsArray = liftFun1 Base.isAsArray
+
+-- | 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 :: MonadZ3 z3 => AST -> z3 FuncDecl
+getAsArrayFuncDecl = liftFun1 Base.getAsArrayFuncDecl
+
+-- | Return the number of entries in the given function interpretation.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>
+funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
+funcInterpGetNumEntries = liftFun1 Base.funcInterpGetNumEntries
+
+-- | Return a "point" of the given function intepretation.
+-- It represents the value of f in a particular point.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>
+funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
+funcInterpGetEntry = liftFun2 Base.funcInterpGetEntry
+
+-- | Return the 'else' value of the given function interpretation.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>
+funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
+funcInterpGetElse = liftFun1 Base.funcInterpGetElse
+
+-- | Return the arity (number of arguments) of the given function
+-- interpretation.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>
+funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
+funcInterpGetArity = liftFun1 Base.funcInterpGetArity
+
+-- | Return the value of this point.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>
+funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
+funcEntryGetValue = liftFun1 Base.funcEntryGetValue
+
+-- | Return the number of arguments in a Z3_func_entry object.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>
+funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
+funcEntryGetNumArgs = liftFun1 Base.funcEntryGetNumArgs
+
+-- | Return an argument of a Z3_func_entry object.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>
+funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
+funcEntryGetArg = liftFun2 Base.funcEntryGetArg
 
 ---------------------------------------------------------------------
 -- Constraints