liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Solver.Instantiate

Description

This module implements "Proof by Logical Evaluation" where we unfold function definitions if they *must* be unfolded, to strengthen the environments with function-definition-equalities. The algorithm is discussed at length in:

  1. "Refinement Reflection", POPL 2018, https://arxiv.org/pdf/1711.03842
  2. "Reasoning about Functions", VMCAI 2018, https://ranjitjhala.github.io/static/reasoning-about-functions.pdf
Synopsis

Documentation

instantiate :: Loc a => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a) Source #

Strengthen Constraint Environments via PLE