name: liquid-fixpoint version: 0.4.0.0 x-revision: 2 Copyright: 2010-15 Ranjit Jhala, University of California, San Diego. synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage: https://github.com/ucsd-progsys/liquid-fixpoint license: BSD3 license-file: LICENSE author: Ranjit Jhala, Niki Vazou, Eric Seidel maintainer: jhala@cs.ucsd.edu category: Language build-type: Custom cabal-version: >=1.10 description: This package is a Haskell wrapper to the SMTLIB-based Horn-Clause/Logical Implication constraint solver used for Liquid Types. . The solver itself is written in Ocaml. . The package includes: . 1. Types for Expressions, Predicates, Constraints, Solutions . 2. Code for serializing the above . 3. Code for parsing the results from the fixpoint.native binary . 4. The Ocaml fixpoint code and pre-compiled binaries . 5. (Deprecated) Z3 binaries if you want to link against the API. . Requirements . In addition to the .cabal dependencies you require . - A Z3 () or CVC4 () binary. If on Windows, please make sure to place the binary and any associated DLLs in your "cabal/bin" folder, right next to the fixpoint.native.exe binary. . - An ocaml compiler (if installing with -fbuild-external). Extra-Source-Files: configure , external/fixpoint/Makefile , external/fixpoint/*.ml , external/fixpoint/smtZ3.mem.ml , external/fixpoint/smtZ3.nomem.ml , external/fixpoint/*.mli , external/fixpoint/*.mll , external/fixpoint/*.mly , external/misc/*.ml , external/misc/*.mli , external/ocamlgraph/Makefile.in , external/ocamlgraph/META.in , external/ocamlgraph/configure , external/ocamlgraph/configure.in , external/ocamlgraph/lib/*.ml , external/ocamlgraph/lib/*.mli , external/ocamlgraph/src/*.ml , external/ocamlgraph/src/*.mli , external/ocamlgraph/src/*.mll , external/ocamlgraph/src/*.mly , external/z3/include/*.h , external/z3/lib/libz3-a-32b , external/z3/lib/libz3-a-64b , external/z3/lib/libz3-so-32b , external/z3/lib/libz3-so-64b , external/z3/ocaml/build-lib.sh , external/z3/ocaml/z3.ml , external/z3/ocaml/*.c , external/fixpoint/fixpoint.native-i386-linux , external/fixpoint/fixpoint.native-i686-w64-mingw32 , external/fixpoint/fixpoint.native-x86_64-darwin , external/fixpoint/fixpoint.native-x86_64-linux , tests/neg/*.fq , tests/pos/*.fq Flag z3mem Description: Link to Z3 Default: False Flag build-external Description: Build fixpoint.native binary from source (requires ocaml) Default: False Source-Repository head Type: git Location: https://github.com/ucsd-progsys/liquid-fixpoint/ -- FIXME: This is a terrible hack. We build Fixpoint.hs *twice*, once -- targeting fixpoint.native so we can then *clobber* it with the -- OCaml fixpoint.native. This is required for cabal-install to detect -- fixpoint.native as an executable, and properly symlink it when -- asked. Executable fixpoint.native default-language: Haskell98 Main-is: Fixpoint.hs Build-Depends: base >= 4.7 && < 5 , array , syb , cmdargs , ansi-terminal , bifunctors , bytestring , containers , deepseq , directory , filepath , mtl , parsec , pretty , process , syb , text , hashable , unordered-containers , text-format , liquid-fixpoint Executable fixpoint default-language: Haskell98 Main-is: Fixpoint.hs Build-Depends: base >= 4.7 && < 5 , array , syb , cmdargs , ansi-terminal , bifunctors , bytestring , containers , deepseq , directory -- , filemanip , filepath , mtl , parsec , pretty , process , syb , text , hashable , unordered-containers , text-format , liquid-fixpoint Library default-language: Haskell98 hs-source-dirs: src Exposed-Modules: Language.Fixpoint.Names, Language.Fixpoint.Files, Language.Fixpoint.Errors, Language.Fixpoint.Config, Language.Fixpoint.Types, Language.Fixpoint.Bitvector, Language.Fixpoint.Visitor, Language.Fixpoint.Sort, Language.Fixpoint.Interface, Language.Fixpoint.Parse, Language.Fixpoint.PrettyPrint, Language.Fixpoint.Smt.Types, Language.Fixpoint.Smt.Theories, Language.Fixpoint.Smt.Serialize, Language.Fixpoint.Smt.Interface, Language.Fixpoint.Misc, Language.Fixpoint.Solver.Solution, Language.Fixpoint.Solver.Worklist, Language.Fixpoint.Solver.Monad, Language.Fixpoint.Solver.Deps, Language.Fixpoint.Solver.Uniqify, Language.Fixpoint.Solver.Eliminate, Language.Fixpoint.Solver.Validate, Language.Fixpoint.Partition, Language.Fixpoint.Statistics, Language.Fixpoint.Solver.Solve Build-Depends: base >= 4.7 && < 5 , array , attoparsec , syb , cmdargs , ansi-terminal , bifunctors , bytestring , containers , deepseq , directory , filemanip , filepath , ghc-prim , intern , mtl , parsec , pretty , process , syb , text , transformers , hashable , unordered-containers , text-format test-suite test default-language: Haskell98 type: exitcode-stdio-1.0 hs-source-dirs: tests ghc-options: -O2 -threaded main-is: test.hs build-depends: base, directory, filepath, process, -- tagged, liquid-fixpoint, -- optparse-applicative == 0.11.*, tasty >= 0.10, -- tasty-quickcheck, tasty-hunit, tasty-rerun >= 1.1, text