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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Utils

Contents

Description

This module has various utility functions for accessing queries. TODO: move the "clients" in Visitors into this module.

Synopsis

Domain of a kvar

kvarDomain :: SInfo a -> KVar -> [Symbol] Source #

Compute the domain of a kvar

Free variables in a refinement

reftFreeVars :: Reft -> HashSet Symbol Source #

Free variables of a refinement

Deconstruct a SortedReft

sortedReftConcKVars :: Symbol -> SortedReft -> ([Pred], [KVSub], [KVSub]) Source #

Split a SortedReft into its concrete and KVar components