Name: jukebox
Version: 0.2.17
Cabal-version: >= 1.8
Build-type: Simple
Author: Nick Smallbone
Maintainer: nicsma@chalmers.se
Copyright: 2009-2016 Nick Smallbone, Koen Claessen, Ann Lillieström

Category:            Logic

Synopsis:            A first-order reasoning toolbox
Description:
  Jukebox is a suite of tools for transforming problems in first-order logic.
  It reads problems in TPTP (FOF and TFF) format.
  .
  Currently it can translate typed problems to untyped (by efficiently
  encoding types) and clausify problems (both typed and untyped).
License: BSD3
License-file: LICENSE
extra-source-files: src/errors.h

flag minisat
  Description: Use minisat. Required for monotonicity inference.
  Default: True

source-repository head
  type:     git
  location: https://github.com/nick8325/jukebox

Library
  Build-depends: base >= 4 && < 5, array, transformers >= 0.4.0.0, directory,
    filepath, pretty >= 1.1.2.0, symbol, dlist, process, containers, uglymemo
  if flag(minisat)
    Build-depends: minisat
    Exposed-modules:
      Jukebox.Sat3
      Jukebox.SatEq
      Jukebox.Sat
      Jukebox.SatMin
      Jukebox.HighSat
  else
    cpp-options: -DNO_MINISAT
  ghc-options: -W -fno-warn-incomplete-patterns
  Build-tools: alex
  Hs-source-dirs: src
  include-dirs: src
  Exposed-modules:
    Jukebox.Clausify
    Jukebox.Form
    Jukebox.GuessModel
    Jukebox.InferTypes
    Jukebox.Monotonox.Monotonicity
    Jukebox.Monotonox.ToFOF
    Jukebox.Name
    Jukebox.Options
    Jukebox.Provers.E
    Jukebox.Provers.SPASS
    Jukebox.SMTLIB
    Jukebox.Toolbox
    Jukebox.TPTP.Parse.Core
    Jukebox.TPTP.FindFile
    Jukebox.TPTP.Lexer
    Jukebox.TPTP.Parsec
    Jukebox.TPTP.Parse
    Jukebox.TPTP.ParseSnippet
    Jukebox.TPTP.Print
    Jukebox.UnionFind
    Jukebox.Utils

Executable jukebox
  Main-is: executable/Main.hs
  Build-depends: base >= 4 && < 5, jukebox
  ghc-options: -W -fno-warn-incomplete-patterns