diff --git a/Language/SMTLib2.hs b/Language/SMTLib2.hs --- a/Language/SMTLib2.hs +++ b/Language/SMTLib2.hs @@ -56,6 +56,7 @@ interpolationGroup, assertInterp, getInterpolant, + interpolate, -- * Expressions var,varNamed,varNamedAnn,varAnn,argVars,argVarsAnn,argVarsAnnNamed, untypedVar,untypedNamedVar, diff --git a/Language/SMTLib2/Internals.hs b/Language/SMTLib2/Internals.hs --- a/Language/SMTLib2/Internals.hs +++ b/Language/SMTLib2/Internals.hs @@ -48,10 +48,11 @@ SMTGetUnsatCore :: SMTRequest [ClauseId] SMTSimplify :: SMTType t => SMTExpr t -> SMTRequest (SMTExpr t) SMTGetInterpolant :: [InterpolationGroup] -> SMTRequest (SMTExpr Bool) + SMTInterpolate :: [SMTExpr Bool] -> SMTRequest [SMTExpr Bool] SMTComment :: String -> SMTRequest () SMTExit :: SMTRequest () SMTApply :: Tactic -> SMTRequest [SMTExpr Bool] - SMTNameExpr :: String -> SMTExpr t -> SMTRequest Integer + SMTNameExpr :: SMTType t => String -> SMTExpr t -> SMTRequest Integer SMTNewInterpolationGroup :: SMTRequest InterpolationGroup SMTNewClauseId :: SMTRequest ClauseId deriving Typeable @@ -109,7 +110,7 @@ mangle :: Mangling t -- | A type class for all types which support arithmetic operations in SMT -class (SMTValue t,Num t) => SMTArith t +class (SMTValue t,Num t,SMTAnnotation t ~ ()) => SMTArith t -- | Lifts the 'Ord' class into SMT class (SMTType t) => SMTOrd t where @@ -208,7 +209,7 @@ Exists :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool Let :: Integer -> [SMTExpr Untyped] -> SMTExpr b -> SMTExpr b App :: (Args arg,SMTType res) => SMTFunction arg res -> arg -> SMTExpr res - Named :: SMTExpr a -> String -> Integer -> SMTExpr a + Named :: SMTExpr a -> Integer -> SMTExpr a InternalObj :: (SMTType t,Typeable a,Ord a,Show a) => a -> SMTAnnotation t -> SMTExpr t UntypedExpr :: SMTType t => SMTExpr t -> SMTExpr Untyped UntypedExprValue :: SMTValue t => SMTExpr t -> SMTExpr UntypedValue @@ -221,7 +222,7 @@ , bvSortUntyped :: Bool } | ArraySort [a] a | NamedSort String [a] - deriving (Eq,Show,Functor,Foldable,Traversable) + deriving (Eq,Ord,Show,Functor,Foldable,Traversable) type Sort = Fix Sort' @@ -231,16 +232,16 @@ | BVValue { bvValueWidth :: Integer , bvValueValue :: Integer } | ConstrValue String [Value] (Maybe (String,[Sort])) - deriving (Eq,Show) + deriving (Eq,Ord,Show) data SMTFunction arg res where SMTEq :: SMTType a => SMTFunction [SMTExpr a] Bool SMTMap :: (Liftable arg,SMTType res,Args i) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res) SMTFun :: (Args arg,SMTType res) => Integer -> SMTAnnotation res -> SMTFunction arg res SMTBuiltIn :: (Liftable arg,SMTType res) => String -> SMTAnnotation res -> SMTFunction arg res - SMTOrd :: (SMTType a) => SMTOrdOp -> SMTFunction (SMTExpr a,SMTExpr a) Bool - SMTArith :: (SMTType a,Num a) => SMTArithOp -> SMTFunction [SMTExpr a] a - SMTMinus :: (SMTType a,Num a) => SMTFunction (SMTExpr a,SMTExpr a) a + SMTOrd :: (SMTArith a) => SMTOrdOp -> SMTFunction (SMTExpr a,SMTExpr a) Bool + SMTArith :: (SMTArith a) => SMTArithOp -> SMTFunction [SMTExpr a] a + SMTMinus :: (SMTArith a) => SMTFunction (SMTExpr a,SMTExpr a) a SMTIntArith :: SMTIntArithOp -> SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer SMTDivide :: SMTFunction (SMTExpr Rational,SMTExpr Rational) Rational SMTNeg :: (SMTType a,Num a) => SMTFunction (SMTExpr a) a @@ -777,7 +778,7 @@ class TypeableNat n where typeOfNat :: Proxy n -> TypeRep - typeOfNat p = Prelude.foldl + typeOfNat p = foldl (\c _ -> mkTyConApp (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'S") [c]) (mkTyConApp (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'Z") []) (genericReplicate (reflectNat p 0) ()) @@ -858,7 +859,7 @@ reifyNat' 0 f = f (Proxy :: Proxy Z) reifyNat' n f = reifyNat' (n-1) (\(_::Proxy n) -> f (Proxy::Proxy (S n))) -data BitVector (b :: BVKind) = BitVector Integer deriving (Eq,Ord) +data BitVector (b :: BVKind) = BitVector Integer deriving (Eq,Ord,Typeable) instance TypeableBVKind k => Typeable (BitVector k) where typeOf _ = mkTyConApp @@ -899,15 +900,16 @@ reifySum :: (Num a,Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r reifySum n1 n2 f - | n1 < 0 || n2 < 0 = error "smtlib2: Cann only reify numbers >= 0." + | n1 < 0 || n2 < 0 = error "smtlib2: Can only reify numbers >= 0." | otherwise = reifySum' n1 n2 f where reifySum' :: (Num a,Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r reifySum' 0 n2' f' = reifyNat n2' $ \(_::Proxy i) -> f' (Proxy::Proxy Z) (Proxy::Proxy i) (Proxy::Proxy i) - reifySum' n1' n2' f' = reifySum' (n1'-1) n2' $ \(_::Proxy i1) (_::Proxy i2) (_::Proxy i3) - -> f' (Proxy::Proxy (S i1)) (Proxy::Proxy i2) (Proxy::Proxy (S i3)) + reifySum' n1' n2' f' = reifySum' (n1'-1) n2' $ + \(_::Proxy i1) (_::Proxy i2) (_::Proxy (Add i1 i2)) + -> f' (Proxy::Proxy (S i1)) (Proxy::Proxy i2) (Proxy::Proxy (S (Add i1 i2))) reifyExtract :: (Num a,Ord a) => a -> a -> a -> (forall n1 n2 n3 n4. (TypeableNat n1,TypeableNat n2,TypeableNat n3,TypeableNat n4,Add n4 n2 ~ S n3) @@ -1079,13 +1081,11 @@ showsPrec 11 fun . showChar ' ' . strArgs) -showExpr p (Named expr name nc) = let strExpr = showExpr 11 expr - in showParen (p>10) (showString "Named " . - strExpr . - showChar ' ' . - showsPrec 11 name . - showChar ' ' . - showsPrec 11 nc) +showExpr p (Named expr i) = let strExpr = showExpr 11 expr + in showParen (p>10) (showString "Named " . + strExpr . + showChar ' ' . + showsPrec 11 i) showExpr p (InternalObj obj ann) = showParen (p>10) (showString "InternalObj " . showsPrec 11 obj . showChar ' ' . @@ -1170,7 +1170,7 @@ quantificationLevel (Exists lvl _ _) = lvl+1 quantificationLevel (Let lvl _ _) = lvl+1 quantificationLevel (App _ arg) = maximum $ fmap quantificationLevel $ fromArgs arg -quantificationLevel (Named expr _ _) = quantificationLevel expr +quantificationLevel (Named expr _) = quantificationLevel expr quantificationLevel (UntypedExpr e) = quantificationLevel e quantificationLevel (UntypedExprValue e) = quantificationLevel e quantificationLevel _ = 0 diff --git a/Language/SMTLib2/Internals/Instances.hs b/Language/SMTLib2/Internals/Instances.hs --- a/Language/SMTLib2/Internals/Instances.hs +++ b/Language/SMTLib2/Internals/Instances.hs @@ -65,7 +65,7 @@ extractAnnotation (Forall _ _ _) = () extractAnnotation (Exists _ _ _) = () extractAnnotation (Let _ _ f) = extractAnnotation f -extractAnnotation (Named x _ _) = extractAnnotation x +extractAnnotation (Named x _) = extractAnnotation x extractAnnotation (App f arg) = inferResAnnotation f (extractArgAnnotation arg) extractAnnotation (InternalObj _ ann) = ann extractAnnotation (UntypedExpr (expr::SMTExpr t)) = ProxyArg (undefined::t) (extractAnnotation expr) @@ -1274,7 +1274,7 @@ (fmap (\s -> withSort mp s ProxyArg) args) f Nothing -> error $ "smtlib2: Datatype "++name++" not defined." -withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTType t,Num t) => t -> SMTAnnotation t -> r) -> Maybe r +withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTArith t) => t -> SMTAnnotation t -> r) -> Maybe r withNumSort _ (Fix IntSort) f = Just $ f (undefined::Integer) () withNumSort _ (Fix RealSort) f = Just $ f (undefined::Rational) () withNumSort _ _ _ = Nothing @@ -1330,9 +1330,9 @@ (s',args') <- foldArgsM f s arg return (s',[ App fun arg' | arg' <- args' ]) -foldExprM f s (Named expr name i) = do +foldExprM f s (Named expr i) = do (s',exprs') <- foldExprM f s expr - return (s',[ Named expr' name i + return (s',[ Named expr' i | expr' <- exprs' ]) foldExprM f s (UntypedExpr e) = do (s',exprs') <- foldExprM f s e @@ -1559,9 +1559,9 @@ x -> x compareExprs (App _ _) _ = LT compareExprs _ (App _ _) = GT -compareExprs (Named _ n1 i1) (Named _ n2 i2) = compare (n1,i1) (n2,i2) -compareExprs (Named _ _ _) _ = LT -compareExprs _ (Named _ _ _) = GT +compareExprs (Named _ i1) (Named _ i2) = compare i1 i2 +compareExprs (Named _ _) _ = LT +compareExprs _ (Named _ _) = GT compareExprs (InternalObj o1 ann1) (InternalObj o2 ann2) = case compare (typeOf o1) (typeOf o2) of EQ -> case compare (typeOf ann1) (typeOf ann2) of EQ -> case cast (o2,ann2) of @@ -1607,9 +1607,9 @@ (Let l1 a1 f1,Let l2 a2 f2) -> if l1==l2 && a1==a2 then eqExpr f1 f2 else Nothing - (Named e1 n1 nc1,Named e2 n2 nc2) -> if n1==n2 && nc1 == nc2 - then eqExpr e1 e2 - else Nothing + (Named e1 i1,Named e2 i2) -> if i1==i2 + then eqExpr e1 e2 + else Nothing (App f1 arg1,App f2 arg2) -> case cast f2 of Nothing -> Nothing Just f2' -> case cast arg2 of diff --git a/Language/SMTLib2/Internals/Interface.hs b/Language/SMTLib2/Internals/Interface.hs --- a/Language/SMTLib2/Internals/Interface.hs +++ b/Language/SMTLib2/Internals/Interface.hs @@ -231,6 +231,9 @@ getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool) getInterpolant grps = smtBackend $ \b -> smtHandle b (SMTGetInterpolant grps) +interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool] +interpolate exprs = smtBackend $ \b -> smtHandle b (SMTInterpolate exprs) + -- | Set an option for the underlying SMT solver setOption :: Monad m => SMTOption -> SMT' m () setOption opt = smtBackend $ \b -> smtHandle b (SMTSetOption opt) @@ -647,7 +650,7 @@ => String -> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a) named name expr = do i <- smtBackend $ \b -> smtHandle b (SMTNameExpr name expr) - return (Named expr name i,Var i (extractAnnotation expr)) + return (Named expr i,Var i (extractAnnotation expr)) -- | Like `named`, but defaults the name to "named". named' :: (SMTType a,SMTAnnotation a ~ (),Monad m) diff --git a/Language/SMTLib2/Pipe.hs b/Language/SMTLib2/Pipe.hs --- a/Language/SMTLib2/Pipe.hs +++ b/Language/SMTLib2/Pipe.hs @@ -6,7 +6,7 @@ withPipe, exprToLisp, exprToLispWith, - lispToExpr, + lispToExpr,lispToExprWith, sortToLisp,lispToSort, renderExpr, renderExpr', @@ -195,6 +195,10 @@ = Left $ L.List [L.Symbol "get-interpolant" ,L.List [ L.Symbol $ T.pack ("i"++show g) | InterpolationGroup g <- grps ] ] +renderSMTRequest _ getName dts (SMTInterpolate exprs) + = Left $ L.List $ (L.Symbol "get-interpolant"): + [ exprToLisp expr getName dts + | expr <- exprs ] renderSMTRequest _ _ _ (SMTSetOption opt) = Left $ L.List $ [L.Symbol "set-option"] ++(case opt of @@ -262,7 +266,7 @@ return ((),pipe { smtState = (smtState pipe) { declaredDataTypes = ndts } }) handleRequest pipe (SMTDeclareSort name arity) = return ((),pipe) handleRequest pipe (SMTDeclareFun info) - = let (v,name,nst) = smtStateAddFun info (smtState pipe) + = let (v,_,nst) = smtStateAddFun info (smtState pipe) in return (v,pipe { smtState = nst }) handleRequest pipe (SMTDefineFun name (_::Proxy arg) argAnn (body::SMTExpr res)) = do let finfo = FunInfo { funInfoProxy = Proxy::Proxy (arg,res) @@ -285,6 +289,19 @@ gcast (Just $ Fix BoolSort) 0 val of Just (Just x) -> return (x,pipe) _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val +handleRequest pipe (SMTInterpolate exprs) = case exprs of + [] -> return ([],pipe) + e:es -> do + resp <- mapM (\_ -> do + val <- parseResponse pipe + case lispToExpr commonFunctions + (findName $ smtState pipe) + (declaredDataTypes $ smtState pipe) + gcast (Just $ Fix BoolSort) 0 val of + Just (Just x) -> return x + _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val + ) es + return (resp,pipe) handleRequest pipe (SMTSetOption opt) = return ((),pipe) handleRequest pipe (SMTSetLogic name) = return ((),pipe) handleRequest pipe SMTGetProof = do @@ -396,13 +413,14 @@ _ -> error $ "smtlib2: Couldn't parse goal "++show expr _ -> error $ "smtlib2: Couldn't parse goal description "++show val ) goals,pipe) -handleRequest pipe (SMTNameExpr name expr) = do - return (nc,pipe { smtState = nst }) +handleRequest pipe (SMTNameExpr name (expr::SMTExpr t)) = do + return (i,pipe { smtState = nst }) where - nc = case Map.lookup name (nameCount $ smtState pipe) of - Just n -> n - Nothing -> 0 - nst = (smtState pipe) { nameCount = Map.insert name (nc+1) (nameCount $ smtState pipe) } + finfo = FunInfo { funInfoProxy = Proxy::Proxy ((),t) + , funInfoArgAnn = () + , funInfoResAnn = extractAnnotation expr + , funInfoName = Just name } + (i,_,nst) = smtStateAddFun finfo (smtState pipe) handleRequest pipe SMTNewInterpolationGroup = do return (InterpolationGroup igrp,pipe { smtState = nst }) where @@ -425,6 +443,9 @@ Unknown -> Just "unknown" renderSMTResponse getName dts (SMTGetInterpolant grps) expr = Just $ renderExpr' getName dts expr +renderSMTResponse getName dts (SMTInterpolate _) exprs + = Just $ unwords [ renderExpr' getName dts expr + | expr <- exprs ] renderSMTResponse getName dts SMTGetProof proof = Just $ renderExpr' getName dts proof renderSMTResponse getName dts (SMTSimplify _) expr @@ -436,7 +457,12 @@ [exprToLisp goal getName dts | goal <- goals ] renderSMTResponse _ _ SMTGetUnsatCore core = Just (show core) -renderSMTResponse _ _ SMTGetModel mdl = Just (show mdl) +renderSMTResponse getName dts SMTGetModel mdl + = Just $ "(model"++concat assignments++")" + where + assignments = [ "\n ("++getName fun++" "++ + renderExpr' getName dts expr++")" + | (fun,(_,_,expr)) <- Map.toList $ modelFunctions mdl ] renderSMTResponse _ _ _ _ = Nothing -- | Spawn a new SMT solver process and create a pipe to communicate with it. @@ -589,11 +615,12 @@ in if Prelude.null x' then l else L.List $ l:x' -exprToLispWith objs (Named expr name nc) mp dts +exprToLispWith objs (Named expr idx) mp dts = let expr' = exprToLispWith objs expr mp dts + name = mp idx in L.List [L.Symbol "!",expr' ,L.Symbol ":named" - ,L.Symbol $ T.pack $ escapeName (Left (name,nc))] + ,L.Symbol $ T.pack name] exprToLispWith objs (InternalObj obj ann) _ _ = objs obj exprToLispWith objs (UntypedExpr expr) mp dts = exprToLispWith objs expr mp dts @@ -973,7 +1000,24 @@ -> Integer -- ^ The current quantification level -> L.Lisp -- ^ The lisp expression to parse -> Maybe b -lispToExpr fun bound dts f expected lvl l = case lispToValue dts expected l of +lispToExpr = lispToExprWith lispToExpr + +lispToExprWith :: (forall b. FunctionParser + -> (T.Text -> Maybe (SMTExpr Untyped)) + -> DataTypeInfo + -> (forall a. SMTType a => SMTExpr a -> b) + -> Maybe Sort + -> Integer + -> L.Lisp -> Maybe b) -- ^ Recursive descend function + -> FunctionParser -- ^ The parser to use for function symbols + -> (T.Text -> Maybe (SMTExpr Untyped)) -- ^ How to handle variable names + -> DataTypeInfo -- ^ Information about declared data types + -> (forall a. SMTType a => SMTExpr a -> b) -- ^ A function to apply to the resulting SMT expression + -> Maybe Sort -- ^ If you know the sort of the expression, you can pass it here. + -> Integer -- ^ The current quantification level + -> L.Lisp -- ^ The lisp expression to parse + -> Maybe b +lispToExprWith recp fun bound dts f expected lvl l = case lispToValue dts expected l of Just val -> valueToHaskell dts (\_ (val'::t) ann -> asValueType (undefined::t) ann $ @@ -985,11 +1029,11 @@ Nothing -> Nothing Just subst -> entype (\expr -> Just $ f expr) subst L.List [L.Symbol "forall",L.List args',body] - -> fmap f $ quantToExpr Forall fun bound dts args' lvl body + -> fmap f $ quantToExpr recp Forall fun bound dts args' lvl body L.List [L.Symbol "exists",L.List args',body] - -> fmap f $ quantToExpr Exists fun bound dts args' lvl body + -> fmap f $ quantToExpr recp Exists fun bound dts args' lvl body L.List [L.Symbol "let",L.List args',body] - -> parseLet fun bound dts f expected args' lvl body + -> parseLet recp fun bound dts f expected args' lvl body L.List [L.Symbol "_",L.Symbol "as-array",fsym] -> case parseFun fun fsym fun dts of Nothing -> Nothing @@ -1020,9 +1064,9 @@ [] -> Just $ App rfun rargs _ -> Nothing) of Just e -> f e - Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++": "++show arg_tps++" ("++show args'++")." + Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++": "++show arg_tps++" (Expected: "++show args'++")." Just (DefinedParser arg_tps _ parse) -> do - nargs <- mapM (\(el,tp) -> lispToExpr fun bound dts mkUntyped (Just tp) lvl el) + nargs <- mapM (\(el,tp) -> recp fun bound dts mkUntyped (Just tp) lvl el) (zip args' arg_tps) parse $ \(rfun :: SMTFunction arg res) -> case (do @@ -1032,16 +1076,16 @@ [] -> Just $ App rfun rargs _ -> Nothing) of Just e -> f e - Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym + Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++" (Expected: "++show arg_tps++")" _ -> Nothing where lispToExprs constr exprs = do - res <- mapM (\arg -> lispToExpr fun bound dts mkUntyped Nothing lvl arg) exprs + res <- mapM (\arg -> recp fun bound dts mkUntyped Nothing lvl arg) exprs let sorts = fmap (entype exprSort) res if constr sorts then return res else (case generalizeSorts sorts of - Just sorts' -> mapM (\(arg,sort') -> lispToExpr fun bound dts mkUntyped (Just sort') lvl arg) (zip exprs sorts') + Just sorts' -> mapM (\(arg,sort') -> recp fun bound dts mkUntyped (Just sort') lvl arg) (zip exprs sorts') Nothing -> return res) preprocessHack (L.List ((L.Symbol "concat"):args)) = foldl1 (\expr arg -> L.List [L.Symbol "concat",expr,arg]) args preprocessHack x = x @@ -1073,12 +1117,19 @@ exprSort :: SMTType a => SMTExpr a -> Sort exprSort (expr::SMTExpr a) = getSort (undefined::a) (extractAnnotation expr) -quantToExpr :: (Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool) +quantToExpr :: (forall b. FunctionParser + -> (T.Text -> Maybe (SMTExpr Untyped)) + -> DataTypeInfo + -> (forall a. SMTType a => SMTExpr a -> b) + -> Maybe Sort + -> Integer + -> L.Lisp -> Maybe b) -- ^ Recursive descend function + -> (Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool) -> FunctionParser -> (T.Text -> Maybe (SMTExpr Untyped)) -> DataTypeInfo -> [L.Lisp] -> Integer -> L.Lisp -> Maybe (SMTExpr Bool) -quantToExpr con fun bound dts args lvl body = do +quantToExpr recp con fun bound dts args lvl body = do argLst <- mapM (\el -> case el of L.List [L.Symbol name,tp] -> do sort <- lispToSort tp @@ -1090,21 +1141,28 @@ bound' name = case Map.lookup name argMp of Just (idx,tp) -> Just (QVar lvl idx tp) Nothing -> bound name - lispToExpr fun bound' dts + recp fun bound' dts (\body' -> case cast body' of Just body'' -> con lvl (fmap snd argLst) body'' ) (Just $ Fix BoolSort) (lvl+1) body -parseLet :: FunctionParser +parseLet :: (forall b. FunctionParser + -> (T.Text -> Maybe (SMTExpr Untyped)) + -> DataTypeInfo + -> (forall a. SMTType a => SMTExpr a -> b) + -> Maybe Sort + -> Integer + -> L.Lisp -> Maybe b) -- ^ Recursive descend function + -> FunctionParser -> (T.Text -> Maybe (SMTExpr Untyped)) -> DataTypeInfo -> (forall a. SMTType a => SMTExpr a -> b) -> Maybe Sort -> [L.Lisp] -> Integer -> L.Lisp -> Maybe b -parseLet fun bound dts app expected args lvl body = do +parseLet recp fun bound dts app expected args lvl body = do argLst <- mapM (\el -> case el of L.List [L.Symbol name,expr] -> do - expr' <- lispToExpr fun bound dts UntypedExpr Nothing (lvl+1) expr + expr' <- recp fun bound dts UntypedExpr Nothing (lvl+1) expr return (name,expr') _ -> Nothing ) args @@ -1113,50 +1171,10 @@ bound' name = case Map.lookup name argMp of Just (idx,tp) -> Just (QVar lvl idx tp) Nothing -> bound name - lispToExpr fun bound' dts + recp fun bound' dts (\body' -> app (Let lvl (fmap snd argLst) body') ) expected (lvl+1) body -{- -data LetStruct where - LetStruct :: SMTType a => SMTAnnotation a -> SMTExpr a -> (SMTExpr a -> LetStruct) -> LetStruct - EndLet :: SMTType a => SMTExpr a -> LetStruct -parseLetStruct :: FunctionParser - -> (T.Text -> Maybe (SMTExpr Untyped)) - -> DataTypeInfo - -> Maybe Sort - -> [L.Lisp] -> L.Lisp -> LetStruct -parseLetStruct fun bound tps expected (L.List [L.Symbol name,expr]:rest) arg - = case lispToExpr fun bound tps - (\expr' -> LetStruct (extractAnnotation expr') expr' $ - \sym -> parseLetStruct fun - (\txt -> if txt==name - then Just $ mkUntyped sym - else bound txt) tps expected rest arg - ) Nothing expr of - Nothing -> error $ "smtlib2: Failed to parse argument in let-expression "++show expr - Just x -> x -parseLetStruct fun bound tps expected [] arg - = case lispToExpr fun bound tps EndLet expected arg of - Nothing -> error $ "smtlib2: Failed to parse body of let-expression: "++show arg - Just x -> x -parseLetStruct _ _ _ _ (el:_) _ = error $ "smtlib2: Invalid entry "++show el++" in let construct." - -extractType :: (forall a. SMTType a => a -> b) -> LetStruct -> b -extractType f (EndLet x) = f (getUndef x) -extractType f (LetStruct _ expr g) = extractType f (g expr) - -convertLetStructT :: SMTType a => LetStruct -> SMTExpr a -convertLetStructT (EndLet x) = case gcast x of - Just x' -> x' - Nothing -> error "smtlib2: Type error while converting let structure." -convertLetStructT (LetStruct ann x g) = Let ann x (\sym -> convertLetStructT (g sym)) - -convertLetStruct :: (forall a. SMTType a => SMTExpr a -> b) -> LetStruct -> b -convertLetStruct f x - = extractType - (\(_::t) -> f (convertLetStructT x :: SMTExpr t)) x --} withFirstArgSort :: DataTypeInfo -> L.Lisp -> [Sort] -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a withFirstArgSort dts _ (s:rest) f = case s of Fix (BVSort i False) -> if any (\sort -> case sort of @@ -1287,9 +1305,9 @@ where p :: L.Lisp -> SMTOrdOp -> DataTypeInfo -> Maybe FunctionParser' p sym op dts = Just $ OverloadedParser allEqConstraint (const $ Just $ getSort (undefined::Bool) ()) $ - \sort_arg _ f -> withFirstArgSort dts sym sort_arg $ - \(_::t) _ - -> Just $ f (SMTOrd op :: SMTFunction (SMTExpr t,SMTExpr t) Bool) + \[sort_arg,_] _ f -> withNumSort dts sort_arg $ + \(_::t) _ + -> f (SMTOrd op :: SMTFunction (SMTExpr t,SMTExpr t) Bool) arithOpParser = FunctionParser $ \sym _ dts -> case sym of L.Symbol "+" -> Just $ OverloadedParser allEqConstraint (\sorts -> Just (head sorts)) $ @@ -1436,13 +1454,13 @@ -> Just $ OverloadedParser (const True) (\sort_arg -> case sort_arg of (Fix (ArraySort _ vsort):_) -> Just vsort - _ -> error "smtlib2: Wrong arguments for select function.") $ + _ -> error $ "smtlib2: Wrong arguments for select function ("++show sort_arg++").") $ \sort_arg sort_ret f -> case sort_arg of (Fix (ArraySort isort1 _):_) -> withSorts dts isort1 $ \(_::i) _ -> withSort dts sort_ret $ \(_::v) _ -> Just $ f (SMTSelect::SMTFunction (SMTExpr (SMTArray i v),i) v) - _ -> error "smtlib2: Wrong arguments for select function." + _ -> error $ "smtlib2: Wrong arguments for select function ("++show sort_arg++")." _ -> Nothing storeParser = FunctionParser $ \sym _ dts -> case sym of diff --git a/smtlib2.cabal b/smtlib2.cabal --- a/smtlib2.cabal +++ b/smtlib2.cabal @@ -1,5 +1,5 @@ Name: smtlib2 -Version: 0.2 +Version: 0.3 Author: Henning Günther Maintainer: guenther@forsyte.at Synopsis: A type-safe interface to communicate with an SMT solver.