From 8159186fac5b4db0bd5f7d7cea0819e240fd555b Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Sat, 19 Oct 2013 08:54:43 -0700 Subject: Generalize to support arbitrary theories. The theory of natural numbers is defined in TcTypeNats. --- compiler/typecheck/TcInteract.lhs | 171 +++++--- compiler/typecheck/TcTypeNats.hs | 799 ++++++++------------------------------ 2 files changed, 289 insertions(+), 681 deletions(-) diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 118b99df78..960a737fb8 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -38,7 +38,7 @@ import TcEvidence import Outputable import TcMType ( zonkTcPredType ) -import TcTypeNats(isLinArithTyCon,decideLinArith,LinArithResult(..)) +import TcTypeNats(Theory(..), Result(..), thyVarName, linArith) import TcRnTypes import TcErrors @@ -47,15 +47,17 @@ import Maybes( orElse ) import Bag import MonadUtils(liftIO) -import Control.Monad ( foldM ) -import Data.Maybe ( catMaybes, mapMaybe ) +import Data.Maybe ( catMaybes, mapMaybe, maybeToList ) +import qualified Data.Map as Map +import Data.List ( tails ) import VarEnv -import Control.Monad( when, unless ) +import Control.Monad( when, unless, foldM, forM ) import Pair (Pair(..)) import Unique( hasKey ) import UniqFM +import UniqSet(foldUniqSet) import FastString ( sLit ) import DynFlags import Util @@ -1473,43 +1475,9 @@ doTopReactFunEq wi fl fun_tc args xi loc fam_ty = mkTyConApp fun_tc args try_improve_and_return - | isLinArithTyCon fun_tc args = - do { (gis,wis) <- getRelevantLinArithInerts - ; res <- liftIO $ decideLinArith gis wis wi - ; let addInerts = mapM_ insertInertItemTcS - setEvidence (ct, ev) = - setEvBind (ctEvId $ ctEvidence ct) ev - ; case res of - SolvedWanted ev -> do - addInerts wis - setEvidence (wi, ev) - traceTcS "[NATS]" (text "SOLVED WANTED") - IgnoreGiven -> do - addInerts wis - traceTcS "[NATS]" (text "IGNORING") - Impossible -> do emitInsoluble wi - traceTcS "[NATS]" (text "IMPOSSIBLE") - Progress new_wanted_work new_work new_is solved -> do - addInerts new_is - let mkWanted (tv, xi) = - do ev <- newWantedEvVarNC (mkEqPred (mkTyVarTy tv) xi) - return $ CTyEqCan - { cc_ev = ev, cc_tyvar = tv, cc_rhs = xi - , cc_loc = cc_loc wi } - mapM_ setEvidence solved - new_wanted_cts <- mapM mkWanted new_wanted_work - updWorkListTcS $ extendWorkListEqs $ - new_wanted_cts ++ new_work - let dbg x ys = text x $$ nest 2 (vcat $ map ppr ys) - traceTcS "[NATS]" $ - text "Progress" $$ - nest 2 (vcat - [ dbg "New wanted work:" (new_wanted_cts ++ new_work) - , dbg "Solved:" (map fst solved) - , dbg "Inerts" new_is - ] - ) - ; return $ SomeTopInt "LinArith" Stop + | thyRelevant linArith fun_tc args = + do { (gis,wis) <- getRelevantCtsFor linArith + ; decideExternal linArith gis wis wi } | otherwise = return NoTopInt @@ -1532,20 +1500,123 @@ doTopReactFunEq wi fl fun_tc args xi loc xcomp _ = panic "No more goals!" xev = XEvTerm xcomp xdecomp --- This gets givens and wanteds relevant to the numeric solver. --- The givens are just copies of what's in the inert set, while the wanteds --- are removed from the inert set. -getRelevantLinArithInerts :: TcS ([Ct], [Ct]) -getRelevantLinArithInerts = +decideExternal :: Theory t e v -> [Ct] -> [Ct] -> Ct -> TcS TopInteractResult +decideExternal thy givenCts wantedCts goalCt = + do proved <- prove assumptions goal + if proved + then do when (ctFlavour goalCt == Wanted) (solve goalCt) + mapM_ insertInertItemTcS wantedCts + done Stop + + -- Check if we are consistent with existing context + else do res <- check (goal : assumptions) + case res of + Unsat -> emitInsoluble goalCt >> done Stop + Unknown -> improve [] >>= prune >> done (ContinueWith goalCt) + Sat mo -> improve mo >>= prune >> done (ContinueWith goalCt) + + where + assumptions + | ctFlavour goalCt == Wanted = givens ++ wanteds + | otherwise = givens + + improve model = + do let candidates = + [ ( thyEq thy (thyVar thy x) (thyVal thy v) + , (xv, thyFromValue thy v) + ) | (x, v) <- model, xv <- maybeToList (Map.lookup x varMap) ] + ++ + [ ( thyEq thy (thyVar thy x) (thyVar thy y) + , (xv, mkTyVarTy yv) + ) | (x,xv):xs <- tails vars + , (y,yv) <- xs + , eqType (tyVarKind xv) (tyVarKind yv) ] + fmap catMaybes $ forM candidates $ \(prop,imp) -> + do proved <- prove (goal : assumptions) prop + return (if proved then Just imp else Nothing) + + prune eqs + | ctFlavour goalCt == Given = addWork (wantedCts ++ map toGivenEqCt eqs) + -- kick-out wanteds, hopefully none! + | otherwise = + do addWork =<< mapM toWantedEqCt eqs + simplifyInerts (zip wanteds wantedCts) (goal : givens) + + simplifyInerts [] _ = return () + simplifyInerts ((p, ct):todo) assmps = + do proved <- prove (map fst todo ++ assmps) p + if proved + then do solve ct + simplifyInerts todo assmps + else do insertInertItemTcS ct + simplifyInerts todo (p:assmps) + + -- Convert to the theory's representations + givens = map ctToTerm givenCts + wanteds = map ctToTerm wantedCts + goal = ctToTerm goalCt + vars = getVars (goalCt : wantedCts ++ givenCts) + varMap = Map.fromList vars + + ctToTerm CFunEqCan { cc_fun = tc, cc_tyargs = ts, cc_rhs = xi } = + thyToProp thy tc (map (thyToTerm thy) ts) (thyToTerm thy xi) + ctToTerm ct = pprPanic "ctToTerm" (text (thyName thy) <+> ppr ct) + + getVars :: [Ct] -> [(String,TyVar)] + getVars = map addName . foldUniqSet (:) [] . tyVarsOfTypes . concatMap ctTypes + where addName x = (thyVarName x, x) + + ctTypes CFunEqCan { cc_tyargs = [t1,t2], cc_rhs = xi } = [t1,t2,xi] + ctTypes ct = pprPanic "getVarTys" (ppr ct) + + -- Convenient names for common things: + toWantedEqCt (tv, xi) = + do ev <- newWantedEvVarNC (mkEqPred (mkTyVarTy tv) xi) + return $ CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = xi + , cc_loc = cc_loc goalCt } + + toGivenEqCt :: (TyVar,Xi) -> Ct + toGivenEqCt (tv, rhs) = + let lhs = mkTyVarTy tv + in CTyEqCan { cc_ev = CtGiven { ctev_pred = mkEqPred lhs rhs + , ctev_evtm =thyEv thy lhs rhs } + , cc_loc = cc_loc goalCt, cc_tyvar = tv, cc_rhs = rhs } + + solve :: Ct -> TcS () + solve ct = setEvBind (ctEvId $ ctEvidence ct) + $ uncurry (thyEv thy) $ getEqPredTys $ ctPred ct + + done :: StopOrContinue -> TcS TopInteractResult + done x = return (SomeTopInt (thyName thy) x) + + addWork :: [Ct] -> TcS () + addWork cs = updWorkListTcS (extendWorkListCts cs) + + check = liftIO . thySat thy [ (x, thyToType thy (tyVarKind xv)) + | (x,xv) <- vars ] + + prove ps p = + do x <- check (thyNot thy p : ps) + case x of + Unsat -> return True + _ -> return False + + + +{- This gets givens and wanteds relevant to the specified theory. +The givens are just copies of what's in the inert set, while the wanteds +are removed from the inert set. -} +getRelevantCtsFor :: Theory t e v -> TcS ([Ct], [Ct]) +getRelevantCtsFor thy = modifyInertTcS $ upd $ \fun_eqs-> - let (wanteds, rest_funeqs) = partCtFamHeadMap (isArith Wanted) fun_eqs - givens = getCtFamHeadMapCts (isArith Given) rest_funeqs + let (wanteds, rest_funeqs) = partCtFamHeadMap (consider Wanted) fun_eqs + givens = getCtFamHeadMapCts (consider Given) rest_funeqs in ((bagToList givens, bagToList wanteds), rest_funeqs) where - isArith fl ct + consider fl ct | fl == ctFlavour ct - , Just (tc,tys) <- isCFunEqCan_maybe ct = isLinArithTyCon tc tys + , Just (tc,tys) <- isCFunEqCan_maybe ct = thyRelevant thy tc tys | otherwise = False upd f i = diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index e4373efd1c..09b12b33dd 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -2,9 +2,8 @@ module TcTypeNats ( typeNatTyCons , typeNatCoAxiomRules , TcBuiltInSynFamily(..) - , LinArithResult(..) - , decideLinArith - , isLinArithTyCon + , Theory(..), Result(..), thyVarName + , linArith ) where import Type @@ -12,13 +11,12 @@ import Pair import TcType ( TcType ) import TyCon ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..) ) import Coercion ( Role(..) ) -import TcRnTypes ( Xi, Ct(..), CtLoc, ctFlavour, ctPred, CtFlavour(..) - , CtEvidence(..) ) +import TcRnTypes ( Xi ) import TcEvidence ( mkTcAxiomRuleCo, TcCoercion, EvTerm(..) ) import CoAxiom ( CoAxiomRule(..) ) import Name ( Name, BuiltInSyntax(..), nameUnique, nameOccName ) import OccName ( occNameString ) -import Var ( tyVarName, tyVarKind ) +import Var ( tyVarName ) import TysWiredIn ( typeNatKind, mkWiredInTyConName , promotedBoolTyCon , promotedFalseDataCon, promotedTrueDataCon @@ -34,21 +32,13 @@ import PrelNames ( gHC_TYPELITS ) import FamInst ( TcBuiltInSynFamily(..) ) import FastString ( FastString, fsLit ) -import Outputable ( ppr, panic, pprPanic ) -import UniqSet ( foldUniqSet ) +import Outputable ( ppr, panic, pprPanic, (<+>), text, int ) import qualified Data.Map as Map -import Data.Map (Map) import Data.Maybe ( isJust ) -import Data.List ( tails, genericReplicate ) -import Data.List ( genericReplicate ) import System.Cmd ( system ) +import System.Exit ( ExitCode(..) ) -isLinArithTyCon :: TyCon -> [Xi] -> Bool -isLinArithTyCon tc ts = - tc `elem` [ typeNatAddTyCon, typeNatLeqTyCon, typeNatSubTyCon ] || - (tc == typeNatMulTyCon && any (isJust . isNumLitTy) ts) - {------------------------------------------------------------------------------- Built-in type constructors for functions on type-lelve nats @@ -582,56 +572,138 @@ genLog x base = Just (exactLoop 0 x) {- ----------------------------------------------------------------------------- -Calling an external decision procedure +Calling an external decision procedure: generic interface ----------------------------------------------------------------------------- -} -data LinArithResult = SolvedWanted EvTerm - | IgnoreGiven - | Impossible - | Progress [(TyVar, Xi)] [Ct] [Ct] [(Ct, EvTerm)] - -- Args: - -- 1) turn into wanted and add to work list, - -- 2) stick in work list, and - -- 3) add to inert set - -- 4) discharged, set evidence - -data Op = Add | Sub | Mul | Leq | Eq | Implies | And - deriving Show - -data Term = Op Term Op Term - | Num Integer - | Bool Bool - | Var String - | Not Term - -termToSMT :: Term -> Expr -termToSMT term = - case term of - Op t1 op t2 -> opToSMT op (termToSMT t1) (termToSMT t2) - Num x -> fromInteger x - Bool x -> if x then true else false - Not t -> eNot (termToSMT t) - Var x -> app x [] - -opToSMT :: Op -> Expr -> Expr -> Expr -opToSMT op = - case op of - Add -> (+) - Sub -> (-) - Mul -> (*) - Leq -> nLeq - Eq -> (====) - Implies -> (===>) - And -> eAnd - -instance Show Term where +data Theory ty expr value = Theory + { thyName :: String + + , thyRelevant :: TyCon -> [Type] -> Bool + + , thyToProp :: TyCon -> [expr] -> expr -> expr + , thyToTerm :: Type -> expr + , thyToType :: Kind -> ty + , thyFromValue :: value -> Xi + + , thyVal :: value -> expr + , thyVar :: String -> expr + , thyEq :: expr -> expr -> expr + , thyNot :: expr -> expr + + , thySat :: [(String,ty)] -> [expr] -> IO (Result value) + , thyEv :: Xi -> Xi -> EvTerm + } + +data Result v = Sat [(String, v)] + | Unsat + | Unknown + deriving (Show) + +thyVarName :: TyVar -> String +thyVarName x = let n = tyVarName x + u = nameUnique n + in occNameString (nameOccName n) ++ "_" ++ show u + + + +{------------------------------------------------------------------------------- +Concrete instance for the theory of natural numbers +-------------------------------------------------------------------------------} + +data Ty = TNat | TBool + +data Op = Add | Sub | Mul | Leq | Eq + +data Expr = Op Op Expr Expr + | Not Expr + | Num Integer + | Bool Bool + | Var String + +data Value = VInt Integer | VBool Bool + +linArith :: Theory Ty Expr Value +linArith = Theory + { thyName = "linArith" + + , thyRelevant = laRelevant + + , thyToProp = laToProp + , thyToTerm = laToExpr + , thyToType = laToType + , thyFromValue = laFromValue + + , thyVal = laValExpr + , thyVar = Var + , thyEq = \e1 e2 -> Op Eq e1 e2 + , thyNot = Not + + , thySat = laSat + , thyEv = evBySMT + } + +laRelevant :: TyCon -> [Type] -> Bool +laRelevant tc ts = + tc `elem` [ typeNatAddTyCon, typeNatLeqTyCon, typeNatSubTyCon ] || + (tc == typeNatMulTyCon && any (isJust . isNumLitTy) ts) + + +laToProp :: TyCon -> [Expr] -> Expr -> Expr +laToProp tc [e1,e2] e = Op Eq (Op (laToOp tc) e1 e2) e +laToProp tc es _ = pprPanic "linArith" + $ text "Unexpected arity for" <+> ppr tc + <+> int (length es) + +laToOp :: TyCon -> Op +laToOp tc + | tc == typeNatAddTyCon = Add + | tc == typeNatSubTyCon = Sub + | tc == typeNatMulTyCon = Mul + | tc == typeNatLeqTyCon = Leq + | otherwise = pprPanic "tyConToOp" (ppr tc) + +laToExpr :: Type -> Expr +laToExpr ty + | Just x <- getTyVar_maybe ty = Var (thyVarName x) + | Just x <- isNumLitTy ty = Num x + | Just (tc,[]) <- splitTyConApp_maybe ty + , Just x <- tyConToBool tc = Bool x + | otherwise = pprPanic "typeToTerm" (ppr ty) + +tyConToBool :: TyCon -> Maybe Bool +tyConToBool tc + | tc == promotedTrueDataCon = Just True + | tc == promotedFalseDataCon = Just False +tyConToBool _ = Nothing + + + +laFromValue :: Value -> Xi +laFromValue (VInt n) = num n +laFromValue (VBool b) = bool b + +laValExpr :: Value -> Expr +laValExpr (VInt n) = Num n +laValExpr (VBool b) = Bool b + +laToType :: Kind -> Ty +laToType k = + case splitTyConApp_maybe k of + Just (tc,[]) + | tc == promotedBoolTyCon -> TBool + | tc == typeNatKindCon -> TNat + _ -> pprPanic "laToType" (text "Unexpected kind:" <+> ppr k) + + +-- For debugging +instance Show Expr where showsPrec p v = case v of Num n -> shows n Var s -> showString s Not v -> showParen (p > 8) $ showString "!" . showsPrec 8 v Bool b -> shows b - Op a o b -> showParen (p > pOp) $ showsPrec pL a . showString opStr + Op o a b -> showParen (p > pOp) $ showsPrec pL a . showString opStr . showsPrec pR b where (pOp, pL, pR, opStr) = @@ -641,151 +713,12 @@ instance Show Term where Mul -> (7, 7, 8, " * ") Leq -> (4, 5, 5, " <= ") Eq -> (4, 5, 5, " == ") - Implies -> (1, 2, 1, " -> ") - And -> (3, 4, 3, " & ") -tyConToOp :: TyCon -> Op -tyConToOp tc - | tc == typeNatAddTyCon = Add - | tc == typeNatSubTyCon = Sub - | tc == typeNatMulTyCon = Mul - | tc == typeNatLeqTyCon = Leq - | otherwise = pprPanic "tyConToOp" (ppr tc) - -tyConToBool :: TyCon -> Maybe Bool -tyConToBool tc - | tc == promotedTrueDataCon = Just True - | tc == promotedFalseDataCon = Just False -tyConToBool _ = Nothing - -varName :: TyVar -> String -varName x = let n = tyVarName x - u = nameUnique n - in occNameString (nameOccName n) ++ "_" ++ show u - -typeToTerm :: Type -> Term -typeToTerm ty - | Just x <- getTyVar_maybe ty = Var (varName x) - | Just x <- isNumLitTy ty = Num x - | Just (tc,[]) <- splitTyConApp_maybe ty - , Just x <- tyConToBool tc = Bool x - | otherwise = pprPanic "typeToTerm" (ppr ty) - -ctToTerm :: Ct -> Term -ctToTerm CFunEqCan { cc_fun = tc, cc_tyargs = [t1,t2], cc_rhs = xi } = - Op (Op (typeToTerm t1) (tyConToOp tc) (typeToTerm t2)) Eq (typeToTerm xi) -ctToTerm ct = pprPanic "ctToTerm" (ppr ct) - -termToType :: VarMap -> Term -> Xi -termToType vmap t = - case t of - Num n -> num n - Bool b -> bool b - Var x -> mkTyVarTy $ stringToTyVar vmap x - _ -> panic ("termToType: " ++ show t) - -stringToTyVar :: VarMap -> String -> TyVar -stringToTyVar vmap x = - case Map.lookup x vmap of - Just ty -> ty - Nothing -> panic ("stringToTyVar: " ++ x) - - -decideLinArith :: [Ct] -> [Ct] -> Ct -> IO LinArithResult -decideLinArith givenCts wantedCts goalCt = decide - where - givens = map ctToTerm givenCts - wanteds = map ctToTerm wantedCts - goal = ctToTerm goalCt - varMap = getVarTys (goalCt : wantedCts ++ givenCts) - flav = ctFlavour goalCt - - bySMT = uncurry evBySMT . getEqPredTys . ctPred - - noProgress = return (Progress [] [] (goalCt : wantedCts)) [] - - assumptions - | flav == Wanted = givens ++ wanteds - | otherwise = givens - - decide = - do yes <- prove varMap (assumptions ==> goal) - if yes - then return (if flav == Given then IgnoreGiven - else SolvedWanted (bySMT goalCt)) - else checkConsistent - - checkConsistent = - do res <- sat varMap (ands $ goal : assumptions) - case res of - Unsat -> return Impossible - Unknown -> improve [] - Sat m -> improve m - - improve model = - do let candidates = - [ (x, valueToTerm v) | (x, v) <- model ] ++ - [ (x, Var y) | (x,xv):xs <- tails (Map.toList varMap) - , (y,yv) <- xs - , eqType (tyVarKind xv) (tyVarKind yv) ] - eqs <- fmap concat $ mapM tryAssign candidates - prune eqs - - tryAssign (x, t) = - do yes <- prove varMap (goal : assumptions ==> Op (Var x) Eq t) - if not yes - then return [] - else return [(x, t)] - - prune eqs - | flav == Given = - do let newGiven = map (mkGivenCt varMap $ cc_loc goalCt) eqs - return $ Progress [] (wantedCts ++ newGiven) [goalCt] [] - | otherwise = - do let newWanted = [ (stringToTyVar varMap x, termToType varMap t) - | (x, t) <- eqs ] - (newInerts, solved) <- - simplifyInerts (zip wanteds wantedCts) - (goal : givens) [goalCt] [] - return $ Progress newWanted [] newInerts solved - - simplifyInerts [] _ done solved = return (done, solved) - simplifyInerts ((p, ct):todo) assmps done solved = - do yes <- prove varMap (map fst todo ++ assmps ==> p) - if yes - then simplifyInerts todo assmps done ((ct, bySMT ct):solved) - else simplifyInerts todo (p:assmps) (ct:done) solved - -mkGivenCt :: VarMap -> CtLoc -> (String, Term) -> Ct -mkGivenCt varMap loc (x, t) = - CTyEqCan { cc_ev = ev, cc_loc = loc, cc_tyvar = tv, cc_rhs = rhs } - where - ev = CtGiven { ctev_pred = mkEqPred lhs rhs - , ctev_evtm = evBySMT lhs rhs } - tv = stringToTyVar varMap x - lhs = mkTyVarTy tv - rhs = termToType varMap t - -getVarTys :: [Ct] -> VarMap -getVarTys = Map.fromList - . map addName - . foldUniqSet (:) [] - . tyVarsOfTypes - . concatMap ctTypes - where - addName x = (varName x, x) - - ctTypes CFunEqCan { cc_tyargs = [t1,t2], cc_rhs = xi } = [t1,t2,xi] - ctTypes ct = pprPanic "getVarTys" (ppr ct) -------------------------------------------------------------------------------- +-- Calling the solver -data Result = Sat [(String, Value)] - | Unsat - | Unknown - deriving (Show) - -instance Read Result where +instance Read (Result Value) where readsPrec _ xs = do ("sat", xs1) <- lex xs (vs,rest) <- readParen True getVals xs1 return (Sat vs, rest) @@ -804,450 +737,54 @@ instance Read Result where return ((name,val), rest1) - -data Value = VInt Integer | VBool Bool - -instance Show Value where - show (VInt n) = show n - show (VBool b) = show b - instance Read Value where readsPrec p s = [ (VInt n, s') | (n, s') <- readsPrec p s ] ++ [ (VBool True, s') | ("true", s') <- lex s ] ++ [ (VBool False, s') | ("false", s') <- lex s ] -valueToTerm :: Value -> Term -valueToTerm (VInt n) = Num n -valueToTerm (VBool b) = Bool b -type VarMap = Map String TyVar - -sat :: VarMap -> Term -> IO Result -sat varMap t = - do writeFile "ghc_input.smt" $ pp script - system ("cvc4 --lang=smtlib2 -m ghc_input.smt > ghc_output.smt") +laSat :: [(String,Ty)] -> [Expr] -> IO (Result Value) +laSat varMap ts = + do writeFile "ghc_input.smt" script + _ <- system ("cvc4 --lang=smtlib2 -m ghc_input.smt > ghc_output.smt") txt <- readFile "ghc_output.smt" - {- - putStrLn (replicate 50 '-') - print t - putStrLn (replicate 50 '-') - putStrLn txt - putStrLn (replicate 50 '-') - -} case reads txt of [(v,_)] -> return v _ -> panic $ "sat:\n" ++ txt where - declareVar (x,tv) = - case splitTyConApp_maybe (tyVarKind tv) of - Just (tc,[]) - | tc == promotedBoolTyCon -> [ CmdDeclareFun (N x) [] tBool ] - | tc == typeNatKindCon -> [ CmdDeclareFun (N x) [] tInt - , CmdAssert (nGeq (app x []) 0) - ] - - -- XXX: Could we encounter a kind variable? - _ -> pprPanic "sat" (ppr (tyVarKind tv)) - - script = - Script $ [ CmdSetLogic (N "QF_LIA") ] - ++ concatMap declareVar (Map.toList varMap) - ++ [ CmdAssert (termToSMT t) - , CmdCheckSat - , CmdGetValue [ app x [] | x <- Map.keys varMap ] - ] - - -prove :: VarMap -> Term -> IO Bool -prove varMap p = - do x <- sat varMap (Not p) - case x of - Unsat -> return True - _ -> return False - -ands :: [Term] -> Term -ands [] = Bool True -ands ps = foldr1 (\x y -> Op x And y) ps + sexpr ws = "(" ++ unwords ws ++ ")" -infixr 1 ==> - -(==>) :: [Term] -> Term -> Term -[] ==> q = q -ps ==> q = Op (ands ps) Implies q - - --------------------------------------------------------------------------------- - - - - -newtype SmtName = N String - deriving (Eq,Ord,Show) - -data Ident = I SmtName [Integer] - deriving (Eq,Ord,Show) - -data Quant = Exists | Forall - deriving (Eq,Ord,Show) - -data Binder = Bind { bindVar :: SmtName, bindSmtType :: SmtType } - deriving (Eq,Ord,Show) - -data Defn = Defn { defVar :: SmtName, defExpr :: Expr } - deriving (Eq,Ord,Show) - -data Literal = LitNum Integer - | LitFrac Rational - | LitStr String - deriving (Eq,Ord,Show) - -data SmtType = TApp Ident [SmtType] - | TVar SmtName - deriving (Eq,Ord,Show) - -data Expr = Lit Literal - | App Ident (Maybe SmtType) [Expr] - | Quant Quant [Binder] Expr - | Let [Defn] Expr - | Annot Expr [Attr] - deriving (Eq,Ord,Show) - -data Attr = Attr { attrName :: SmtName , attrVal :: Maybe AttrVal } - deriving (Eq,Ord,Show) - -type AttrVal = Expr -- A bit of an approximation.... - - -data Option - = OptPrintSuccess Bool - | OptExpandDefinitions Bool - | OptInteractiveMode Bool - | OptProduceProofs Bool - | OptProduceUnsatCores Bool - | OptProduceModels Bool - | OptProduceAssignments Bool - | OptRegularOutputChannel String - | OptDiagnosticOutputChannel String - | OptRandomSeed Integer - | OptVerbosity Integer - | OptAttr Attr - -data InfoFlag - = InfoAllStatistics - | InfoErrorBehavior - | InfoName - | InfoAuthors - | InfoVersion - | InfoStatus - | InfoReasonUnknown - | InfoAttr Attr - -data Command - = CmdSetLogic SmtName - | CmdSetOption Option - | CmdSetInfo Attr - | CmdDeclareSmtType SmtName Integer - | CmdDefineSmtType SmtName [SmtName] SmtType - | CmdDeclareFun SmtName [SmtType] SmtType - | CmdDefineFun SmtName [Binder] SmtType Expr - | CmdPush Integer - | CmdPop Integer - | CmdAssert Expr - | CmdCheckSat - | CmdGetAssertions - | CmdGetValue [Expr] - | CmdGetProof - | CmdGetUnsatCore - | CmdGetInfo InfoFlag - | CmdGetOption SmtName - | CmdExit - -newtype Script = Script [Command] - - --------------------------------------------------------------------------------- --- To make it a bit simpler to write terms in the above AST --- we provide some instances. They are intended to be used only --- for writing simple literals, and not any of the computational --- operations associated with the classes. - -{- --- Strings -instance IsString SmtName where fromString = N -instance IsString Ident where fromString x = I (fromString x) [] -instance IsString SmtType where fromString x = TApp (fromString x) [] -instance IsString Expr where fromString = Lit . LitStr . fromString --} - --- Integers - --- NOTE: Some of these might not mean anything, depending on the theory. -instance Num Expr where - fromInteger x = Lit (LitNum x) - x + y = app "+" [x,y] - x - y = app "-" [x,y] - x * y = app "*" [x,y] - signum x = app "signum" [x] - abs x = app "abs" [x] - - --- Fractional numbers -instance Fractional Expr where - fromRational x = Lit (LitFrac x) - x / y = app "/" [x,y] - -app :: String -> [Expr] -> Expr -app f es = App (I (N f) []) Nothing es - --------------------------------------------------------------------------------- -type Doc = String - -x <+> y = fsep [x,y] -(<>) = (++) -nest _ x = x -integer = show -char x = [x] -parens x = "(" ++ x ++ ")" -fsep = unwords -x $$ y = x ++ "\n" ++ y -vcat = unlines -text = id -empty = "" - - -class PP t where - pp :: t -> Doc - -instance PP Bool where - pp True = text "true" - pp False = text "false" - -instance PP Integer where - pp = integer - -ppString :: String -> Doc -ppString = text . show - -instance PP SmtName where - pp (N x) = text x - -instance PP Ident where - pp (I x []) = pp x - pp (I x is) = parens (char '_' <+> pp x <+> fsep (map integer is)) - -instance PP Attr where - pp (Attr x v) = char ':' <> pp x <+> maybe empty pp v - -instance PP Quant where - pp Forall = text "forall" - pp Exists = text "exists" - -instance PP Expr where - pp expr = - case expr of - - Lit l -> pp l - - App c ty ts -> - case ts of - [] -> ppFun - _ -> parens (ppFun <+> fsep (map pp ts)) - - where ppFun = case ty of - Nothing -> pp c - Just t -> parens (text "as" <+> pp c <+> pp t) - - Quant q bs e -> - case bs of - [] -> pp e - _ -> parens (pp q <+> parens (fsep (map pp bs)) $$ nest 2 (pp e)) - - Let ds e -> - case ds of - [] -> pp e - _ -> parens (text "let" <+> (parens (vcat (map pp ds)) $$ pp e)) - - Annot e as -> - case as of - [] -> pp e - _ -> parens (char '!' <+> pp e $$ nest 2 (vcat (map pp as))) - - -instance PP Binder where - pp (Bind x t) = parens (pp x <+> pp t) - -instance PP Defn where - pp (Defn x e) = parens (pp x <+> pp e) - -instance PP SmtType where - pp ty = + declareVar (x,ty) = case ty of - TApp c ts -> - case ts of - [] -> pp c - _ -> parens (pp c <+> fsep (map pp ts)) - TVar x -> pp x - -instance PP Literal where - pp lit = - case lit of - - LitNum n -> integer n - - LitFrac x -> text (show (fromRational x :: Double)) -- XXX: Good enough? - - LitStr x -> ppString x - - - -instance PP Option where - pp opt = - case opt of - OptPrintSuccess b -> std "print-success" b - OptExpandDefinitions b -> std "expand-definitions" b - OptInteractiveMode b -> std "interactive-mode" b - OptProduceProofs b -> std "produce-proofs" b - OptProduceUnsatCores b -> std "produce-unsat-cores" b - OptProduceModels b -> std "produce-models" b - OptProduceAssignments b -> std "produce-assignments" b - OptRegularOutputChannel s -> str "regular-output-channel" s - OptDiagnosticOutputChannel s -> str "diagnostic-output-channel" s - OptRandomSeed n -> std "random-seed" n - OptVerbosity n -> std "verbosity" n - OptAttr a -> pp a - - where mk a b = char ':' <> text a <+> b - std a b = mk a (pp b) - str a b = mk a (ppString b) - -instance PP InfoFlag where - pp info = - case info of - InfoAllStatistics -> mk "all-statistics" - InfoErrorBehavior -> mk "error-behavior" - InfoName -> mk "name" - InfoAuthors -> mk "authors" - InfoVersion -> mk "version" - InfoStatus -> mk "status" - InfoReasonUnknown -> mk "reason-unknown" - InfoAttr a -> pp a - where mk x = char ':' <> text x - -instance PP Command where - pp cmd = - case cmd of - CmdSetLogic n -> std "set-logic" n - CmdSetOption o -> std "set-options" o - CmdSetInfo a -> std "set-info" a - CmdDeclareSmtType x n -> mk "declare-sort" (pp x <+> integer n) - CmdDefineSmtType x as t -> fun "define-sort" x as (pp t) - CmdDeclareFun x ts t -> fun "declare-fun" x ts (pp t) - CmdDefineFun x bs t e -> fun "define-fun" x bs (pp t $$ nest 2 (pp e)) - CmdPush n -> std "push" n - CmdPop n -> std "pop" n - CmdAssert e -> std "assert" e - CmdCheckSat -> one "check-sat" - CmdGetAssertions -> one "get-assertions" - CmdGetValue es -> mk "get-value" (parens (fsep (map pp es))) - CmdGetProof -> one "get-proof" - CmdGetUnsatCore -> one "get-unsat-core" - CmdGetInfo i -> std "get-info" i - CmdGetOption n -> std "get-option" n - CmdExit -> one "exit" - where mk x d = parens (text x <+> d) - one x = mk x empty - std x a = mk x (pp a) - fun x y as d = mk x (pp y <+> parens (fsep (map pp as)) <+> d) - -instance PP Script where - pp (Script cs) = vcat (map pp cs) - - - -tBool :: SmtType -tBool = TApp (I (N "Bool") []) [] - -true :: Expr -true = app "true" [] - -false :: Expr -false = app "false" [] - -eNot :: Expr -> Expr -eNot p = app "not" [p] - -(===>) :: Expr -> Expr -> Expr -p ===> q = app "=>" [p,q] - -eAnd :: Expr -> Expr -> Expr -eAnd p q = app "and" [p,q] - -eOr :: Expr -> Expr -> Expr -eOr p q = app "or" [p,q] - -eXor :: Expr -> Expr -> Expr -eXor p q = app "xor" [p,q] - -(====) :: Expr -> Expr -> Expr -x ==== y = app "=" [x,y] - -(=/=) :: Expr -> Expr -> Expr -x =/= y = app "distinct" [x,y] - -ite :: Expr -> Expr -> Expr -> Expr -ite b x y = app "ite" [b,x,y] - - - -tInt :: SmtType -tInt = TApp (I (N "Int") []) [] - -nNeg :: Expr -> Expr -nNeg x = app "-" [x] - -nSub :: Expr -> Expr -> Expr -nSub x y = app "-" [x,y] - -nAdd :: Expr -> Expr -> Expr -nAdd x y = app "+" [x,y] - -nMul :: Expr -> Expr -> Expr -nMul x y = app "*" [x,y] - -nDiv :: Expr -> Expr -> Expr -nDiv x y = app "div" [x,y] - -nMod :: Expr -> Expr -> Expr -nMod x y = app "mod" [x,y] - -nAbs :: Expr -> Expr -nAbs x = app "abs" [x] - -nLeq :: Expr -> Expr -> Expr -nLeq x y = app "<=" [x,y] - -nLt :: Expr -> Expr -> Expr -nLt x y = app "<" [x,y] - -nGeq :: Expr -> Expr -> Expr -nGeq x y = app ">=" [x,y] - -nGt :: Expr -> Expr -> Expr -nGt x y = app ">" [x,y] - - - -example = - Script - [ CmdSetLogic (N "QF_LIA") - , CmdDeclareFun (N "x") [] tInt - , CmdDeclareFun (N "y") [] tInt - , CmdDeclareFun (N "z") [] tBool - , CmdAssert $ nGeq (app "x" []) (app "y" []) ==== (app "z" []) - , CmdCheckSat - , CmdGetValue [ app "x" [], app "y" [], app "z" [] ] - ] - - + TBool -> [ sexpr [ "declare-fun", x, sexpr [], "Bool" ] ] + TNat -> [ sexpr [ "declare-fun", x, sexpr [], "Int" ] + , sexpr [ "assert", sexpr [ "<=", "0", x ] ] + ] + + script = unlines + $ [ sexpr [ "set-logic", "QF_LIA" ] ] + ++ concatMap declareVar varMap + ++ [ sexpr ["assert", termToSMT t] | t <- ts ] + ++ [ sexpr [ "check-sat" ] + , sexpr [ "get-value", sexpr (map fst varMap) ] + ] + + + termToSMT term = + case term of + Op op e1 e2 -> sexpr [opToSMT op, termToSMT e1, termToSMT e2] + Not e -> sexpr ["not", termToSMT e] + Num x | x >= 0 -> show x + | otherwise -> sexpr ["-", show (negate x)] + Bool x -> if x then "true" else "false" + Var x -> x + + opToSMT op = + case op of + Add -> "+" + Sub -> "-" + Mul -> "*" + Leq -> "<=" + Eq -> "=" -- cgit v1.2.1