Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Stackage Nightly 2020-09-22:
Latest on Hackage:

See all snapshots liquid-fixpoint appears in

BSD-3-Clause licensed by Ranjit Jhala, Niki Vazou, Eric Seidel
Maintained by

Module documentation for

This version can be pinned in stack with:liquid-fixpoint-,7306

This package implements an SMTLIB based Horn-Clause/Logical Implication constraint solver used for Liquid Types.

The package includes:

  1. Types for Expressions, Predicates, Constraints, Solutions

  2. Code for solving constraints


In addition to the .cabal dependencies you require