yices-painless 0.1.1 → 0.1.2
raw patch · 6 files changed
+176/−88 lines, 6 files
Files
- Yices/Painless/Language.hs +152/−32
- Yices/Painless/Type.hs +18/−0
- tests/examples/ex24.hs +0/−16
- tests/examples/ex5.ys +0/−18
- tests/examples/ex6.ys +0/−18
- yices-painless.cabal +6/−4
Yices/Painless/Language.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -52,6 +53,26 @@ -- > x1 => 0b100 -- > Satisfiable --+-- /Uninterpreted functions/+--+-- > {-# LANGUAGE ScopedTypeVariables #-}+-- > import Yices.Painless.Language+-- >+-- > main = print =<< solve p+-- >+-- > p f g (n :: Exp Int) = f n &&* g (f n)+--+-- Returns an assignment to the variables, and a model for the functions+-- (using Yices pretty printer):+--+-- > $ runhaskell ex0.hs+-- > x0 => 1+-- >+-- > (= x0 1)+-- > (= (f2 1) true)+-- > (= (f1 true) true)+--+-- > Satisfiable module Yices.Painless.Language ( @@ -60,6 +81,7 @@ -- * Building Yices propositions. Yices, Exp,+ BitVector, -- ** Scalar introduction -- constant,@@ -71,6 +93,9 @@ -- ** Bit vectors -- $BitInstances + -- ** Uninterpreted functions+ -- $Functions+ -- ** Conditional expressions (?), @@ -86,12 +111,15 @@ -- * Design discussion -- $Notes + module Data.Bits+ ) where import Prelude hiding (not, or, and, min, max) import Data.Typeable import qualified Data.Map as M+import Data.Maybe import Data.Bits @@ -134,6 +162,16 @@ -- into their symbolic form. -- +-- $Functions+-- +-- Uninterpreted functions may be introduced as variables (alongside+-- scalar variables). +--+-- E.g.+--+-- > \f g x -> f (g x) ==* 7+--+ ------------------------------------------------------------------------ -- Language @@ -469,9 +507,13 @@ data Exp t where -- Needed for conversion to de Bruijn form- Tag :: (IsScalar t) => Int -> Exp t- -- environment size at defining occurrence+ Tag :: (IsAType t) => Int -> Exp t + -- NNN+ TagFn :: (IsAType (a -> b)) => Int -> (Exp a -> Exp b)+ -- application of a symbolic function to an argument.+ -- TODO: basically, a restricted form of application. Sort this out.+ Const :: (Show t, IsScalar t) => t -> Exp t @@ -531,13 +573,24 @@ -- Convert expressions convert lyt e = OBody (convertOpenExp lyt e) -instance (IsScalar a, Yices f r) => Yices (Exp a -> f) (a -> r) where+instance (IsAType a, 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 ++-- No instance for (Yices ((Exp Int -> Exp Int) -> Exp Int -> Exp Bool) r)++-- Convert functions. Identical for the other recursive case.+instance (IsScalar a, IsScalar b, Yices f r)+ => Yices ((Exp a -> Exp b) -> f) ((a -> b) -> r) where+ convert lyt f = OLam (convert lyt' (f g))+ where+ g = TagFn (size lyt) -- :: Exp a -> Exp b -- generate a fresh, anonymous function!+ lyt' = inc lyt `PushLayout` ZeroIdx+ ------------------------------------------------------------------------ -- |Conversion from HOAS to de Bruijn expression AST@@ -565,6 +618,8 @@ where cvt :: Exp t' -> OpenExp env t' cvt (Tag i) = Var (prjIdx (size lyt - i - 1) lyt) -- indexing!+ cvt (TagFn i arg) = VarFn (prjIdx (size lyt - i - 1) lyt) (cvt arg)-- indexing!+ -- application. cvt (Const v) = OConst v cvt (Tuple tup) = OTuple (convertTuple lyt tup) cvt (Cond e1 e2 e3) = OCond (cvt e1) (cvt e2) (cvt e3)@@ -670,8 +725,9 @@ -- |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)+ OBody :: OpenExp env t -> OpenFun env t+ -- OLam :: {-IsScalar a =>-} OpenFun (env, a) t -> OpenFun env (a -> t)+ OLam :: IsAType a => OpenFun (env, a) t -> OpenFun env (a -> t) -- |Function without free scalar variables --@@ -686,11 +742,15 @@ -- data OpenExp env t where - -- Variable index, ranging only over tuples or scalars- Var :: IsScalar t+ -- Variable index+ Var :: IsAType t => Idx env t -> OpenExp env t + VarFn :: IsAType (a -> b) =>+ Idx env (a -> b) -> (OpenExp env a -> OpenExp env b)+ -- TODO: restricted form of application+ -- Constant values OConst :: (Show t, IsScalar t) => t@@ -837,18 +897,25 @@ prettyFun :: Int -> OpenFun env a -> Doc prettyFun lvl fun =- let (n, bodyDoc) = count fun+ let (n, vs, bodyDoc) = count fun in if n < 0 then bodyDoc else - char '\\' <> hsep [text $ "x" ++ show idx | idx <- reverse [0..n]] <+>+ char '\\' <> hsep [text $ case ei of Left i -> "f" ++ show i ;+ Right i -> "x" ++ show i+ | ei <- vs] <+> 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)+ count :: OpenFun env fun -> (Int, [Either Int Int], Doc)+ count (OBody body) = ((-1), [], prettyExp lvl noParens body) + count (OLam (f :: OpenFun (env, a) t)) | (AFunctionType _ _) <- aType :: AType a =+ let (n, vs, body) = count f in (1 + n, Left (1+n) : vs, body)++ count (OLam (f :: OpenFun (env, a) t)) =+ let (n, vs, body) = count f in (1 + n, Right (1+n) : vs, body)+ -- Pretty print an expression. -- -- * Apply the wrapping combinator (1st argument) to any compound expressions.@@ -856,7 +923,9 @@ prettyExp :: forall t env . Int -> (Doc -> Doc) -> OpenExp env t -> Doc +-- TODO: function types prettyExp _ _ (Var idx) = text $ "x" ++ show (idxToInt idx)+prettyExp lvl wrap (VarFn idx e) = text ( "f" ++ show (idxToInt idx)) <+> prettyExp lvl wrap e prettyExp _ _ (OConst v) = text $ show (v :: t) -- dispatch differently for BitVector types prettyExp lvl _ (OTuple tup) = prettyTuple lvl tup @@ -934,7 +1003,7 @@ Yices.setTypeChecker True let t = convertYices q -- bind all the variables- print t+ -- print t (g,e) <- execY c t @@ -953,7 +1022,7 @@ Nothing -> return Yices.Satisfiable Just m -> do - vs <- sequence+ vs <- catMaybes `fmap` sequence [ get m v t' d | (v,(t',d)) <- M.toList g ] @@ -963,25 +1032,32 @@ Nothing -> putStrLn "_" Just v -> print v) + -- TODO: extract functions.+ Yices.display m+ -- print cs return Yices.Satisfiable --- | Retrieving bindings by type+-- | Retrieving bindings by type (can't retrieve functions) ---get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (String, YValue)-get m v (YType (ty :: ScalarType t)) d+get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (Maybe (String, YValue))+get m v (YType (ty :: AType t)) d - | NumScalarType (IntegralNumType (TypeInt _)) <- ty+ | AScalarType (NumScalarType (IntegralNumType (TypeInt _))) <- ty = do mn <- Yices.getValueInt m d- return (v, YValue mn)+ return $ Just (v, YValue mn) - | NonNumScalarType (TypeBool _) <- ty+ | AScalarType (NonNumScalarType (TypeBool _)) <- ty = do mn <- Yices.getValueBool m d- return (v, YValue mn)+ return $ Just (v, YValue mn) - | NumScalarType (IntegralNumType (TypeVectorBool _)) <- ty+ | AScalarType (NumScalarType (IntegralNumType (TypeVectorBool _))) <- ty = do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word))- return (v, YValue $ fmap BitVector mn)+ return $ Just (v, YValue $ fmap BitVector mn)++ -- Can't return function models?+ | AFunctionType _ _ <- ty+ = return Nothing | otherwise = error "Yices.Painless.get: don't know how to get this type yet" @@ -992,9 +1068,9 @@ -- type YEnv = M.Map String (YType, Yices.Decl) -data YType = forall a. IsScalar a => YType (ScalarType a)+data YType = forall a. IsAType a => YType (AType a) -data YValue = forall a. (Show a, IsScalar a) => YValue (Maybe a)+data YValue = forall a. (Show a, IsAType a) => YValue (Maybe a) -- -- To run,@@ -1013,42 +1089,70 @@ -- 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+execF c fn = go fn (count fn) M.empty where+ -- determine size of environment+ count :: OpenFun env f -> Int+ count (OBody _) = (-1)+ count (OLam f) = 1 + count f+ 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+ | ty@(AScalarType (NumScalarType (IntegralNumType (TypeInt _)))) <- aType :: AType 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)+ 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+ | ty@(AScalarType (NonNumScalarType (TypeBool _))) <- aType :: AType a = do let nm = "x" ++ show n d <- Yices.mkBoolDecl c nm- go f (n + 1) (M.insert nm (YType ty, d) g)+ go f (n - 1) (M.insert nm (YType ty, d) g) -- Bit vectors go (OLam (f :: OpenFun (env, a) t)) n g- | ty@(NumScalarType (IntegralNumType (TypeVectorBool _))) <- scalarType :: ScalarType a+ | ty@(AScalarType (NumScalarType (IntegralNumType (TypeVectorBool _)))) <- aType :: AType 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 f (n - 1) (M.insert nm (YType ty, d) g) + -- Uninterpreted functions+ go (OLam (f :: OpenFun (env, a) t)) n g+ | ty@(AFunctionType+ [a] + r + ) <- aType :: AType a+ = do let nm = "f" ++ show n -- we get to actually name things+ argty <- toBuiltInYicesType c a+ resty <- toBuiltInYicesType c r+ tynm <- Yices.mkFunctionType c [argty] resty+ 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" ++-- Only built in types.+-- number, real, int, nat, bool, any+toBuiltInYicesType :: Yices.Context -> ScalarType a -> IO Yices.Type+toBuiltInYicesType c a = case a of+ (NumScalarType (IntegralNumType (TypeInt _))) -> Yices.mkType c "int"+ (NonNumScalarType (TypeBool _)) -> Yices.mkType c "bool"+ _ -> error $ "Don't know how to bind this type yet: " ++ show a++-- TODO: map ScalarTypes to yices strings.+ -- | Execute an expression with free variables. -- -- /TODO:/@@ -1084,6 +1188,22 @@ case v of Nothing -> error "Undefined variable" Just d -> Yices.mkVarFromDecl c d++-- Application+exec c (VarFn i e) = do+ let n = "f" ++ show (idxToInt i)+ v <- Yices.getVarDeclFromName c n -- sneaky. using Yices environment. TODO: use YEnv+-- print n++ -- get our yices function+ yf <- case v of+ Nothing -> error $ "Undefined variable: " ++ show n+ Just d -> Yices.mkVarFromDecl c d++ -- compile the expression+ ye <- exec c e++ Yices.mkApp c yf [ye] -- Conditionals exec c (OCond b t e) = do
Yices/Painless/Type.hs view
@@ -214,6 +214,12 @@ NumScalarType :: NumType a -> ScalarType a NonNumScalarType :: NonNumType a -> ScalarType a +-- | All Yices types: functions over scalar types, or scalar types.+data AType a where+ AFunctionType :: [ScalarType t] -> ScalarType r -> AType (t -> r)+ -- todo: tuples+ AScalarType :: ScalarType a -> AType a+ -- Showing type names -- @@ -266,6 +272,7 @@ -- Querying scalar type representations -- + -- |Integral types -- class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where@@ -515,6 +522,17 @@ instance IsBounded CUChar where boundedType = NonNumBoundedType nonNumType++-- | All types we can bind+class Typeable a => IsAType a where+ aType :: AType a++instance IsAType Int where+ aType = AScalarType scalarType++instance (IsScalar a, IsScalar b) => IsAType (a -> b) where+ aType = AFunctionType [scalarType] scalarType+ -- todo: tuples -- |All scalar type --
− tests/examples/ex24.hs
@@ -1,16 +0,0 @@-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/ex5.ys
@@ -1,18 +0,0 @@--(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
@@ -1,18 +0,0 @@--(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))))-
yices-painless.cabal view
@@ -1,5 +1,5 @@ Name: yices-painless-Version: 0.1.1+Version: 0.1.2 Synopsis: An embedded language for programming the Yices SMT solver Description: This library defines an embedded language in Haskell for programming@@ -13,14 +13,16 @@ 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.+ The embedded language embeds both terms, functions 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.+ Uninterpreted functions may be introduced via variables as well. . More information about Yices: .