|
definition:
|
solveSMTVars :: [Term] -> [Command]
-> SMTSess (Either [SMTError] [ValuationPair])
solveSMTVars vars 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 bindings of given variables for SMT problem"
vps <- getValues vars
optReset
return vps
res -> do
info "No variable bindings 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 given variables
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,_) |-> _}
|
|
name:
|
solveSMTVars
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
[Language.SMTLIB.Types.Term] -> [Language.SMTLIB.Types.Command]
-> Solver.SMTLIB.Internal.Interaction.SMTSess (Prelude.Either [Solver.SMTLIB.Types.SMTError] [(Language.SMTLIB.Types.Term, Language.SMTLIB.Types.Term)])
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|