liquid-fixpoint-0.4.0.0: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Language.Fixpoint.Solver.Monad
Contents
Description
This is a wrapper around IO that permits SMT queries
Synopsis
type SolveM = StateT SolverState IO Source
Solver Monadic API ---------------------------------------------------
runSolverM :: Config -> FInfo b -> SolveM a -> IO a Source
getBinds :: SolveM BindEnv Source
filterValid :: Pred -> Cand a -> SolveM [a] Source
SMT Interface --------------------------------------------------------
tickIter :: SolveM Int Source