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.