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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Minimize

Description

This module implements a "delta-debugging" based query minimizer. Exported clients of that minimizer include one that attempts to shrink UNSAT queries down to a minimal subset of constraints, one that shrinks SAT queries down to a minimal subset of qualifiers, and one that shrinks SAT queries down to a minimal subset of KVars (replacing all others by True).

Documentation

minQuery :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> IO (Result (Integer, a)) Source #

minQuals :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> IO (Result (Integer, a)) Source #

minKvars :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> IO (Result (Integer, a)) Source #