|
definition:
|
checkUnsatisfiabilityWithSMT :: Options -> QName -> String -> IORef ProgInfo
-> [(QName,ConsInfo)] -> [(Int,TypeExpr)] -> Expr -> IO (Maybe Bool)
checkUnsatisfiabilityWithSMT opts qf scripttitle pistore consinfos
vartypes assertionexp0 = do
let assertionexp = wrapCaseWithId assertionexp0
(cnames,fnames) = both nub
(partitionEithers (allQNamesInExp assertionexp))
cnamesreq = filter (`notElem` [pre "False", pre "True", anonCons]) cnames
--printInfoLine $ "ASSERTION EXPRESSION: " ++ showExp assertionexp
--printInfoLine $ "NAMES IN ASSERTION: " ++ show (cnamesreq ++ fnames)
loadModulesForQNames opts pistore (cnamesreq ++ fnames)
pinfos <- fmap progInfos $ readIORef pistore
let typedassertion = addTypes2VarExp pinfos vartypes assertionexp fcBool
--printInfoLine $ "TYPED ASSERTION EXPRESSION: " ++ showExp typedassertion
let foassertexp = replaceHigherOrderInExp (simpExpr typedassertion)
foassertfuncs = rights (allQNamesInExp foassertexp)
--printInfoLine $ "SIMPLE TYPED ASSERTION EXPRESSION: " ++ showExp foassertexp
maybe
(transExpError typedassertion)
(\ (assertion,varsorts) ->
catch (checkUnsatWithSMT opts qf scripttitle pistore consinfos vartypes
varsorts assertion cnamesreq foassertfuncs)
(\e -> print e >> return Nothing))
(exp2SMTWithVars (maximum (0 : map fst vartypes))
Nothing foassertexp)
where
transExpError e = do printInfoLine $ "Cannot translate expression:\n" ++ showExp e
return Nothing
-- Wrap all case arguments with the identity operation.
-- This is a work-around to fix a problem with pattern matching
-- w.r.t. algebraic data types occurring in Z3 version 4.13.0
-- (see example Z3BUG/match-error.smt).
wrapCaseWithId =
updCases (\ct e brs -> Case ct (Comb FuncCall (pre "id") [e]) brs)
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
------------------------------------------------------------------------------
-- Calls the SMT solver to check whether an assertion implies some
-- property (represented as FlatCurry expressions).
-- If the implication is `False`, the unsatisfiability of the assertion
-- is checked.
-- `Nothing` is returned if there is some error w.r.t. SMT solving.
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,_,_,_,_,_,_) |-> _}
|
|
name:
|
checkUnsatisfiabilityWithSMT
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Verify.Options.Options -> (String, String) -> String
-> Data.IORef.IORef Verify.ProgInfo.ProgInfo
-> [((String, String), (Prelude.Int, Verify.ProgInfo.ConsType, [((String, String), Prelude.Int)]))]
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)] -> FlatCurry.Types.Expr
-> Prelude.IO (Prelude.Maybe Prelude.Bool)
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|