{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- |
-- Module : Yices.Painless.Base
-- Copyright : (c) Galois, Inc. 2010
-- License : BSD3
-- Maintainer: Don Stewart <dons@galois.com>
-- Stability : stable
--
-- Medium level bindings to the Yices SMT solver. This layer provides an
-- imperative, native Haskell interface to Yices.
--
-- For the pure, embedded
-- language, use "Yices.Painless.Language".
--
-- Documentation in this module is based on quotations from the C API documentation.
--
-- In contrast to the low level API provided by "Yices.Painless.Base.C", this
-- interface adds:
--
-- * Increased improved type checking;
--
-- * Automatic resource management;
--
-- * Lazy lists instead of imperative iterators;
--
-- * Thread safe resource access;
--
-- * Checking for semantic errors.
--
module Yices.Painless.Base (
-- * Core Yices types
Context,
Expr,
Model,
Type,
Decl,
-- ** Utility types
Result(..),
Assert, Weight, Cost,
-- * Yices Types and Values
-- ** Literals
mkTrue, mkFalse,
mkNum, mkNumFromString,
-- ** Variables
mkBool,
mkFreshBool,
mkBoolDecl,
-- ** Declarations
getDecl,
getVarDeclFromName,
mkVarDecl,
mkVarFromDecl,
-- ** Logical operators
mkNot,
mkOr, mkAnd,
mkEq, mkNeq,
mkIte,
-- ** Expressions
-- ** Types
mkType,
mkFunctionType,
mkBitVectorType,
-- ** Functions
mkApp,
mkSum, mkSub, mkMul,
mkLt, mkLe,
mkGt, mkGe,
-- ** Bit vectors
mkBVConstant,
mkBVConstantFromVector,
-- *** Arithmetic
mkBVAdd, mkBVSub, mkBVMul, mkBVMinus,
-- *** Strings
mkBVConcat, mkBVExtract,
-- *** Logical
mkBVAnd, mkBVOr, mkBVXor,
mkBVNot,
-- *** Shifting
mkBVSignExtend,
mkBVShiftLeft0, mkBVShiftLeft1,
mkBVShiftRight0, mkBVShiftRight1,
-- *** Comparisons
mkBVLt, mkBVLe,
mkBVGt, mkBVGe,
mkBVSlt, mkBVSle,
mkBVSgt, mkBVSge,
-- *** IO
ppExpr,
-- * System Information
version,
-- * Configuration
setVerbosity,
setMaxNumConflictsInMaxSatIteration,
setTypeChecker,
setMaxNumIterationsInMaxSat,
setMaxSatInitialCost,
setArithmeticOnly,
setLogFile,
-- * Making assertions
assert,
assertWeighted,
assertRetractable,
retract,
-- * Finding solutions
inconsistent,
check,
maxSat, maxSatCost,
findWeightedModel,
evalInModel,
getModel,
display,
getCost, getCostDouble,
-- * Manipulating contexts
mkContext,
ctxReset,
ctxDump,
ctxPush,
ctxPop,
getDecls,
-- * Queries
-- ** Extracting values
YValue(..),
-- ** Extracting via types
getValueBool,
getValueInt,
getValueRational,
getValueDouble,
getValueBitVector,
getAssertValue,
-- ** Queries on cores
getUnsatCoreSize,
getUnsatCore,
) where
import Yices.Painless.Base.C
import Foreign
import Foreign.C.String
import qualified Foreign.Concurrent as F
import Control.Applicative ((<$>))
import System.IO.Unsafe (unsafeInterleaveIO)
import Data.Ratio
import qualified Data.Vector.Storable.Mutable as MV
import qualified Data.Vector.Storable as V
import Control.Concurrent.MVar.Strict
------------------------------------------------------------------------
-- Types
-- | A Yices /context/.
--
-- A context is an environment of declarations and assertions.
--
-- /Notes:/
--
-- * The resource is automatically managed by the Haskell garbage
-- collector, and the structure is automatically deleted once it is out
-- of scope (no need to call 'c_del_context').
--
-- * Improving on the C API, we maintain a stack depth, to prevent errors
-- relating to uneven numbers of 'push' and 'pop' operations. 'pop' on a
-- zero depth stack leaves the stack at zero.
--
-- /Reference:/ <http://yices.csl.sri.com/capi.shtml#ga3>
--
data Context = Context { yContext :: ForeignPtr YContext
, yDepth :: !(MVar Integer) -- We have a semaphore to prevent push/pop errors
}
deriving Eq
-- | Yices /expressions/
--
-- /Reference:/ <http://yices.csl.sri.com/capi.shtml#ga0>
--
newtype Expr = Expr { unExpr :: Ptr YExpr }
deriving (Eq, Ord, Show, Storable)
-- TODO: AST node types in Expr type. Size types for bit vectors.
-- | A Yices Model.
--
-- A model assigns constant values to variables defined in a context.
-- The context must be known to be consistent for a model to be
-- available.
--
-- The model is constructed by calling 'check' (or its
-- relatives) then 'getModel'.
--
-- /Reference:/ <http://yices.csl.sri.com/capi.shtml#ga5>
--
newtype Model = Model { unModel :: Ptr YModel }
deriving (Eq, Ord, Show, Storable)
-- | Yices types (abstract syntax tree).
--
-- /Reference:/ <http://yices.csl.sri.com/capi.shtml#ga1>
--
newtype Type = Type { unType :: Ptr YType }
deriving (Eq, Ord, Show, Storable)
-- | A Yices variable declaration.
--
-- A declaration consists of a name and a type.
--
-- An instance of the declaration represents the term. Instances are
-- also called /name expressions/.
--
-- Instances can be created using 'mkBoolDecl' or 'mkVarDecl'.
--
-- /Reference:/ <http://yices.csl.sri.com/capi.shtml#ga2>
--
newtype Decl = Decl { unDecl :: Ptr YVarDecl }
deriving (Eq, Ord, Show, Storable)
-- | An assertion weight.
newtype Weight = Weight { _unWeight :: YWeight }
deriving (Eq,Ord,Bounded,Enum,Show,Read,Num,Integral,Real)
-- | A model cost.
newtype Cost = Cost { _unCost :: YCost }
deriving (Eq,Ord,Bounded,Enum,Show,Read,Num,Integral,Real)
-- | Assertion index, to identify retractable assertions.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga4>
--
newtype Assert = Assert { _unAssert :: YAssertId }
deriving (Eq,Ord,Bounded,Enum,Show,Read,Num,Integral,Real,Storable)
-- | Iterator for scanning the boolean variables.
--
-- The resource is automatically managed by the Haskell garbage
-- collector, and the structure is automatically deleted once it is out
-- of scope (no need to call 'c_del_iterator').
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga6>
--
newtype Iterator = Iterator { unIterator :: ForeignPtr YIterator }
-- | Extended booleans: to represent the value of literals in the context.
--
-- The high level interface represents this with @Maybe Bool@, where 'Nothing'
-- corresponds to undefinedness.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga107>
--
data Result
= Satisfiable
| Unsatisfiable
| Undefined
deriving (Eq, Ord, Enum, Bounded, Read, Show)
toResult :: YBool -> Result
toResult n
| n == yFalse = Unsatisfiable
| n == yTrue = Satisfiable
| otherwise = Undefined
------------------------------------------------------------------------
-- Context manipulation
-- | Create a new logical context.
-- When the context goes out of scope, it will be automatically deleted.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga15>
--
mkContext :: IO Context
mkContext = do
ptr <- c_yices_mk_context
fp <- F.newForeignPtr ptr (c_yices_del_context ptr)
n <- newMVar 0
return $! Context fp n
-- | Reset the given logical context.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga17>
--
ctxReset :: Context -> IO ()
ctxReset c = do
withForeignPtr (yContext c) $ c_yices_reset
modifyMVar_ (yDepth c) $ \_ -> return 0
-- | Display the internal representation of the given logical context on
-- stderr. This function is mostly for debugging.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga18>
--
ctxDump :: Context -> IO ()
ctxDump c = withForeignPtr (yContext c) $ c_yices_dump_context
-- | Create a backtracking point in the given logical context.
--
-- The logical context can be viewed as a stack of contexts. The scope
-- level is the number of elements on this stack. The stack of contexts
-- is simulated using trail (undo) stacks.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga19>
--
ctxPush :: Context -> IO ()
ctxPush c = modifyMVar_ (yDepth c) $ \n ->
if n < 0
then error "Yices.Base.push: Corrupted Context. Stack depth < 0"
else do
withForeignPtr (yContext c) $ c_yices_push
return (n+1)
-- | Backtrack.
--
-- Restores the context from the top of the stack, and pops it off the
-- stack. Any changes to the logical context (by 'c_yices_assert' or
-- other functions) between the matching 'push' and 'pop' operators are
-- flushed, and the context is completely restored to what it was right
-- before the 'push'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga20>
--
ctxPop :: Context -> IO ()
ctxPop c = modifyMVar_ (yDepth c) $ \n -> case () of
_ | n < 0 -> error "Yices.Base.pop: Corrupted context. Stack depth < 0"
| n == 0 -> return n
| otherwise -> do
withForeignPtr (yContext c) $ c_yices_pop
return (n-1)
------------------------------------------------------------------------
-- Assertions
-- | Assert a constraint in the logical context.
--
-- After one assertion, the logical context may become inconsistent. The
-- function 'inconsistent' may be used to check that.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga21>
--
assert :: Context -> Expr -> IO ()
assert c e = withForeignPtr (yContext c) $ \cptr ->
c_yices_assert cptr (unExpr e)
-- | Assert a constraint in the logical context with weight @w@.
-- Returns an identifier that can be used to retract the constraint later.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga22>
--
assertWeighted :: Context -> Expr -> Weight -> IO Assert
assertWeighted c e w = withForeignPtr (yContext c) $ \cptr -> fromIntegral <$>
c_yices_assert_weighted cptr (unExpr e) (fromIntegral w)
-- | Assert a constraint that can be later retracted.
-- Returns an id that can be used to retract the constraint. This is similar
-- to 'assertWeighted', but the weight is considered to be infinite.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga23>
--
assertRetractable :: Context -> Expr -> IO Assert
assertRetractable c e = withForeignPtr (yContext c) $ \cptr -> fromIntegral <$>
c_yices_assert_retractable cptr (unExpr e)
-- | Retract a retractable or weighted constraint.
--
-- For use with 'assertWeighted' and 'assertRetractable'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga24>
--
retract :: Context -> Assert -> IO ()
retract c a =
withForeignPtr (yContext c) $ \cptr ->
c_yices_retract cptr (fromIntegral a)
------------------------------------------------------------------------
-- Logical operations
-- | Return 'True' if the logical context is known to be inconsistent.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga25>
inconsistent :: Context -> IO Bool
inconsistent c = do
i <- withForeignPtr (yContext c) $ c_yices_inconsistent
return $ case i of
1 -> True
_ -> False
-- | Check if the logical context is satisfiable.
--
-- * @Satisfiable@ means the context is satisfiable.
--
-- * @Unsatisfiable@ means the context is unsatisfiable.
--
-- * @Undefined@ means it was not possible to decide due to an incompletness.
--
-- If the context is satisfiable, then 'getModel' can be used to obtain a model.
--
-- /Warning:/ This method ignore the weights associated with the constraints.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga26>
--
check :: Context -> IO Result
check c = toResult <$>
withForeignPtr (yContext c) c_yices_check
-- | Search for a model of the constraints asserted in ctx and compute its
-- cost. If @random@ is 'True', then random search is used, otherwise, the
-- default decision heuristic is used. If there are no weighted constaints in
-- the context, then this function is the same as 'check'.
--
-- Otherwise, it searches for a model that satisfies all the non-weighted
-- constraints but not necessarily the weighted constraints. The function
-- returns 'Satisfiable' if such a model is found, and the model can be
-- obtained using 'getModel'. The cost of this model is the sum of the weights
-- of the unsatisfied weighted constraints.
--
-- The function returns 'Unsatisfiable' if it cannot find such a model.
--
-- The function may also return 'Undefined', if the context contains formulas
-- for which yices is incomplete (e.g., quantifiers). Do not use the model in
-- this case.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga27>
--
findWeightedModel :: Context -> Bool -> IO Result
findWeightedModel c r = withForeignPtr (yContext c) $ \cptr ->
toResult <$> c_yices_find_weighted_model cptr (fromIntegral (fromEnum r))
-- | Print the given model to 'stdout'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga40>
--
display :: Model -> IO ()
display = c_yices_display_model . unModel
-- | Return the cost of model m.
-- The cost is the sum of the weights of unsatisfied constraints.
--
-- /Warning:/ The model cost is computed automatically by 'maxSat' but
-- not by 'check'. If 'check' returns 'Satisfiable' (or 'Undefined'),
-- you can call 'computeModelCost' to compute the cost explicitly.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga41>
--
getCost :: Model -> IO Cost
getCost m = fromIntegral <$> c_yices_get_cost (unModel m)
-- | Return the cost of the model m, converted to a double-precision
-- floating point number.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga42>
--
getCostDouble :: Model -> IO Double
getCostDouble m = realToFrac <$> c_yices_get_cost_as_double (unModel m)
------------------------------------------------------------------------
-- Model manipulation
-- | Evaluate a formula in a model.
--
-- A model, /m/ can be obtained via 'getModel', after a call to
-- 'check', 'maxSat', or 'findWeightedModel'.
--
-- * 'Satisfiable' means the formula is true in the model
--
-- * 'Unsatisfiable' means the formula is false in the model
--
-- * 'Undefined' means the model does not have enough information.
--
-- Typically this is due to a function application, e.g., the model
-- defines @f 1@ and @f 2@, but the formula references @f 3@
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga28>
--
evalInModel :: Model -> Expr -> IO Result
evalInModel m e = toResult <$>
c_yices_evaluate_in_model (unModel m) (unExpr e)
-- | Compute the maximal satisfying assignment for the asserted weighted
-- constraints.
--
-- * 'Satisfiable' means the maximal satisfying assignment was found
--
-- * 'Unsatisfiable' means it is unsatisfiable (this may happen if the
-- context has unweighted constraints)
--
-- * 'Undefined' means it was not possible to decide due to an
-- incompleteness.
--
-- If the result is 'Satisfiable' then 'getModel' can be used to obtain
-- a model.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga29>
--
maxSat :: Context -> IO Result
maxSat c = toResult <$>
withForeignPtr (yContext c) c_yices_max_sat
-- Similar to 'maxSat', but start looking for models with cost less than
-- of equal to max_cost.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga30>
--
maxSatCost :: Context -> Cost -> IO Result
maxSatCost c i = toResult <$>
withForeignPtr (yContext c) (\cptr -> c_yices_max_sat_cost_leq cptr (fromIntegral i))
-- | Return a model for a satisfiable logical context.
--
-- /Warning:/ The should be only called if 'check' or 'maxSat'
-- returned 'Satisfiable' or 'Undefined'.
-- Returns 'Nothing' if a model is not available. Calls to functions
-- which modify the context invalidate the model.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga31>
--
getModel :: Context -> IO (Maybe Model)
getModel c = do
i <- withForeignPtr (yContext c) c_yices_get_model
return $! if i == nullPtr
then Nothing
else Just (Model i)
------------------------------------------------------------------------
-- Querying the result
-- | Return the size of the unsat core or 'Nothing' it there's no unsat core.
getUnsatCoreSize :: Context -> IO (Maybe Word)
getUnsatCoreSize c = do
i <- fromIntegral <$> withForeignPtr (yContext c) c_yices_get_unsat_core_size
return $! case i of
0 -> Nothing
n -> Just n
-- | Extract the unsatisfiable core.
--
-- Each assertion in the core is identified by an 'Assert' as returned by
-- 'assertRetractable'. The unsatisfiable core is a (small) subset of the
-- retractable assertions that is inconsistent by itself.
--
-- The function returns an empty list if there's no unsat core.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga111>
--
getUnsatCore :: Context -> IO [Assert]
getUnsatCore c = do
m <- getUnsatCoreSize c
case m of
Nothing -> return []
Just n -> do
withForeignPtr (yContext c) $ \cptr -> do
allocaArray (fromIntegral n) $ \arr -> do
k <- c_yices_get_unsat_core cptr (castPtr arr)
peekArray (fromIntegral k) arr
------------------------------------------------------------------------
-- Extracting bindings
-- | Return the assignment for the variable of type @a@'.
-- The result is 'Nothing' if the value of the decl is "don't care".
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga32>
--
--
class YValue a where
getValue :: Model -> Decl -> IO (Maybe a)
instance YValue Bool where getValue = getValueBool
instance YValue Int where getValue = getValueInt
instance YValue Rational where getValue = getValueRational
instance YValue Double where getValue = getValueDouble
-- Derived marshalling instances
instance YValue Word where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Int32 where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Int16 where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Int8 where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Word32 where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Word16 where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Word8 where
getValue m d = fmap fromIntegral <$> getValueInt m d
instance YValue Float where
getValue m d = fmap realToFrac <$> getValueDouble m d
-- | Return the assignment for the boolean variable @v@.
-- The result is 'Nothing' if the value of @v@ is a "don't care".
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga32>
--
getValueBool :: Model -> Decl -> IO (Maybe Bool)
getValueBool m d = do
i <- c_yices_get_value (unModel m) (unDecl d)
return $ case toResult i of
Unsatisfiable -> Just False
Satisfiable -> Just True
_ -> Nothing
-- | Get the 'Int' value assigned to variable @v@ in model @m@.
--
-- A return value of 'Nothing' indicates one of the following errors:
--
-- * @v@ is not a proper declaration or not the declaration of a
-- numerically-typed variable
--
-- * @v@ has no value assigned in model m (typically, this means that v does
-- not occur in the asserted constraints)
--
-- * @v@ has a value that cannot be converted to long, because it is rational
-- or too big
--
getValueInt :: Model -> Decl -> IO (Maybe Int)
getValueInt m d = do
alloca $ \iptr -> do
n <- c_yices_get_int_value (unModel m) (unDecl d) iptr
case n of
0 -> return Nothing
_ -> Just . fromIntegral <$> peek iptr
-- | Get the rational value assigned to variable @v@ in model @m@.
--
-- A return code of 'Nothing' indicates one of the following errors:
--
-- * @v@ is not a proper declaration or not the declaration of a numerical
-- variable
--
-- * @v@ has no value assigned in model m (typically, this means that v does
-- not occur in the asserted constraints)
--
-- * @v@ has a value that cannot be converted to a 'Rational', because the
-- numerator or the denominator is too big for the underlying C representation.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga34>
--
getValueRational :: Model -> Decl -> IO (Maybe Rational)
getValueRational m d =
alloca $ \nptr ->
alloca $ \dptr -> do
r <- c_yices_get_arith_value (unModel m) (unDecl d) nptr dptr
case r of
0 -> return Nothing
_ -> do nm <- fromIntegral <$> peek nptr
dm <- fromIntegral <$> peek dptr
return $ Just (nm % dm)
-- | Extract the value assigned to variable @v@ in model @m@ as a floating
-- point number.
--
-- A return value of 'Nothing' indicates one of the following errors:
--
-- * @v@ is not a proper declaration or not the declaration of a numerical
-- variable
--
-- * @v@ has no value assigned in model @m@ (typically, this means that @v@ does
-- not occur in the asserted constraints)
--
getValueDouble :: Model -> Decl -> IO (Maybe Double)
getValueDouble m d =
alloca $ \dptr -> do
r <- c_yices_get_double_value (unModel m) (unDecl d) dptr
case r of
0 -> return Nothing
_ -> Just . realToFrac <$> peek dptr
{-
-- XXX Integers can be supported, via low level casting to mpq values and back.
-- Look at primitives in integer-gmp for ideas.
-- Might be possible to allocate new primitive ByteArray#'s, pin, then copy mpq_t's in.
-- Convert the value assigned to variable v in model m to a GMP rational (mpq_t).
int yices_get_mpq_value (
yices_model m,
yices_var_decl d,
mpq_t value
)
-- Convert the value assigned to variable v in model m to a GMP integer (mpz_t).
int yices_get_mpz_value (
yices_model m,
yices_var_decl d,
mpz_t value
)
-}
-- | Get the bitvector constant assigned to a variable @v@ in model @m@.
--
-- @n@ should be the size of the bitvector variable v. Otherwise, if @n@ is
-- smaller than @v@'s size, the @n@ lower-order bits of @v@ are returned. If
-- @n@ is larger than @v@'s size then the extra high-order bits are set to 0.
--
-- The value is 'Nothing' if an error occurs. Possible errors are:
--
-- * @d@ is not the declaration of a bitvector variable.
--
-- * @d@ is not assigned a value in model @m@
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga38>
--
getValueBitVector :: Model -> Decl -> Int -> IO (Maybe (V.Vector Bool))
getValueBitVector m d sz = do
v <- MV.new sz
i <- MV.unsafeWith v $ \vptr ->
c_yices_get_bitvector_value
(unModel m)
(unDecl d)
(fromIntegral sz)
(castPtr vptr)
case i of
0 -> return Nothing
_ -> Just <$> V.unsafeFreeze v
--
-- Notes on the representation: The bit vector on the C side is stored as an
-- int array. The Storable instance of Bool on the Haskell side uses an Int
-- encoding. So we should be fine.
--
-- The requirement to provide a size also complicates using a type class
-- interface. Size types?
--
-- | Return 'True' or 'False' if the assertion of the given id is
-- satisfied (or not satisfied) in the model @m@.
--
-- This function is only useful for 'Assert's obtained using
-- 'assertWeighted', and 'maxSat' was used to build the model. That is
-- the only scenario where an assertion may not be satisfied in a model
-- produced by yices.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga39>
--
getAssertValue :: Model -> Assert -> IO Bool
getAssertValue m a = do
i <- c_yices_get_assertion_value (unModel m) (fromIntegral a)
return $ case i of
0 -> False
_ -> True
------------------------------------------------------------------------
-- Constructing values
-- | Return an expression representing 'True'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga43>
--
mkTrue :: Context -> IO Expr
mkTrue c = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_true cptr
-- | Return an expression representing 'False'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga44>
--
mkFalse :: Context -> IO Expr
mkFalse c = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_false cptr
-- | Return a name expression for the given variable name.
-- Expressions constructed via this function are equivalent, when
-- constructed by strings with identical names.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga45>
--
mkBool :: Context -> String -> IO Expr
mkBool c n =
withCString n $ \cstr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bool_var cptr cstr
-- | Return a fresh boolean variable.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga46>
--
mkFreshBool :: Context -> IO Expr
mkFreshBool c = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_fresh_bool_var cptr
-- | Return a new boolean variable declaration.
--
-- It is an error to create two variables with the same name.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga48>
--
mkBoolDecl :: Context -> String -> IO Decl
mkBoolDecl c n =
withForeignPtr (yContext c) $ \cptr ->
withCString n $ \cstr ->
Decl <$> c_yices_mk_bool_var_decl cptr cstr
------------------------------------------------------------------------
-- Logical operations
-- | Return an expression representing the /n/-ary /OR/ of the given arguments.
--
-- > or [a1, ..]
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga51>
--
mkOr :: Context -> [Expr] -> IO Expr
mkOr _ [] = error "Yices.Base.mkOr: empty list of expressions"
mkOr c es =
withArray es $ \aptr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_or cptr (castPtr aptr) (fromIntegral (length es))
-- | Return an expression representing the /n/-ary /AND/ of the given arguments.
--
-- > and [a1, ..]
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga52>
--
mkAnd :: Context -> [Expr] -> IO Expr
mkAnd _ [] = error "Yices.Base.mkAnd: empty list of expressions"
mkAnd c es =
withArray es $ \aptr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_and cptr (castPtr aptr) (fromIntegral (length es))
-- | Return an expression representing:
--
-- > a1 == a2
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga53>
--
mkEq :: Context -> Expr -> Expr -> IO Expr
mkEq c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_eq cptr (unExpr e1) (unExpr e2)
-- | Return an expression representing:
--
-- > a1 /= a2
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga54>
--
mkNeq :: Context -> Expr -> Expr -> IO Expr
mkNeq c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_diseq cptr (unExpr e1) (unExpr e2)
-- | Return an expression representing:
--
-- > if c then t else e
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga55>
--
mkIte :: Context -> Expr -> Expr -> Expr -> IO Expr
mkIte c b e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_ite cptr (unExpr b) (unExpr e1) (unExpr e2)
-- | Return an expression representing:
--
-- > not a
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga56>
--
mkNot :: Context -> Expr -> IO Expr
mkNot c e = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_not cptr (unExpr e)
------------------------------------------------------------------------
-- Types
-- | Return the type associated with the given name. If the type does
-- not exist, a new uninterpreted type is created.
--
-- /Remarks:/ @number@, @real@, @int@, @nat@, @bool@, @any@ are builtin types.
--
mkType :: Context -> String -> IO Type
mkType c s =
withCString s $ \cstr ->
withForeignPtr (yContext c) $ \cptr ->
Type <$> c_yices_mk_type cptr cstr
-- | Return a function type:
--
-- > (d1 -> ... dn -> r)
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga63>
--
mkFunctionType :: Context -> [Type] -> Type -> IO Type
mkFunctionType c tys ty =
withArray tys $ \tysptr ->
withForeignPtr (yContext c) $ \cptr ->
Type <$> c_yices_mk_function_type cptr
(castPtr tysptr)
(fromIntegral (length tys))
(unType ty)
-- | Returns a bitvector type of @n@ size.
--
-- Size must be greater than @0@.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga64>
--
mkBitVectorType :: Context -> Word -> IO Type
mkBitVectorType _ 0 = error "Yices.Base: mkBitVectorType: size must be positive."
mkBitVectorType c n = withForeignPtr (yContext c) $ \cptr ->
Type <$> c_yices_mk_bitvector_type cptr (fromIntegral n)
------------------------------------------------------------------------
{-
-- |
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga65>
--
mkTupleType :: Context -> [Type] -> IO Type
mkTupleType c ts =
-- TODO: whats up with the nested type?
-}
------------------------------------------------------------------------
-- | Return a new (global) variable declaration. It is an error to
-- create two variables with the same name.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga66>
--
mkVarDecl :: Context -> String -> Type -> IO Decl
mkVarDecl c s ty =
withCString s $ \cstr ->
withForeignPtr (yContext c) $ \cptr ->
Decl <$> c_yices_mk_var_decl cptr cstr (unType ty)
-- | Return a variable declaration associated with the given name.
--
-- Return 'Nothing' if there is no variable declaration associated with
-- the given name.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga67>
--
getVarDeclFromName :: Context -> String -> IO (Maybe Decl)
getVarDeclFromName c s =
withCString s $ \cstr ->
withForeignPtr (yContext c) $ \cptr -> do
p <- c_yices_get_var_decl_from_name cptr cstr
return $! if p == nullPtr
then Nothing
else Just (Decl p)
-- | Return a name expression (instance) using the given variable
-- declaration
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga68>
--
mkVarFromDecl :: Context -> Decl -> IO Expr
mkVarFromDecl c d = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_var_from_decl cptr (unDecl d)
-- | Return a function application term:
--
-- > f t1 ... tn
--
-- The type of @f@ must be a function-type, and its arity must be equal
-- to the number of arguments.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga69>
--
mkApp :: Context -> Expr -> [Expr] -> IO Expr
mkApp c f xs =
withArray xs $ \xsptr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_app cptr (unExpr f) (castPtr xsptr) (fromIntegral (length xs))
-- | Return an expression representing the given integer.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga70>
--
mkNum :: Context -> Int -> IO Expr
mkNum c n = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_num cptr (fromIntegral n)
-- | Return an expression representing the number provided in ASCII
-- format
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga71>
--
mkNumFromString :: Context -> String -> IO Expr
mkNumFromString c s =
withCString s $ \cstr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_num_from_string cptr cstr
{-
TODO:
yices_expr yices_mk_num_from_mpz (yices_context ctx, const mpz_t z)
Construct a numerical expression form a GMP integer.
yices_expr yices_mk_num_from_mpq (yices_context ctx, const mpq_t q)
Construct a numerical expression form a GMP rational.
-}
------------------------------------------------------------------------
-- Expressions
-- | Return an expression representing the sum of the argument expressions.
--
-- > sum [e1, e2 ..]
--
-- The expression list must be non-empty.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga74>
--
mkSum :: Context -> [Expr] -> IO Expr
mkSum c es =
withArray es $ \esptr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_sum cptr (castPtr esptr) (fromIntegral (length es))
-- | Return an expression representing the subtraction of the argument expressions.
--
-- > e1 - e2 - e3 ..
--
-- The expression list must be non-empty.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga75>
--
mkSub :: Context -> [Expr] -> IO Expr
mkSub c es =
withArray es $ \esptr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_sub cptr (castPtr esptr) (fromIntegral (length es))
-- | Return an expression representing the product of the argument expressions.
--
-- > product [e1, e2 ..]
--
-- The expression list must be non-empty.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga76>
--
mkMul :: Context -> [Expr] -> IO Expr
mkMul c es =
withArray es $ \esptr ->
withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_mul cptr (castPtr esptr) (fromIntegral (length es))
-- | Return an expression representing:
--
-- > a1 < a2
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga77>
--
mkLt :: Context -> Expr -> Expr -> IO Expr
mkLt c a1 a2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_lt cptr (unExpr a1) (unExpr a2)
-- | Return an expression representing:
--
-- > a1 <= a2
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga78>
--
mkLe :: Context -> Expr -> Expr -> IO Expr
mkLe c a1 a2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_le cptr (unExpr a1) (unExpr a2)
-- | Return an expression representing:
--
-- > a1 > a2
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga79>
--
mkGt :: Context -> Expr -> Expr -> IO Expr
mkGt c a1 a2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_gt cptr (unExpr a1) (unExpr a2)
-- | Return an expression representing:
--
-- > a1 >= a2
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga80>
--
mkGe :: Context -> Expr -> Expr -> IO Expr
mkGe c a1 a2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_ge cptr (unExpr a1) (unExpr a2)
------------------------------------------------------------------------
-- Operations on bit vectors
-- | Create a bit vector constant of size bits and of the given value.
--
-- @size@ must be positive
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga81>
--
mkBVConstant :: Context -> Int -> Word -> IO Expr
mkBVConstant c n v = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_constant cptr (fromIntegral n) (fromIntegral v)
-- | Create a bit vector constant from an array.
--
-- Array must be non-empty.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga82>
--
mkBVConstantFromVector :: Context -> V.Vector Bool -> IO Expr
mkBVConstantFromVector _ v | V.null v = error "Yices.Base: can't create empty bit vector"
mkBVConstantFromVector c v =
withForeignPtr (yContext c) $ \cptr ->
V.unsafeWith v $ \vptr ->
Expr <$> c_yices_mk_bv_constant_from_array cptr (fromIntegral (V.length v)) (castPtr vptr)
-- | Bitvector addition.
--
-- @a1@ and @a2@ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga83>
--
mkBVAdd :: Context -> Expr -> Expr -> IO Expr
mkBVAdd c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_add cptr (unExpr e1) (unExpr e2)
-- | Bitvector subtraction.
--
-- @a1@ and @a2@ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga84>
--
mkBVSub :: Context -> Expr -> Expr -> IO Expr
mkBVSub c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_sub cptr (unExpr e1) (unExpr e2)
-- | Bitvector multiplication.
--
-- @a1@ and @a2@ must be bitvector expression of same size.
-- The result is truncated to that size too. E.g., multiplication of two 8-bit vectors gives an 8-bit result.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga85>
--
mkBVMul :: Context -> Expr -> Expr -> IO Expr
mkBVMul c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_mul cptr (unExpr e1) (unExpr e2)
-- | Bitvector minus.
--
-- @a1@ must be bitvector expression. The result is @(- a1)@.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga86>
--
mkBVMinus :: Context -> Expr -> IO Expr
mkBVMinus c e = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_minus cptr (unExpr e)
-- | Bitvector concatenation.
--
-- @a1@ and @a2@ must be two bitvector expressions.
-- @a1@ is the left part of the result and @a2@ the right part.
--
-- Assuming /a1/ and /a2/ have /n1/ and /n2/ bits, respectively, then the
-- result is a bitvector concat of size /n1 + n2/. Bit 0 of concat is bit 0 of
-- /a2/ and bit n2 of concat is bit 0 of /a1/.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga87>
--
mkBVConcat :: Context -> Expr -> Expr -> IO Expr
mkBVConcat c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_concat cptr (unExpr e1) (unExpr e2)
-- | Bitwise @and@.
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga88>
--
mkBVAnd :: Context -> Expr -> Expr -> IO Expr
mkBVAnd c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_and cptr (unExpr e1) (unExpr e2)
-- | Bitwise @or@.
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga89>
--
mkBVOr :: Context -> Expr -> Expr -> IO Expr
mkBVOr c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_or cptr (unExpr e1) (unExpr e2)
-- | Bitwise @xor@.
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga90>
--
mkBVXor :: Context -> Expr -> Expr -> IO Expr
mkBVXor c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_xor cptr (unExpr e1) (unExpr e2)
-- | Bitwise negation.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga91>
--
mkBVNot :: Context -> Expr -> IO Expr
mkBVNot c e = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_not cptr (unExpr e)
-- | Bitvector extraction.
--
-- The first @Int@ argument is the initial index, the second is the end index.
-- /Note/: this is reversed wrt. the C API.
--
-- /a/ must a bitvector expression of size /n/ with @begin < end < n@.
-- The result is the subvector slice @a[begin .. end]@.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga92>
--
mkBVExtract :: Context -> Int -> Int -> Expr -> IO Expr
mkBVExtract c begin end e = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_extract cptr (fromIntegral end) (fromIntegral begin) (unExpr e)
-- | Sign extension.
--
-- Append /n/ times the most-significant bit of to the left of /a/.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga93>
--
mkBVSignExtend :: Context -> Expr -> Int -> IO Expr
mkBVSignExtend c e n = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_sign_extend cptr (unExpr e) (fromIntegral n)
-- | Left shift by n bits, padding with zeros.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga94>
--
mkBVShiftLeft0 :: Context -> Expr -> Int -> IO Expr
mkBVShiftLeft0 c e n = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_shift_left0 cptr (unExpr e) (fromIntegral n)
-- | Left shift by n bits, padding with ones
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga95>
--
mkBVShiftLeft1 :: Context -> Expr -> Int -> IO Expr
mkBVShiftLeft1 c e n = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_shift_left1 cptr (unExpr e) (fromIntegral n)
-- | Right shift by n bits, padding with zeros.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga96>
--
mkBVShiftRight0 :: Context -> Expr -> Int -> IO Expr
mkBVShiftRight0 c e n = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_shift_right0 cptr (unExpr e) (fromIntegral n)
-- | Right shift by n bits, padding with ones.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga97>
--
mkBVShiftRight1 :: Context -> Expr -> Int -> IO Expr
mkBVShiftRight1 c e n = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_shift_right1 cptr (unExpr e) (fromIntegral n)
------------------------------------------------------------------------
-- | Unsigned bitvector comparison:
--
-- > a1 < a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga98>
--
mkBVLt :: Context -> Expr -> Expr -> IO Expr
mkBVLt c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_lt cptr (unExpr e1) (unExpr e2)
-- | Unsigned bitvector comparison:
--
-- > a1 <= a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga99>
--
mkBVLe :: Context -> Expr -> Expr -> IO Expr
mkBVLe c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_le cptr (unExpr e1) (unExpr e2)
-- | Unsigned bitvector comparison:
--
-- > a1 > a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga100>
--
mkBVGt :: Context -> Expr -> Expr -> IO Expr
mkBVGt c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_gt cptr (unExpr e1) (unExpr e2)
-- | Unsigned bitvector comparison:
--
-- > a1 >= a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga101>
--
mkBVGe :: Context -> Expr -> Expr -> IO Expr
mkBVGe c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_ge cptr (unExpr e1) (unExpr e2)
------------------------------------------------------------------------
-- | Signed bitvector comparison:
--
-- > a1 < a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga102>
--
mkBVSlt :: Context -> Expr -> Expr -> IO Expr
mkBVSlt c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_slt cptr (unExpr e1) (unExpr e2)
-- | Signed bitvector comparison:
--
-- > a1 <= a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga103>
--
mkBVSle :: Context -> Expr -> Expr -> IO Expr
mkBVSle c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_sle cptr (unExpr e1) (unExpr e2)
-- | Signed bitvector comparison:
--
-- > a1 > a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga104>
--
mkBVSgt :: Context -> Expr -> Expr -> IO Expr
mkBVSgt c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_sgt cptr (unExpr e1) (unExpr e2)
-- | Signed bitvector comparison:
--
-- > a1 >= a2
--
-- /a1/ and /a2/ must be bitvector expressions of same size.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga105>
--
mkBVSge :: Context -> Expr -> Expr -> IO Expr
mkBVSge c e1 e2 = withForeignPtr (yContext c) $ \cptr ->
Expr <$> c_yices_mk_bv_sge cptr (unExpr e1) (unExpr e2)
------------------------------------------------------------------------
-- IO on Expr
-- | Pretty print the given expression in the standard output.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga106>
--
ppExpr :: Expr -> IO ()
ppExpr e = do c_yices_pp_expr (unExpr e)
putChar '\n'
------------------------------------------------------------------------
-- Iterators
-- | Lazily return the boolean variables in a given logical context.
--
-- This is particularly useful when we want to extract the assignment
-- (model) produced by 'check'.
--
getDecls :: Context -> IO [Decl]
getDecls c = do
i <- newIterator c
go i
where
go i = unsafeInterleaveIO $ do
b <- iteratorHasNext i
if b then do
d <- iteratorNext i
ds <- go i
return (d:ds)
else
return []
-- Hidden:
-- | Create an iterator that can be used to traverse the boolean variables
-- ('Decl' values) in the given logical context.
--
-- An 'Iterator' is particulary useful when we want to extract the assignment
-- (model) produced by the 'check' command.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga57>
--
newIterator :: Context -> IO Iterator
newIterator c = do
iptr <- withForeignPtr (yContext c) c_yices_create_var_decl_iterator
fp <- F.newForeignPtr iptr (c_yices_del_iterator iptr)
return $! Iterator fp
-- | 'True' if the iterator has elements remaining.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga58>
--
iteratorHasNext :: Iterator -> IO Bool
iteratorHasNext i = do
n <- withForeignPtr (unIterator i) c_yices_iterator_has_next
return $ case n of
1 -> True
_ -> False
-- | Return the next variable, and move the iterator.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga59>
--
iteratorNext :: Iterator -> IO Decl
iteratorNext i = Decl <$>
withForeignPtr (unIterator i) c_yices_iterator_next
{-
-- | Reset the given iterator, that is, move it back to the first element.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga60>
--
iteratorReset :: Iterator -> IO ()
iteratorReset i = do
withForeignPtr (unIterator i) c_yices_iterator_reset
-}
------------------------------------------------------------------------
-- Accessing declarations
-- | Return the variable declaration object associated with the given
-- name expression.
--
-- @e@ must be a name expression created using methods such as:
--
-- * 'mkBool'
--
-- * 'mkFreshBool'
--
-- * 'mkBoolDecl'
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga47>
--
getDecl :: Expr -> IO Decl
getDecl e = Decl <$> c_yices_get_var_decl (unExpr e)
------------------------------------------------------------------------
-- System information
-- | Return the yices version number.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga8>
--
version :: String
version = unsafePerformIO $ do
peekCString c_yices_version
------------------------------------------------------------------------
-- System configuration
-- | Set the verbosity level.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga7>
--
setVerbosity :: Int -> IO ()
setVerbosity n = c_yices_set_verbosity (fromIntegral n)
-- | Set the initial cost for a maxsat problem.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga12>
--
setMaxSatInitialCost :: Int64 -> IO ()
setMaxSatInitialCost n = c_yices_set_maxsat_initial_cost (fromIntegral n)
-- | Set the maximum number of conflicts that are allowed in a maxsat
-- iteration. If the maximum is reached, then 'YUndef' is returned by
-- 'c_maxsat'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga9>
--
setMaxNumConflictsInMaxSatIteration :: Word -> IO ()
setMaxNumConflictsInMaxSatIteration n = c_yices_set_max_num_conflicts_in_maxsat_iteration (fromIntegral n)
-- | Force Yices to type check expressions when they are asserted. By
-- default type checking is disabled.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga10>
--
setTypeChecker :: Bool -> IO ()
setTypeChecker False = c_yices_enable_type_checker 0
setTypeChecker True = c_yices_enable_type_checker 1
-- | Set the maximum number of iterations in the MaxSAT algorithm.
-- If the maximum is reached, then 'YUndef' is returned by 'c_maxsat'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga11>
--
setMaxNumIterationsInMaxSat :: Word -> IO ()
setMaxNumIterationsInMaxSat n = c_yices_set_max_num_iterations_in_maxsat (fromIntegral n)
-- | Inform yices that only arithmetic theory is going to be used.
--
-- This flag usually improves performance, and Yices defaults to 'False'.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga13>
--
setArithmeticOnly :: Bool -> IO ()
setArithmeticOnly False = c_yices_set_arith_only 0
setArithmeticOnly True = c_yices_set_arith_only 1
-- | Enable a log file that will store the assertions, checks, decls.
--
-- If the log file is already open, then nothing happens.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga14>
--
setLogFile :: FilePath -> IO ()
setLogFile f = do
withCString f $ c_yices_enable_log_file