packages feed

yices-painless 0.1 → 0.1.1

raw patch · 11 files changed

+235/−91 lines, 11 files

Files

Yices/Painless/Language.hs view
@@ -1,11 +1,10 @@-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE PatternGuards        #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE OverlappingInstances #-}-{-# LANGUAGE UndecidableInstances #-}--{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE PatternGuards          #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE OverlappingInstances   #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE MultiParamTypeClasses  #-} {-# LANGUAGE FunctionalDependencies #-}  {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -28,6 +27,15 @@ -- Terms and types are embedded in Haskell, so all the usual type -- inference and checking works for Yices propositions. --+-- /A simple example: integers/+--+-- > import Yices.Painless.Language+-- >+-- > main = print =<< solve p+-- >+-- > p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool+-- > p x y z = (3 * x) + (6 * y) ==* 1+-- -- /A simple example: bitvectors/ -- -- > solve $ \b1 (b2 :: Exp BitVector) @@ -86,7 +94,6 @@ import qualified Data.Map as M  import Data.Bits-import qualified Data.Vector.Storable as V  import Control.Monad import Control.Applicative ((<$>))@@ -105,9 +112,6 @@ -- -- /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.@@ -118,13 +122,17 @@ -- -- * A 'Monoid' instance for bit vectors? --+-- * A monoid for conjunction?+-- -- * Support other numeric types. -- -- * Support function types in the core language. ----- * Support more Yices types: tuples, records, recursive types.+-- * Support more SMT types: functions, tuples, records, recursive types. ---+-- * Deriving Exp. A (derivable) class for lifting Haskell data types+-- into their symbolic form.+--  ------------------------------------------------------------------------ -- Language@@ -225,38 +233,16 @@ -}  instance (IsScalar t) => Prelude.Eq (Exp t) where-  -- FIXME: instance makes no sense with standard signatures+  -- 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+  -- 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@@ -267,17 +253,24 @@    -- needs size types!  -- $BitInstances--- The 'Exp BitVector' type is an instance of 'Bits', allowing the usual+-- The 'Exp BitVector' type is an instance of 'Bits' and 'Num', allowing the usual -- Haskell bitwise operators to be used to construct propositions involving -- bitwise operations on bit vectors. ----- > (.&,), (.|.), xor, complement, shiftL, shiftR+-- > (.&.) :: Exp BitVector -> Exp BitVector -> Exp BitVector+-- > (.|.)+-- > xor+-- > complement+-- > shiftL+-- > shiftR -- -- Currently bit vectors are fixed at 'sizeOf (undefined :: Word)' bits. -- -- Bit vector constants can be constructed using overloaded numeric -- literals. --+-- TODO: instance Bits a => Bits (Exp a)+--  instance Bits (Exp BitVector) where     (.&.)       = mkBVAnd@@ -288,7 +281,6 @@     shiftR      = mkBVShiftR0     isSigned _  = False     bitSize  _  = 8 * sizeOf (undefined :: Word) -- TODO! size type-          ------------------------------------------------------------------------ @@ -357,17 +349,10 @@  -- 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 -mkBVNeg :: Exp BitVector -> Exp BitVector-mkBVNeg x = PrimBVNeg `PrimApp` x+-- Bits instance  mkBVAnd :: Exp BitVector -> Exp BitVector -> Exp BitVector mkBVAnd x y = PrimBVAnd `PrimApp` tup2 (x, y)@@ -387,8 +372,11 @@ mkBVShiftR0 :: Exp BitVector -> Int -> Exp BitVector mkBVShiftR0 x n = PrimBVSR0 `PrimApp` tup2 (x, constant n) -- shiftR fills with 0 --- Operators from Num+------------------------------------------------------------------------+-- Scalar operations +-- Operators from Num, also includes BitVector operations+ mkAdd :: (IsNum t) => Exp t -> Exp t -> Exp t mkAdd x y = PrimAdd numType `PrimApp` tup2 (x, y) @@ -429,6 +417,7 @@ mkLNot :: Exp Bool -> Exp Bool mkLNot x = PrimLNot `PrimApp` x +------------------------------------------------------------------------ -- Smart constructor for literals  -- | Literal 'True'@@ -990,7 +979,7 @@     = do mn <- Yices.getValueBool m d          return (v, YValue mn) -    | NonNumScalarType (TypeVectorBool _)                <- ty+    | NumScalarType (IntegralNumType (TypeVectorBool _))               <- ty     = do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word))          return (v, YValue $ fmap BitVector mn)             @@ -1048,7 +1037,7 @@          -- Bit vectors         go (OLam (f :: OpenFun (env, a) t)) n g-            | ty@(NonNumScalarType (TypeVectorBool _))                <- scalarType :: ScalarType a+            | ty@(NumScalarType (IntegralNumType (TypeVectorBool _)))   <- scalarType :: ScalarType a             = do                 let nm = "x" ++ show n                 -- TODO: hack, no size information for bit vectors yet.@@ -1083,7 +1072,7 @@     = if n then Yices.mkTrue  c            else Yices.mkFalse c -    | NonNumScalarType (TypeVectorBool _)            <- scalarType :: ScalarType t+    | NumScalarType (IntegralNumType (TypeVectorBool _))  <- scalarType :: ScalarType t     = Yices.mkBVConstantFromVector c (unBV n)  @@ -1118,7 +1107,7 @@             Yices.mkNeq c e1 e2  -- Specialize for BitVector first-exec c (OPrimApp  (PrimLt (NonNumScalarType (TypeVectorBool _)))+exec c (OPrimApp  (PrimLt (NumScalarType (IntegralNumType (TypeVectorBool _))))         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2@@ -1132,7 +1121,7 @@             Yices.mkLt c e1 e2  -- Specialize for BitVector first-exec c (OPrimApp  (PrimLtEq (NonNumScalarType (TypeVectorBool _)))+exec c (OPrimApp  (PrimLtEq (NumScalarType (IntegralNumType (TypeVectorBool _))))         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2@@ -1145,7 +1134,7 @@             Yices.mkLe c e1 e2  -- Specialize for BitVector first-exec c (OPrimApp  (PrimGt (NonNumScalarType (TypeVectorBool _)))+exec c (OPrimApp  (PrimGt (NumScalarType (IntegralNumType (TypeVectorBool _))))         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2@@ -1159,7 +1148,7 @@  -- TODO think about what gets through the overloading incorrectly. -- Specialize for BitVector first-exec c (OPrimApp  (PrimGtEq (NonNumScalarType (TypeVectorBool _)))+exec c (OPrimApp  (PrimGtEq (NumScalarType (IntegralNumType (TypeVectorBool _))))         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2@@ -1189,45 +1178,49 @@  -- Numerical operations -exec c (OPrimApp  (PrimAdd _)-        (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do+-- overloaded on bit vectors+exec c (OPrimApp  (PrimAdd (IntegralNumType (TypeVectorBool _)))+          (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2-            Yices.mkSum c [e1,e2]+            Yices.mkBVAdd c e1 e2 -exec c (OPrimApp  (PrimSub _)+exec c (OPrimApp  (PrimAdd _)         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2-            Yices.mkSub c [e1,e2]+            Yices.mkSum c [e1,e2] -exec c (OPrimApp  (PrimMul _)+-- overloaded on bit vectors+exec c (OPrimApp  (PrimSub (IntegralNumType (TypeVectorBool _)))           (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2-            Yices.mkMul c [e1,e2]----------------------------------------------------------------------------- Bit Vector operations+            Yices.mkBVSub c e1 e2 -exec c (OPrimApp PrimBVAdd-          (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do+exec c (OPrimApp  (PrimSub _)+        (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2-            Yices.mkBVAdd c e1 e2+            Yices.mkSub c [e1,e2] -exec c (OPrimApp PrimBVMul+-- overloaded on bit vectors+exec c (OPrimApp  (PrimMul (IntegralNumType (TypeVectorBool _)))           (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2             Yices.mkBVMul c e1 e2 -exec c (OPrimApp PrimBVSub+exec c (OPrimApp  (PrimMul _)           (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do             e1 <- exec c x1             e2 <- exec c x2-            Yices.mkBVSub c e1 e2+            Yices.mkMul c [e1,e2] +------------------------------------------------------------------------+-- Bit Vector operations++-- TODO exec c (OPrimApp PrimBVNeg           (OTuple (NilTup `SnocTup` x1))) = do             e1 <- exec c x1
Yices/Painless/Type.hs view
@@ -136,6 +136,8 @@   TypeCLLong  :: IntegralDict CLLong  -> IntegralType CLLong   TypeCULLong :: IntegralDict CULLong -> IntegralType CULLong +  TypeVectorBool  :: IntegralDict BitVector -> IntegralType BitVector+ -- |Floating-point types supported in yices computations. -- data FloatingType a where@@ -153,16 +155,35 @@   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) +instance Num BitVector where+    (+)         = error "Prelude.Num.+ applied to BitVectors"+    (-)         = error "Prelude.Num.- applied to BitVectors"+    (*)         = error "Prelude.Num.* applied to BitVectors"+    negate      = error "Prelude.Num.negate applied to BitVectors"+    abs _       = error "Prelude.Num.abs applied to EDSL types"+    signum _    = error "Prelude.Num.signum applied to EDSL types"++    -- TODO: size is fixed+    fromInteger n = BitVector $ V.generate (8 * sizeOf (undefined :: Word)) (testBit w)+        where+            w :: Word+            w = fromIntegral n++-- Fake instances so we can get Num BitVector. We could do it for real via Integer...+-- Or just use Integers++instance Integral BitVector+instance Bits     BitVector+instance Enum     BitVector+instance Bounded  BitVector+instance Real     BitVector+ -- Smart show instance. instance Show BitVector where     show (BitVector v) @@ -215,6 +236,7 @@   show (TypeCULong _)  = "CULong"   show (TypeCLLong _)  = "CLLong"   show (TypeCULLong _) = "CULLong"+  show (TypeVectorBool _) = "(Vector Bool)"  instance Show (FloatingType a) where   show (TypeFloat _)   = "Float"@@ -228,7 +250,6 @@   show (TypeCChar _)  = "CChar"   show (TypeCSChar _) = "CSChar"   show (TypeCUChar _) = "CUChar"-  show (TypeVectorBool _) = "(Vector Bool)"  instance Show (NumType a) where   show (IntegralNumType ty) = show ty@@ -253,6 +274,9 @@ instance IsIntegral Int where   integralType = TypeInt IntegralDict +instance IsIntegral BitVector where+  integralType = TypeVectorBool IntegralDict+ instance IsIntegral Int8 where   integralType = TypeInt8 IntegralDict @@ -341,9 +365,6 @@ instance IsNonNum CUChar where   nonNumType = TypeCUChar NonNumDict -instance IsNonNum BitVector where-  nonNumType = TypeVectorBool NonNumDict- -- |Numeric types -- class (Num a, IsScalar a) => IsNum a where@@ -403,6 +424,9 @@ instance IsNum CULLong where   numType = IntegralNumType integralType +instance IsNum BitVector where+  numType = IntegralNumType integralType+ instance IsNum Float where   numType = FloatingNumType floatingType @@ -423,6 +447,9 @@ instance IsBounded Int where   boundedType = IntegralBoundedType integralType +instance IsBounded BitVector where+  boundedType = IntegralBoundedType integralType+ instance IsBounded Int8 where   boundedType = IntegralBoundedType integralType @@ -560,6 +587,9 @@ instance IsScalar CDouble where   scalarType = NumScalarType numType +instance IsScalar BitVector where+  scalarType = NumScalarType numType+ -- Non-numerical scalar types  instance IsScalar Bool where@@ -577,9 +607,6 @@ instance IsScalar CUChar where   scalarType = NonNumScalarType nonNumType -instance IsScalar BitVector where-  scalarType = NonNumScalarType nonNumType -- false for bitvectors...- -- Extract reified dictionaries --  @@ -602,6 +629,7 @@ integralDict (TypeCULong  dict) = dict integralDict (TypeCLLong  dict) = dict integralDict (TypeCULLong dict) = dict+integralDict (TypeVectorBool dict) = dict  floatingDict :: FloatingType a -> FloatingDict a floatingDict (TypeFloat dict) = dict@@ -615,7 +643,6 @@ nonNumDict (TypeCChar  dict) = dict nonNumDict (TypeCSChar dict) = dict nonNumDict (TypeCUChar dict) = dict-nonNumDict (TypeVectorBool dict) = dict  -- Tuple type -- ----------
+ tests/examples/ex1.hs view
@@ -0,0 +1,5 @@+import Yices.Painless.Language++main = print =<< solve p++p = 0 ==* (1 :: Exp Int)
+ tests/examples/ex2.hs view
@@ -0,0 +1,5 @@+import Yices.Painless.Language++main = print =<< solve p++p = false
+ tests/examples/ex24.hs view
@@ -0,0 +1,16 @@+import Yices.Painless.Language++main = print =<< solve p++data S = S1 | S2 | S3+    deriving (Show, Enum)++p x1 x2 x3 x4 = +    and +      [ (/=*) x1 x2+      , (/=*) x1 x3+      , (/=*) x1 x4+      , (/=*) x2 x3+      , (/=*) x2 x4+      , (/=*) x3 x4+      ]
+ tests/examples/ex3.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE ScopedTypeVariables #-}++import Yices.Painless.Language+import Prelude hiding (and)++main = print =<< solve p++-- Currently, need to derive Int, then translate in and out.++data PC = Sleeping | Trying | Critical+    deriving (Show, Enum)++p x1 x2 z1 z2 (w1 :: Exp Int) (w2 :: Exp Int) =+  and+    [ x1 ==* x2+    , x1 ==* z1+    , x2 ==* fromIntegral (fromEnum Critical)+    , x2 ==* z2+    , x2 ==* w1+    , x1 ==* fromIntegral (fromEnum Trying)+    ]++{-+-- (define-type pc (scalar sleeping trying critical))+(define x1::pc)+(define x2::pc)+(define z1::pc)+(define z2::pc)+(define w1::pc)+(define w2::pc)++(assert (= x1 x2))+(assert (= x1 z1))+(assert (= x2 critical))+(assert (= x2 z2))+(assert (= z2 w1))+(assert (= x1 trying))+-}
+ tests/examples/ex5.ys view
@@ -0,0 +1,18 @@++(define-type pc (scalar sleeping trying critical))+(define f::(-> pc pc))+(define g::(-> pc pc))+(define x1::pc)+(define x2::pc)+(define x3::pc)+(define x4::pc)+(define x5::pc)+(define x6::pc)++++(assert (/= (g (f x1)) (g (f x2))))+(assert (= x1 x3))+(assert (= x1 x4))+(assert (= x3 x2))+
+ tests/examples/ex6.ys view
@@ -0,0 +1,18 @@++(define-type pc (scalar sleeping trying critical))+(define f::(-> pc pc))+(define g::(-> pc pc))+(define x1::pc)+(define x2::pc)+(define x3::pc)+(define x4::pc)+(define x5::pc)+(define x6::pc)++++(assert (= x1 x3))+(assert (= x1 x4))+(assert (= x3 x2))+(assert (/= (g (f x1)) (g (f x2))))+
+ tests/examples/ex66.hs view
@@ -0,0 +1,7 @@+import Yices.Painless.Language++main = print =<< solve p++p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool+p x y z = (3 * x) + (6 * y) ==* 1+
+ tests/examples/ex67.hs view
@@ -0,0 +1,10 @@+import Yices.Painless.Language++main = print =<< solve p++p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool +p x y z =+    (3 * x) + (6 * y) + z ==* 1+  &&*+    z ==* 2+
yices-painless.cabal view
@@ -1,5 +1,5 @@ Name:                yices-painless-Version:             0.1+Version:             0.1.1 Synopsis:            An embedded language for programming the Yices SMT solver Description:              This library defines an embedded language in Haskell for programming@@ -26,9 +26,16 @@     .     * <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.+    The primary interface is via the EDSL, "Yices.Painless.Language",+    however, low and medium-level bindings to the Yices C API are also provided+    ("Yices.Painless.Base.C" and "Yices.Painless.Base"). The+    medium-level bindings add significant type and resource safety to+    that which the C API provides.+    .+    Documentation for this package is available:+    .+    * <http://www.galois.com/~dons/yices-painless/>+    .  Homepage:            http://code.haskell.org/~dons/code/yices-painless License:             BSD3