CurryInfo: contract-prover-4.0.0 / ContractProver.checkImplicationWithSMT

definition: 
checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)]
                        -> Term -> Term -> Term -> IO (Maybe String)
checkImplicationWithSMT opts vstref scripttitle vartypes
                        assertion impbindings imp = do
  let allsyms = catMaybes
                  (map (\n -> maybe Nothing Just (untransOpName n))
                       (map qidName
                         (allQIdsOfTerm (tConj [assertion, impbindings, imp]))))
  unless (null allsyms) $ printWhenIntermediate opts $
    "Translating operations into SMT: " ++ unwords (map showQName allsyms)
  (smtfuncs,fdecls,ndinfo) <- funcs2SMT opts vstref allsyms
  smttypes <- genSMTTypes vstref vartypes fdecls [assertion,impbindings,imp]
  let freshvar = maximum (map fst vartypes) + 1
      ([assertionC,impbindingsC,impC],newix) =
         nondetTransL ndinfo freshvar [assertion,impbindings,imp]
      smt = smttypes ++
            [ EmptyLine, smtfuncs, EmptyLine
            , Comment "Free variables:" ] ++
            map typedVar2SMT
                (vartypes ++ map toChoiceVar [freshvar .. newix-1]) ++
            [ EmptyLine
            , Comment "Boolean formula of assertion (known properties):"
            , sAssert assertionC, EmptyLine
            , Comment "Bindings of implication:"
            , sAssert impbindingsC, EmptyLine
            , Comment "Assert negated implication:"
            , sAssert (tNot impC), EmptyLine
            , Comment "check satisfiability:"
            , CheckSat
            , Comment "if unsat, we can omit this part of the contract check"
            ]
  smtstdtypes <- readInclude "Prelude.smt"
  smtchoice   <- if or (map snd ndinfo)
                   then readInclude "Prelude_Choice.smt"
                   else return ""
  let smtprelude = smtstdtypes ++ smtchoice
  callSMT opts $ "; " ++ scripttitle ++ "\n\n" ++ smtprelude ++ showSMT smt
 where
  readInclude f = getIncludePath f >>= readFile
  toChoiceVar i = (i, TCons (pre "Choice") [])
demand: 
no demanded arguments
deterministic: 
deterministic operation
documentation: 
-- Calls the SMT solver to check whether an assertion implies some
-- (pre/post) condition.
-- Returns `Nothing` if the proof was not successful, otherwise
-- the SMT script containing the proof (to obtain `unsat`) is returned.
failfree: 
<FAILING>
indeterministic: 
referentially transparent operation
infix: 
no fixity defined
iotype: 
{(_,_,_,_,_,_,_) |-> _}
name: 
checkImplicationWithSMT
precedence: 
no precedence defined
result-values: 
_
signature: 
ToolOptions.Options -> Data.IORef.IORef VerifierState.VState -> String
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)] -> ESMT.Term -> ESMT.Term
-> ESMT.Term -> Prelude.IO (Prelude.Maybe String)
solution-complete: 
operation might suspend on free variables
terminating: 
possibly non-terminating
totally-defined: 
possibly non-reducible on same data term