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

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

The package includes:

Types for Expressions, Predicates, Constraints, Solutions

Code for solving constraints

Requirements

In addition to the .cabal dependencies you require

A Z3 (http://z3.codeplex.com) or CVC4 (http://cvc4.cs.nyu.edu) binary.

[Skip to Readme]

## Modules

[Index] [Quick Jump]

*Data**Language**Fixpoint**Conditional*- Language.Fixpoint.Defunctionalize
- Language.Fixpoint.Graph
*Horn*- Language.Fixpoint.Minimize
- Language.Fixpoint.Misc
- Language.Fixpoint.Parse
*Smt*- Language.Fixpoint.Solver
- Language.Fixpoint.Solver.Common
- Language.Fixpoint.Solver.Eliminate
- Language.Fixpoint.Solver.EnvironmentReduction
- Language.Fixpoint.Solver.Extensionality
- Language.Fixpoint.Solver.GradualSolution
- Language.Fixpoint.Solver.GradualSolve
- Language.Fixpoint.Solver.Instantiate
- Language.Fixpoint.Solver.Interpreter
- Language.Fixpoint.Solver.Monad
- Language.Fixpoint.Solver.PLE
- Language.Fixpoint.Solver.Prettify
- Language.Fixpoint.Solver.Rewrite
- Language.Fixpoint.Solver.Sanitize
- Language.Fixpoint.Solver.Simplify
- Language.Fixpoint.Solver.Solution
- Language.Fixpoint.Solver.Solve
- Language.Fixpoint.Solver.Stats
- Language.Fixpoint.Solver.TrivialSort
- Language.Fixpoint.Solver.UniqifyBinds
- Language.Fixpoint.Solver.UniqifyKVars
- Language.Fixpoint.Solver.Worklist

- Language.Fixpoint.SortCheck
- Language.Fixpoint.Types
- Language.Fixpoint.Types.Config
- Language.Fixpoint.Types.Constraints
- Language.Fixpoint.Types.Environments
- Language.Fixpoint.Types.Errors
- Language.Fixpoint.Types.Graduals
- Language.Fixpoint.Types.Names
- Language.Fixpoint.Types.PrettyPrint
- Language.Fixpoint.Types.Refinements
- Language.Fixpoint.Types.Solutions
- Language.Fixpoint.Types.Sorts
- Language.Fixpoint.Types.Spans
- Language.Fixpoint.Types.Substitutions
- Language.Fixpoint.Types.Templates
- Language.Fixpoint.Types.Theories
- Language.Fixpoint.Types.Triggers
- Language.Fixpoint.Types.Utils
- Language.Fixpoint.Types.Visitor

*Utils*

*Text**PrettyPrint**HughesPJ*

## Flags

### Manual Flags

Name | Description | Default |
---|---|---|

link-z3-as-a-library | link z3 as a library for faster interactions with the SMT solver | Disabled |

devel | turn on stricter error reporting for development | Disabled |

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

## Downloads

- liquid-fixpoint-0.9.6.3.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)

#### Maintainer's Corner

For package maintainers and hackage trustees

Candidates