diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c)2010, Don Stewart + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Don Stewart nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Yices/Painless/Base.hs b/Yices/Painless/Base.hs new file mode 100644 --- /dev/null +++ b/Yices/Painless/Base.hs @@ -0,0 +1,1560 @@ +{-# 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 diff --git a/Yices/Painless/Base/C.hsc b/Yices/Painless/Base/C.hsc new file mode 100644 --- /dev/null +++ b/Yices/Painless/Base/C.hsc @@ -0,0 +1,731 @@ +{-# LANGUAGE ForeignFunctionInterface #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | +-- Module : Yices.Painless.Base.C +-- Copyright : (c) Galois, Inc. 2010 +-- License : BSD3 +-- Maintainer: Don Stewart +-- +-- Low level bindings to the Yices SMT solver. +-- +-- A native, imperative Haskell layer is provided by "Yices.Painless.Base" +-- +-- A very high level EDSL is provided by "Yices.Painless.Language" +-- +-- Direct export of the underlying C API, with some convenient newtype +-- wrappers adding a small level of type safety. +-- +-- The C interface preserves the semantics of the underlying C API. That +-- is, calls to functions prefixed with @c_@ do /no/ additional error +-- checking, and only a light amount of additional type checking. +-- +-- This module corresponds approximately to the /Internal/ modules of +-- the /bindings-yices/ package, by Jose Iborra. +-- +-- * +-- +module Yices.Painless.Base.C ( + + -- * C types + YExpr, + YModel, + YContext, + YType, + YVarDecl, + YIterator, + + -- ** Value types + YAssertId, + YWeight, + YCost, + + -- ** Booleans + YBool, + yFalse, yTrue, yUndef, + + -- * Context manipulation + c_yices_mk_context, + c_yices_del_context, + c_yices_reset, + c_yices_push, + c_yices_pop, + + -- ** IO + c_yices_dump_context, + + -- * Assertions + c_yices_assert, + c_yices_assert_weighted, + c_yices_assert_retractable, + c_yices_retract, + + -- * Solving + c_yices_inconsistent, + c_yices_check, + c_yices_find_weighted_model, + c_yices_max_sat, + c_yices_evaluate_in_model, + c_yices_get_model, + c_yices_get_unsat_core, + + -- ** Cost of a solution + c_yices_get_cost, + c_yices_get_cost_as_double, + c_yices_max_sat_cost_leq, + c_yices_get_unsat_core_size, + + -- ** IO + c_yices_display_model, + + -- * Extracting variable bindings + c_yices_get_value, + c_yices_get_int_value, + c_yices_get_arith_value, + c_yices_get_double_value, + c_yices_get_bitvector_value, + c_yices_get_assertion_value, + + -- * Expressions + -- ** Literals + + c_yices_mk_true, + c_yices_mk_false, + c_yices_mk_bool_var, + c_yices_mk_fresh_bool_var, + c_yices_mk_bool_var_decl, + + -- ** Numbers + c_yices_mk_num, + c_yices_mk_num_from_string, + + -- ** Equality and Comparison + c_yices_mk_or, + c_yices_mk_and, + c_yices_mk_eq, + c_yices_mk_diseq, + + -- ** Negation + c_yices_mk_not, + + -- ** Implication + c_yices_mk_ite, + + -- ** Function application + c_yices_mk_app, + + -- ** Numerical expressions + c_yices_mk_sum, + c_yices_mk_sub, + c_yices_mk_mul, + c_yices_mk_lt, + c_yices_mk_le, + c_yices_mk_gt, + c_yices_mk_ge, + + -- * Types + c_yices_mk_type, + c_yices_mk_function_type, + c_yices_mk_bitvector_type, + c_yices_mk_tuple_type, + + -- * Bit vectors + c_yices_mk_bv_constant, + c_yices_mk_bv_constant_from_array, + + -- ** Bit vector arithmetic + c_yices_mk_bv_add, + c_yices_mk_bv_sub, + c_yices_mk_bv_mul, + c_yices_mk_bv_minus, + + -- ** Bit vector /string/ operations + c_yices_mk_bv_concat, + c_yices_mk_bv_extract, + + -- ** Bitwise operations + c_yices_mk_bv_and, + c_yices_mk_bv_or, + c_yices_mk_bv_xor, + c_yices_mk_bv_not, + + -- ** Shifting and signs + c_yices_mk_bv_sign_extend, + c_yices_mk_bv_shift_left0, + c_yices_mk_bv_shift_left1, + c_yices_mk_bv_shift_right0, + c_yices_mk_bv_shift_right1, + + -- ** Comparisons + c_yices_mk_bv_lt, + c_yices_mk_bv_le, + c_yices_mk_bv_gt, + c_yices_mk_bv_ge, + + c_yices_mk_bv_slt, + c_yices_mk_bv_sle, + c_yices_mk_bv_sgt, + c_yices_mk_bv_sge, + + -- *** IO + c_yices_pp_expr, + + -- * Iterators + c_yices_create_var_decl_iterator, + c_yices_iterator_has_next, + c_yices_iterator_next, + c_yices_iterator_reset, + c_yices_del_iterator, + + -- * Declarations + c_yices_mk_var_decl, + c_yices_mk_var_from_decl, + c_yices_get_var_decl_from_name, + c_yices_get_var_decl, + c_yices_get_var_decl_name, + c_yices_mk_bool_var_from_decl, + + -- * System info + c_yices_version, + + -- * Configuring Yices + c_yices_set_verbosity, + c_yices_enable_type_checker, + c_yices_set_maxsat_initial_cost, + c_yices_set_max_num_conflicts_in_maxsat_iteration, + c_yices_set_max_num_iterations_in_maxsat, + c_yices_set_arith_only, + c_yices_enable_log_file, + + ) where + +import Foreign +import Foreign.C.Types +import Foreign.C.String + +#include "yices_c.h" + +------------------------------------------------------------------------ +-- Types + +-- | Abstract type representing a Yices expression. +-- +-- Reference: +-- +data YExpr + +-- | Abstract type representing a Yices model. +-- +-- Reference: +-- +data YModel + +-- | Abstract type representing a Yices context. +-- +-- Reference: +-- +data YContext + +-- | Abstract type representing a Yices types. +-- +-- Reference: +-- +data YType + +-- | Abstract type for variable declarations. +-- +-- Reference: +-- +data YVarDecl + +-- | Abstract type for variable declaration iterators. +-- +-- Reference: +-- +data YIterator + +-- | Low level type for assertion ids. +-- +-- Reference: +-- +type YAssertId = CInt + +-- | Low level type for weights. +type YWeight = CLLong + +-- | Low level type for costs. +type YCost = CLLong + +-- | Low level type for boolean or undefined results. +type YBool = CInt + +yFalse, yTrue, yUndef :: YBool +yFalse = + #const l_false +yTrue = + #const l_true +yUndef = + #const l_undef + +------------------------------------------------------------------------ +-- Function bindings + +-- Contexts + +-- | Reference: +foreign import ccall unsafe "yices_mk_context" + c_yices_mk_context :: IO (Ptr YContext) + +-- | Reference: +foreign import ccall unsafe "yices_del_context" + c_yices_del_context :: Ptr YContext -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_reset" + c_yices_reset :: Ptr YContext -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_dump_context" + c_yices_dump_context :: Ptr YContext -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_push" + c_yices_push :: Ptr YContext -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_pop" + c_yices_pop :: Ptr YContext -> IO () + +-- Assertions + +-- | Reference: +foreign import ccall unsafe "yices_assert" + c_yices_assert :: Ptr YContext -> Ptr YExpr -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_assert_weighted" + c_yices_assert_weighted :: Ptr YContext -> Ptr YExpr -> YWeight -> IO YAssertId + +-- | Reference: +foreign import ccall unsafe "yices_assert_retractable" + c_yices_assert_retractable :: Ptr YContext -> Ptr YExpr -> IO YAssertId + +-- | Reference: +foreign import ccall unsafe "yices_retract" + c_yices_retract :: Ptr YContext -> YAssertId -> IO () + +-- Solving + +-- | Reference: +foreign import ccall unsafe "yices_inconsistent" + c_yices_inconsistent :: Ptr YContext -> IO CInt + +-- | Reference: +foreign import ccall unsafe "yices_check" + c_yices_check :: Ptr YContext -> IO YBool + +-- | Reference: +foreign import ccall unsafe "yices_find_weighted_model" + c_yices_find_weighted_model :: Ptr YContext -> CInt -> IO YBool + +-- | Reference: +foreign import ccall unsafe "yices_get_cost" + c_yices_get_cost :: Ptr YModel -> IO YCost + +-- | Reference: +foreign import ccall unsafe "yices_get_cost_as_double" + c_yices_get_cost_as_double :: Ptr YModel -> IO CDouble + +-- Models + +-- | Reference: +foreign import ccall unsafe "yices_display_model" + c_yices_display_model :: Ptr YModel -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_evaluate_in_model" + c_yices_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> IO YBool + +-- | Reference: +foreign import ccall unsafe "yices_max_sat" + c_yices_max_sat :: Ptr YContext -> IO YBool + +-- | Reference: +foreign import ccall unsafe "yices_max_sat_cost_leq" + c_yices_max_sat_cost_leq :: Ptr YContext -> YCost -> IO YBool + +-- | Reference: +foreign import ccall unsafe "yices_get_model" + c_yices_get_model :: Ptr YContext -> IO (Ptr YModel) + +-- Querying the result + +-- | Reference: +foreign import ccall unsafe "yices_get_unsat_core_size" + c_yices_get_unsat_core_size :: Ptr YContext -> IO CUInt + +-- | Reference: +foreign import ccall unsafe "yices_get_unsat_core" + c_yices_get_unsat_core :: Ptr YContext -> Ptr YAssertId -> IO CUInt + +-- Extracting bindings + +-- | Reference: +foreign import ccall unsafe "yices_get_value" + c_yices_get_value :: Ptr YModel -> Ptr YVarDecl -> IO YBool + +-- | Reference: +foreign import ccall unsafe "yices_get_int_value" + c_yices_get_int_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CLong -> IO CInt + +-- | Reference: +foreign import ccall unsafe "yices_get_arith_value" + c_yices_get_arith_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CLong -> Ptr CLong -> IO CInt + +-- | Reference: +foreign import ccall unsafe "yices_get_double_value" + c_yices_get_double_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CDouble -> IO CInt + +{- +-- TODO 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 + ) +-} + +-- | Reference: +foreign import ccall unsafe "yices_get_bitvector_value" + c_yices_get_bitvector_value :: Ptr YModel -> Ptr YVarDecl -> CUInt -> Ptr CInt -> IO CInt + +-- | Reference: +foreign import ccall unsafe "yices_get_assertion_value" + c_yices_get_assertion_value :: Ptr YModel -> YAssertId -> IO CInt + +-- Constructing values + +-- | Reference: +foreign import ccall unsafe "yices_mk_true" + c_yices_mk_true :: Ptr YContext -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_false" + c_yices_mk_false :: Ptr YContext -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bool_var" + c_yices_mk_bool_var :: Ptr YContext -> CString -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_fresh_bool_var" + c_yices_mk_fresh_bool_var :: Ptr YContext -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bool_var_decl" + c_yices_mk_bool_var_decl :: Ptr YContext -> CString -> IO (Ptr YVarDecl) + +-- | Reference: +foreign import ccall unsafe "yices_get_var_decl_name" + c_yices_get_var_decl_name :: Ptr YVarDecl -> IO CString + +-- | Reference: +foreign import ccall unsafe "yices_mk_bool_var_from_decl" + c_yices_mk_bool_var_from_decl :: Ptr YContext -> Ptr YVarDecl -> IO (Ptr YExpr) + +-- Logical operations + +-- | Reference: +foreign import ccall unsafe "yices_mk_or" + c_yices_mk_or :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_and" + c_yices_mk_and :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_eq" + c_yices_mk_eq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_diseq" + c_yices_mk_diseq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_ite" + c_yices_mk_ite :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_not" + c_yices_mk_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr) + +-- Types + +-- | Reference: +foreign import ccall unsafe "yices_mk_type" + c_yices_mk_type :: Ptr YContext -> CString -> IO (Ptr YType) + +-- | Reference: +foreign import ccall unsafe "yices_mk_function_type" + c_yices_mk_function_type :: Ptr YContext -> Ptr (Ptr YType) -> CUInt -> Ptr YType -> IO (Ptr YType) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bitvector_type" + c_yices_mk_bitvector_type :: Ptr YContext -> CUInt -> IO (Ptr YType) + +-- | Reference: +foreign import ccall unsafe "yices_mk_tuple_type" + c_yices_mk_tuple_type :: Ptr YContext -> Ptr (Ptr (Ptr YType)) -> CUInt -> IO (Ptr YType) + +-- | Reference: +foreign import ccall unsafe "yices_mk_var_decl" + c_yices_mk_var_decl :: Ptr YContext -> CString -> Ptr YType -> IO (Ptr YVarDecl) + +-- | Reference: +foreign import ccall unsafe "yices_get_var_decl_from_name" + c_yices_get_var_decl_from_name :: Ptr YContext -> CString -> IO (Ptr YVarDecl) + +-- | Reference: +foreign import ccall unsafe "yices_mk_var_from_decl" + c_yices_mk_var_from_decl :: Ptr YContext -> Ptr YVarDecl -> IO (Ptr YExpr) + +-- Application + +-- | Reference: +foreign import ccall unsafe "yices_mk_app" + c_yices_mk_app :: Ptr YContext -> Ptr YExpr -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) + +-- Numbers + +-- | Reference: +foreign import ccall unsafe "yices_mk_num" + c_yices_mk_num :: Ptr YContext -> CInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_num_from_string" + c_yices_mk_num_from_string :: Ptr YContext -> CString -> IO (Ptr YExpr) + +{- + +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 + +-- | Reference: +foreign import ccall unsafe "yices_mk_sum" + c_yices_mk_sum :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_sub" + c_yices_mk_sub :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_mul" + c_yices_mk_mul :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_lt" + c_yices_mk_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_le" + c_yices_mk_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_gt" + c_yices_mk_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_ge" + c_yices_mk_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- Operations on bit vectors + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_constant" + c_yices_mk_bv_constant :: Ptr YContext -> CUInt -> CULong -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_constant_from_array" + c_yices_mk_bv_constant_from_array :: Ptr YContext -> CUInt -> Ptr CInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_add" + c_yices_mk_bv_add :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_sub" + c_yices_mk_bv_sub :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_mul" + c_yices_mk_bv_mul :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_minus" + c_yices_mk_bv_minus :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_concat" + c_yices_mk_bv_concat :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_and" + c_yices_mk_bv_and :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_or" + c_yices_mk_bv_or :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_xor" + c_yices_mk_bv_xor :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_not" + c_yices_mk_bv_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_extract" + c_yices_mk_bv_extract :: Ptr YContext -> CUInt -> CUInt -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_sign_extend" + c_yices_mk_bv_sign_extend :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_shift_left0" + c_yices_mk_bv_shift_left0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_shift_left1" + c_yices_mk_bv_shift_left1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_shift_right0" + c_yices_mk_bv_shift_right0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_shift_right1" + c_yices_mk_bv_shift_right1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_lt" + c_yices_mk_bv_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_le" + c_yices_mk_bv_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_gt" + c_yices_mk_bv_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_ge" + c_yices_mk_bv_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_slt" + c_yices_mk_bv_slt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_sle" + c_yices_mk_bv_sle :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_sgt" + c_yices_mk_bv_sgt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_mk_bv_sge" + c_yices_mk_bv_sge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) + +-- | Reference: +foreign import ccall unsafe "yices_pp_expr" + c_yices_pp_expr :: Ptr YExpr -> IO () + +-- Iterators + +-- | Reference: +foreign import ccall unsafe "yices_create_var_decl_iterator" + c_yices_create_var_decl_iterator :: Ptr YContext -> IO (Ptr YIterator) + +-- | Reference: +foreign import ccall unsafe "yices_iterator_has_next" + c_yices_iterator_has_next :: Ptr YIterator -> IO CInt + +-- | Reference: +foreign import ccall unsafe "yices_iterator_next" + c_yices_iterator_next :: Ptr YIterator -> IO (Ptr YVarDecl) + +-- | Reference: +foreign import ccall unsafe "yices_iterator_reset" + c_yices_iterator_reset :: Ptr YIterator -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_del_iterator" + c_yices_del_iterator :: Ptr YIterator -> IO () + +-- Accessing declarations + +-- | Reference: +foreign import ccall unsafe "yices_get_var_decl" + c_yices_get_var_decl :: Ptr YExpr -> IO (Ptr YVarDecl) + +-- System information + +-- | Reference: +foreign import ccall unsafe "yices_version" + c_yices_version :: CString + +-- System configuration + +-- | Reference: +foreign import ccall unsafe "yices yices_set_verbosity" + c_yices_set_verbosity :: CInt -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_set_maxsat_initial_cost" + c_yices_set_maxsat_initial_cost :: CLLong -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_set_max_num_conflicts_in_maxsat_iteration" + c_yices_set_max_num_conflicts_in_maxsat_iteration :: CUInt -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_enable_type_checker" + c_yices_enable_type_checker :: CInt -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_set_max_num_iterations_in_maxsat" + c_yices_set_max_num_iterations_in_maxsat :: CUInt -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_set_arith_only" + c_yices_set_arith_only :: CInt -> IO () + +-- | Reference: +foreign import ccall unsafe "yices_enable_log_file" + c_yices_enable_log_file :: CString -> IO () + diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs new file mode 100644 --- /dev/null +++ b/Yices/Painless/Language.hs @@ -0,0 +1,1284 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | +-- Module : Yices.Painless.Language +-- Copyright : (c) Don Stewart 2010 +-- License : BSD3 +-- Maintainer: Don Stewart +-- Stability : experimental +-- +-- This module defines an embedded language of propositions for use by +-- the Yices SMT solver. Propositions are represented as +-- first-order, typed, pure functions with quantified variables +-- in the proposition encoded as (Haskell) variables bound at the outer scope. +-- +-- Propositions are represented as higher-order abstract syntax +-- embedded in Haskell. +-- +-- Terms and types are embedded in Haskell, so all the usual type +-- inference and checking works for Yices propositions. +-- +-- /A simple example: bitvectors/ +-- +-- > solve $ \b1 (b2 :: Exp BitVector) +-- > -> b1 + 1 ==* b2 &&* b2 /=* b2 `xor` 7 + (1 + b1) +-- +-- Constructs the AST term: +-- +-- > \x1 x0 -> (&&*) ((==*) ((+) (x1, 0b1), x0), +-- > (/=*) (x0, (+) (xor (x0, 0b111), (+) (0b1, x1)))) +-- +-- And the satisfying assignment: +-- +-- > x0 => 0b101 +-- > x1 => 0b100 +-- > Satisfiable +-- + +module Yices.Painless.Language ( + + -- * Running the solver + solve, + + -- * Building Yices propositions. + Yices, Exp, + + -- ** Scalar introduction + -- constant, + true, false, + + -- ** Arithmetic. + -- $Instances + + -- ** Bit vectors + -- $BitInstances + + -- ** Conditional expressions + (?), + + -- ** Comparisons. + (==*), (/=*), (<*), (<=*), (>*), (>=*), + + -- ** Logical operations. + (&&*), (||*), not, + + -- ** Implication, /n/-ary operations. + (-->), and, or, max, min, + + -- * Design discussion + -- $Notes + + ) where + +import Prelude hiding (not, or, and, min, max) + +import Data.Typeable +import qualified Data.Map as M + +import Data.Bits +import qualified Data.Vector.Storable as V + +import Control.Monad +import Control.Applicative ((<$>)) +import Foreign.Storable (sizeOf) + +import Text.PrettyPrint + +import qualified Yices.Painless.Base as Yices + +import Yices.Painless.Type + +import Yices.Painless.Tuple hiding (Tuple) +import qualified Yices.Painless.Tuple as Tuple + +-- $Notes +-- +-- /Future work/: +-- +-- * Separate 'BitVector's into their own type, so that we can reuse +-- their 'Num' instance, avoiding OverlappingInstances. +-- +-- * BitVectors are sized, yet we do not represent their size at all +-- currently. Size types would let us statically check e.g. bit vector +-- concatenation. +-- +-- * BitVectors are represented under the hood as 'Vector Bool'. Yices +-- supports construction also via a 'Word' literal. Support both forms +-- (similar to the 'Integer' type) +-- +-- * A 'Monoid' instance for bit vectors? +-- +-- * Support other numeric types. +-- +-- * Support function types in the core language. +-- +-- * Support more Yices types: tuples, records, recursive types. +-- + + +------------------------------------------------------------------------ +-- Language + +-- We use the dictionary view of overloaded operations (such as arithmetic and +-- bit manipulation) to reify such expressions. With non-overloaded +-- operations (such as, the logical connectives) and partially overloaded +-- operations (such as comparisons), we use the standard operator names with a +-- '*' attached. We keep the standard alphanumeric names as they can be +-- easily qualified. + +-- Methods from H98 classes, where we need other signatures + +infix 4 ==*, /=*, <*, <=*, >*, >=* + +-- | Equality lifted into Yices expressions. +-- +(==*) :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +(==*) = mkEq + +-- |Inequality lifted into Yices expressions. +-- +(/=*) :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +(/=*) = mkNEq + +-- | '<' lifted into Yices expressions. +-- +(<*) :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +(<*) = mkLt + +-- | '<=' lifted into Yices expressions. +-- +(>=*) :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +(>=*) = mkGtEq + +-- | '>' lifted into Yices expressions. +-- +(>*) :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +(>*) = mkGt + +-- | '<=' lifted into Yices expressions. +-- +(<=*) :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +(<=*) = mkLtEq + +-- Conditional expressions +-- ----------------------- + +-- |Conditional expression. +-- +infix 0 ? +(?) :: Exp Bool -> (Exp t, Exp t) -> Exp t +c ? (t, e) = Cond c t e + +-- Non-overloaded standard functions, where we need other signatures +-- ----------------------------------------------------------------- + +-- |Conjunction +-- +infixr 3 &&* +(&&*) :: Exp Bool -> Exp Bool -> Exp Bool +(&&*) = mkLAnd + +-- |Disjunction +-- +infixr 2 ||* +(||*) :: Exp Bool -> Exp Bool -> Exp Bool +(||*) = mkLOr + +-- | 'and' returns the conjunction of a Boolean list. +and :: [Exp Bool] -> Exp Bool +and = foldr (&&*) true + +-- | 'or' returns the disjunction of a Boolean list. +or :: [Exp Bool] -> Exp Bool +or = foldr (||*) false + +-- TODO: implement in terms of underlying primitive conjunction and +-- disjunction, which accepts lists. + +-- |Negation +-- +not :: Exp Bool -> Exp Bool +not = mkLNot + +-- | Implication +infixr 1 --> +(-->) :: Exp Bool -> Exp Bool -> Exp Bool +x --> y = not x ||* y + +------------------------------------------------------------------------ + +{- +instance (IsScalar t) => Enum (Exp t) +-- succ = mkSucc +-- pred = mkPred + -- FIXME: ops +-} + +instance (IsScalar t) => Prelude.Eq (Exp t) where + -- FIXME: instance makes no sense with standard signatures + (==) = error "Prelude.Eq.== applied to EDSL types" + +instance (IsScalar t) => Prelude.Ord (Exp t) where + -- FIXME: instance makes no sense with standard signatures + compare = error "Prelude.Ord.compare applied to EDSL types" + +------------------------------------------------------------------------ +-- Bit vector operations + +-- /TODO/ Vector Bool isn't an instance of num, but abstract Exp BitVectors are! +-- +-- We could have an instance of Num BitVector and overload the operators. +-- via the Num (Exp a) instance. +-- + +instance Num (Exp BitVector) where + (+) = mkBVAdd + (-) = mkBVSub + (*) = mkBVMul + negate = mkBVNeg + + fromInteger n = constant . BitVector $ + V.generate (8 * sizeOf (undefined :: Word)) (testBit w) + where + w :: Word + w = fromIntegral n + + abs _ = error "Prelude.Num.abs applied to EDSL types" + -- if n >= 0 then n else negate n + signum _ = error "Prelude.Num.signum applied to EDSL types" + + -- TODO: fromInteger should probably build from mkBVConstant + -- TOD0: need size information. + -- TOD0: support construction of a specific size + +-- TODO monoid instance +-- instance Monoid (Exp BitVector) where + -- mappend = mkBVAppend + -- needs size types! + +-- $BitInstances +-- The 'Exp BitVector' type is an instance of 'Bits', allowing the usual +-- Haskell bitwise operators to be used to construct propositions involving +-- bitwise operations on bit vectors. +-- +-- > (.&,), (.|.), xor, complement, shiftL, shiftR +-- +-- Currently bit vectors are fixed at 'sizeOf (undefined :: Word)' bits. +-- +-- Bit vector constants can be constructed using overloaded numeric +-- literals. +-- + +instance Bits (Exp BitVector) where + (.&.) = mkBVAnd + (.|.) = mkBVOr + xor = mkBVXor + complement = mkBVNot + shiftL = mkBVShiftL0 + shiftR = mkBVShiftR0 + isSigned _ = False + bitSize _ = 8 * sizeOf (undefined :: Word) -- TODO! size type + + +------------------------------------------------------------------------ + +-- $Instances +-- 'Exp' is an instance of 'Num' at the usual types. +-- +-- > (+) :: IsNum t => Exp t -> Exp t -> Exp t +-- +-- > (-) :: IsNum t => Exp t -> Exp t -> Exp t +-- +-- > (*) :: IsNum t => Exp t -> Exp t -> Exp t +-- +-- > negate :: IsNum t => Exp t -> Exp t +-- +-- Numeric literals are overloaded at Exp t type, so you may write, e.g. +-- +-- In addition, 'Exp BitVector' allows for bit vector arithmetic +-- instances. +-- + +instance (IsNum t) => Num (Exp t) where + (+) = mkAdd + (-) = mkSub + (*) = mkMul + + negate x = 0 - x + + abs _ = error "Prelude.Num.abs applied to EDSL types" + -- if n >= 0 then n else negate n + signum _ = error "Prelude.Num.signum applied to EDSL types" + +{- + signum n | n < 0 = negate 1 + | n == 0 = 0 + | otherwise = 1 +-} + + fromInteger = constant . fromInteger + +{- + +instance (Elem t, IsNum t, IsIntegral t) => Bits (Exp t) where + (.&.) = mkBAnd + (.|.) = mkBOr + xor = mkBXor + complement = mkBNot + +-} + +------------------------------------------------------------------------ + +-- |Determine the maximum of two scalars. +max :: IsScalar t => Exp t -> Exp t -> Exp t +max x y = x <* y ? (y , x) + +-- |Determine the minimum of two scalars. +min :: IsScalar t => Exp t -> Exp t -> Exp t +min x y = x <* y ? (x , y) + +------------------------------------------------------------------------ +-- Smart + +-- This modules defines the AST of the user-visible embedded language using +-- more convenient higher-order abstract syntax (instead of de Bruijn +-- indices). Moreover, it defines smart constructors to construct programs. + +-- Bit vector operators + +mkBVAdd :: Exp BitVector -> Exp BitVector -> Exp BitVector +mkBVAdd x y = PrimBVAdd `PrimApp` tup2 (x, y) + +mkBVMul :: Exp BitVector -> Exp BitVector -> Exp BitVector +mkBVMul x y = PrimBVMul `PrimApp` tup2 (x, y) + +mkBVSub :: Exp BitVector -> Exp BitVector -> Exp BitVector +mkBVSub x y = PrimBVSub `PrimApp` tup2 (x, y) + +mkBVNeg :: Exp BitVector -> Exp BitVector +mkBVNeg x = PrimBVNeg `PrimApp` x + +mkBVAnd :: Exp BitVector -> Exp BitVector -> Exp BitVector +mkBVAnd x y = PrimBVAnd `PrimApp` tup2 (x, y) + +mkBVOr :: Exp BitVector -> Exp BitVector -> Exp BitVector +mkBVOr x y = PrimBVOr `PrimApp` tup2 (x, y) + +mkBVXor :: Exp BitVector -> Exp BitVector -> Exp BitVector +mkBVXor x y = PrimBVXor `PrimApp` tup2 (x, y) + +mkBVNot :: Exp BitVector -> Exp BitVector +mkBVNot x = PrimBVNot `PrimApp` x + +mkBVShiftL0 :: Exp BitVector -> Int -> Exp BitVector +mkBVShiftL0 x n = PrimBVSL0 `PrimApp` tup2 (x, constant n) -- lift the int shift. + +mkBVShiftR0 :: Exp BitVector -> Int -> Exp BitVector +mkBVShiftR0 x n = PrimBVSR0 `PrimApp` tup2 (x, constant n) -- shiftR fills with 0 + +-- Operators from Num + +mkAdd :: (IsNum t) => Exp t -> Exp t -> Exp t +mkAdd x y = PrimAdd numType `PrimApp` tup2 (x, y) + +mkSub :: (IsNum t) => Exp t -> Exp t -> Exp t +mkSub x y = PrimSub numType `PrimApp` tup2 (x, y) + +mkMul :: (IsNum t) => Exp t -> Exp t -> Exp t +mkMul x y = PrimMul numType `PrimApp` tup2 (x, y) + +-- Relational and equality operators + +mkLt :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +mkLt x y = PrimLt scalarType `PrimApp` tup2 (x, y) + +mkGt :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +mkGt x y = PrimGt scalarType `PrimApp` tup2 (x, y) + +mkLtEq :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +mkLtEq x y = PrimLtEq scalarType `PrimApp` tup2 (x, y) + +mkGtEq :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +mkGtEq x y = PrimGtEq scalarType `PrimApp` tup2 (x, y) + +mkEq :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +mkEq x y = PrimEq scalarType `PrimApp` tup2 (x, y) + +mkNEq :: (IsScalar t) => Exp t -> Exp t -> Exp Bool +mkNEq x y = PrimNEq scalarType `PrimApp` tup2 (x, y) + +-- Logical operators + +mkLAnd :: Exp Bool -> Exp Bool -> Exp Bool +mkLAnd x y = PrimLAnd `PrimApp` tup2 (x, y) + +mkLOr :: Exp Bool -> Exp Bool -> Exp Bool +mkLOr x y = PrimLOr `PrimApp` tup2 (x, y) + +mkLNot :: Exp Bool -> Exp Bool +mkLNot x = PrimLNot `PrimApp` x + +-- Smart constructor for literals + +-- | Literal 'True' +true :: Exp Bool +true = constant True + +-- | Literal 'False' +false :: Exp Bool +false = constant False + +-- |Constant scalar expression +-- +constant :: (Show t, IsScalar t) => t -> Exp t +constant = Const + +-- Smart constructor and destructors for tuples + +tup2 :: (Exp a, Exp b) -> Exp (a, b) +tup2 (x1, x2) = Tuple (NilTup `SnocTup` x1 `SnocTup` x2) + +------------------------------------------------------------------------ + +-- Embedded expressions of the surface language + +-- HOAS expressions mirror the constructors of `OpenExp', but with the +-- `Tag' constructor instead of variables in the form of de Bruijn indices. +-- Moreover, HOAS expression use n-tuples and the type class 'Elem' to +-- constrain element types, whereas `OpenExp' uses nested pairs and the +-- GADT 'TupleType'. + +-- +-- Yices programs should be closed wrt. scalar variables. +-- All /variables/ must be 'defined' in Yices before use. +-- Nesting should be ok. So bound under a lambda. +-- +-- To restrict functions to first-order, we separate function +-- abstraction from the main expression type. Functions are represented +-- using de Bruijn indices. + +-- Helpful wrapper +data YicesProg r where + Y :: Yices f r => f -> YicesProg r + +-- +-- Allow embedded functions?? + +-- | Yices scalar formula. +-- +data Exp t where + + -- Needed for conversion to de Bruijn form + Tag :: (IsScalar t) => Int -> Exp t + -- environment size at defining occurrence + + Const :: (Show t, IsScalar t) + => t -> Exp t + + Tuple :: (IsTuple t) + => Tuple.Tuple Exp (TupleRepr t) -> Exp t + + Cond :: Exp Bool -> Exp t -> Exp t -> Exp t + + PrimApp :: PrimFun (a -> r) -> Exp a -> Exp r + +{- + + Lam :: (Typeable s, Typeable t, + Show s, Show t) + => (Term s -> Term t) -> Term (s -> t) + + App :: (Typeable s, Typeable t, + Show s, Show t) + => Term (s -> t) -> Term s -> Term t + + -} + +------------------------------------------------------------------------ + +-- | Well-formed Yices propositions (with /n/ quantified variables). +-- +-- The current design requires all free variables in the proposition to +-- be bound at the outermost level. In higher-order abstract syntax, +-- this represents an n-ary, polyvariadic function. +-- +-- Examples: +-- +-- > true +-- +-- > \(x :: Exp Int) -> x >* 8 &&* x <* 10 +-- +-- > \x y -> x ==* y + 1 +-- +-- The language supports polymorphic scalar and numerical operations, so +-- some explicit type information may be required to resolve overloading. +-- +-- E.g. +-- +-- > > solve $ \x y -> x ==* y + (1 :: Exp Int) +-- > +-- > \x1 x0 -> (==*) (x1, (+) (x0, 1)) +-- > +-- > x0 => 1 +-- > x1 => 2 +-- > Satisfiable +-- +class Yices f r | f -> r where + -- Convert a HOAS fragment into its deBruijn form, binding variables in a typed environment + convert :: Layout env env -> f -> OpenFun env r + +instance Yices (Exp b) b where + -- Convert expressions + convert lyt e = OBody (convertOpenExp lyt e) + +instance (IsScalar a, Yices f r) => Yices (Exp a -> f) (a -> r) where + -- Convert binders, one bind at a time. + convert lyt f = OLam (convert lyt' (f a)) + where + a = Tag (size lyt) + lyt' = inc lyt `PushLayout` ZeroIdx + +------------------------------------------------------------------------ + +-- |Conversion from HOAS to de Bruijn expression AST +-- +-- Based on: +-- +-- * Chakravarty. /Converting a HOAS term GADT into a de Bruijn term GADT/, 2009. +-- +-- + +-- |Convert a closed Yices program. +-- +convertYices :: YicesProg r -> OpenYices r +convertYices (Y f) = OY $ convert EmptyLayout f + +------------------------------------------------------------------------ + +-- |Convert an open expression with a given environment layout. +-- +convertOpenExp :: forall t env. + Layout env env -- scalar environment + -> Exp t -- expression to be converted + -> OpenExp env t +convertOpenExp lyt = cvt + where + cvt :: Exp t' -> OpenExp env t' + cvt (Tag i) = Var (prjIdx (size lyt - i - 1) lyt) -- indexing! + cvt (Const v) = OConst v + cvt (Tuple tup) = OTuple (convertTuple lyt tup) + cvt (Cond e1 e2 e3) = OCond (cvt e1) (cvt e2) (cvt e3) + cvt (PrimApp p e) = OPrimApp p (cvt e) + +-- |Convert a tuple expression +-- +convertTuple :: Layout env env + -> Tuple.Tuple Exp t + -> Tuple.Tuple (OpenExp env) t +convertTuple _lyt NilTup = NilTup +convertTuple lyt (es `SnocTup` e) = convertTuple lyt es `SnocTup` convertOpenExp lyt e + +-- |Convert an expression closed wrt to scalar variables +-- +convertExp :: Exp t -> OExp t +convertExp = convertOpenExp EmptyLayout + +------------------------------------------------------------------------ + +-- | +-- A layout of an environment an entry for each entry of the environment. +-- Each entry in the layout holds the deBruijn index that refers to the +-- corresponding entry in the environment. +-- +-- TODO: explain the two type variables +-- +data Layout env env' where + EmptyLayout :: Layout env () + PushLayout :: Typeable t + => Layout env env' -> Idx env t -> Layout env (env', t) + +-- Project the nth index out of an environment layout. +-- +prjIdx :: forall t env env'. Typeable t => Int -> Layout env env' -> Idx env t +prjIdx 0 (PushLayout _ (ix :: Idx env u)) = case gcast ix of + Just ix' -> ix' + Nothing -> error $ + "EDSL Compiler Type Error.\n" ++ + "Couldn't match expected type `" ++ show (typeOf (undefined :: t)) ++ + "' against inferred type `" ++ show (typeOf (undefined :: u)) ++ "'" + +prjIdx n (PushLayout l _) = prjIdx (n - 1) l +prjIdx _ EmptyLayout = + error "Yices.Painless.Language.prjIdx" "inconsistent valuation" + +-- | More functions on layouts, from +-- +-- + +-- Yield the number of entries in an environment layout +-- +size :: Layout env env' -> Int +size EmptyLayout = 0 +size (PushLayout lyt _) = size lyt + 1 + +-- Add an entry to a layout, incrementing all indices +-- +inc :: Layout env env' -> Layout (env, t) env' +inc EmptyLayout = EmptyLayout +inc (PushLayout lyt ix) = PushLayout (inc lyt) (SuccIdx ix) + +------------------------------------------------------------------------ +-- AST + +-- +-- The embedded language is marginally two-levels. Formula with free variables +-- are bound with Define. Thus Yices programs are closed expressions of yices formula. +-- +-- There is no explicit sharing in the initial AST form, but sharing can be recovered +-- subsequently by common subexpression elimination. +-- +-- TODO: add functions to the Exp type. +-- +-- The AST contains both reified dictionaries and type class constraints. +-- Type classes are used for yices-related functionality that is uniformly +-- available for all supported types. In contrast, reified dictionaries are +-- used for functionality that is only available for certain types, such as +-- arithmetic operations. +-- + +-- | Yices computations parameterized by Yices /variables/ represented with de +-- Bruijn indices. +-- +-- * Scalar functions and expressions embedded in well-formed Yices +-- computations cannot contain free scalar variable indices. The latter +-- cannot be bound in Yices computations, and hence, cannot appear in any +-- well-formed program. +-- +-- The data type is parametrised over the surface types (not the representation +-- type). + +-- data OpenYices a where +-- ODefine :: IsScalar t => Fun (t -> u) -> OpenYices u + +-- | Yices programs with an environment. +-- +data OpenYices t where + OY :: OFun t -> OpenYices t + +-- execF shows nicely how to recurse over the OpenFun structure. + +-- |Function abstraction +-- +data OpenFun env t where + OBody :: OpenExp env t -> OpenFun env t + OLam :: IsScalar a => OpenFun (env, a) t -> OpenFun env (a -> t) + +-- |Function without free scalar variables +-- +type OFun t = OpenFun () t + +-- |Open expressions using de Bruijn indices for variables ranging over tuples +-- of scalars. All code, except Cond, is evaluated eagerly. N-tuples are +-- represented as nested pairs. +-- +-- The data type is parametrised over the surface types (not the representation +-- type). +-- +data OpenExp env t where + + -- Variable index, ranging only over tuples or scalars + Var :: IsScalar t + => Idx env t + -> OpenExp env t + + -- Constant values + OConst :: (Show t, IsScalar t) + => t + -> OpenExp env t + + -- Tuples + OTuple :: (IsTuple t) + => Tuple.Tuple (OpenExp env) (TupleRepr t) + -> OpenExp env t + + -- Conditional expression + OCond :: OpenExp env Bool + -> OpenExp env t + -> OpenExp env t + -> OpenExp env t + + -- Primitive scalar operations + OPrimApp :: PrimFun (a -> r) + -> OpenExp env a + -> OpenExp env r + + +-- |Expression without free scalar variables +-- +type OExp t = OpenExp () t + +------------------------------------------------------------------------ + +-- Typed de Bruijn indices +-- ----------------------- + +-- De Bruijn variable index projecting a specific type from a type +-- environment. Type envionments are nested pairs (..((), t1), t2, ..., tn). +-- +data Idx env t where + ZeroIdx :: Idx (env, t) t + SuccIdx :: Idx env t -> Idx (env, s) t + +-- Environments +-- ------------ + +-- Valuation for an environment +-- +{- +data Val env where +-- Empty :: Val () +-- Push :: Val env -> t -> Val (env, t) + +-- Projection of a value from a valuation using a de Bruijn index +-- +prj :: Idx env t -> Val env -> t +prj ZeroIdx (Push _ v) = v +prj (SuccIdx idx) (Push val _) = prj idx val +prj _ _ = + error "Yices.Painless.Language.prj" "inconsistent valuation" +-} + +-- Convert a typed de Brujin index to the corresponding integer +-- +idxToInt :: Idx env t -> Int +idxToInt ZeroIdx = 0 +idxToInt (SuccIdx idx) = 1 + idxToInt idx + +------------------------------------------------------------------------ +-- AST + +-- |Primitive scalar operations +-- +data PrimFun sig where + -- relational and equality operators + PrimLt :: ScalarType a -> PrimFun ((a, a) -> Bool) + PrimGt :: ScalarType a -> PrimFun ((a, a) -> Bool) + PrimLtEq :: ScalarType a -> PrimFun ((a, a) -> Bool) + PrimGtEq :: ScalarType a -> PrimFun ((a, a) -> Bool) + PrimEq :: ScalarType a -> PrimFun ((a, a) -> Bool) + PrimNEq :: ScalarType a -> PrimFun ((a, a) -> Bool) + + -- operators from Num + PrimAdd :: NumType a -> PrimFun ((a, a) -> a) + PrimSub :: NumType a -> PrimFun ((a, a) -> a) + PrimMul :: NumType a -> PrimFun ((a, a) -> a) + + -- logical operators + PrimLAnd :: PrimFun ((Bool, Bool) -> Bool) + PrimLOr :: PrimFun ((Bool, Bool) -> Bool) + PrimLNot :: PrimFun (Bool -> Bool) + + -- TODO: just use the overloaded instance? + + -- bit vector arithmetic + PrimBVAdd :: PrimFun ((BitVector,BitVector) -> BitVector) + PrimBVSub :: PrimFun ((BitVector,BitVector) -> BitVector) + PrimBVMul :: PrimFun ((BitVector,BitVector) -> BitVector) + PrimBVNeg :: PrimFun (BitVector -> BitVector) + + -- bit vector bit operations + PrimBVAnd :: PrimFun ((BitVector,BitVector) -> BitVector) + PrimBVOr :: PrimFun ((BitVector,BitVector) -> BitVector) + PrimBVXor :: PrimFun ((BitVector,BitVector) -> BitVector) + PrimBVNot :: PrimFun (BitVector -> BitVector) + -- Todo: enforce size constraints. + + PrimBVSL0 :: PrimFun ((BitVector,Int) -> BitVector) + PrimBVSR0 :: PrimFun ((BitVector,Int) -> BitVector) + + -- Others are already overloaded on Eq/Neq/Lt/Lte/Ge/Gte + +-- Bit vector logical operators +{- + mkBVConcat, mkBVExtract, + mkBVSignExtend, + mkBVShiftLeft1, + mkBVShiftRight1, + mkBVSlt, mkBVSle, -- can be interpreted as signed types. + mkBVSgt, mkBVSge, +-} + +------------------------------------------------------------------------ +-- Pretty printing + +-- Generic instance for the AST, to avoid a wrapper type. +instance Yices f r => Show f where + show = show . Y + +instance Show (YicesProg as) where + show = show . convertYices + +instance Show (Exp a) where + show = show . convertExp + +instance Show (OpenYices a) where + show c = render $ prettyYices 0 c + +instance Show (OpenFun env f) where + show f = render $ prettyFun 0 f + +instance Show (OpenExp env t) where + show e = render $ prettyExp 0 noParens e + +------------------------------------------------------------------------ + +prettyYices :: Int -> OpenYices a -> Doc +prettyYices n (OY f) = prettyFun n f + +prettyFun :: Int -> OpenFun env a -> Doc +prettyFun lvl fun = + let (n, bodyDoc) = count fun + in + if n < 0 + then bodyDoc + else + char '\\' <> hsep [text $ "x" ++ show idx | idx <- reverse [0..n]] <+> + text "->" <+> bodyDoc + where + count :: OpenFun env fun -> (Int, Doc) + count (OBody body) = (-1, prettyExp lvl noParens body) + count (OLam fun') = let (n, body) = count fun' in (1 + n, body) + +-- Pretty print an expression. +-- +-- * Apply the wrapping combinator (1st argument) to any compound expressions. +-- +prettyExp :: forall t env . + Int -> (Doc -> Doc) -> OpenExp env t -> Doc + +prettyExp _ _ (Var idx) = text $ "x" ++ show (idxToInt idx) +prettyExp _ _ (OConst v) = text $ show (v :: t) -- dispatch differently for BitVector types +prettyExp lvl _ (OTuple tup) = prettyTuple lvl tup + +-- prettyExp lvl wrap (Prj idx e) +-- = wrap $ prettyTupleIdx idx <+> prettyExp lvl parens e + +prettyExp lvl wrap (OCond c t e) + = wrap $ sep [prettyExp lvl parens c <+> char '?', + parens (prettyExp lvl noParens t <> comma <+> + prettyExp lvl noParens e)] + +prettyExp lvl wrap (OPrimApp p a) + = wrap $ prettyPrim p <+> prettyExp lvl parens a + +-- Pretty print nested pairs as a proper tuple. +-- +prettyTuple :: Int -> Tuple.Tuple (OpenExp env) t -> Doc +prettyTuple lvl e = parens $ sep (map (<> comma) (init es) ++ [last es]) + where + es = collect e + + collect :: Tuple.Tuple (OpenExp env) t -> [Doc] + collect NilTup = [] + collect (SnocTup tup e') = collect tup ++ [prettyExp lvl noParens e'] + +-- Pretty print a primitive operation +-- +prettyPrim :: PrimFun a -> Doc +prettyPrim (PrimAdd _) = text "(+)" +prettyPrim (PrimSub _) = text "(-)" +prettyPrim (PrimMul _) = text "(*)" +prettyPrim (PrimLt _) = text "(<*)" +prettyPrim (PrimGt _) = text "(>*)" +prettyPrim (PrimLtEq _) = text "(<=*)" +prettyPrim (PrimGtEq _) = text "(>=*)" +prettyPrim (PrimEq _) = text "(==*)" +prettyPrim (PrimNEq _) = text "(/=*)" +prettyPrim PrimLAnd = text "(&&*)" +prettyPrim PrimLOr = text "(||*)" +prettyPrim PrimLNot = text "not" + +-- Overloaded bit vector ops +prettyPrim PrimBVAdd = text "(+)" +prettyPrim PrimBVMul = text "(*)" +prettyPrim PrimBVSub = text "(-)" +prettyPrim PrimBVNeg = text "negate" +prettyPrim PrimBVAnd = text "(.&.)" +prettyPrim PrimBVOr = text "(.|.)" +prettyPrim PrimBVXor = text "xor" +prettyPrim PrimBVNot = text "complement" +prettyPrim PrimBVSL0 = text "shiftL" +prettyPrim PrimBVSR0 = text "shiftR" + +-- Auxilliary pretty printing combinators +-- +noParens :: Doc -> Doc +noParens = id + + +------------------------------------------------------------------------ +-- +-- Execute the AST. +-- +-- TODO: check use of 'Context' is pure. +-- + +-- | Run Yices on a well-formed proposition, returning either a +-- satisfying assignment of variables that makes the proposition hold, or +-- establish that the proposition is unsatisfiable. +-- +solve :: (Yices f r) => f -> IO Yices.Result +solve q' = do + let q = Y q' + c <- Yices.mkContext + Yices.setTypeChecker True + + let t = convertYices q -- bind all the variables + print t + + (g,e) <- execY c t + + Yices.assert c e + +-- Yices.ctxDump c +-- Yices.ppExpr e + + sat <- Yices.check c + case sat of + Yices.Unsatisfiable -> return $ Yices.Unsatisfiable + Yices.Undefined -> return $ Yices.Undefined + Yices.Satisfiable -> do + mm <- Yices.getModel c + case mm of + Nothing -> return Yices.Satisfiable + Just m -> do + + vs <- sequence + [ get m v t' d + | (v,(t',d)) <- M.toList g ] + + forM_ vs (\(n, YValue mv) -> do + putStr (n ++ " => ") + case mv of + Nothing -> putStrLn "_" + Just v -> print v) + + -- print cs + return Yices.Satisfiable + +-- | Retrieving bindings by type +-- +get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (String, YValue) +get m v (YType (ty :: ScalarType t)) d + + | NumScalarType (IntegralNumType (TypeInt _)) <- ty + = do mn <- Yices.getValueInt m d + return (v, YValue mn) + + | NonNumScalarType (TypeBool _) <- ty + = do mn <- Yices.getValueBool m d + return (v, YValue mn) + + | NonNumScalarType (TypeVectorBool _) <- ty + = do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word)) + return (v, YValue $ fmap BitVector mn) + + | otherwise = error "Yices.Painless.get: don't know how to get this type yet" + + +-- | Map free variable names that we come up with to their type and decl +-- in the context. This will then be used to extract solutions after +-- solving. +-- +type YEnv = M.Map String (YType, Yices.Decl) + +data YType = forall a. IsScalar a => YType (ScalarType a) + +data YValue = forall a. (Show a, IsScalar a) => YValue (Maybe a) + +-- +-- To run, +-- +-- * take the Exp +-- * extract the set of declared variables +-- * bind them in a context +-- * evaluate the assertions. +-- +-- return the bindings. +-- +execY :: Yices.Context -> OpenYices t -> IO (YEnv, Yices.Expr) +execY c (OY f) = execF c f + +-- +-- Declaring variables. Begin with a closed Yices program. +-- +execF :: Yices.Context -> OFun t -> IO (YEnv, Yices.Expr) +execF c fn = go fn 0 M.empty + where + go :: OpenFun env u -> Int -> YEnv -> IO (YEnv, Yices.Expr) + go (OBody b) _ g = (,) g <$> exec c b + + -- Numbers + go (OLam (f :: OpenFun (env, a) t)) n g + | ty@(NumScalarType (IntegralNumType (TypeInt _))) <- scalarType :: ScalarType a + = do + let nm = "x" ++ show n -- we get to actually name things + tynm <- Yices.mkType c "int" + d <- Yices.mkVarDecl c nm tynm + go f (n + 1) (M.insert nm (YType ty, d) g) + + -- Booleans + go (OLam (f :: OpenFun (env, a) t)) n g + | ty@(NonNumScalarType (TypeBool _)) <- scalarType :: ScalarType a + = do + let nm = "x" ++ show n + d <- Yices.mkBoolDecl c nm + go f (n + 1) (M.insert nm (YType ty, d) g) + + -- Bit vectors + go (OLam (f :: OpenFun (env, a) t)) n g + | ty@(NonNumScalarType (TypeVectorBool _)) <- scalarType :: ScalarType a + = do + let nm = "x" ++ show n + -- TODO: hack, no size information for bit vectors yet. + -- TODO: show bvs in a better form. + tynm <- Yices.mkBitVectorType c (fromIntegral $ 8 * sizeOf (undefined :: Word)) + d <- Yices.mkVarDecl c nm tynm + go f (n + 1) (M.insert nm (YType ty, d) g) + + + go _ _ _ = error "Yices.execF: don't know how to bind variables of this type yet" + +-- | Execute an expression with free variables. +-- +-- /TODO:/ +-- +-- * support bit vector operations. +-- +-- * function application and creation other than at the top level +-- +-- * Rational, Double types. +-- +-- * Tuples +-- +exec :: forall env t. Yices.Context -> OpenExp env t -> IO Yices.Expr + +-- GADTs are magic +exec c (OConst n) + | NumScalarType (IntegralNumType (TypeInt _)) <- scalarType :: ScalarType t + = Yices.mkNum c n + + | NonNumScalarType (TypeBool _) <- scalarType :: ScalarType t + = if n then Yices.mkTrue c + else Yices.mkFalse c + + | NonNumScalarType (TypeVectorBool _) <- scalarType :: ScalarType t + = Yices.mkBVConstantFromVector c (unBV n) + + +exec c (Var i) = do + let n = "x" ++ show (idxToInt i) +-- print n + + v <- Yices.getVarDeclFromName c n -- sneaky. using Yices environment. TODO: use YEnv + case v of + Nothing -> error "Undefined variable" + Just d -> Yices.mkVarFromDecl c d + +-- Conditionals +exec c (OCond b t e) = do + eb <- exec c b + et <- exec c t + ee <- exec c e + Yices.mkIte c eb et ee + +-- Works on bitvectors straight up. +exec c (OPrimApp (PrimEq _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkEq c e1 e2 + +-- Ok for bitvectors +exec c (OPrimApp (PrimNEq _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkNeq c e1 e2 + +-- Specialize for BitVector first +exec c (OPrimApp (PrimLt (NonNumScalarType (TypeVectorBool _))) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVLt c e1 e2 + +-- Only numeric types? +exec c (OPrimApp (PrimLt _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkLt c e1 e2 + +-- Specialize for BitVector first +exec c (OPrimApp (PrimLtEq (NonNumScalarType (TypeVectorBool _))) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVLe c e1 e2 + +exec c (OPrimApp (PrimLtEq _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkLe c e1 e2 + +-- Specialize for BitVector first +exec c (OPrimApp (PrimGt (NonNumScalarType (TypeVectorBool _))) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVGt c e1 e2 + +exec c (OPrimApp (PrimGt _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkGt c e1 e2 + +-- TODO think about what gets through the overloading incorrectly. +-- Specialize for BitVector first +exec c (OPrimApp (PrimGtEq (NonNumScalarType (TypeVectorBool _))) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVGe c e1 e2 + +exec c (OPrimApp (PrimGtEq _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkGe c e1 e2 + +exec c (OPrimApp PrimLAnd + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkAnd c [e1, e2] + +exec c (OPrimApp PrimLOr + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkOr c [e1, e2] + +exec c (OPrimApp PrimLNot x) = do + e <- exec c x + Yices.mkNot c e + +-- Numerical operations + +exec c (OPrimApp (PrimAdd _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkSum c [e1,e2] + +exec c (OPrimApp (PrimSub _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkSub c [e1,e2] + +exec c (OPrimApp (PrimMul _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkMul c [e1,e2] + +------------------------------------------------------------------------ +-- Bit Vector operations + +exec c (OPrimApp PrimBVAdd + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVAdd c e1 e2 + +exec c (OPrimApp PrimBVMul + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVMul c e1 e2 + +exec c (OPrimApp PrimBVSub + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVSub c e1 e2 + +exec c (OPrimApp PrimBVNeg + (OTuple (NilTup `SnocTup` x1))) = do + e1 <- exec c x1 + Yices.mkBVMinus c e1 + +exec c (OPrimApp PrimBVAnd + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVAnd c e1 e2 + +exec c (OPrimApp PrimBVOr + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVOr c e1 e2 + +exec c (OPrimApp PrimBVXor + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do + e1 <- exec c x1 + e2 <- exec c x2 + Yices.mkBVXor c e1 e2 + +exec c (OPrimApp PrimBVNot + (OTuple (NilTup `SnocTup` x1))) = do + e1 <- exec c x1 + Yices.mkBVNot c e1 + +exec c (OPrimApp PrimBVSL0 + (OTuple (NilTup `SnocTup` x1 `SnocTup` (OConst n)))) = do + e1 <- exec c x1 + Yices.mkBVShiftLeft0 c e1 n + +exec c (OPrimApp PrimBVSR0 + (OTuple (NilTup `SnocTup` x1 `SnocTup` (OConst n)))) = do + e1 <- exec c x1 + Yices.mkBVShiftRight0 c e1 n + +exec _ _ = error "Not implemented" + +{- + _ (Tuple _) + _ (Const _) + _ (PrimApp (PrimEq _) (Const _)) +-} + +-- exec _ e = error (show e) + +{- +evalTuple :: Tuple (OpenExp env aenv) t -> Val env -> Val aenv -> t +evalTuple NilTup _env _aenv = () +evalTuple (tup `SnocTup` e) env aenv = (evalTuple tup env aenv, + evalOpenExp e env aenv) +-} diff --git a/Yices/Painless/Tuple.hs b/Yices/Painless/Tuple.hs new file mode 100644 --- /dev/null +++ b/Yices/Painless/Tuple.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE GADTs, TypeFamilies, FlexibleInstances #-} +{-# OPTIONS_HADDOCK hide #-} + +-- Module : Yices.Painless.Tuple +-- Copyright : [2009..2010] Manuel M T Chakravarty, Gabriele Keller, Sean Lee +-- 2010 Don Stewart +-- License : BSD3 +-- +-- Maintainer : Don Stewart +-- Stability : experimental +-- Portability : non-portable (GHC extensions) +-- +-- Our representation of tuples are heterogenous snoc lists, which are typed +-- by type lists, where '()' and '(,)' are type-level nil and snoc, +-- respectively. The components may only be drawn from types that can be +-- used as array elements. + +module Yices.Painless.Tuple ( + + -- * Tuple representation + Tuple(..), TupleIdx(..), IsTuple(..) + +) where + +-- Tuple representation +-- -------------------- + +-- |We represent tuples as heterogenous lists, typed by a type list. +-- +data Tuple c t where + NilTup :: Tuple c () + SnocTup :: Tuple c s -> c t -> Tuple c (s, t) + +-- |Type-safe projection indicies for tuples. +-- +-- NB: We index tuples by starting to count from the *right*! +-- +data TupleIdx t e where + ZeroTupIdx :: TupleIdx (t, s) s + SuccTupIdx :: TupleIdx t e -> TupleIdx (t, s) e + +-- |Conversion between surface n-tuples and our tuple representation. +-- +class IsTuple tup where + type TupleRepr tup + fromTuple :: tup -> TupleRepr tup + toTuple :: TupleRepr tup -> tup + +instance IsTuple (a, b) where + type TupleRepr (a, b) = (((), a), b) + fromTuple (x, y) = (((), x), y) + toTuple (((), x), y) = (x, y) + +instance IsTuple (a, b, c) where + type TupleRepr (a, b, c) = (TupleRepr (a, b), c) + fromTuple (x, y, z) = ((((), x), y), z) + toTuple ((((), x), y), z) = (x, y, z) + +instance IsTuple (a, b, c, d) where + type TupleRepr (a, b, c, d) = (TupleRepr (a, b, c), d) + fromTuple (x, y, z, v) = (((((), x), y), z), v) + toTuple (((((), x), y), z), v) = (x, y, z, v) + +instance IsTuple (a, b, c, d, e) where + type TupleRepr (a, b, c, d, e) = (TupleRepr (a, b, c, d), e) + fromTuple (x, y, z, v, w) = ((((((), x), y), z), v), w) + toTuple ((((((), x), y), z), v), w) = (x, y, z, v, w) + +instance IsTuple (a, b, c, d, e, f) where + type TupleRepr (a, b, c, d, e, f) = (TupleRepr (a, b, c, d, e), f) + fromTuple (x, y, z, v, w, r) = (((((((), x), y), z), v), w), r) + toTuple (((((((), x), y), z), v), w), r) = (x, y, z, v, w, r) + +instance IsTuple (a, b, c, d, e, f, g) where + type TupleRepr (a, b, c, d, e, f, g) = (TupleRepr (a, b, c, d, e, f), g) + fromTuple (x, y, z, v, w, r, s) = ((((((((), x), y), z), v), w), r), s) + toTuple ((((((((), x), y), z), v), w), r), s) = (x, y, z, v, w, r, s) + +instance IsTuple (a, b, c, d, e, f, g, h) where + type TupleRepr (a, b, c, d, e, f, g, h) = (TupleRepr (a, b, c, d, e, f, g), h) + fromTuple (x, y, z, v, w, r, s, t) = (((((((((), x), y), z), v), w), r), s), t) + toTuple (((((((((), x), y), z), v), w), r), s), t) = (x, y, z, v, w, r, s, t) + +instance IsTuple (a, b, c, d, e, f, g, h, i) where + type TupleRepr (a, b, c, d, e, f, g, h, i) = (TupleRepr (a, b, c, d, e, f, g, h), i) + fromTuple (x, y, z, v, w, r, s, t, u) + = ((((((((((), x), y), z), v), w), r), s), t), u) + toTuple ((((((((((), x), y), z), v), w), r), s), t), u) + = (x, y, z, v, w, r, s, t, u) + diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs new file mode 100644 --- /dev/null +++ b/Yices/Painless/Type.hs @@ -0,0 +1,627 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE DeriveDataTypeable #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_HADDOCK hide #-} + +-- Module : Yices.Painless.Type +-- Copyright : [2008..2010] Manuel M T Chakravarty, Gabriele Keller, Sean Lee +-- 2010 Don Stewart +-- License : BSD3 +-- +-- Maintainer : Don Stewart +-- Portability : non-portable (GHC extensions) +-- +-- /Scalar types supported in Yices SMT computations/ +-- +-- Integral types: Int, Int8, Int16, Int32, Int64, Word, Word8, Word16, Word32, +-- Word64, CShort, CUShort, CInt, CUInt, CLong, CULong, CLLong, CULLong +-- +-- Floating types: Float, Double, CFloat, CDouble +-- +-- Non-numeric types: Bool, Char, CChar, CSChar, CUChar +-- +-- 'Int' has the same bitwidth as in plain Haskell computations, and 'Float' +-- and 'Double' represent IEEE single and double precision floating point +-- numbers, respectively. +-- +-- TODO: support bit vectors +-- +module Yices.Painless.Type ( + + module Data.Int, + module Data.Word, + module Foreign.C.Types, + module Yices.Painless.Type + +) where + +-- standard libraries +import Data.Bits +import Data.Int +import Data.Typeable +import Data.Word +import Foreign.C.Types ( + CChar, CSChar, CUChar, CShort, CUShort, CInt, CUInt, CLong, CULong, + CLLong, CULLong, CFloat, CDouble) + -- in the future, CHalf + +import Foreign.Storable (sizeOf) +import Numeric +import Data.Char (intToDigit) +import qualified Data.Vector.Storable as V + +{- +-- Extend Typeable support for 8- and 9-tuple +-- ------------------------------------------ + +class Typeable8 t where + typeOf8 :: t a b c d e f g h -> TypeRep + +instance Typeable8 (,,,,,,,) where + typeOf8 _ = mkTyCon "(,,,,,,,)" `mkTyConApp` [] + +typeOf7Default :: (Typeable8 t, Typeable a) => t a b c d e f g h -> TypeRep +typeOf7Default x = typeOf7 x `mkAppTy` typeOf (argType x) + where + argType :: t a b c d e f g h -> a + argType = undefined + +instance (Typeable8 s, Typeable a) + => Typeable7 (s a) where + typeOf7 = typeOf7Default + +class Typeable9 t where + typeOf9 :: t a b c d e f g h i -> TypeRep + +instance Typeable9 (,,,,,,,,) where + typeOf9 _ = mkTyCon "(,,,,,,,,)" `mkTyConApp` [] + +typeOf8Default :: (Typeable9 t, Typeable a) => t a b c d e f g h i -> TypeRep +typeOf8Default x = typeOf8 x `mkAppTy` typeOf (argType x) + where + argType :: t a b c d e f g h i -> a + argType = undefined + +instance (Typeable9 s, Typeable a) + => Typeable8 (s a) where + typeOf8 = typeOf8Default +-} + + +-- Scalar types +-- ------------ + +-- Reified dictionaries +-- + +data IntegralDict a where + IntegralDict :: ( Bounded a, Enum a, Eq a, Ord a, Show a + , Bits a, Integral a, Num a, Real a) + => IntegralDict a + +data FloatingDict a where + FloatingDict :: ( Enum a, Eq a, Ord a, Show a + , Floating a, Fractional a, Num a, Real a, RealFrac a + , RealFloat a) + => FloatingDict a + +data NonNumDict a where + NonNumDict :: (Eq a, Ord a, Show a) + => NonNumDict a + +-- Scalar type representation +-- + +-- |Integral types supported in yices computations. +-- +data IntegralType a where + TypeInt :: IntegralDict Int -> IntegralType Int + TypeInt8 :: IntegralDict Int8 -> IntegralType Int8 + TypeInt16 :: IntegralDict Int16 -> IntegralType Int16 + TypeInt32 :: IntegralDict Int32 -> IntegralType Int32 + TypeInt64 :: IntegralDict Int64 -> IntegralType Int64 + TypeWord :: IntegralDict Word -> IntegralType Word + TypeWord8 :: IntegralDict Word8 -> IntegralType Word8 + TypeWord16 :: IntegralDict Word16 -> IntegralType Word16 + TypeWord32 :: IntegralDict Word32 -> IntegralType Word32 + TypeWord64 :: IntegralDict Word64 -> IntegralType Word64 + TypeCShort :: IntegralDict CShort -> IntegralType CShort + TypeCUShort :: IntegralDict CUShort -> IntegralType CUShort + TypeCInt :: IntegralDict CInt -> IntegralType CInt + TypeCUInt :: IntegralDict CUInt -> IntegralType CUInt + TypeCLong :: IntegralDict CLong -> IntegralType CLong + TypeCULong :: IntegralDict CULong -> IntegralType CULong + TypeCLLong :: IntegralDict CLLong -> IntegralType CLLong + TypeCULLong :: IntegralDict CULLong -> IntegralType CULLong + +-- |Floating-point types supported in yices computations. +-- +data FloatingType a where + TypeFloat :: FloatingDict Float -> FloatingType Float + TypeDouble :: FloatingDict Double -> FloatingType Double + TypeCFloat :: FloatingDict CFloat -> FloatingType CFloat + TypeCDouble :: FloatingDict CDouble -> FloatingType CDouble + +-- |Non-numeric types supported in yices computations. +-- +data NonNumType a where + TypeBool :: NonNumDict Bool -> NonNumType Bool -- marshaled to CInt + TypeChar :: NonNumDict Char -> NonNumType Char + TypeCChar :: NonNumDict CChar -> NonNumType CChar + TypeCSChar :: NonNumDict CSChar -> NonNumType CSChar + TypeCUChar :: NonNumDict CUChar -> NonNumType CUChar + + -- Could define a Num instance + TypeVectorBool :: NonNumDict BitVector -> NonNumType BitVector + + +------------------------------------------------------------------------ + +-- Todo: support 'Word' packed representation (for fast constants). +newtype BitVector = BitVector { unBV :: V.Vector Bool } + deriving (Eq, Ord, Typeable) + +-- Smart show instance. +instance Show BitVector where + show (BitVector v) + | r <= 65535 = "0b" ++ showIntAtBase 2 intToDigit r [] + | otherwise = "0x" ++ showHex r [] + where + r = foldr (\i b -> if v V.! i then setBit b i else clearBit b i) w [0 .. n-1] + w = 0 :: Word + n = 8 * sizeOf w + +------------------------------------------------------------------------ + +-- |Numeric element types implement Num & Real +-- +data NumType a where + IntegralNumType :: IntegralType a -> NumType a + FloatingNumType :: FloatingType a -> NumType a + +-- |Bounded element types implement Bounded +-- +data BoundedType a where + IntegralBoundedType :: IntegralType a -> BoundedType a + NonNumBoundedType :: NonNumType a -> BoundedType a + +-- |All scalar element types implement Eq, Ord & Enum +-- +data ScalarType a where + NumScalarType :: NumType a -> ScalarType a + NonNumScalarType :: NonNumType a -> ScalarType a + +-- Showing type names +-- + +instance Show (IntegralType a) where + show (TypeInt _) = "Int" + show (TypeInt8 _) = "Int8" + show (TypeInt16 _) = "Int16" + show (TypeInt32 _) = "Int32" + show (TypeInt64 _) = "Int64" + show (TypeWord _) = "Word" + show (TypeWord8 _) = "Word8" + show (TypeWord16 _) = "Word16" + show (TypeWord32 _) = "Word32" + show (TypeWord64 _) = "Word64" + show (TypeCShort _) = "CShort" + show (TypeCUShort _) = "CUShort" + show (TypeCInt _) = "CInt" + show (TypeCUInt _) = "CUInt" + show (TypeCLong _) = "CLong" + show (TypeCULong _) = "CULong" + show (TypeCLLong _) = "CLLong" + show (TypeCULLong _) = "CULLong" + +instance Show (FloatingType a) where + show (TypeFloat _) = "Float" + show (TypeDouble _) = "Double" + show (TypeCFloat _) = "CFloat" + show (TypeCDouble _) = "CDouble" + +instance Show (NonNumType a) where + show (TypeBool _) = "Bool" + show (TypeChar _) = "Char" + show (TypeCChar _) = "CChar" + show (TypeCSChar _) = "CSChar" + show (TypeCUChar _) = "CUChar" + show (TypeVectorBool _) = "(Vector Bool)" + +instance Show (NumType a) where + show (IntegralNumType ty) = show ty + show (FloatingNumType ty) = show ty + +instance Show (BoundedType a) where + show (IntegralBoundedType ty) = show ty + show (NonNumBoundedType ty) = show ty + +instance Show (ScalarType a) where + show (NumScalarType ty) = show ty + show (NonNumScalarType ty) = show ty + +-- Querying scalar type representations +-- + +-- |Integral types +-- +class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where + integralType :: IntegralType a + +instance IsIntegral Int where + integralType = TypeInt IntegralDict + +instance IsIntegral Int8 where + integralType = TypeInt8 IntegralDict + +instance IsIntegral Int16 where + integralType = TypeInt16 IntegralDict + +instance IsIntegral Int32 where + integralType = TypeInt32 IntegralDict + +instance IsIntegral Int64 where + integralType = TypeInt64 IntegralDict + +instance IsIntegral Word where + integralType = TypeWord IntegralDict + +instance IsIntegral Word8 where + integralType = TypeWord8 IntegralDict + +instance IsIntegral Word16 where + integralType = TypeWord16 IntegralDict + +instance IsIntegral Word32 where + integralType = TypeWord32 IntegralDict + +instance IsIntegral Word64 where + integralType = TypeWord64 IntegralDict + +instance IsIntegral CShort where + integralType = TypeCShort IntegralDict + +instance IsIntegral CUShort where + integralType = TypeCUShort IntegralDict + +instance IsIntegral CInt where + integralType = TypeCInt IntegralDict + +instance IsIntegral CUInt where + integralType = TypeCUInt IntegralDict + +instance IsIntegral CLong where + integralType = TypeCLong IntegralDict + +instance IsIntegral CULong where + integralType = TypeCULong IntegralDict + +instance IsIntegral CLLong where + integralType = TypeCLLong IntegralDict + +instance IsIntegral CULLong where + integralType = TypeCULLong IntegralDict + +-- |Floating types +-- +class (Floating a, IsScalar a, IsNum a) => IsFloating a where + floatingType :: FloatingType a + +instance IsFloating Float where + floatingType = TypeFloat FloatingDict + +instance IsFloating Double where + floatingType = TypeDouble FloatingDict + +instance IsFloating CFloat where + floatingType = TypeCFloat FloatingDict + +instance IsFloating CDouble where + floatingType = TypeCDouble FloatingDict + +-- |Non-numeric types +-- +class IsNonNum a where + nonNumType :: NonNumType a + +instance IsNonNum Bool where + nonNumType = TypeBool NonNumDict + +instance IsNonNum Char where + nonNumType = TypeChar NonNumDict + +instance IsNonNum CChar where + nonNumType = TypeCChar NonNumDict + +instance IsNonNum CSChar where + nonNumType = TypeCSChar NonNumDict + +instance IsNonNum CUChar where + nonNumType = TypeCUChar NonNumDict + +instance IsNonNum BitVector where + nonNumType = TypeVectorBool NonNumDict + +-- |Numeric types +-- +class (Num a, IsScalar a) => IsNum a where + numType :: NumType a + +instance IsNum Int where + numType = IntegralNumType integralType + +instance IsNum Int8 where + numType = IntegralNumType integralType + +instance IsNum Int16 where + numType = IntegralNumType integralType + +instance IsNum Int32 where + numType = IntegralNumType integralType + +instance IsNum Int64 where + numType = IntegralNumType integralType + +instance IsNum Word where + numType = IntegralNumType integralType + +instance IsNum Word8 where + numType = IntegralNumType integralType + +instance IsNum Word16 where + numType = IntegralNumType integralType + +instance IsNum Word32 where + numType = IntegralNumType integralType + +instance IsNum Word64 where + numType = IntegralNumType integralType + +instance IsNum CShort where + numType = IntegralNumType integralType + +instance IsNum CUShort where + numType = IntegralNumType integralType + +instance IsNum CInt where + numType = IntegralNumType integralType + +instance IsNum CUInt where + numType = IntegralNumType integralType + +instance IsNum CLong where + numType = IntegralNumType integralType + +instance IsNum CULong where + numType = IntegralNumType integralType + +instance IsNum CLLong where + numType = IntegralNumType integralType + +instance IsNum CULLong where + numType = IntegralNumType integralType + +instance IsNum Float where + numType = FloatingNumType floatingType + +instance IsNum Double where + numType = FloatingNumType floatingType + +instance IsNum CFloat where + numType = FloatingNumType floatingType + +instance IsNum CDouble where + numType = FloatingNumType floatingType + +-- |Bounded types +-- +class IsBounded a where + boundedType :: BoundedType a + +instance IsBounded Int where + boundedType = IntegralBoundedType integralType + +instance IsBounded Int8 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Int16 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Int32 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Int64 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Word where + boundedType = IntegralBoundedType integralType + +instance IsBounded Word8 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Word16 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Word32 where + boundedType = IntegralBoundedType integralType + +instance IsBounded Word64 where + boundedType = IntegralBoundedType integralType + +instance IsBounded CShort where + boundedType = IntegralBoundedType integralType + +instance IsBounded CUShort where + boundedType = IntegralBoundedType integralType + +instance IsBounded CInt where + boundedType = IntegralBoundedType integralType + +instance IsBounded CUInt where + boundedType = IntegralBoundedType integralType + +instance IsBounded CLong where + boundedType = IntegralBoundedType integralType + +instance IsBounded CULong where + boundedType = IntegralBoundedType integralType + +instance IsBounded CLLong where + boundedType = IntegralBoundedType integralType + +instance IsBounded CULLong where + boundedType = IntegralBoundedType integralType + +instance IsBounded Bool where + boundedType = NonNumBoundedType nonNumType + +instance IsBounded Char where + boundedType = NonNumBoundedType nonNumType + +instance IsBounded CChar where + boundedType = NonNumBoundedType nonNumType + +instance IsBounded CSChar where + boundedType = NonNumBoundedType nonNumType + +instance IsBounded CUChar where + boundedType = NonNumBoundedType nonNumType + +-- |All scalar type +-- +class Typeable a => IsScalar a where + scalarType :: ScalarType a + +instance IsScalar Int where + scalarType = NumScalarType numType + +instance IsScalar Int8 where + scalarType = NumScalarType numType + +instance IsScalar Int16 where + scalarType = NumScalarType numType + +instance IsScalar Int32 where + scalarType = NumScalarType numType + +instance IsScalar Int64 where + scalarType = NumScalarType numType + +instance IsScalar Word where + scalarType = NumScalarType numType + +instance IsScalar Word8 where + scalarType = NumScalarType numType + +instance IsScalar Word16 where + scalarType = NumScalarType numType + +instance IsScalar Word32 where + scalarType = NumScalarType numType + +instance IsScalar Word64 where + scalarType = NumScalarType numType + +instance IsScalar CShort where + scalarType = NumScalarType numType + +instance IsScalar CUShort where + scalarType = NumScalarType numType + +instance IsScalar CInt where + scalarType = NumScalarType numType + +instance IsScalar CUInt where + scalarType = NumScalarType numType + +instance IsScalar CLong where + scalarType = NumScalarType numType + +instance IsScalar CULong where + scalarType = NumScalarType numType + +instance IsScalar CLLong where + scalarType = NumScalarType numType + +instance IsScalar CULLong where + scalarType = NumScalarType numType + +instance IsScalar Float where + scalarType = NumScalarType numType + +instance IsScalar Double where + scalarType = NumScalarType numType + +instance IsScalar CFloat where + scalarType = NumScalarType numType + +instance IsScalar CDouble where + scalarType = NumScalarType numType + +-- Non-numerical scalar types + +instance IsScalar Bool where + scalarType = NonNumScalarType nonNumType + +instance IsScalar Char where + scalarType = NonNumScalarType nonNumType + +instance IsScalar CChar where + scalarType = NonNumScalarType nonNumType + +instance IsScalar CSChar where + scalarType = NonNumScalarType nonNumType + +instance IsScalar CUChar where + scalarType = NonNumScalarType nonNumType + +instance IsScalar BitVector where + scalarType = NonNumScalarType nonNumType -- false for bitvectors... + +-- Extract reified dictionaries +-- + +integralDict :: IntegralType a -> IntegralDict a +integralDict (TypeInt dict) = dict +integralDict (TypeInt8 dict) = dict +integralDict (TypeInt16 dict) = dict +integralDict (TypeInt32 dict) = dict +integralDict (TypeInt64 dict) = dict +integralDict (TypeWord dict) = dict +integralDict (TypeWord8 dict) = dict +integralDict (TypeWord16 dict) = dict +integralDict (TypeWord32 dict) = dict +integralDict (TypeWord64 dict) = dict +integralDict (TypeCShort dict) = dict +integralDict (TypeCUShort dict) = dict +integralDict (TypeCInt dict) = dict +integralDict (TypeCUInt dict) = dict +integralDict (TypeCLong dict) = dict +integralDict (TypeCULong dict) = dict +integralDict (TypeCLLong dict) = dict +integralDict (TypeCULLong dict) = dict + +floatingDict :: FloatingType a -> FloatingDict a +floatingDict (TypeFloat dict) = dict +floatingDict (TypeDouble dict) = dict +floatingDict (TypeCFloat dict) = dict +floatingDict (TypeCDouble dict) = dict + +nonNumDict :: NonNumType a -> NonNumDict a +nonNumDict (TypeBool dict) = dict +nonNumDict (TypeChar dict) = dict +nonNumDict (TypeCChar dict) = dict +nonNumDict (TypeCSChar dict) = dict +nonNumDict (TypeCUChar dict) = dict +nonNumDict (TypeVectorBool dict) = dict + +-- Tuple type +-- ---------- + +data TupleType a where + UnitTuple :: TupleType () + SingleTuple :: ScalarType a -> TupleType a + PairTuple :: TupleType a -> TupleType b -> TupleType (a, b) + diff --git a/tests/calls.hs b/tests/calls.hs new file mode 100644 --- /dev/null +++ b/tests/calls.hs @@ -0,0 +1,31 @@ +import Yices.Base + +main = do + print version + + setVerbosity 7 + setMaxSatInitialCost 99 + setMaxNumConflictsInMaxSatIteration 100 + setTypeChecker True + setMaxNumIterationsInMaxSat 1000 + setMaxSatInitialCost 200 + setArithmeticOnly True + setLogFile "x.dat" + + c <- empty + reset c + dump c + push c + pop c + print =<< inconsistent c + + print =<< check c + + setVerbosity 0 + print =<< check c + + print =<< getUnsatCoreSize c + + print =<< getModel c + + print =<< getUnsatCore c diff --git a/tests/push-pop.hs b/tests/push-pop.hs new file mode 100644 --- /dev/null +++ b/tests/push-pop.hs @@ -0,0 +1,579 @@ +import Yices.Base + +main = do + c <- empty + push c + push c + push c + push c + pop c + pop c + pop c + pop c + + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + push c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + pop c + dump c diff --git a/yices-painless.cabal b/yices-painless.cabal new file mode 100644 --- /dev/null +++ b/yices-painless.cabal @@ -0,0 +1,71 @@ +Name: yices-painless +Version: 0.1 +Synopsis: An embedded language for programming the Yices SMT solver +Description: + This library defines an embedded language in Haskell for programming + the Yices SMT solver. + . + Yices is an efficient SMT solver that decides the satisfiability of + arbitrary formulas containing uninterpreted function symbols with + equality, linear real and integer arithmetic, scalar types, + recursive datatypes, tuples, records, extensional arrays, fixed-size + bit-vectors, quantifiers, and lambda expressions. Yices also does + MaxSMT (and, dually, unsat cores) and is competitive as an ordinary + SAT and MaxSAT solver. + . + The embedded language embeds both terms and types into Haskell, via + a typed higher-order abstract syntax representation. Propositions in + the embedding are represented as (typed) pure expressions. + . + Solution variables in the proposition (notionally, free variables) + are bound an the outermost lambda term. Propositions constructed + from logical primitives can then be executed by the solver to yield + a satisfying assignment to those free variables in the proposition. + . + More information about Yices: + . + * + . + Low and medium-level bindings to the Yices C API are also provided. + The medium-level bindings add significant type and resource safety + to that which the C API provides. + +Homepage: http://code.haskell.org/~dons/code/yices-painless +License: BSD3 +License-file: LICENSE +Author: Don Stewart +Maintainer: dons@galois.com +Copyright: Don Stewart 2010. +Category: Math, Theorem Provers, Formal Methods +Build-type: Simple +Cabal-version: >=1.2 + +Flag yices-dynamic + default: True + +Library + Exposed-modules: + Yices.Painless.Language + + Yices.Painless.Base + Yices.Painless.Base.C + + Yices.Painless.Type + Yices.Painless.Tuple + + ghc-options: -Wall + + Build-depends: base > 3 && < 5, + pretty, + strict-concurrency, + containers >= 0.2, + vector >= 0.7 + + Build-tools: hsc2hs + Extensions: ForeignFunctionInterface + includes: yices_c.h + extra-libraries: yices + + if flag(yices-dynamic) + extra-libraries: gmp +