Language.Fixpoint.Minimize

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))

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

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