liquid-fixpoint-0.4.0.0: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Monad

Contents

Description

This is a wrapper around IO that permits SMT queries

Synopsis

Type

type SolveM = StateT SolverState IO Source

Solver Monadic API ---------------------------------------------------

Execution

runSolverM :: Config -> FInfo b -> SolveM a -> IO a Source

Get Binds

getBinds :: SolveM BindEnv Source

SMT Query

filterValid :: Pred -> Cand a -> SolveM [a] Source

SMT Interface --------------------------------------------------------

Debug

tickIter :: SolveM Int Source