summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDonaldStewart <>2011-01-15 21:48:10 (GMT)
committerLuite Stegeman <luite@luite.com>2011-01-15 21:48:10 (GMT)
commit387a1531dccd766da6b49b7bd5b03dc688348781 (patch)
tree002c79f47cea3881287451d85eddb609347cc9fa
version 0.10.1
-rw-r--r--LICENSE30
-rw-r--r--Setup.hs2
-rw-r--r--Yices/Painless/Base.hs1560
-rw-r--r--Yices/Painless/Base/C.hsc731
-rw-r--r--Yices/Painless/Language.hs1284
-rw-r--r--Yices/Painless/Tuple.hs90
-rw-r--r--Yices/Painless/Type.hs627
-rw-r--r--tests/calls.hs31
-rw-r--r--tests/push-pop.hs579
-rw-r--r--yices-painless.cabal71
10 files changed, 5005 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..70df6fd
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c)2010, Don Stewart
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of Don Stewart nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Yices/Painless/Base.hs b/Yices/Painless/Base.hs
new file mode 100644
index 0000000..edd6b3f
--- /dev/null
+++ b/Yices/Painless/Base.hs
@@ -0,0 +1,1560 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+-- |
+-- Module : Yices.Painless.Base
+-- Copyright : (c) Galois, Inc. 2010
+-- License : BSD3
+-- Maintainer: Don Stewart <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
diff --git a/Yices/Painless/Base/C.hsc b/Yices/Painless/Base/C.hsc
new file mode 100644
index 0000000..d568855
--- /dev/null
+++ b/Yices/Painless/Base/C.hsc
@@ -0,0 +1,731 @@
+{-# LANGUAGE ForeignFunctionInterface #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- |
+-- Module : Yices.Painless.Base.C
+-- Copyright : (c) Galois, Inc. 2010
+-- License : BSD3
+-- Maintainer: Don Stewart <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 ()
+
diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs
new file mode 100644
index 0000000..eaf56cd
--- /dev/null
+++ b/Yices/Painless/Language.hs
@@ -0,0 +1,1284 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- |
+-- Module : Yices.Painless.Language
+-- Copyright : (c) Don Stewart 2010
+-- License : BSD3
+-- Maintainer: Don Stewart <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)
+-}
diff --git a/Yices/Painless/Tuple.hs b/Yices/Painless/Tuple.hs
new file mode 100644
index 0000000..cfbab12
--- /dev/null
+++ b/Yices/Painless/Tuple.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE GADTs, TypeFamilies, FlexibleInstances #-}
+{-# OPTIONS_HADDOCK hide #-}
+
+-- Module : Yices.Painless.Tuple
+-- Copyright : [2009..2010] Manuel M T Chakravarty, Gabriele Keller, Sean Lee
+-- 2010 Don Stewart
+-- License : BSD3
+--
+-- Maintainer : Don Stewart
+-- Stability : experimental
+-- Portability : non-portable (GHC extensions)
+--
+-- Our representation of tuples are heterogenous snoc lists, which are typed
+-- by type lists, where '()' and '(,)' are type-level nil and snoc,
+-- respectively. The components may only be drawn from types that can be
+-- used as array elements.
+
+module Yices.Painless.Tuple (
+
+ -- * Tuple representation
+ Tuple(..), TupleIdx(..), IsTuple(..)
+
+) where
+
+-- Tuple representation
+-- --------------------
+
+-- |We represent tuples as heterogenous lists, typed by a type list.
+--
+data Tuple c t where
+ NilTup :: Tuple c ()
+ SnocTup :: Tuple c s -> c t -> Tuple c (s, t)
+
+-- |Type-safe projection indicies for tuples.
+--
+-- NB: We index tuples by starting to count from the *right*!
+--
+data TupleIdx t e where
+ ZeroTupIdx :: TupleIdx (t, s) s
+ SuccTupIdx :: TupleIdx t e -> TupleIdx (t, s) e
+
+-- |Conversion between surface n-tuples and our tuple representation.
+--
+class IsTuple tup where
+ type TupleRepr tup
+ fromTuple :: tup -> TupleRepr tup
+ toTuple :: TupleRepr tup -> tup
+
+instance IsTuple (a, b) where
+ type TupleRepr (a, b) = (((), a), b)
+ fromTuple (x, y) = (((), x), y)
+ toTuple (((), x), y) = (x, y)
+
+instance IsTuple (a, b, c) where
+ type TupleRepr (a, b, c) = (TupleRepr (a, b), c)
+ fromTuple (x, y, z) = ((((), x), y), z)
+ toTuple ((((), x), y), z) = (x, y, z)
+
+instance IsTuple (a, b, c, d) where
+ type TupleRepr (a, b, c, d) = (TupleRepr (a, b, c), d)
+ fromTuple (x, y, z, v) = (((((), x), y), z), v)
+ toTuple (((((), x), y), z), v) = (x, y, z, v)
+
+instance IsTuple (a, b, c, d, e) where
+ type TupleRepr (a, b, c, d, e) = (TupleRepr (a, b, c, d), e)
+ fromTuple (x, y, z, v, w) = ((((((), x), y), z), v), w)
+ toTuple ((((((), x), y), z), v), w) = (x, y, z, v, w)
+
+instance IsTuple (a, b, c, d, e, f) where
+ type TupleRepr (a, b, c, d, e, f) = (TupleRepr (a, b, c, d, e), f)
+ fromTuple (x, y, z, v, w, r) = (((((((), x), y), z), v), w), r)
+ toTuple (((((((), x), y), z), v), w), r) = (x, y, z, v, w, r)
+
+instance IsTuple (a, b, c, d, e, f, g) where
+ type TupleRepr (a, b, c, d, e, f, g) = (TupleRepr (a, b, c, d, e, f), g)
+ fromTuple (x, y, z, v, w, r, s) = ((((((((), x), y), z), v), w), r), s)
+ toTuple ((((((((), x), y), z), v), w), r), s) = (x, y, z, v, w, r, s)
+
+instance IsTuple (a, b, c, d, e, f, g, h) where
+ type TupleRepr (a, b, c, d, e, f, g, h) = (TupleRepr (a, b, c, d, e, f, g), h)
+ fromTuple (x, y, z, v, w, r, s, t) = (((((((((), x), y), z), v), w), r), s), t)
+ toTuple (((((((((), x), y), z), v), w), r), s), t) = (x, y, z, v, w, r, s, t)
+
+instance IsTuple (a, b, c, d, e, f, g, h, i) where
+ type TupleRepr (a, b, c, d, e, f, g, h, i) = (TupleRepr (a, b, c, d, e, f, g, h), i)
+ fromTuple (x, y, z, v, w, r, s, t, u)
+ = ((((((((((), x), y), z), v), w), r), s), t), u)
+ toTuple ((((((((((), x), y), z), v), w), r), s), t), u)
+ = (x, y, z, v, w, r, s, t, u)
+
diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs
new file mode 100644
index 0000000..a4e56a8
--- /dev/null
+++ b/Yices/Painless/Type.hs
@@ -0,0 +1,627 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# OPTIONS_HADDOCK hide #-}
+
+-- Module : Yices.Painless.Type
+-- Copyright : [2008..2010] Manuel M T Chakravarty, Gabriele Keller, Sean Lee
+-- 2010 Don Stewart
+-- License : BSD3
+--
+-- Maintainer : Don Stewart
+-- Portability : non-portable (GHC extensions)
+--
+-- /Scalar types supported in Yices SMT computations/
+--
+-- Integral types: Int, Int8, Int16, Int32, Int64, Word, Word8, Word16, Word32,
+-- Word64, CShort, CUShort, CInt, CUInt, CLong, CULong, CLLong, CULLong
+--
+-- Floating types: Float, Double, CFloat, CDouble
+--
+-- Non-numeric types: Bool, Char, CChar, CSChar, CUChar
+--
+-- 'Int' has the same bitwidth as in plain Haskell computations, and 'Float'
+-- and 'Double' represent IEEE single and double precision floating point
+-- numbers, respectively.
+--
+-- TODO: support bit vectors
+--
+module Yices.Painless.Type (
+
+ module Data.Int,
+ module Data.Word,
+ module Foreign.C.Types,
+ module Yices.Painless.Type
+
+) where
+
+-- standard libraries
+import Data.Bits
+import Data.Int
+import Data.Typeable
+import Data.Word
+import Foreign.C.Types (
+ CChar, CSChar, CUChar, CShort, CUShort, CInt, CUInt, CLong, CULong,
+ CLLong, CULLong, CFloat, CDouble)
+ -- in the future, CHalf
+
+import Foreign.Storable (sizeOf)
+import Numeric
+import Data.Char (intToDigit)
+import qualified Data.Vector.Storable as V
+
+{-
+-- Extend Typeable support for 8- and 9-tuple
+-- ------------------------------------------
+
+class Typeable8 t where
+ typeOf8 :: t a b c d e f g h -> TypeRep
+
+instance Typeable8 (,,,,,,,) where
+ typeOf8 _ = mkTyCon "(,,,,,,,)" `mkTyConApp` []
+
+typeOf7Default :: (Typeable8 t, Typeable a) => t a b c d e f g h -> TypeRep
+typeOf7Default x = typeOf7 x `mkAppTy` typeOf (argType x)
+ where
+ argType :: t a b c d e f g h -> a
+ argType = undefined
+
+instance (Typeable8 s, Typeable a)
+ => Typeable7 (s a) where
+ typeOf7 = typeOf7Default
+
+class Typeable9 t where
+ typeOf9 :: t a b c d e f g h i -> TypeRep
+
+instance Typeable9 (,,,,,,,,) where
+ typeOf9 _ = mkTyCon "(,,,,,,,,)" `mkTyConApp` []
+
+typeOf8Default :: (Typeable9 t, Typeable a) => t a b c d e f g h i -> TypeRep
+typeOf8Default x = typeOf8 x `mkAppTy` typeOf (argType x)
+ where
+ argType :: t a b c d e f g h i -> a
+ argType = undefined
+
+instance (Typeable9 s, Typeable a)
+ => Typeable8 (s a) where
+ typeOf8 = typeOf8Default
+-}
+
+
+-- Scalar types
+-- ------------
+
+-- Reified dictionaries
+--
+
+data IntegralDict a where
+ IntegralDict :: ( Bounded a, Enum a, Eq a, Ord a, Show a
+ , Bits a, Integral a, Num a, Real a)
+ => IntegralDict a
+
+data FloatingDict a where
+ FloatingDict :: ( Enum a, Eq a, Ord a, Show a
+ , Floating a, Fractional a, Num a, Real a, RealFrac a
+ , RealFloat a)
+ => FloatingDict a
+
+data NonNumDict a where
+ NonNumDict :: (Eq a, Ord a, Show a)
+ => NonNumDict a
+
+-- Scalar type representation
+--
+
+-- |Integral types supported in yices computations.
+--
+data IntegralType a where
+ TypeInt :: IntegralDict Int -> IntegralType Int
+ TypeInt8 :: IntegralDict Int8 -> IntegralType Int8
+ TypeInt16 :: IntegralDict Int16 -> IntegralType Int16
+ TypeInt32 :: IntegralDict Int32 -> IntegralType Int32
+ TypeInt64 :: IntegralDict Int64 -> IntegralType Int64
+ TypeWord :: IntegralDict Word -> IntegralType Word
+ TypeWord8 :: IntegralDict Word8 -> IntegralType Word8
+ TypeWord16 :: IntegralDict Word16 -> IntegralType Word16
+ TypeWord32 :: IntegralDict Word32 -> IntegralType Word32
+ TypeWord64 :: IntegralDict Word64 -> IntegralType Word64
+ TypeCShort :: IntegralDict CShort -> IntegralType CShort
+ TypeCUShort :: IntegralDict CUShort -> IntegralType CUShort
+ TypeCInt :: IntegralDict CInt -> IntegralType CInt
+ TypeCUInt :: IntegralDict CUInt -> IntegralType CUInt
+ TypeCLong :: IntegralDict CLong -> IntegralType CLong
+ TypeCULong :: IntegralDict CULong -> IntegralType CULong
+ TypeCLLong :: IntegralDict CLLong -> IntegralType CLLong
+ TypeCULLong :: IntegralDict CULLong -> IntegralType CULLong
+
+-- |Floating-point types supported in yices computations.
+--
+data FloatingType a where
+ TypeFloat :: FloatingDict Float -> FloatingType Float
+ TypeDouble :: FloatingDict Double -> FloatingType Double
+ TypeCFloat :: FloatingDict CFloat -> FloatingType CFloat
+ TypeCDouble :: FloatingDict CDouble -> FloatingType CDouble
+
+-- |Non-numeric types supported in yices computations.
+--
+data NonNumType a where
+ TypeBool :: NonNumDict Bool -> NonNumType Bool -- marshaled to CInt
+ TypeChar :: NonNumDict Char -> NonNumType Char
+ TypeCChar :: NonNumDict CChar -> NonNumType CChar
+ TypeCSChar :: NonNumDict CSChar -> NonNumType CSChar
+ TypeCUChar :: NonNumDict CUChar -> NonNumType CUChar
+
+ -- Could define a Num instance
+ TypeVectorBool :: NonNumDict BitVector -> NonNumType BitVector
+
+
+------------------------------------------------------------------------
+
+-- Todo: support 'Word' packed representation (for fast constants).
+newtype BitVector = BitVector { unBV :: V.Vector Bool }
+ deriving (Eq, Ord, Typeable)
+
+-- Smart show instance.
+instance Show BitVector where
+ show (BitVector v)
+ | r <= 65535 = "0b" ++ showIntAtBase 2 intToDigit r []
+ | otherwise = "0x" ++ showHex r []
+ where
+ r = foldr (\i b -> if v V.! i then setBit b i else clearBit b i) w [0 .. n-1]
+ w = 0 :: Word
+ n = 8 * sizeOf w
+
+------------------------------------------------------------------------
+
+-- |Numeric element types implement Num & Real
+--
+data NumType a where
+ IntegralNumType :: IntegralType a -> NumType a
+ FloatingNumType :: FloatingType a -> NumType a
+
+-- |Bounded element types implement Bounded
+--
+data BoundedType a where
+ IntegralBoundedType :: IntegralType a -> BoundedType a
+ NonNumBoundedType :: NonNumType a -> BoundedType a
+
+-- |All scalar element types implement Eq, Ord & Enum
+--
+data ScalarType a where
+ NumScalarType :: NumType a -> ScalarType a
+ NonNumScalarType :: NonNumType a -> ScalarType a
+
+-- Showing type names
+--
+
+instance Show (IntegralType a) where
+ show (TypeInt _) = "Int"
+ show (TypeInt8 _) = "Int8"
+ show (TypeInt16 _) = "Int16"
+ show (TypeInt32 _) = "Int32"
+ show (TypeInt64 _) = "Int64"
+ show (TypeWord _) = "Word"
+ show (TypeWord8 _) = "Word8"
+ show (TypeWord16 _) = "Word16"
+ show (TypeWord32 _) = "Word32"
+ show (TypeWord64 _) = "Word64"
+ show (TypeCShort _) = "CShort"
+ show (TypeCUShort _) = "CUShort"
+ show (TypeCInt _) = "CInt"
+ show (TypeCUInt _) = "CUInt"
+ show (TypeCLong _) = "CLong"
+ show (TypeCULong _) = "CULong"
+ show (TypeCLLong _) = "CLLong"
+ show (TypeCULLong _) = "CULLong"
+
+instance Show (FloatingType a) where
+ show (TypeFloat _) = "Float"
+ show (TypeDouble _) = "Double"
+ show (TypeCFloat _) = "CFloat"
+ show (TypeCDouble _) = "CDouble"
+
+instance Show (NonNumType a) where
+ show (TypeBool _) = "Bool"
+ show (TypeChar _) = "Char"
+ show (TypeCChar _) = "CChar"
+ show (TypeCSChar _) = "CSChar"
+ show (TypeCUChar _) = "CUChar"
+ show (TypeVectorBool _) = "(Vector Bool)"
+
+instance Show (NumType a) where
+ show (IntegralNumType ty) = show ty
+ show (FloatingNumType ty) = show ty
+
+instance Show (BoundedType a) where
+ show (IntegralBoundedType ty) = show ty
+ show (NonNumBoundedType ty) = show ty
+
+instance Show (ScalarType a) where
+ show (NumScalarType ty) = show ty
+ show (NonNumScalarType ty) = show ty
+
+-- Querying scalar type representations
+--
+
+-- |Integral types
+--
+class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where
+ integralType :: IntegralType a
+
+instance IsIntegral Int where
+ integralType = TypeInt IntegralDict
+
+instance IsIntegral Int8 where
+ integralType = TypeInt8 IntegralDict
+
+instance IsIntegral Int16 where
+ integralType = TypeInt16 IntegralDict
+
+instance IsIntegral Int32 where
+ integralType = TypeInt32 IntegralDict
+
+instance IsIntegral Int64 where
+ integralType = TypeInt64 IntegralDict
+
+instance IsIntegral Word where
+ integralType = TypeWord IntegralDict
+
+instance IsIntegral Word8 where
+ integralType = TypeWord8 IntegralDict
+
+instance IsIntegral Word16 where
+ integralType = TypeWord16 IntegralDict
+
+instance IsIntegral Word32 where
+ integralType = TypeWord32 IntegralDict
+
+instance IsIntegral Word64 where
+ integralType = TypeWord64 IntegralDict
+
+instance IsIntegral CShort where
+ integralType = TypeCShort IntegralDict
+
+instance IsIntegral CUShort where
+ integralType = TypeCUShort IntegralDict
+
+instance IsIntegral CInt where
+ integralType = TypeCInt IntegralDict
+
+instance IsIntegral CUInt where
+ integralType = TypeCUInt IntegralDict
+
+instance IsIntegral CLong where
+ integralType = TypeCLong IntegralDict
+
+instance IsIntegral CULong where
+ integralType = TypeCULong IntegralDict
+
+instance IsIntegral CLLong where
+ integralType = TypeCLLong IntegralDict
+
+instance IsIntegral CULLong where
+ integralType = TypeCULLong IntegralDict
+
+-- |Floating types
+--
+class (Floating a, IsScalar a, IsNum a) => IsFloating a where
+ floatingType :: FloatingType a
+
+instance IsFloating Float where
+ floatingType = TypeFloat FloatingDict
+
+instance IsFloating Double where
+ floatingType = TypeDouble FloatingDict
+
+instance IsFloating CFloat where
+ floatingType = TypeCFloat FloatingDict
+
+instance IsFloating CDouble where
+ floatingType = TypeCDouble FloatingDict
+
+-- |Non-numeric types
+--
+class IsNonNum a where
+ nonNumType :: NonNumType a
+
+instance IsNonNum Bool where
+ nonNumType = TypeBool NonNumDict
+
+instance IsNonNum Char where
+ nonNumType = TypeChar NonNumDict
+
+instance IsNonNum CChar where
+ nonNumType = TypeCChar NonNumDict
+
+instance IsNonNum CSChar where
+ nonNumType = TypeCSChar NonNumDict
+
+instance IsNonNum CUChar where
+ nonNumType = TypeCUChar NonNumDict
+
+instance IsNonNum BitVector where
+ nonNumType = TypeVectorBool NonNumDict
+
+-- |Numeric types
+--
+class (Num a, IsScalar a) => IsNum a where
+ numType :: NumType a
+
+instance IsNum Int where
+ numType = IntegralNumType integralType
+
+instance IsNum Int8 where
+ numType = IntegralNumType integralType
+
+instance IsNum Int16 where
+ numType = IntegralNumType integralType
+
+instance IsNum Int32 where
+ numType = IntegralNumType integralType
+
+instance IsNum Int64 where
+ numType = IntegralNumType integralType
+
+instance IsNum Word where
+ numType = IntegralNumType integralType
+
+instance IsNum Word8 where
+ numType = IntegralNumType integralType
+
+instance IsNum Word16 where
+ numType = IntegralNumType integralType
+
+instance IsNum Word32 where
+ numType = IntegralNumType integralType
+
+instance IsNum Word64 where
+ numType = IntegralNumType integralType
+
+instance IsNum CShort where
+ numType = IntegralNumType integralType
+
+instance IsNum CUShort where
+ numType = IntegralNumType integralType
+
+instance IsNum CInt where
+ numType = IntegralNumType integralType
+
+instance IsNum CUInt where
+ numType = IntegralNumType integralType
+
+instance IsNum CLong where
+ numType = IntegralNumType integralType
+
+instance IsNum CULong where
+ numType = IntegralNumType integralType
+
+instance IsNum CLLong where
+ numType = IntegralNumType integralType
+
+instance IsNum CULLong where
+ numType = IntegralNumType integralType
+
+instance IsNum Float where
+ numType = FloatingNumType floatingType
+
+instance IsNum Double where
+ numType = FloatingNumType floatingType
+
+instance IsNum CFloat where
+ numType = FloatingNumType floatingType
+
+instance IsNum CDouble where
+ numType = FloatingNumType floatingType
+
+-- |Bounded types
+--
+class IsBounded a where
+ boundedType :: BoundedType a
+
+instance IsBounded Int where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Int8 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Int16 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Int32 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Int64 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Word where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Word8 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Word16 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Word32 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Word64 where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CShort where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CUShort where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CInt where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CUInt where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CLong where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CULong where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CLLong where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded CULLong where
+ boundedType = IntegralBoundedType integralType
+
+instance IsBounded Bool where
+ boundedType = NonNumBoundedType nonNumType
+
+instance IsBounded Char where
+ boundedType = NonNumBoundedType nonNumType
+
+instance IsBounded CChar where
+ boundedType = NonNumBoundedType nonNumType
+
+instance IsBounded CSChar where
+ boundedType = NonNumBoundedType nonNumType
+
+instance IsBounded CUChar where
+ boundedType = NonNumBoundedType nonNumType
+
+-- |All scalar type
+--
+class Typeable a => IsScalar a where
+ scalarType :: ScalarType a
+
+instance IsScalar Int where
+ scalarType = NumScalarType numType
+
+instance IsScalar Int8 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Int16 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Int32 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Int64 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Word where
+ scalarType = NumScalarType numType
+
+instance IsScalar Word8 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Word16 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Word32 where
+ scalarType = NumScalarType numType
+
+instance IsScalar Word64 where
+ scalarType = NumScalarType numType
+
+instance IsScalar CShort where
+ scalarType = NumScalarType numType
+
+instance IsScalar CUShort where
+ scalarType = NumScalarType numType
+
+instance IsScalar CInt where
+ scalarType = NumScalarType numType
+
+instance IsScalar CUInt where
+ scalarType = NumScalarType numType
+
+instance IsScalar CLong where
+ scalarType = NumScalarType numType
+
+instance IsScalar CULong where
+ scalarType = NumScalarType numType
+
+instance IsScalar CLLong where
+ scalarType = NumScalarType numType
+
+instance IsScalar CULLong where
+ scalarType = NumScalarType numType
+
+instance IsScalar Float where
+ scalarType = NumScalarType numType
+
+instance IsScalar Double where
+ scalarType = NumScalarType numType
+
+instance IsScalar CFloat where
+ scalarType = NumScalarType numType
+
+instance IsScalar CDouble where
+ scalarType = NumScalarType numType
+
+-- Non-numerical scalar types
+
+instance IsScalar Bool where
+ scalarType = NonNumScalarType nonNumType
+
+instance IsScalar Char where
+ scalarType = NonNumScalarType nonNumType
+
+instance IsScalar CChar where
+ scalarType = NonNumScalarType nonNumType
+
+instance IsScalar CSChar where
+ scalarType = NonNumScalarType nonNumType
+
+instance IsScalar CUChar where
+ scalarType = NonNumScalarType nonNumType
+
+instance IsScalar BitVector where
+ scalarType = NonNumScalarType nonNumType -- false for bitvectors...
+
+-- Extract reified dictionaries
+--
+
+integralDict :: IntegralType a -> IntegralDict a
+integralDict (TypeInt dict) = dict
+integralDict (TypeInt8 dict) = dict
+integralDict (TypeInt16 dict) = dict
+integralDict (TypeInt32 dict) = dict
+integralDict (TypeInt64 dict) = dict
+integralDict (TypeWord dict) = dict
+integralDict (TypeWord8 dict) = dict
+integralDict (TypeWord16 dict) = dict
+integralDict (TypeWord32 dict) = dict
+integralDict (TypeWord64 dict) = dict
+integralDict (TypeCShort dict) = dict
+integralDict (TypeCUShort dict) = dict
+integralDict (TypeCInt dict) = dict
+integralDict (TypeCUInt dict) = dict
+integralDict (TypeCLong dict) = dict
+integralDict (TypeCULong dict) = dict
+integralDict (TypeCLLong dict) = dict
+integralDict (TypeCULLong dict) = dict
+
+floatingDict :: FloatingType a -> FloatingDict a
+floatingDict (TypeFloat dict) = dict
+floatingDict (TypeDouble dict) = dict
+floatingDict (TypeCFloat dict) = dict
+floatingDict (TypeCDouble dict) = dict
+
+nonNumDict :: NonNumType a -> NonNumDict a
+nonNumDict (TypeBool dict) = dict
+nonNumDict (TypeChar dict) = dict
+nonNumDict (TypeCChar dict) = dict
+nonNumDict (TypeCSChar dict) = dict
+nonNumDict (TypeCUChar dict) = dict
+nonNumDict (TypeVectorBool dict) = dict
+
+-- Tuple type
+-- ----------
+
+data TupleType a where
+ UnitTuple :: TupleType ()
+ SingleTuple :: ScalarType a -> TupleType a
+ PairTuple :: TupleType a -> TupleType b -> TupleType (a, b)
+
diff --git a/tests/calls.hs b/tests/calls.hs
new file mode 100644
index 0000000..16c2d57
--- /dev/null
+++ b/tests/calls.hs
@@ -0,0 +1,31 @@
+import Yices.Base
+
+main = do
+ print version
+
+ setVerbosity 7
+ setMaxSatInitialCost 99
+ setMaxNumConflictsInMaxSatIteration 100
+ setTypeChecker True
+ setMaxNumIterationsInMaxSat 1000
+ setMaxSatInitialCost 200
+ setArithmeticOnly True
+ setLogFile "x.dat"
+
+ c <- empty
+ reset c
+ dump c
+ push c
+ pop c
+ print =<< inconsistent c
+
+ print =<< check c
+
+ setVerbosity 0
+ print =<< check c
+
+ print =<< getUnsatCoreSize c
+
+ print =<< getModel c
+
+ print =<< getUnsatCore c
diff --git a/tests/push-pop.hs b/tests/push-pop.hs
new file mode 100644
index 0000000..a0e107b
--- /dev/null
+++ b/tests/push-pop.hs
@@ -0,0 +1,579 @@
+import Yices.Base
+
+main = do
+ c <- empty
+ push c
+ push c
+ push c
+ push c
+ pop c
+ pop c
+ pop c
+ pop c
+
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ push c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ pop c
+ dump c
diff --git a/yices-painless.cabal b/yices-painless.cabal
new file mode 100644
index 0000000..125fdad
--- /dev/null
+++ b/yices-painless.cabal
@@ -0,0 +1,71 @@
+Name: yices-painless
+Version: 0.1
+Synopsis: An embedded language for programming the Yices SMT solver
+Description:
+ This library defines an embedded language in Haskell for programming
+ the Yices SMT solver.
+ .
+ Yices is an efficient SMT solver that decides the satisfiability of
+ arbitrary formulas containing uninterpreted function symbols with
+ equality, linear real and integer arithmetic, scalar types,
+ recursive datatypes, tuples, records, extensional arrays, fixed-size
+ bit-vectors, quantifiers, and lambda expressions. Yices also does
+ MaxSMT (and, dually, unsat cores) and is competitive as an ordinary
+ SAT and MaxSAT solver.
+ .
+ The embedded language embeds both terms and types into Haskell, via
+ a typed higher-order abstract syntax representation. Propositions in
+ the embedding are represented as (typed) pure expressions.
+ .
+ Solution variables in the proposition (notionally, free variables)
+ are bound an the outermost lambda term. Propositions constructed
+ from logical primitives can then be executed by the solver to yield
+ a satisfying assignment to those free variables in the proposition.
+ .
+ More information about Yices:
+ .
+ * <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
+