{-# LANGUAGE OverloadedStrings #-}

module Language.Fixpoint.Solver.Common (askSMT, toSMT) where

import Language.Fixpoint.Types.Config (Config, solver, solverFlags)
import Language.Fixpoint.Smt.Interface (Context(..), checkValidWithContext)
import Language.Fixpoint.Types
import Language.Fixpoint.Types.Visitor (kvarsExpr)
import Language.Fixpoint.Defunctionalize (defuncAny)
import Language.Fixpoint.SortCheck (ElabParam(..), elaborate)

mytracepp :: (PPrint a) => String -> a -> a
mytracepp :: forall a. PPrint a => [Char] -> a -> a
mytracepp = [Char] -> a -> a
forall a. PPrint a => [Char] -> a -> a
notracepp

askSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
askSMT :: Config -> Context -> [(Symbol, Sort)] -> Pred -> IO Bool
askSMT Config
cfg Context
ctx [(Symbol, Sort)]
xs Pred
e
--   | isContraPred e  = return False
  | Pred -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred  Pred
e     = Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  | [KVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Pred -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr Pred
e) = Context -> [(Symbol, Sort)] -> Pred -> Pred -> IO Bool
checkValidWithContext Context
ctx [(Symbol, Sort)]
xs Pred
forall v. ExprV v
PTrue Pred
e'
  | Bool
otherwise          = Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  where
    e' :: Pred
e' = [Char] -> Config -> Context -> [(Symbol, Sort)] -> Pred -> Pred
toSMT [Char]
"askSMT" Config
cfg Context
ctx [(Symbol, Sort)]
xs Pred
e

toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred
toSMT :: [Char] -> Config -> Context -> [(Symbol, Sort)] -> Pred -> Pred
toSMT [Char]
msg Config
cfg Context
ctx [(Symbol, Sort)]
xs Pred
e =
    Config -> SymEnv -> Pred -> Pred
forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
symenv (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        ElabParam -> Pred -> Pred
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver Config
cfg) ([Char] -> Located [Char]
forall a. a -> Located a
dummyLoc [Char]
msg) ([(Symbol, Sort)] -> SymEnv
elabEnv [(Symbol, Sort)]
xs)) (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            [Char] -> Pred -> Pred
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"toSMT from " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pred -> [Char]
forall a. PPrint a => a -> [Char]
showpp Pred
e) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
                Pred
e
  where
    elabEnv :: [(Symbol, Sort)] -> SymEnv
elabEnv = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
symenv
    symenv :: SymEnv
symenv  = Context -> SymEnv
ctxSymEnv Context
ctx