Commits

Iago Abal committed 4d5bc01

Many documentation fixes

Comments (0)

Files changed (6)

 -- Maintainer: Iago Abal <iago.abal@gmail.com>,
 --             David Castro <david.castro.dcp@gmail.com>
 --
--- Medium-level bindings.
+-- Low-level bindings to Z3 API.
 
+-- TODO Rename showModel and showContext to match Z3 C API names.
 module Z3.Base (
 
     -- * Types
 ---------------------------------------------------------------------
 -- Constraints
 
+-- | Create a backtracking point.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad651ad68c7a060cbb5616349233cb10f>
 push :: Context -> IO ()
 push c = checkError c $ z3_push $ unContext c
 
+-- | Backtrack /n/ backtracking points.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab2b3a542006c86c8d86dc37872f88b61>
 pop :: Context -> Int -> IO ()
 pop ctx cnt = checkError ctx $ z3_pop (unContext ctx) $ fromIntegral cnt
 
 delModel :: Context -> Model -> IO ()
 delModel c m = checkError c $ z3_del_model (unContext c) (unModel m)
 
+-- | Convert the given model into a string.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>
 showModel :: Context -> Model -> IO String
 showModel c m = checkError c $ z3_model_to_string (unContext c) (unModel m) >>= peekCString
 
+-- | Convert the given logical context into a string.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216>
 showContext :: Context -> IO String
 showContext c = checkError c $ z3_context_to_string (unContext c) >>= peekCString
 
 
 -- | Solvers available in Z3.
 --
--- NB: These are described at http://smtlib.cs.uiowa.edu/logics.html
+-- These are described at <http://smtlib.cs.uiowa.edu/logics.html>
+--
+-- /WARNING/: Support for solvers is fragile, you may experience segmentation
+-- faults!
 data Logic
   = AUFLIA
     -- ^ Closed formulas over the theory of linear integer arithmetic
       Compilable(..)
     , IsTy(..)
     , IsFun(..)
+    , Castable(..)
 
     -- ** Numeric types
     , IsNum
     , Pattern (..)
     , Quantifier(..)
     , QExpr(..)
-    , Castable(..)
     , FunApp (..)
     , BoolBinOp (..)
     , BoolMultiOp (..)
 -- | Quantifier layout level.
 type Layout = Int
 
--- | Abstract syntax.
+-- | Expressions.
 data Expr :: * -> * where
   --  | Literals
   Lit :: IsTy a => a -> Expr a
   --  | Casting between compatible types
   Cast :: (IsTy a, IsTy b, Castable a b) => Expr a -> Expr b
 
+-- | Quantifiable expressions.
 class QExpr t where
   compileQuant :: Quantifier -> [Base.Symbol] -> [Base.Sort] -> t -> Z3 Base.AST
 
-class Castable a b where
+-- | Convertible types.
 class (IsTy a, IsTy b) => Castable a b where
   compileCast :: TY (a,b) -> Base.AST -> Z3 Base.AST
 
     ,  softTimeout :: Maybe Int
         -- ^ soft timeout (in milliseconds)
     , options      :: Opts
+        -- ^ Z3 options
     }
 
 stdArgs :: Args

Z3/Lang/Prelude.hs

     , IsNum
     , IsInt
     , IsReal
+    , Castable
     , literal
     , true
     , false
     , iff, (<=>)
     , forall
     , exists
-    , cast
     , instanceWhen
     , (//), (%*), (%%)
     , divides
     , (>=*), (>*)
     , min_, max_
     , ite
+    , cast
 
     ) where
 
 ----------------------------------------------------------------------
 -- Models
 
+-- | A computation derived from a model.
 newtype Model a = Model { unModel :: ReaderT Base.Model Z3 a }
     deriving (Applicative,Functor,Monad)
 
 checkModel = checkModelWith (const id)
 {-# INLINE checkModel #-}
 
+-- | Check satisfiability and evaluate a model if some exists.
 checkModelWith :: (Result -> Maybe a -> b) -> Model a -> Z3 b
 checkModelWith f m = uncurry f <$> checkModelWithResult m
 {-# INLINE checkModelWith #-}
 checkModelWithResult :: Model a -> Z3 (Result, Maybe a)
 checkModelWithResult m = MonadZ3.withModel $ runReaderT (unModel m)
 
+-- | Show Z3's internal model.
 showModel :: Model String
 showModel = Model $ ask >>= lift . MonadZ3.showModel
 
+-- | Evaluate an expression within a model.
 eval :: forall a. IsTy a => Expr a -> Model a
 eval e = Model $ do
   a <- lift $ compileWithTCC e
         peek (Just a) = getValue a
         peek Nothing  = error "Z3.Lang.Prelude.eval: quantified expression or partial model!"
 
+-- | Evaluate a collection of expressions within a model.
 evalT :: (IsTy a,Traversable t) => t (Expr a) -> Model (t a)
 evalT = T.traverse eval
 
 ---------------------------------------------------------------------
 -- Constraints
 
+-- | Create a backtracking point.
 push :: MonadZ3 z3 => z3 ()
 push = liftSolver0 Base.solverPush Base.push
 
+-- | Backtrack /n/ backtracking points.
 pop :: MonadZ3 z3 => Int -> z3 ()
 pop = liftSolver1 Base.solverPop Base.pop
 
  void $ T.traverse delModel mb_m
  return (r, mb_e)
 
+-- | Convert the given model into a string.
 showModel :: MonadZ3 z3 => Model -> z3 String
 showModel = liftFun1 Base.showModel
 
+-- | Convert Z3's logical context into a string.
 showContext :: MonadZ3 z3 => z3 String
 showContext = liftScalar Base.showContext
 
 -- | 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 :: MonadZ3 z3 => z3 Result
 check = liftSolver0 Base.solverCheck Base.check
 
 Version:             0.3.0
 Synopsis:            Bindings for the Z3 Theorem Prover
 Description:
-    Bindings for the Z3 Theorem Prover.
+    Bindings for the Z3 Theorem Prover (<http://z3.codeplex.com>).
     .
-    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.Lang") is still very experimental and likely to change.
+    Low-level bindings to the Z3 API are provided by "Z3.Base", this API is
+    still incomplete but pretty much stable.
     .
-    Installation (Unix-like): Just be sure to use the standard locations for
-    dynamic libraries (\/usr\/lib) and header files (\/usr\/include), or else use
-    the appropriate Cabal flags.
+    A simple but convenient wrapper for "Z3.Base" is provided by "Z3.Monad".
     .
-    Haddock documentation: <http://www.iagoabal.eu/z3-haskell/doc>
+    The "Z3.Lang" API provides a high-level interface to Z3, but it is still
+    very experimental and likely to change.
     .
-    More information about Z3:
+    Important notes:
     .
-    * <http://z3.codeplex.com>
+    * Installation (Unix-like): Just be sure to use the standard locations for
+    dynamic libraries (\/usr\/lib) and header files (\/usr\/include), or else
+    use the --extra-lib-dirs and --extra-include-dirs Cabal flags.
+    .
+    * Hackage fails to compile this package because of the z3 dependency.
+    .
+    * Haddock documentation can be found at
+    <http://www.iagoabal.eu/z3-haskell/doc/0.3.0>
 Homepage:            http://bitbucket.org/iago/z3-haskell
 License:             BSD3
 License-file:        LICENSE