{-# LANGUAGE OverloadedStrings #-}

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

import Control.Monad.State
import Language.Fixpoint.Types.Config (Config, solverFlags)
import Language.Fixpoint.Smt.Interface (Context(..), checkValidWithContext)
import Language.Fixpoint.Smt.Types (SmtM)
import Language.Fixpoint.Types
import Language.Fixpoint.Types.Visitor (kvarsExpr)
import Language.Fixpoint.Defunctionalize (defuncAny)
import Language.Fixpoint.SortCheck (ElabParam(..), elaborate)
import GHC.Stack (HasCallStack)

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

askSMT
  :: HasCallStack
  => Config
  -> [(Symbol, Sort)] -- ^ symbols already declared in the SMT solver
  -> [(Symbol, Sort)] -- ^ symbols to declare in the SMT solver
  -> Expr
  -> SmtM Bool
askSMT :: HasCallStack =>
Config -> [(Symbol, Sort)] -> [(Symbol, Sort)] -> Expr -> SmtM Bool
askSMT Config
cfg [(Symbol, Sort)]
bsInSMT [(Symbol, Sort)]
xs Expr
e
  | Expr -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred  Expr
e     = Bool -> SmtM Bool
forall a. a -> StateT Context 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 (Expr -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr Expr
e) =
      do Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
         let e' :: Expr
e' = HasCallStack =>
String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT String
"askSMT" Config
cfg Context
ctx ([(Symbol, Sort)]
xs [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
bsInSMT) Expr
e
         HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
[(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValidWithContext [(Symbol, Sort)]
xs Expr
forall v. ExprV v
PTrue Expr
e'
  | Bool
otherwise          = Bool -> SmtM Bool
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

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