| definition: |
isUnsatisfiable :: TermDomain a => Expr -> VerifyStateM a Bool
isUnsatisfiable bexp = do
st <- get
if optSMT (vstToolOpts st)
then do
fname <- getCurrentFuncName
vts <- fmap (map (\(v,te,_) -> (v,te))) getVarExps
let allvs = allFreeVars bexp
let vtypes = filter ((`elem` allvs) . fst) vts
question = "Verifying function " ++ snd fname ++ ":\n\n" ++
"IS\n " ++ showSimpExp bexp ++ "\nUNSATISFIABLE?"
unless (all (`elem` map fst vtypes) allvs) $ lift $ printInfoLine $
"WARNING in operation '" ++ snd fname ++
"': missing variables in unsatisfiability check!"
consinfos <- getConsInfos
answer <- lift $ checkUnsatisfiabilityWithSMT (vstToolOpts st)
fname question (vstModules st) consinfos vtypes bexp
maybe (setToolError >> return False) return answer
else return False
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| documentation: |
--- Checks the unsatisfiability of a Boolean expression w.r.t. a set --- of variables (second argument) with an SMT solver. |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
isUnsatisfiable |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Analysis.TermDomain.TermDomain a => FlatCurry.Types.Expr -> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO Prelude.Bool |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |