Revision 130f3a90c46e1c2922bbe6494850626fad5b9213 authored by Ranjit Jhala on 11 April 2019, 19:50:01 UTC, committed by Ranjit Jhala on 11 April 2019, 19:50:01 UTC
1 parent 876cd13
liquid-fixpoint.cabal
name: liquid-fixpoint
version: 0.8.0.2
Copyright: 2010-17 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: Simple
cabal-version: >=1.10
Tested-With: GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4
description: 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
.
- A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.
Extra-Source-Files: tests/neg/*.fq
, tests/pos/*.fq
, unix/Language/Fixpoint/Utils/*.hs
, win/Language/Fixpoint/Utils/*.hs
, tests/logs/cur/pin
, Makefile
Source-Repository head
Type: git
Location: https://github.com/ucsd-progsys/liquid-fixpoint/
Flag devel
Description: turn on stricter error reporting for development
Default: False
Manual: True
Executable fixpoint
default-language: Haskell98
Main-is: Fixpoint.hs
ghc-options: -threaded -W -fno-warn-missing-methods
if flag(devel)
ghc-options: -Werror
hs-source-dirs: bin
Build-Depends: base >=4.9.1.0 && <5
, liquid-fixpoint
Library
default-language: Haskell98
ghc-options: -W -fno-warn-missing-methods
if flag(devel)
ghc-options: -Werror
hs-source-dirs: src
Exposed-Modules: Language.Fixpoint.Types.Names,
Language.Fixpoint.Types.Errors,
Language.Fixpoint.Types.Config,
Language.Fixpoint.Types.Visitor,
Language.Fixpoint.Types.Theories,
Language.Fixpoint.Types.PrettyPrint,
Language.Fixpoint.Types.Spans,
Language.Fixpoint.Types.Sorts,
Language.Fixpoint.Types.Refinements,
Language.Fixpoint.Types.Substitutions,
Language.Fixpoint.Types.Environments,
Language.Fixpoint.Types.Constraints,
Language.Fixpoint.Types.Triggers,
Language.Fixpoint.Types.Solutions,
Language.Fixpoint.Types.Utils,
Language.Fixpoint.Types.Templates,
Language.Fixpoint.Types.Graduals,
Language.Fixpoint.Types,
Language.Fixpoint.Graph.Types,
Language.Fixpoint.Graph.Reducible,
Language.Fixpoint.Graph.Indexed,
Language.Fixpoint.Graph.Partition,
Language.Fixpoint.Graph.Deps,
Language.Fixpoint.Graph,
Language.Fixpoint.Defunctionalize,
Language.Fixpoint.Smt.Types,
Language.Fixpoint.Smt.Bitvector,
Language.Fixpoint.Smt.Theories,
Language.Fixpoint.Smt.Serialize,
Language.Fixpoint.Smt.Interface,
Language.Fixpoint.Minimize,
Language.Fixpoint.Solver,
Language.Fixpoint.Parse,
Language.Fixpoint.SortCheck,
Language.Fixpoint.Misc,
Language.Fixpoint.Utils.Progress,
Language.Fixpoint.Utils.Files,
Language.Fixpoint.Utils.Trie,
Language.Fixpoint.Solver.GradualSolution,
Language.Fixpoint.Solver.Solution,
Language.Fixpoint.Solver.Worklist,
Language.Fixpoint.Solver.Monad,
Language.Fixpoint.Solver.TrivialSort,
Language.Fixpoint.Solver.UniqifyKVars,
Language.Fixpoint.Solver.UniqifyBinds,
Language.Fixpoint.Solver.Eliminate,
Language.Fixpoint.Solver.Instantiate,
Language.Fixpoint.Solver.Sanitize,
Language.Fixpoint.Utils.Statistics,
Language.Fixpoint.Solver.Solve,
Language.Fixpoint.Horn.Types,
Language.Fixpoint.Horn.Parse,
Language.Fixpoint.Horn.Solve,
Text.PrettyPrint.HughesPJ.Compat
Other-Modules: Paths_liquid_fixpoint
Build-Depends: base >=4.9.1.0 && <5
, array
, async
, attoparsec
, syb
, cmdargs
, ansi-terminal
, bifunctors
, binary
, bytestring
, containers
, deepseq
, directory
, filemanip
, filepath
, ghc-prim
, intern
, mtl
, parsec
, pretty >=1.1.3.1
, boxes
, parallel
, process
, syb
, text
, transformers
, hashable
, unordered-containers
, cereal
, text-format
, fgl
, fgl-visualize
, dotgen
, time
, parallel-io
-- unconditionally depend on located-base
Build-Depends: located-base
if !os(windows)
Build-Depends: ascii-progress >= 0.3
hs-source-dirs: unix
if os(windows)
hs-source-dirs: win
test-suite test
default-language: Haskell98
type: exitcode-stdio-1.0
hs-source-dirs: tests
ghc-options: -threaded
if flag(devel)
ghc-options: -Werror
main-is: test.hs
Other-Modules: Paths_liquid_fixpoint
build-depends: base >= 4.9.1.0 && < 5,
directory,
filepath,
process,
stm >= 2.4,
containers >= 0.5,
mtl >= 2.2.2,
transformers >= 0.5,
tasty >= 0.10,
tasty-hunit,
tasty-rerun >= 1.1.12,
tasty-ant-xml,
tasty-hunit >= 0.9,
text
test-suite testparser
default-language: Haskell98
type: exitcode-stdio-1.0
hs-source-dirs: tests
ghc-options: -threaded
if flag(devel)
ghc-options: -Werror
main-is: testParser.hs
build-depends: base >= 4.9.1.0 && < 5,
directory,
filepath,
tasty >= 0.10,
tasty-hunit,
tasty-rerun >= 1.1,
tasty-ant-xml,
tasty-hunit >= 0.9,
text,
liquid-fixpoint
if flag(devel)
hs-source-dirs: tests src
other-modules:
Language.Fixpoint.Misc
Language.Fixpoint.Parse
Language.Fixpoint.Smt.Bitvector
Language.Fixpoint.Smt.Types
Language.Fixpoint.Types
Language.Fixpoint.Types.Config
Language.Fixpoint.Types.Constraints
Language.Fixpoint.Types.Environments
Language.Fixpoint.Types.Errors
Language.Fixpoint.Types.Names
Language.Fixpoint.Types.PrettyPrint
Language.Fixpoint.Types.Refinements
Language.Fixpoint.Types.Sorts
Language.Fixpoint.Types.Templates
Language.Fixpoint.Types.Spans
Language.Fixpoint.Types.Substitutions
Language.Fixpoint.Types.Theories
Language.Fixpoint.Types.Triggers
Language.Fixpoint.Types.Utils
Language.Fixpoint.Utils.Files
Language.Fixpoint.Utils.Trie
Text.PrettyPrint.HughesPJ.Compat
build-depends:
array
, async
, attoparsec
, syb
, cmdargs
, ansi-terminal
, bifunctors
, binary
, bytestring
, containers
, deepseq
, directory
, filemanip
, filepath
, ghc-prim
, intern
, mtl
, parsec
, pretty
, boxes
, parallel
, process
, syb
, text
, transformers
, hashable
, unordered-containers
, cereal
, text-format
, fgl
, fgl-visualize
, dotgen
, time
if impl(ghc >= 7.10.2)
Build-Depends: located-base
else
build-depends: liquid-fixpoint
Computing file changes ...