cabal-version: 2.4 name: liquid-fixpoint version: 0.8.0.2 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver 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 () or CVC4 () binary. license: BSD-3-Clause license-file: LICENSE copyright: 2010-17 Ranjit Jhala, University of California, San Diego. author: Ranjit Jhala, Niki Vazou, Eric Seidel maintainer: jhala@cs.ucsd.edu tested-with: GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4 category: Language homepage: https://github.com/ucsd-progsys/liquid-fixpoint build-type: Simple 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 default: False manual: True description: turn on stricter error reporting for development library autogen-modules: Paths_liquid_fixpoint exposed-modules: Language.Fixpoint.Defunctionalize Language.Fixpoint.Graph Language.Fixpoint.Graph.Deps Language.Fixpoint.Graph.Indexed Language.Fixpoint.Graph.Partition Language.Fixpoint.Graph.Reducible Language.Fixpoint.Graph.Types Language.Fixpoint.Horn.Parse Language.Fixpoint.Horn.Solve Language.Fixpoint.Horn.Types Language.Fixpoint.Horn.Transformations Language.Fixpoint.Horn.Info Language.Fixpoint.Minimize Language.Fixpoint.Misc Language.Fixpoint.Parse Language.Fixpoint.Smt.Bitvector Language.Fixpoint.Smt.Interface Language.Fixpoint.Smt.Serialize Language.Fixpoint.Smt.Theories Language.Fixpoint.Smt.Types Language.Fixpoint.Solver Language.Fixpoint.Solver.Eliminate Language.Fixpoint.Solver.GradualSolution Language.Fixpoint.Solver.Instantiate Language.Fixpoint.Solver.PLE Language.Fixpoint.Solver.Monad Language.Fixpoint.Solver.Rewrite Language.Fixpoint.Solver.Sanitize 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.Solver.Extensionality 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 Language.Fixpoint.Utils.Files Language.Fixpoint.Utils.Progress Language.Fixpoint.Utils.Statistics Language.Fixpoint.Utils.Trie Text.PrettyPrint.HughesPJ.Compat other-modules: Paths_liquid_fixpoint hs-source-dirs: src build-depends: base >= 4.9.1.0 && < 5 , ansi-terminal , array , async , attoparsec , binary , boxes , cereal , cmdargs , containers , deepseq , directory , fgl , filepath , hashable , intern , mtl , parallel , parsec , pretty >= 1.1.3.1 , process , syb , syb , text , text-format , transformers , unordered-containers default-language: Haskell98 ghc-options: -W -fno-warn-missing-methods -fwarn-missing-signatures if flag(devel) ghc-options: -Werror if !os(windows) hs-source-dirs: unix build-depends: ascii-progress >= 0.3 if os(windows) hs-source-dirs: win executable fixpoint main-is: Fixpoint.hs hs-source-dirs: bin build-depends: base >= 4.9.1.0 && < 5, liquid-fixpoint default-language: Haskell98 ghc-options: -threaded -W -fno-warn-missing-methods if flag(devel) ghc-options: -Werror test-suite test type: exitcode-stdio-1.0 main-is: test.hs other-modules: Paths_liquid_fixpoint hs-source-dirs: tests build-depends: base >= 4.9.1.0 && < 5 , containers >= 0.5 , directory , filepath , mtl >= 2.2.2 , process , stm >= 2.4 , tasty >= 0.10 , tasty-ant-xml , tasty-hunit , tasty-hunit >= 0.9 , tasty-rerun >= 1.1.12 , transformers >= 0.5 default-language: Haskell98 ghc-options: -threaded if flag(devel) ghc-options: -Werror test-suite testparser type: exitcode-stdio-1.0 main-is: testParser.hs hs-source-dirs: tests build-depends: base >= 4.9.1.0 && < 5 , liquid-fixpoint , tasty >= 0.10 , tasty-hunit , tasty-hunit >= 0.9 default-language: Haskell98 ghc-options: -threaded if flag(devel) ghc-options: -Werror