liquid-fixpoint

Predicate Abstraction-based Horn-Clause/Implication Constraint Solver https://github.com/ucsd-progsys/liquid-fixpoint

Stackage Nightly 2020-10-20:0.8.10.2
Latest on Hackage:0.8.10.2

See all snapshots liquid-fixpoint appears in

BSD-3-Clause licensed by Ranjit Jhala, Niki Vazou, Eric Seidel
Maintained by jhala@cs.ucsd.edu

Module documentation for 0.8.10.2

This version can be pinned in stack with:liquid-fixpoint-0.8.10.2@sha256:1646c4cc5f81349356a0d37bd3c8f4db74ced9e1707a2e19915c8d2fa6ae9e43,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

Requirements

In addition to the .cabal dependencies you require