{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeSynonymInstances #-} -- | -- Module : Yices.Painless.Base -- Copyright : (c) Galois, Inc. 2010 -- License : BSD3 -- Maintainer: Don Stewart -- 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:/ -- data Context = Context { yContext :: ForeignPtr YContext , yDepth :: !(MVar Integer) -- We have a semaphore to prevent push/pop errors } deriving Eq -- | Yices /expressions/ -- -- /Reference:/ -- 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:/ -- newtype Model = Model { unModel :: Ptr YModel } deriving (Eq, Ord, Show, Storable) -- | Yices types (abstract syntax tree). -- -- /Reference:/ -- 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:/ -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- -- 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: -- 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: -- 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: -- 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: -- 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: -- mkTrue :: Context -> IO Expr mkTrue c = withForeignPtr (yContext c) $ \cptr -> Expr <$> c_yices_mk_true cptr -- | Return an expression representing 'False'. -- -- Reference: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- 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: -- getDecl :: Expr -> IO Decl getDecl e = Decl <$> c_yices_get_var_decl (unExpr e) ------------------------------------------------------------------------ -- System information -- | Return the yices version number. -- -- Reference: -- version :: String version = unsafePerformIO $ do peekCString c_yices_version ------------------------------------------------------------------------ -- System configuration -- | Set the verbosity level. -- -- Reference: -- setVerbosity :: Int -> IO () setVerbosity n = c_yices_set_verbosity (fromIntegral n) -- | Set the initial cost for a maxsat problem. -- -- Reference: -- 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: -- 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: -- 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: -- 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: -- 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: -- setLogFile :: FilePath -> IO () setLogFile f = do withCString f $ c_yices_enable_log_file