diff options
| -rw-r--r-- | Yices/Painless/Language.hs | 184 | ||||
| -rw-r--r-- | Yices/Painless/Type.hs | 18 | ||||
| -rw-r--r-- | tests/examples/ex24.hs | 16 | ||||
| -rw-r--r-- | tests/examples/ex5.ys | 18 | ||||
| -rw-r--r-- | tests/examples/ex6.ys | 18 | ||||
| -rw-r--r-- | yices-painless.cabal | 10 |
6 files changed, 176 insertions, 88 deletions
diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs index a607f60..f95fa56 100644 --- a/Yices/Painless/Language.hs +++ b/Yices/Painless/Language.hs @@ -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 @@ module Yices.Painless.Language ( -- * Building Yices propositions. Yices, Exp, + BitVector, -- ** Scalar introduction -- constant, @@ -71,6 +93,9 @@ module Yices.Painless.Language ( -- ** Bit vectors -- $BitInstances + -- ** Uninterpreted functions + -- $Functions + -- ** Conditional expressions (?), @@ -86,12 +111,15 @@ module Yices.Painless.Language ( -- * 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 @@ import qualified Yices.Painless.Tuple as Tuple -- 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,8 +507,12 @@ data YicesProg r where 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 @@ 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 +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 @@ convertOpenExp lyt = cvt 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 @@ data OpenYices t where -- |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 @@ type OFun t = OpenFun () t -- 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,17 +897,24 @@ prettyYices n (OY f) = prettyFun n f 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. -- @@ -856,7 +923,9 @@ prettyFun lvl fun = 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 @@ solve q' = do Yices.setTypeChecker True let t = convertYices q -- bind all the variables - print t + -- print t (g,e) <- execY c t @@ -953,7 +1022,7 @@ solve q' = do 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 @@ solve q' = do 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 @@ get m v (YType (ty :: ScalarType t)) d -- 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 @@ 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 +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:/ @@ -1085,6 +1189,22 @@ exec c (Var i) = do 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 eb <- exec c b diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs index ad9bfb4..791e352 100644 --- a/Yices/Painless/Type.hs +++ b/Yices/Painless/Type.hs @@ -214,6 +214,12 @@ data ScalarType a where 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 @@ instance Show (ScalarType a) where -- Querying scalar type representations -- + -- |Integral types -- class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where @@ -516,6 +523,17 @@ instance IsBounded CSChar where 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 -- class Typeable a => IsScalar a where diff --git a/tests/examples/ex24.hs b/tests/examples/ex24.hs deleted file mode 100644 index 6327503..0000000 --- a/tests/examples/ex24.hs +++ /dev/null @@ -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 - ] diff --git a/tests/examples/ex5.ys b/tests/examples/ex5.ys deleted file mode 100644 index e813861..0000000 --- a/tests/examples/ex5.ys +++ /dev/null @@ -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)) - diff --git a/tests/examples/ex6.ys b/tests/examples/ex6.ys deleted file mode 100644 index 0bd00f3..0000000 --- a/tests/examples/ex6.ys +++ /dev/null @@ -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)))) - diff --git a/yices-painless.cabal b/yices-painless.cabal index b215e4d..2aa8722 100644 --- a/yices-painless.cabal +++ b/yices-painless.cabal @@ -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 @@ Description: 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: . |