module Cryptol.TypeCheck.Solver.Smtlib (simpDelayed) where
import Cryptol.TypeCheck.AST as Cry
import Cryptol.TypeCheck.Subst (fvs)
import Cryptol.TypeCheck.InferTypes(Goal(..))
import Cryptol.TypeCheck.Solver.FinOrd
import SMTLib2 as SMT
import SMTLib2.Int as SMT
import SMTLib2.Core as SMT
import qualified Control.Exception as X
import Data.String(fromString)
import Data.List(partition)
import Data.Maybe(mapMaybe)
import qualified Data.Set as Set
import System.Directory(findExecutable)
import System.Environment(getExecutablePath)
import System.FilePath((</>), takeDirectory)
import System.Process(readProcessWithExitCode)
import System.Exit(ExitCode(..))
simpDelayed :: [TParam] -> OrdFacts -> [Prop] -> [Goal] -> IO [Goal]
simpDelayed _qvars ordAsmp origAsmps goals =
do ans <- mapM tryGoal goals
let (_natsDone,natsNot) = partition snd ans
return (map fst natsNot)
where
vs = map toVar (Set.toList (fvs (ordFactsToProps ordAsmp,
(origAsmps,map goal goals))))
asmps = mapMaybe toPred (ordFactsToProps ordAsmp ++ origAsmps)
tryGoal g = case toPred (goal g) of
Just q -> do res <- cvc4 (toScript vs asmps q)
return (g, res == Unsat)
Nothing -> return (g, False)
toTerm :: Cry.Type -> Maybe SMT.Expr
toTerm ty =
case ty of
TCon tc ts ->
do es <- mapM toTerm ts
case (tc, es) of
(TC (TCNum x), []) -> return (SMT.num x)
(TF TCAdd, [e1,e2]) -> return (SMT.nAdd e1 e2)
(TF TCSub, [e1,e2]) -> return (SMT.nSub e1 e2)
(TF TCMul, [e1,e2]) -> return (SMT.nMul e1 e2)
(TF TCDiv, [e1,e2]) -> return (SMT.nDiv e1 e2)
(TF TCMod, [e1,e2]) -> return (SMT.nMod e1 e2)
(TF TCMin, [e1,e2]) -> return (SMT.ite (SMT.nLeq e1 e2) e1 e2)
(TF TCMax, [e1,e2]) -> return (SMT.ite (SMT.nLeq e1 e2) e2 e1)
(TF TCLg2, [_]) -> Nothing
(TF TCExp, [e1,e2])
| Lit (LitNum x) <- e2
, x >= 0 -> return $
if x == 0
then SMT.num (1 :: Int)
else foldr1 SMT.nMul
$ replicate (fromInteger x) e1
| otherwise -> Nothing
(TF TCWidth, [_]) -> Nothing
(TF TCLenFromThen, _) -> Nothing
(TF TCLenFromThenTo, _) -> Nothing
_ -> Nothing
Cry.TVar x -> return (smtVar (toVar x))
TUser _ _ t -> toTerm t
TRec _ -> Nothing
toVar :: TVar -> SMT.Name
toVar (TVFree x _ _ _) = fromString ("free" ++ show x)
toVar (TVBound x _) = fromString ("bound" ++ show x)
smtVar :: SMT.Name -> SMT.Expr
smtVar x = app (I x []) []
toPred :: Cry.Prop -> Maybe SMT.Expr
toPred ty =
case ty of
TCon tc ts ->
do es <- mapM toTerm ts
case (tc,es) of
(PC PEqual, [e1,e2]) -> return (e1 === e2)
(PC PGeq, [e1,e2]) -> return (SMT.nLeq e2 e1)
_ -> Nothing
Cry.TVar {} -> Nothing
TUser _ _ t -> toPred t
TRec {} -> Nothing
toScript :: [SMT.Name] -> [SMT.Expr] -> SMT.Expr -> SMT.Script
toScript vs pes q =
Script $
[ SMT.CmdSetLogic "QF_LIA" ] ++
[ SMT.CmdDeclareFun x [] SMT.tInt | x <- vs ] ++
[ SMT.CmdAssert (SMT.nLeq (SMT.num (0::Int)) (smtVar x)) | x <- vs ] ++
[ SMT.CmdAssert p | p <- pes ] ++
[ SMT.CmdAssert (SMT.not q) ] ++
[ SMT.CmdCheckSat ]
data SMTResult = Sat | Unsat | Unknown
deriving (Eq,Show)
findCvc4 :: IO FilePath
findCvc4 = do
mfp <- findExecutable "cvc4"
case mfp of
Just fp -> return fp
Nothing -> do
bindir <- takeDirectory `fmap` getExecutablePath
return (bindir </> "cvc4")
cvc4 :: SMT.Script -> IO SMTResult
cvc4 script =
X.handle (\(_::X.IOException) -> return Unknown) $
do let txt = show (SMT.pp script)
cvc4path <- findCvc4
(ex,out,err) <- readProcessWithExitCode cvc4path ["--lang=smtlib2","--rewrite-divk","-"] txt
case ex of
ExitFailure 10 -> return Sat
ExitFailure 20 -> return Unsat
ExitFailure 127 -> return Unknown
ExitSuccess
| out == "sat\n" -> return Sat
| out == "unsat\n" -> return Unsat
| out == "unknwon\n" -> return Unknown
x -> do putStrLn "Called to CVC4 failed!!!"
putStrLn ("Exit code: " ++ show x)
putStrLn "Script"
putStrLn txt
putStrLn "Standard out:"
putStrLn out
putStrLn "Standard error:"
putStrLn err
return Unknown