Commits

em...@rice.edu  committed d1e837a

changes to support Z3 logics

  • Participants
  • Parent commits b00c47f

Comments (0)

Files changed (5)

     , App
     , Pattern
     , Model
+    , Params
+    , Solver
 
     -- ** Satisfiability result
     , Result(..)
     , push
     , pop
 
+
+    -- * Parameters
+    , mkParams
+    , paramsSetBool
+    , paramsSetUInt
+    , paramsSetDouble
+    , paramsSetSymbol
+    , paramsToString
+
+    -- * Solvers
+    , mkSolver
+    , mkSimpleSolver
+    , mkSolverForLogic
+    , solverSetParams
+    , solverPush
+    , solverPop
+    , solverReset
+    , solverAssertCnstr
+    , solverAssertAndTrack
+    , solverCheck
+    --, solverGetModel
+    , solverCheckAndGetModel
+    , solverGetReasonUnknown
     ) where
 
 import Z3.Base.C
 newtype Model = Model { unModel :: Ptr Z3_model }
     deriving Eq
 
+-- | A Z3 parameter set. Starting at Z3 4.0, parameter sets are used
+-- to configure many components such as: simplifiers, tactics,
+-- solvers, etc.
+newtype Params = Params { unParams :: Ptr Z3_params }
+    deriving Eq
+
+-- | A Z3 solver engine
+newtype Solver = Solver { unSolver :: Ptr Z3_solver }
+    deriving Eq
+
 -- | Result of a satisfiability check.
 data Result
     = Sat
 -- TODO Constraints: Z3_get_implied_equalities
 
 -- TODO From section 'Constraints' on.
+
+
+---------------------------------------------------------------------
+-- * Parameters
+
+mkParams :: Context -> IO Params
+mkParams c = Params <$> z3_mk_params (unContext c)
+
+paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
+paramsSetBool c params sym b =
+  z3_params_set_bool (unContext c) (unParams params) (unSymbol sym)
+                     (if b then z3_true else z3_false)
+
+paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()
+paramsSetUInt c params sym v =
+  z3_params_set_uint (unContext c) (unParams params) (unSymbol sym)
+                     (fromIntegral v)
+
+paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
+paramsSetDouble c params sym v =
+  z3_params_set_double (unContext c) (unParams params) (unSymbol sym)
+                       (realToFrac v)
+
+paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
+paramsSetSymbol c params sym v =
+  z3_params_set_symbol (unContext c) (unParams params) (unSymbol sym)
+                       (unSymbol v)
+
+paramsToString :: Context -> Params -> IO String
+paramsToString (Context c) (Params params) =
+  z3_params_to_string c params >>= peekCString
+
+
+---------------------------------------------------------------------
+-- * Solvers
+
+mkSolver :: Context -> IO Solver
+mkSolver c = Solver <$> z3_mk_solver (unContext c)
+
+mkSimpleSolver :: Context -> IO Solver
+mkSimpleSolver c = Solver <$> z3_mk_simple_solver (unContext c)
+
+mkSolverForLogic :: Context -> String -> IO Solver
+mkSolverForLogic c str =
+  do sym <- mkStringSymbol c str
+     Solver <$> z3_mk_solver_for_logic (unContext c) (unSymbol sym)
+
+solverSetParams :: Context -> Solver -> Params -> IO ()
+solverSetParams c solver params =
+  z3_solver_set_params (unContext c) (unSolver solver) (unParams params)
+
+solverPush :: Context -> Solver -> IO ()
+solverPush c solver = z3_solver_push (unContext c) (unSolver solver)
+
+solverPop :: Context -> Solver -> Int -> IO ()
+solverPop c solver i =
+  z3_solver_pop (unContext c) (unSolver solver) (fromIntegral i)
+
+solverReset :: Context -> Solver -> IO ()
+solverReset c solver = z3_solver_reset (unContext c) (unSolver solver)
+
+solverAssertCnstr :: Context -> Solver -> AST -> IO ()
+solverAssertCnstr c solver ast =
+  z3_solver_assert (unContext c) (unSolver solver) (unAST ast)
+
+solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
+solverAssertAndTrack c solver constraint var =
+  z3_solver_assert_and_track (unContext c) (unSolver solver)
+                             (unAST constraint) (unAST var)
+
+solverCheck :: Context -> Solver -> IO Result
+solverCheck c solver =
+  toResult <$> z3_solver_check (unContext c) (unSolver solver)
+
+solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)
+solverCheckAndGetModel (Context c) (Solver s) =
+  do res <- toResult <$> z3_solver_check c s
+     mmodel <- case res of
+                 Sat -> (Just . Model) <$> z3_solver_get_model c s
+                 _ -> return Nothing
+     return (res, mmodel)
+
+solverGetReasonUnknown :: Context -> Solver -> IO String
+solverGetReasonUnknown c solver =
+  z3_solver_get_reason_unknown (unContext c) (unSolver solver) >>= peekCString

File Z3/Base/C.hsc

 -- | A model for the constraints asserted into the logical context.
 data Z3_model
 
+-- | A solver for Z3, that is, an engine for collecting and solving
+-- constraints using a specific algorithm or set of algorithms.
+data Z3_solver
+     
+-- | A parameter set for Z3.
+data Z3_params
+     
 -- | Lifted Boolean type: false, undefined, true.
 type Z3_lbool = CInt
 
 
 
 -- TODO From section 'Constraints' on.
+
+
+---------------------------------------------------------------------
+-- * Parameters
+
+-- | Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter
+-- sets are used to configure many components such as: simplifiers,
+-- tactics, solvers, etc.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac7f883536538ab0ad234fde58988e673>
+--
+foreign import ccall unsafe "Z3_mk_params"
+    z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params)
+
+-- | Increment the reference counter of the given parameter set.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a91c9f749b89e1dcf1493177d395d0c>
+-- 
+foreign import ccall unsafe "Z3_params_inc_ref"
+    z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
+
+-- | Decrement the reference counter of the given parameter set.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae4df28ba713b81ee99abd929e32484ea>
+-- 
+foreign import ccall unsafe "Z3_params_dec_ref"
+    z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
+
+-- | Add a Boolean parameter k with value v to the parameter set p.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga39e3df967eaad45b343256d56c54e91c>
+-- 
+foreign import ccall unsafe "Z3_params_set_bool"
+    z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
+                          Z3_bool -> IO ()
+
+-- | Add an unsigned parameter k with value v to the parameter set p.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4974397cb652c7f7f479012eb465e250>
+-- 
+foreign import ccall unsafe "Z3_params_set_uint"
+    z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
+                          CUInt -> IO ()
+
+-- | Add a double parameter k with value v to the parameter set p.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga11498ce4b25d294f5f89ab7ac1b74c62>
+-- 
+foreign import ccall unsafe "Z3_params_set_double"
+    z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
+                            CDouble -> IO ()
+
+-- | Add a symbol parameter k with value v to the parameter set p.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac2e899a4906b6133a23fdb60ef992ec9>
+-- 
+foreign import ccall unsafe "Z3_params_set_symbol"
+    z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
+                            Ptr Z3_symbol -> IO ()
+
+-- | Convert a parameter set into a string. This function is mainly
+-- used for printing the contents of a parameter set.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga624e692e180a8b2f617156b1e1ae9722>
+-- 
+foreign import ccall unsafe "Z3_params_to_string"
+    z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string
+
+{-
+-- | Validate the parameter set p against the parameter description
+-- set d.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ae64e7f89201589424191a9b824d3ca>
+-- 
+foreign import ccall unsafe "Z3_params_validate"
+    z3_params_validate :: Ptr Z3_context -> Ptr Z3_params ->  Z3_param_descrs -> IO ()
+-}
+
+---------------------------------------------------------------------
+-- * Solvers
+
+-- | Create an SMT solver that uses a set of builtin tactics.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c>
+--
+foreign import ccall unsafe "Z3_mk_solver"
+    z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
+
+-- | Create a simple solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c>
+--
+foreign import ccall unsafe "Z3_mk_simple_solver"
+    z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
+
+-- | Create a solver for a particular logic, as given by the SMTLIB
+-- standard here:
+--
+-- <http://smtlib.cs.uiowa.edu/logics.html>
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga54244cfc9d9cd2ca8f08c3909d700628>
+--
+foreign import ccall unsafe "Z3_mk_solver_for_logic"
+    z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver)
+
+-- | Set the parameters for a solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga887441b3468a1bc605bbf564ddebf2ae>
+--
+foreign import ccall unsafe "Z3_solver_set_params"
+    z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params ->
+                            IO ()
+
+-- | Increment the reference counter of the given solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga388e25a8b477abbd49f08c6c29dfa12d>
+foreign import ccall unsafe "Z3_solver_inc_ref"
+    z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
+ 
+-- | Decrement the reference counter of the given solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2362dcef4e9b8ede41298a50428902ff>
+foreign import ccall unsafe "Z3_solver_dec_ref"
+    z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
+ 
+-- | Create a backtracking point in a solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae41bebe15b1b1105f9abb8690188d1e2>
+--
+foreign import ccall unsafe "Z3_solver_push"
+    z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
+
+-- | Backtrack to the nth-most recent backtracking point.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40aa98e15aceffa5be3afad2e065478a>
+--
+foreign import ccall unsafe "Z3_solver_pop"
+    z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO ()
+
+-- | Remove all assertions from a solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4a4a215b9130d7980e3c393fe857335f>
+--
+foreign import ccall unsafe "Z3_solver_reset"
+    z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
+
+-- | Add a constraint to a solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72afadf5e8b216f2c6ae675e872b8be4>
+--
+foreign import ccall unsafe "Z3_solver_assert"
+    z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO ()
+
+-- | Add a constraint to a solver and track it using a Boolean
+-- constant, given as the last argument.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46fb6f3aa3ef451d6be01a737697810>
+--
+foreign import ccall unsafe "Z3_solver_assert_and_track"
+    z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver ->
+                                  Ptr Z3_ast -> Ptr Z3_ast -> IO ()
+
+-- | Check whether the assertions in a given solver are consistent.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga000e369de7b71caa4ee701089709c526>
+--
+foreign import ccall unsafe "Z3_solver_check"
+    z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool
+
+-- | Retrieve the model for the last call to Z3_solver_check or
+-- Z3_solver_check_assumptions on the given solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf14a54d904a7e45eecc00c5fb8a9d5c9>
+--
+foreign import ccall unsafe "Z3_solver_get_model"
+    z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model)
+
+-- | Return a brief justification for an "unknown" result (i.e.,
+-- Z3_L_UNDEF) for the last call to Z3_solver_check or
+-- Z3_solver_check_assumptions on the given solver.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaed5d19000004b43dd75e487682e91b55>
+--
+foreign import ccall unsafe "Z3_solver_get_reason_unknown"
+    z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver ->
+                                    IO Z3_string

File Z3/Lang/Monad.hs

     , evalZ3
     , Args(..)
     , stdArgs
+    , Z3Logic(..)
     , evalZ3With
     , fresh
     , deBruijnIx
 
 import qualified Z3.Base as Base
 
-import Control.Applicative ( Applicative )
+import Control.Applicative ( Applicative, (<$>) )
 import Control.Monad.State
 import Data.Traversable ( traverse )
 
 data Z3State
     = Z3State { uniqVal :: !Uniq
               , context :: Base.Context
+              , solver :: Maybe Base.Solver
               , qLayout :: !Layout
               }
 
 --    Base.setParamValue cfg "WARNING" "false"
     iniConfig cfg args
     Base.withContext cfg $ \ctx ->
-      evalStateT s Z3State { uniqVal = 0
-                           , context = ctx
-                           , qLayout = 0
-                           }
+      do msolver <- case logicName args of
+                      Just l ->
+                        Just <$> Base.mkSolverForLogic ctx (z3logic2String l)
+                      _ -> return Nothing
+         evalStateT s Z3State { uniqVal = 0
+                              , context = ctx
+                              , solver = msolver
+                              , qLayout = 0
+                              }
 
 -- | Fresh symbol name.
 --
     return (uniqVal st, 'v':show i)
 
 -------------------------------------------------
+-- Solvers available in Z3
+--
+-- NOTE: These are described at http://smtlib.cs.uiowa.edu/logics.html
+
+data Z3Logic
+  = Logic_AUFLIA
+    -- ^ Closed formulas over the theory of linear integer arithmetic
+    -- and arrays extended with free sort and function symbols but
+    -- restricted to arrays with integer indices and values.
+
+  | Logic_AUFLIRA
+    -- ^ Closed linear formulas with free sort and function symbols over
+    -- one- and two-dimentional arrays of integer index and real
+    -- value.
+
+  | Logic_AUFNIRA
+    -- ^ Closed formulas with free function and predicate symbols over a
+    -- theory of arrays of arrays of integer index and real value.
+
+  | Logic_LRA
+    -- ^ Closed linear formulas in linear real arithmetic.
+
+  | Logic_QF_ABV
+    -- ^ Closed quantifier-free formulas over the theory of bitvectors
+    -- and bitvector arrays.
+
+  | Logic_QF_AUFBV
+    -- ^ Closed quantifier-free formulas over the theory of bitvectors
+    -- and bitvector arrays extended with free sort and function
+    -- symbols.
+
+  | Logic_QF_AUFLIA
+    -- ^ Closed quantifier-free linear formulas over the theory of
+    -- integer arrays extended with free sort and function symbols.
+
+  | Logic_QF_AX
+    -- ^ Closed quantifier-free formulas over the theory of arrays with
+    -- extensionality.
+
+  | Logic_QF_BV
+    -- ^ Closed quantifier-free formulas over the theory of fixed-size
+    -- bitvectors.
+
+  | Logic_QF_IDL
+    -- ^ Difference Logic over the integers. In essence, Boolean
+    -- combinations of inequations of the form x - y < b where x and y
+    -- are integer variables and b is an integer constant.
+
+  | Logic_QF_LIA
+    -- ^ Unquantified linear integer arithmetic. In essence, Boolean
+    -- combinations of inequations between linear polynomials over
+    -- integer variables.
+
+  | Logic_QF_LRA
+    -- ^ Unquantified linear real arithmetic. In essence, Boolean
+    -- combinations of inequations between linear polynomials over
+    -- real variables.
+
+  | Logic_QF_NIA
+    -- ^ Quantifier-free integer arithmetic.
+
+  | Logic_QF_NRA
+    -- ^ Quantifier-free real arithmetic.
+
+  | Logic_QF_RDL
+    -- ^ Difference Logic over the reals. In essence, Boolean
+    -- combinations of inequations of the form x - y < b where x and y
+    -- are real variables and b is a rational constant.
+
+  | Logic_QF_UF
+    -- ^ Unquantified formulas built over a signature of uninterpreted
+    -- (i.e., free) sort and function symbols.
+
+  | Logic_QF_UFBV
+    -- ^ Unquantified formulas over bitvectors with uninterpreted sort
+    -- function and symbols.
+
+  | Logic_QF_UFIDL
+    -- ^ Difference Logic over the integers (in essence) but with
+    -- uninterpreted sort and function symbols.
+
+  | Logic_QF_UFLIA
+    -- ^ Unquantified linear integer arithmetic with uninterpreted sort
+    -- and function symbols.
+
+  | Logic_QF_UFLRA
+    -- ^ Unquantified linear real arithmetic with uninterpreted sort and
+    -- function symbols.
+
+  | Logic_QF_UFNRA
+    -- ^ Unquantified non-linear real arithmetic with uninterpreted sort
+    -- and function symbols.
+
+  | Logic_UFLRA
+    -- ^ Linear real arithmetic with uninterpreted sort and function
+    -- symbols.
+
+  | Logic_UFNIA
+    -- ^ Non-linear integer arithmetic with uninterpreted sort and
+    -- function symbols.
+
+z3logic2String :: Z3Logic -> String
+z3logic2String Logic_AUFLIA = "AUFLIA"
+z3logic2String Logic_AUFLIRA = "AUFLIRA"
+z3logic2String Logic_AUFNIRA = "AUFNIRA"
+z3logic2String Logic_LRA = "LRA"
+z3logic2String Logic_QF_ABV = "QF_ABV"
+z3logic2String Logic_QF_AUFBV = "QF_AUFBV"
+z3logic2String Logic_QF_AUFLIA = "QF_AUFLIA"
+z3logic2String Logic_QF_AX = "QF_AX"
+z3logic2String Logic_QF_BV = "QF_BV"
+z3logic2String Logic_QF_IDL = "QF_IDL"
+z3logic2String Logic_QF_LIA = "QF_LIA"
+z3logic2String Logic_QF_LRA = "QF_LRA"
+z3logic2String Logic_QF_NIA = "QF_NIA"
+z3logic2String Logic_QF_NRA = "QF_NRA"
+z3logic2String Logic_QF_RDL = "QF_RDL"
+z3logic2String Logic_QF_UF = "QF_UF"
+z3logic2String Logic_QF_UFBV = "QF_UFBV"
+z3logic2String Logic_QF_UFIDL = "QF_UFIDL"
+z3logic2String Logic_QF_UFLIA = "QF_UFLIA"
+z3logic2String Logic_QF_UFLRA = "QF_UFLRA"
+z3logic2String Logic_QF_UFNRA = "QF_UFNRA"
+z3logic2String Logic_UFLRA = "UFLRA"
+z3logic2String Logic_UFNIA = "UFNIA"
+
+
+-------------------------------------------------
 -- Arguments
 
 data Args
   = Args {
       softTimeout :: Maybe Int
         -- ^ soft timeout (in milliseconds)
+      , logicName :: Maybe Z3Logic
+        -- ^ an optional name for the logic to use; logic names are
+        -- described at <http://smtlib.cs.uiowa.edu/logics.html>
     }
 
 stdArgs :: Args
 stdArgs
   = Args {
-      softTimeout = Nothing
+      softTimeout = Nothing,
+      logicName = Nothing
     }
 
 iniConfig :: Base.Config -> Args -> IO ()
 liftZ3Op5 :: (Base.Context -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d -> Z3 e
 liftZ3Op5 f a b c d = gets context >>= \ctx -> liftZ3 (f ctx a b c d)
 
+liftZ3SolverOp :: (Base.Context -> Base.Solver -> IO b) ->
+                  (Base.Context -> IO b) -> Z3 b
+liftZ3SolverOp f_s f_no_s =
+  do ctx <- gets context
+     maybe_solver <- gets solver
+     case maybe_solver of
+       Just solver -> liftZ3 (f_s ctx solver)
+       Nothing -> liftZ3 (f_no_s ctx)
+
+liftZ3SolverOp2 :: (Base.Context -> Base.Solver -> a -> IO b) ->
+                   (Base.Context -> a -> IO b) -> a -> Z3 b
+liftZ3SolverOp2 f_s f_no_s a =
+  liftZ3SolverOp (\c s -> f_s c s a) (\c -> f_no_s c a)
+
 assertCnstr :: Base.AST -> Z3 ()
-assertCnstr = liftZ3Op2 Base.assertCnstr
+assertCnstr = liftZ3SolverOp2 Base.solverAssertCnstr Base.assertCnstr
 
 -- | Check satisfiability.
 check :: Z3 Base.Result
-check = liftZ3Op Base.check
+check = liftZ3SolverOp Base.solverCheck Base.check
 
 eval :: Base.Model -> Base.AST -> Z3 (Maybe Base.AST)
 eval = liftZ3Op3 Base.eval
 getBool = liftZ3Op2 Base.getBool
 
 push :: Z3 ()
-push = liftZ3Op Base.push
+push = liftZ3SolverOp Base.solverPush Base.push
 
 pop :: Int -> Z3 ()
-pop = liftZ3Op2 Base.pop
+pop = liftZ3SolverOp2 Base.solverPop Base.pop
 
 getInt :: Base.AST -> Z3 Integer
 getInt = liftZ3Op2 Base.getInt
 getReal = liftZ3Op2 Base.getReal
 
 getModel :: Z3 (Base.Result, Maybe Base.Model)
-getModel = liftZ3Op Base.getModel
+getModel = liftZ3SolverOp Base.solverCheckAndGetModel Base.getModel
 
 delModel :: Base.Model -> Z3 ()
 delModel = liftZ3Op2 Base.delModel

File Z3/Lang/Prelude.hs

     , evalZ3
     , Args(..)
     , stdArgs
+    , Z3Logic(..)
     , evalZ3With
 
     -- ** Commands
 -- Options
 
 -- | Configuration option.
-data Opt = Opt String  -- ^ id
-               String  -- ^ value
+data Opt = Opt String  -- id
+               String  -- value
 
 -- | Set an option.
 setOpt :: Base.Config -> Opt -> IO ()