cabal-version: 2.4 name: liquid-fixpoint version: 0.9.6.3 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. category: Language homepage: https://github.com/ucsd-progsys/liquid-fixpoint#readme bug-reports: https://github.com/ucsd-progsys/liquid-fixpoint/issues author: Ranjit Jhala, Niki Vazou, Eric Seidel maintainer: jhala@cs.ucsd.edu copyright: 2010-17 Ranjit Jhala, University of California, San Diego. license: BSD-3-Clause license-file: LICENSE build-type: Simple tested-with: GHC == 9.6.3, GHC == 9.4.7, GHC == 9.2.3 extra-source-files: tests/neg/*.fq tests/pos/*.fq unix/Language/Fixpoint/Utils/*.hs win/Language/Fixpoint/Utils/*.hs tests/logs/cur/pin Makefile extra-doc-files: CHANGES.md README.md common warnings ghc-options: -Wall source-repository head type: git location: https://github.com/ucsd-progsys/liquid-fixpoint flag link-z3-as-a-library description: link z3 as a library for faster interactions with the SMT solver manual: True default: False flag devel description: turn on stricter error reporting for development manual: True default: False library import: warnings exposed-modules: Data.ShareMap Language.Fixpoint.Conditional.Z3 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.Info Language.Fixpoint.Horn.Parse Language.Fixpoint.Horn.Solve Language.Fixpoint.Horn.Transformations Language.Fixpoint.Horn.Types Language.Fixpoint.Minimize Language.Fixpoint.Misc Language.Fixpoint.Parse Language.Fixpoint.Smt.Interface Language.Fixpoint.Smt.Serialize Language.Fixpoint.Smt.Theories Language.Fixpoint.Smt.Types Language.Fixpoint.Solver Language.Fixpoint.Solver.Common Language.Fixpoint.Solver.Eliminate Language.Fixpoint.Solver.EnvironmentReduction Language.Fixpoint.Solver.Extensionality Language.Fixpoint.Solver.GradualSolution Language.Fixpoint.Solver.GradualSolve Language.Fixpoint.Solver.Instantiate Language.Fixpoint.Solver.Interpreter Language.Fixpoint.Solver.Monad Language.Fixpoint.Solver.PLE Language.Fixpoint.Solver.Prettify Language.Fixpoint.Solver.Rewrite Language.Fixpoint.Solver.Sanitize Language.Fixpoint.Solver.Simplify 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.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.Builder 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 autogen-modules: Paths_liquid_fixpoint hs-source-dirs: src ghc-options: -W -Wno-missing-methods -Wmissing-signatures build-depends: aeson , ansi-terminal , array , async , attoparsec , base >= 4.9.1.0 && < 5 , binary , boxes , bytestring >= 0.10.2.1 , cereal , cmdargs , containers , deepseq , directory , fgl , filepath , hashable , intern , lens-family , megaparsec >= 7.0.0 && < 10 , mtl , parallel , parser-combinators , pretty >= 1.1.3.1 , process , typed-process , rest-rewrite >= 0.3.0 , smtlib-backends >= 0.3 , smtlib-backends-process >= 0.3 , stm , store , vector < 0.14 , syb , text , transformers , unordered-containers ghc-options: -fwrite-ide-info -hiedir=.hie if flag(link-z3-as-a-library) build-depends: smtlib-backends-z3 >= 0.3 hs-source-dirs: src-cond/with-z3 else hs-source-dirs: src-cond/without-z3 if impl(ghc<9.6) ghc-options: -Wno-unused-imports 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 default-language: Haskell98 executable fixpoint import: warnings main-is: Fixpoint.hs other-modules: Paths_liquid_fixpoint autogen-modules: Paths_liquid_fixpoint hs-source-dirs: bin ghc-options: -threaded -W -Wno-missing-methods build-depends: base >= 4.9.1.0 && < 5, liquid-fixpoint if flag(devel) ghc-options: -Werror default-language: Haskell98 test-suite test import: warnings type: exitcode-stdio-1.0 main-is: test.hs other-modules: Paths_liquid_fixpoint autogen-modules: Paths_liquid_fixpoint hs-source-dirs: tests ghc-options: -threaded build-depends: base >= 4.9.1.0 && < 5 , containers >= 0.5 , directory , filepath , mtl >= 2.2.2 , optparse-applicative , process , typed-process , stm >= 2.4 , tagged , tasty >= 0.10 && < 1.5 , tasty-ant-xml , tasty-hunit >= 0.9 , tasty-rerun >= 1.1.12 , transformers >= 0.5 if flag(devel) ghc-options: -Werror build-tool-depends: liquid-fixpoint:fixpoint default-language: Haskell98 test-suite tasty import: warnings type: exitcode-stdio-1.0 main-is: Main.hs other-modules: Arbitrary InterpretTests ParserTests ShareMapReference ShareMapTests SimplifyInterpreter SimplifyPLE SimplifyTests UndoANFTests Paths_liquid_fixpoint autogen-modules: Paths_liquid_fixpoint hs-source-dirs: tests/tasty ghc-options: -threaded build-depends: base >= 4.9.1.0 && < 5 , containers , hashable , liquid-fixpoint , tasty >= 0.10 , tasty-hunit >= 0.9 , tasty-quickcheck , text , unordered-containers if flag(devel) ghc-options: -Werror default-language: Haskell98