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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Eliminate

Description

This module exports a single function that computes the dependency information needed to eliminate non-cut KVars, and then transitively collapse the resulting constraint dependencies. See the type of SolverInfo for details.

Synopsis

Documentation

solverInfo :: Config -> SInfo a -> SolverInfo a b Source #

solverInfo constructs a SolverInfo comprising the Solution and various indices needed by the worklist-based refinement loop