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