|
definition:
|
solveSMT :: [Command] -> SMTSess (Either [SMTError] [ModelRsp])
solveSMT cmds = evalSession $ do
bufferGlobalDefs
info "Asserting definitions and constraints"
sendCmds cmds
info "Checking satisfiability of constraints"
isSat <- checkSat
case isSat of
Sat -> do
info "Satisfiable -> Getting model for SMT problem"
m <- getModel
optReset
return m
res -> do
info "No model found for given SMT problem"
optReset
return $ Left $ res2Msgs res
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
--- Solve the SMT problem specified by the given SMT-LIB commands and
--- try to find a binding for all variables used
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_) |-> _}
|
|
name:
|
solveSMT
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
[Language.SMTLIB.Types.Command]
-> Solver.SMTLIB.Internal.Interaction.SMTSess (Prelude.Either [Solver.SMTLIB.Types.SMTError] [Language.SMTLIB.Types.ModelRsp])
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|