{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleContexts #-}
{-# Language FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Cryptol.TypeCheck.Solver.SMT
(
Solver
, SolverConfig
, withSolver
, startSolver
, stopSolver
, isNumeric
, resetSolver
, debugBlock
, debugLog
, proveImp
, checkUnsolvable
, tryGetModel
, shrinkModel
) where
import SimpleSMT (SExpr)
import qualified SimpleSMT as SMT
import Data.Map ( Map )
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe(catMaybes)
import Data.List(partition)
import Control.Exception
import Control.Monad(msum,zipWithM,void)
import Data.Char(isSpace)
import Text.Read(readMaybe)
import qualified System.IO.Strict as StrictIO
import System.FilePath((</>))
import System.Directory(doesFileExist)
import Cryptol.Prelude(cryptolTcContents)
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.TypeCheck.TypePat hiding ((~>),(~~>))
import Cryptol.TypeCheck.Subst(Subst)
import Cryptol.Utils.Panic
import Cryptol.Utils.PP ( Doc, pp )
data Solver = Solver
{ Solver -> Solver
solver :: SMT.Solver
, Solver -> Logger
logger :: SMT.Logger
}
setupSolver :: Solver -> SolverConfig -> IO ()
setupSolver :: Solver -> SolverConfig -> IO ()
setupSolver Solver
s SolverConfig
cfg = do
Bool
_ <- Solver -> String -> String -> IO Bool
SMT.setOptionMaybe (Solver -> Solver
solver Solver
s) String
":global-decls" String
"false"
Solver -> [String] -> IO ()
loadTcPrelude Solver
s (SolverConfig -> [String]
solverPreludePath SolverConfig
cfg)
startSolver :: IO () -> SolverConfig -> IO Solver
startSolver :: IO () -> SolverConfig -> IO Solver
startSolver IO ()
onExit SolverConfig
sCfg =
do Logger
logger <- if (SolverConfig -> Int
solverVerbose SolverConfig
sCfg) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Int -> IO Logger
SMT.newLogger Int
0
else Logger -> IO Logger
forall (m :: * -> *) a. Monad m => a -> m a
return Logger
quietLogger
let smtDbg :: Maybe Logger
smtDbg = if (SolverConfig -> Int
solverVerbose SolverConfig
sCfg) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 then Logger -> Maybe Logger
forall a. a -> Maybe a
Just Logger
logger else Maybe Logger
forall a. Maybe a
Nothing
Solver
solver <- String
-> [String]
-> Maybe Logger
-> Maybe (ExitCode -> IO ())
-> IO Solver
SMT.newSolverNotify
(SolverConfig -> String
solverPath SolverConfig
sCfg) (SolverConfig -> [String]
solverArgs SolverConfig
sCfg) Maybe Logger
smtDbg ((ExitCode -> IO ()) -> Maybe (ExitCode -> IO ())
forall a. a -> Maybe a
Just (IO () -> ExitCode -> IO ()
forall a b. a -> b -> a
const IO ()
onExit))
let sol :: Solver
sol = Solver -> Logger -> Solver
Solver Solver
solver Logger
logger
Solver -> SolverConfig -> IO ()
setupSolver Solver
sol SolverConfig
sCfg
Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
sol
where
quietLogger :: Logger
quietLogger = Logger :: (String -> IO ())
-> IO Int -> (Int -> IO ()) -> IO () -> IO () -> Logger
SMT.Logger { logMessage :: String -> IO ()
SMT.logMessage = \String
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, logLevel :: IO Int
SMT.logLevel = Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
, logSetLevel :: Int -> IO ()
SMT.logSetLevel= \Int
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, logTab :: IO ()
SMT.logTab = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, logUntab :: IO ()
SMT.logUntab = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
stopSolver :: Solver -> IO ()
stopSolver :: Solver -> IO ()
stopSolver Solver
s = IO ExitCode -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO ExitCode -> IO ()) -> IO ExitCode -> IO ()
forall a b. (a -> b) -> a -> b
$ Solver -> IO ExitCode
SMT.stop (Solver -> Solver
solver Solver
s)
resetSolver :: Solver -> SolverConfig -> IO ()
resetSolver :: Solver -> SolverConfig -> IO ()
resetSolver Solver
s SolverConfig
sCfg = do
()
_ <- Solver -> [String] -> IO ()
SMT.simpleCommand (Solver -> Solver
solver Solver
s) [String
"reset"]
Solver -> SolverConfig -> IO ()
setupSolver Solver
s SolverConfig
sCfg
withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a
withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a
withSolver IO ()
onExit SolverConfig
cfg = IO Solver -> (Solver -> IO ()) -> (Solver -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket (IO () -> SolverConfig -> IO Solver
startSolver IO ()
onExit SolverConfig
cfg) Solver -> IO ()
stopSolver
loadTcPrelude :: Solver -> [FilePath] -> IO ()
loadTcPrelude :: Solver -> [String] -> IO ()
loadTcPrelude Solver
s [] = Solver -> String -> IO ()
loadString Solver
s String
cryptolTcContents
loadTcPrelude Solver
s (String
p : [String]
ps) =
do let file :: String
file = String
p String -> String -> String
</> String
"CryptolTC.z3"
Bool
yes <- String -> IO Bool
doesFileExist String
file
if Bool
yes then Solver -> String -> IO ()
loadFile Solver
s String
file
else Solver -> [String] -> IO ()
loadTcPrelude Solver
s [String]
ps
loadFile :: Solver -> FilePath -> IO ()
loadFile :: Solver -> String -> IO ()
loadFile Solver
s String
file = Solver -> String -> IO ()
loadString Solver
s (String -> IO ()) -> IO String -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> IO String
StrictIO.readFile String
file
loadString :: Solver -> String -> IO ()
loadString :: Solver -> String -> IO ()
loadString Solver
s String
str = String -> IO ()
go (String -> String
dropComments String
str)
where
go :: String -> IO ()
go String
txt
| (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
txt = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise =
case String -> Maybe (SExpr, String)
SMT.readSExpr String
txt of
Just (SExpr
e,String
rest) -> Solver -> SExpr -> IO SExpr
SMT.command (Solver -> Solver
solver Solver
s) SExpr
e IO SExpr -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
go String
rest
Maybe (SExpr, String)
Nothing -> String -> [String] -> IO ()
forall a. HasCallStack => String -> [String] -> a
panic String
"loadFile" [ String
"Failed to parse SMT file."
, String
txt
]
dropComments :: String -> String
dropComments = [String] -> String
unlines ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
dropComment ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
dropComment :: String -> String
dropComment String
xs = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
';') String
xs of
(String
as,Char
_:String
_) -> String
as
(String, String)
_ -> String
xs
debugBlock :: Solver -> String -> IO a -> IO a
debugBlock :: Solver -> String -> IO a -> IO a
debugBlock s :: Solver
s@Solver { Solver
Logger
logger :: Logger
solver :: Solver
logger :: Solver -> Logger
solver :: Solver -> Solver
.. } String
name IO a
m =
do Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s String
name
Logger -> IO ()
SMT.logTab Logger
logger
a
a <- IO a
m
Logger -> IO ()
SMT.logUntab Logger
logger
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
class DebugLog t where
debugLog :: Solver -> t -> IO ()
debugLogList :: Solver -> [t] -> IO ()
debugLogList Solver
s [t]
ts = case [t]
ts of
[] -> Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s String
"(none)"
[t]
_ -> (t -> IO ()) -> [t] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> t -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s) [t]
ts
instance DebugLog Char where
debugLog :: Solver -> Char -> IO ()
debugLog Solver
s Char
x = Logger -> String -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) (Char -> String
forall a. Show a => a -> String
show Char
x)
debugLogList :: Solver -> String -> IO ()
debugLogList Solver
s String
x = Logger -> String -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) String
x
instance DebugLog a => DebugLog [a] where
debugLog :: Solver -> [a] -> IO ()
debugLog = Solver -> [a] -> IO ()
forall a. DebugLog a => Solver -> [a] -> IO ()
debugLogList
instance DebugLog a => DebugLog (Maybe a) where
debugLog :: Solver -> Maybe a -> IO ()
debugLog Solver
s Maybe a
x = case Maybe a
x of
Maybe a
Nothing -> Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s String
"(nothing)"
Just a
a -> Solver -> a -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s a
a
instance DebugLog Doc where
debugLog :: Solver -> Doc -> IO ()
debugLog Solver
s Doc
x = Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Doc -> String
forall a. Show a => a -> String
show Doc
x)
instance DebugLog Type where
debugLog :: Solver -> Type -> IO ()
debugLog Solver
s Type
x = Solver -> Doc -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Type -> Doc
forall a. PP a => a -> Doc
pp Type
x)
instance DebugLog Goal where
debugLog :: Solver -> Goal -> IO ()
debugLog Solver
s Goal
x = Solver -> Type -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Goal -> Type
goal Goal
x)
instance DebugLog Subst where
debugLog :: Solver -> Subst -> IO ()
debugLog Solver
s Subst
x = Solver -> Doc -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
x)
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
proveImp :: Solver -> [Type] -> [Goal] -> IO [Goal]
proveImp Solver
sol [Type]
ps [Goal]
gs0 =
Solver -> String -> IO [Goal] -> IO [Goal]
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"PROVE IMP" (IO [Goal] -> IO [Goal]) -> IO [Goal] -> IO [Goal]
forall a b. (a -> b) -> a -> b
$
do let gs1 :: [Goal]
gs1 = (Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
flatGoal [Goal]
gs0
([Goal]
gs,[Goal]
rest) = (Goal -> Bool) -> [Goal] -> ([Goal], [Goal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Type -> Bool
isNumeric (Type -> Bool) -> (Goal -> Type) -> Goal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs1
numAsmp :: [Type]
numAsmp = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
isNumeric ((Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd [Type]
ps)
vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (([Type], [Type]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ([Type]
numAsmp, (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
gs))
Map TVar SExpr
tvs <- Solver -> String -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"VARIABLES" (IO (Map TVar SExpr) -> IO (Map TVar SExpr))
-> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
[(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ Int
0 .. ] [TVar]
vs
Solver -> String -> IO () -> IO ()
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"ASSUMPTIONS" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
(Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
numAsmp
[Maybe Goal]
gs' <- (Goal -> IO (Maybe Goal)) -> [Goal] -> IO [Maybe Goal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Map TVar SExpr -> Goal -> IO (Maybe Goal)
prove Solver
sol Map TVar SExpr
tvs) [Goal]
gs
Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
[Goal] -> IO [Goal]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe Goal] -> [Goal]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Goal]
gs' [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
rest)
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable Solver
sol [Goal]
gs0 =
Solver -> String -> IO Bool -> IO Bool
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"CHECK UNSOLVABLE" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
do let ps :: [Type]
ps = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
isNumeric
([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal
([Goal] -> [Type]) -> [Goal] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
flatGoal [Goal]
gs0
vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList ([Type] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Type]
ps)
Map TVar SExpr
tvs <- Solver -> String -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"VARIABLES" (IO (Map TVar SExpr) -> IO (Map TVar SExpr))
-> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
push Solver
sol
[(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ Int
0 .. ] [TVar]
vs
Bool
ans <- Solver -> Map TVar SExpr -> [Type] -> IO Bool
unsolvable Solver
sol Map TVar SExpr
tvs [Type]
ps
Solver -> IO ()
pop Solver
sol
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ans
tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar,Nat')])
tryGetModel :: Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
as [Type]
ps =
Solver
-> String -> IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')])
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"TRY GET MODEL" (IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')]))
-> IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')])
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
push Solver
sol
Map TVar SExpr
tvs <- [(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ Int
0 .. ] [TVar]
as
(Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
ps
Result
sat <- Solver -> IO Result
SMT.check (Solver -> Solver
solver Solver
sol)
Maybe [(TVar, Nat')]
su <- case Result
sat of
Result
SMT.Sat ->
case [TVar]
as of
[] -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TVar, Nat')] -> Maybe [(TVar, Nat')]
forall a. a -> Maybe a
Just [])
[TVar]
_ -> do [(SExpr, Value)]
res <- Solver -> [SExpr] -> IO [(SExpr, Value)]
SMT.getExprs (Solver -> Solver
solver Solver
sol) (Map TVar SExpr -> [SExpr]
forall k a. Map k a -> [a]
Map.elems Map TVar SExpr
tvs)
let parse :: TVar -> Maybe (TVar, Nat')
parse TVar
x = do SExpr
e <- TVar -> Map TVar SExpr -> Maybe SExpr
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
x Map TVar SExpr
tvs
Nat'
t <- Value -> Maybe Nat'
parseNum (Value -> Maybe Nat') -> Maybe Value -> Maybe Nat'
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SExpr -> [(SExpr, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup SExpr
e [(SExpr, Value)]
res
(TVar, Nat') -> Maybe (TVar, Nat')
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x, Nat'
t)
Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar -> Maybe (TVar, Nat')) -> [TVar] -> Maybe [(TVar, Nat')]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TVar -> Maybe (TVar, Nat')
parse [TVar]
as)
Result
_ -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TVar, Nat')]
forall a. Maybe a
Nothing
Solver -> IO ()
pop Solver
sol
Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TVar, Nat')]
su
where
parseNum :: Value -> Maybe Nat'
parseNum Value
a
| SMT.Other SExpr
s <- Value
a
, SMT.List [SExpr
con,SExpr
val,SExpr
isFin,SExpr
isErr] <- SExpr
s
, SMT.Atom String
"mk-infnat" <- SExpr
con
, SMT.Atom String
"false" <- SExpr
isErr
, SMT.Atom String
fin <- SExpr
isFin
, SMT.Atom String
v <- SExpr
val
, Just Integer
n <- String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
v
= Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (if String
fin String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"false" then Nat'
Inf else Integer -> Nat'
Nat Integer
n)
parseNum Value
_ = Maybe Nat'
forall a. Maybe a
Nothing
shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar,Nat')] -> IO [(TVar,Nat')]
shrinkModel :: Solver -> [TVar] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel Solver
sol [TVar]
as [Type]
ps0 [(TVar, Nat')]
mdl = [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go [] [Type]
ps0 [(TVar, Nat')]
mdl
where
go :: [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go [(TVar, Nat')]
done [Type]
ps ((TVar
x,Nat Integer
k) : [(TVar, Nat')]
more) =
do Integer
k1 <- [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k
[(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go ((TVar
x,Integer -> Nat'
Nat Integer
k1) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) ((Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k1 Type -> Type -> Type
>== TVar -> Type
TVar TVar
x) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps) [(TVar, Nat')]
more
go [(TVar, Nat')]
done [Type]
ps ((TVar
x,Nat'
i) : [(TVar, Nat')]
more) = [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go ((TVar
x,Nat'
i) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) [Type]
ps [(TVar, Nat')]
more
go [(TVar, Nat')]
done [Type]
_ [] = [(TVar, Nat')] -> IO [(TVar, Nat')]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TVar, Nat')]
done
shrink1 :: [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k
| Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
| Bool
otherwise =
do let k1 :: Integer
k1 = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
k Integer
2
p1 :: Type
p1 = Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k1 Type -> Type -> Type
>== TVar -> Type
TVar TVar
x
Maybe [(TVar, Nat')]
mb <- Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
as (Type
p1 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps)
case Maybe [(TVar, Nat')]
mb of
Maybe [(TVar, Nat')]
Nothing -> Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
k
Just [(TVar, Nat')]
newMdl ->
case TVar -> [(TVar, Nat')] -> Maybe Nat'
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TVar
x [(TVar, Nat')]
newMdl of
Just (Nat Integer
k2) -> [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k2
Maybe Nat'
_ -> String -> [String] -> IO Integer
forall a. HasCallStack => String -> [String] -> a
panic String
"shrink" [String
"model is missing variable", TVar -> String
forall a. Show a => a -> String
show TVar
x]
push :: Solver -> IO ()
push :: Solver -> IO ()
push Solver
sol = Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
pop :: Solver -> IO ()
pop :: Solver -> IO ()
pop Solver
sol = Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
s Int
x TVar
v =
do let name :: String
name = (if TVar -> Bool
isFreeTV TVar
v then String
"fv" else String
"kv") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x
SExpr
e <- Solver -> String -> SExpr -> IO SExpr
SMT.declare (Solver -> Solver
solver Solver
s) String
name SExpr
cryInfNat
Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (String -> [SExpr] -> SExpr
SMT.fun String
"cryVar" [ SExpr
e ])
(TVar, SExpr) -> IO (TVar, SExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
v,SExpr
e)
assume :: Solver -> TVars -> Prop -> IO ()
assume :: Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
s Map TVar SExpr
tvs Type
p = Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (String -> [SExpr] -> SExpr
SMT.fun String
"cryAssume" [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
p ])
prove :: Solver -> TVars -> Goal -> IO (Maybe Goal)
prove :: Solver -> Map TVar SExpr -> Goal -> IO (Maybe Goal)
prove Solver
sol Map TVar SExpr
tvs Goal
g =
Solver -> String -> IO (Maybe Goal) -> IO (Maybe Goal)
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"PROVE" (IO (Maybe Goal) -> IO (Maybe Goal))
-> IO (Maybe Goal) -> IO (Maybe Goal)
forall a b. (a -> b) -> a -> b
$
do let s :: Solver
s = Solver -> Solver
solver Solver
sol
Solver -> IO ()
push Solver
sol
Solver -> SExpr -> IO ()
SMT.assert Solver
s (String -> [SExpr] -> SExpr
SMT.fun String
"cryProve" [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs (Goal -> Type
goal Goal
g) ])
Result
res <- Solver -> IO Result
SMT.check Solver
s
Solver -> IO ()
pop Solver
sol
case Result
res of
Result
SMT.Unsat -> Maybe Goal -> IO (Maybe Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Goal
forall a. Maybe a
Nothing
Result
_ -> Maybe Goal -> IO (Maybe Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Maybe Goal
forall a. a -> Maybe a
Just Goal
g)
unsolvable :: Solver -> TVars -> [Prop] -> IO Bool
unsolvable :: Solver -> Map TVar SExpr -> [Type] -> IO Bool
unsolvable Solver
sol Map TVar SExpr
tvs [Type]
ps =
Solver -> String -> IO Bool -> IO Bool
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"UNSOLVABLE" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
(Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
ps
Result
res <- Solver -> IO Result
SMT.check (Solver -> Solver
solver Solver
sol)
Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
case Result
res of
Result
SMT.Unsat -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Result
_ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
flatGoal :: Goal -> [Goal]
flatGoal :: Goal -> [Goal]
flatGoal Goal
g = [ Goal
g { goal :: Type
goal = Type
p } | Type
p <- Type -> [Type]
pSplitAnd (Goal -> Type
goal Goal
g) ]
isNumeric :: Prop -> Bool
isNumeric :: Type -> Bool
isNumeric Type
ty = Bool -> Match Bool -> Bool
forall a. a -> Match a -> a
matchDefault Bool
False (Match Bool -> Bool) -> Match Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Match Bool] -> Match Bool
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|=|), (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|/=|), (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|>=|), (Type -> Match Type) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match Type
aFin ]
where
is :: (Type -> m a) -> m Bool
is Type -> m a
f = Type -> m a
f Type
ty m a -> m Bool -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
type TVars = Map TVar SExpr
cryInfNat :: SExpr
cryInfNat :: SExpr
cryInfNat = String -> SExpr
SMT.const String
"InfNat"
toSMT :: TVars -> Type -> SExpr
toSMT :: Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
ty = SExpr -> Match SExpr -> SExpr
forall a. a -> Match a -> a
matchDefault (String -> [String] -> SExpr
forall a. HasCallStack => String -> [String] -> a
panic String
"toSMT" [ String
"Unexpected type", Type -> String
forall a. Show a => a -> String
show Type
ty ])
(Match SExpr -> SExpr) -> Match SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$ [Match SExpr] -> Match SExpr
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Match SExpr] -> Match SExpr) -> [Match SExpr] -> Match SExpr
forall a b. (a -> b) -> a -> b
$ ((Map TVar SExpr -> Type -> Match SExpr) -> Match SExpr)
-> [Map TVar SExpr -> Type -> Match SExpr] -> [Match SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\Map TVar SExpr -> Type -> Match SExpr
f -> Map TVar SExpr -> Type -> Match SExpr
f Map TVar SExpr
tvs Type
ty)
[ Pat Type ()
aInf Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryInf"
, Pat Type Integer
aNat Pat Type Integer -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryNat"
, Type -> Match Type
aFin (Type -> Match Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryFin"
, Type -> Match (Type, Type)
(|=|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryEq"
, Type -> Match (Type, Type)
(|/=|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryNeq"
, Type -> Match (Type, Type)
(|>=|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryGeq"
, Type -> Match (Type, Type)
aAnd (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryAnd"
, Pat Type ()
aTrue Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryTrue"
, Type -> Match (Type, Type)
anAdd (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryAdd"
, Type -> Match (Type, Type)
(|-|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"crySub"
, Type -> Match (Type, Type)
aMul (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMul"
, Type -> Match (Type, Type)
(|^|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryExp"
, Type -> Match (Type, Type)
(|/|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryDiv"
, Type -> Match (Type, Type)
(|%|) (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMod"
, Type -> Match (Type, Type)
aMin (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMin"
, Type -> Match (Type, Type)
aMax (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMax"
, Type -> Match Type
aWidth (Type -> Match Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryWidth"
, Type -> Match (Type, Type)
aCeilDiv (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryCeilDiv"
, Type -> Match (Type, Type)
aCeilMod (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryCeilMod"
, Pat Type (Type, Type, Type)
aLenFromThenTo Pat Type (Type, Type, Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryLenFromThenTo"
, Kind -> Pat Type ()
anError Kind
KNum Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryErr"
, Kind -> Pat Type ()
anError Kind
KProp Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryErrProp"
, Pat Type TVar
aTVar Pat Type TVar -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"(unused)"
]
(~>) :: Mk a => (Type -> Match a) -> String -> TVars -> Type -> Match SExpr
(Type -> Match a
m ~> :: (Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
f) Map TVar SExpr
tvs Type
t = Type -> Match a
m Type
t Match a -> (a -> Match SExpr) -> Match SExpr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> SExpr -> Match SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TVar SExpr -> String -> a -> SExpr
forall t. Mk t => Map TVar SExpr -> String -> t -> SExpr
mk Map TVar SExpr
tvs String
f a
a)
class Mk t where
mk :: TVars -> String -> t -> SExpr
instance Mk () where
mk :: Map TVar SExpr -> String -> () -> SExpr
mk Map TVar SExpr
_ String
f ()
_ = String -> SExpr
SMT.const String
f
instance Mk Integer where
mk :: Map TVar SExpr -> String -> Integer -> SExpr
mk Map TVar SExpr
_ String
f Integer
x = String -> [SExpr] -> SExpr
SMT.fun String
f [ Integer -> SExpr
SMT.int Integer
x ]
instance Mk TVar where
mk :: Map TVar SExpr -> String -> TVar -> SExpr
mk Map TVar SExpr
tvs String
_ TVar
x = Map TVar SExpr
tvs Map TVar SExpr -> TVar -> SExpr
forall k a. Ord k => Map k a -> k -> a
Map.! TVar
x
instance Mk Type where
mk :: Map TVar SExpr -> String -> Type -> SExpr
mk Map TVar SExpr
tvs String
f Type
x = String -> [SExpr] -> SExpr
SMT.fun String
f [Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x]
instance Mk (Type,Type) where
mk :: Map TVar SExpr -> String -> (Type, Type) -> SExpr
mk Map TVar SExpr
tvs String
f (Type
x,Type
y) = String -> [SExpr] -> SExpr
SMT.fun String
f [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
y]
instance Mk (Type,Type,Type) where
mk :: Map TVar SExpr -> String -> (Type, Type, Type) -> SExpr
mk Map TVar SExpr
tvs String
f (Type
x,Type
y,Type
z) = String -> [SExpr] -> SExpr
SMT.fun String
f [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
y, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
z ]