opam-version: "2.0"
synopsis: "Model finder for geometric theories using the chase"
description: """
Chase is a model finder for first order logic with equality.  It finds
minimal models of a theory expressed in geometric form, where
functions in models may be partial.  A formula is in geometric form if
it is a sentence consisting of a single implication, the antecedent is
a conjunction of atomic formulas, and the consequent is a disjunction.
Each disjunct is a possibly existentially quantified conjunction of
atomic formulas.  A function is partial if it is defined only on a
proper subset of its domain.
"""
maintainer: "John D. Ramsdell <ramsdell@mitre.org>"
authors: "John D. Ramsdell <ramsdell@mitre.org>"
license: "BSD"
homepage: "https://github.com/ramsdell/chase"
dev-repo: "git+https://github.com/ramsdell/chase.git"
bug-reports: "https://github.com/ramsdell/chase/issues"
depends: ["ocaml" { >= "4.05" } "getopt" "dune" { >= "1.1" }]
build: ["dune" "build" "-p" name "-j" jobs]
url {
  src: "https://github.com/ramsdell/chase/archive/1.4.tar.gz"
  checksum: [
    "sha256=e8d8840b9ede0a8b97735777647aa9f52304579db33a001215f1b661926e7969"
    "md5=937e96273bb2bea1be60a3e7d2672fd9"
  ]
}