opam-version: "2.0"
synopsis: "Model finder for geometric theories using the chase"
description: """
The chase program 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.2.tar.gz"
  checksum: [
    "sha256=4b2da98d6f9036e569a31d06f5977f4e396d634614e9ffc34c6c14d7c94d2ce3"
    "md5=157a6b2be81bdb0afc4cde76b6f0e88a"
  ]
}