|
definition:
|
addConditionRestriction :: TermDomain a => QName -> Expr -> VerifyStateM a ()
addConditionRestriction qf cond = do
st <- get
when (optSMT (vstToolOpts st)) $ do
let (_,_,vs) = vstCurrFunc st
oldcalltype <- getCallType qf 0
let totaloldct = isTotalACallType oldcalltype
-- express oldcalltype as a condition to be added to `cond`:
oldcalltypecond = aCallType2Bool (vstConsInfos st) vs oldcalltype
branchcond <- getExpandedCondition
newbranchcond <- getExpandedConditionWithConj cond
let newcond = fcAnd oldcalltypecond
(if cond == fcTrue
then fcNot branchcond
else -- current branch condition implies new condition:
fcOr (fcNot branchcond) newbranchcond)
printIfVerb 2 $ "New call condition for function '" ++ snd qf ++ "': " ++
showSimpExp newcond ++
(if totaloldct then "" else " (due to non-trivial call type)")
printIfVerb 3 $ "Check satisfiability of new call condition..."
unsat <- isUnsatisfiable newcond
when unsat $ printIfVerb 2 $ "...is unsatisfiable"
vartypes <- fmap (map (\(v,t,_) -> (v,t))) getVarExps
setNewFunCondition qf (if unsat then nfcFalse
else genNonFailCond vartypes newcond)
addCallTypeRestriction qf failACallType
|
|
documentation:
|
-- Adds a new condition (provided as the second argument as a FlatCurry
-- expression) to the call condition for the current function (first argument)
-- so that it will be used in the next iteration.
-- If there is already a new refined call condition, they will be combined.
-- If the condition is `True`, i.e., the call condition cannot be refined,
-- then the current branch condition will be negated and added
-- so that the current branch is not reachable.
-- Furthermore, the call type of the current function is set to
-- always failing.
|