|
definition:
|
solveAllSMTVars :: [Term] -> [Command] -> Int
-> SMTSess (Either [SMTError] [[ValuationPair]])
solveAllSMTVars vars cmds i = 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
case vps of
Right vps' -> do
vpss <- concatMapM (getCounterExamples vps' i) vars
optReset
return $ Right $ nub vpss
Left e -> optReset >> (return $ Left e)
Unsat -> do
info "No variable bindings found for given SMT problem"
optReset
return $ Right []
res -> do
info "An error occurred while solving given SMT problem"
optReset
return $ Left $ res2Msgs res
where
getCounterExamples :: [ValuationPair] -> Int -> Term
-> SMT [[ValuationPair]]
getCounterExamples vps i' var = do
bufferCmds [Push 1]
vpss <- assertCounterExamples (fromJust $ lookup var vps) [vps] var i'
bufferCmds [Pop 1]
return vpss
assertCounterExamples :: Term -> [[ValuationPair]] -> Term -> Int
-> SMT [[ValuationPair]]
assertCounterExamples v vpss var i' = do
sendCmds [assert [var /=% v]]
isSat <- checkSat
case isSat of
Sat -> do
vps <- getValues vars
case vps of
Right vps' | i' > 1 -> assertCounterExamples
(fromJust $ lookup var vps')
(vps':vpss) var (i' - 1)
_ -> return vpss
_ -> return vpss
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
--- Solve the SMT problem specified by the given SMT-LIB commands and
--- try to find all bindings for the given variable.
--- The given integer determines how many counter examples are returned at
--- maximum for each variable.
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,_,_) |-> _}
|
|
name:
|
solveAllSMTVars
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
[Language.SMTLIB.Types.Term] -> [Language.SMTLIB.Types.Command] -> Prelude.Int
-> 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
|