liquid-fixpoint: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
This package is a Haskell wrapper to the 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.
Modules
[Index]
- Language
- Fixpoint
- Language.Fixpoint.Minimize
- Language.Fixpoint.Misc
- Language.Fixpoint.Parse
- Language.Fixpoint.Partition
- Smt
- Language.Fixpoint.Solver
- Language.Fixpoint.Solver.Eliminate
- Language.Fixpoint.Solver.Graph
- Language.Fixpoint.Solver.Monad
- Language.Fixpoint.Solver.Solution
- Language.Fixpoint.Solver.Solve
- Language.Fixpoint.Solver.TrivialSort
- Language.Fixpoint.Solver.Types
- Language.Fixpoint.Solver.UniqifyBinds
- Language.Fixpoint.Solver.UniqifyKVars
- Language.Fixpoint.Solver.Validate
- 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.Graphs
- Language.Fixpoint.Types.Names
- Language.Fixpoint.Types.PrettyPrint
- Language.Fixpoint.Types.Refinements
- Language.Fixpoint.Types.Sorts
- Language.Fixpoint.Types.Spans
- Language.Fixpoint.Types.Substitutions
- Language.Fixpoint.Types.Utils
- Language.Fixpoint.Types.Visitor
- Utils
- Fixpoint
Downloads
- liquid-fixpoint-0.5.0.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates