nunchaku

nunchaku copied to clipboard

= Nunchaku :toc: macro :source-highlighter: pygments

image::https://github.com/nunchaku-inria/nunchaku/workflows/build/badge.svg[Build status on github]

A counter-example finder for higher-order logic, designed to be used from various proof assistants. A spiritual successor to Nitpick. Documentation at https://nunchaku-inria.github.io/nunchaku/.

Nunchaku requires http://cvc4.cs.nyu.edu/web/[CVC4] 1.5 or later. Alternatively, it can use other backends:

• https://github.com/c-cube/smbc[smbc], a solver written in OCaml, for computational logic
• kodkod with its https://github.com/nunchaku-inria/kodkodi-pkg[kodkodi frontend]
• Paradox (https://github.com/c-cube/paradox[snapshot here])

We have https://github.com/nunchaku-inria/nunchaku-problems[a set of problems] for tests and regressions, that can also be helpful to grasp the input syntax and see how to use the constructs of Nunchaku.

toc::[]

== Basic Usage

After installing nunchaku (see <>) and at least one backend, call the tool on problem files written in one of the accepted syntaxes (<>) as follows:

$ git clone https://github.com/nunchaku-inria/nunchaku-problems $ nunchaku nunchaku-problems/tests/first_order.nun SAT: { type term := {$term_0, $term_1}. type list := {$list_0, $list_1}. val nil := $list_1. val a := $term_1. val b := $term_0. val cons := (fun (v_0/75:term) (v_1/76:list). if v_0/75 = $term_0 then $list_0 else if v_1/76 = $list_0 then $list_1 else $list_0).} {backend:smbc, time:0.0s}

A list of options can be obtained by calling nunchaku --help. A few particularly useful options are:

• --help for listing options.
• --timeout <n> (or -t <n>): maximal amount of seconds before returning "unknown"
• j <n> for controlling the number of backend solvers active at the same time.
• --solvers s1,s2 (or -s s1,s2) for using only the listed solvers.
• --debug <n> (where n=1,2,…5) to enable debug printing. The maximal verbosity level is 5, and it is very verbose. Consider using nunchaku --debug 5 foo.nun | less -R to not drown in pages of text.
• --pp-all (and each --pp-<pass>) for printing the problem after each transformation.
• -nc to disable colored output if your terminal does not support it..

== Contact

There is a dedicated mailing list at [email protected] (https://lists.gforge.inria.fr/mailman/listinfo/nunchaku-users[register]). The https://github.com/nunchaku-inria/nunchaku/issues[issue tracker] can be used for reporting bugs.

== Documentation

See the website https://nunchaku-inria.github.io/nunchaku/ and link:/docs/index.adoc[the documentation sources].

[[install]] == Build/Install

To build Nunchaku, there are several ways.

=== Released versions

Releases can be found on https://gforge.inria.fr/projects/nunchaku .

=== Opam

The easiest way is to use http://opam.ocaml.org/[opam], the package manager for OCaml. Once opam is installed (don't forget to run eval opam config env`` when you want to use opam), the following should suffice:

opam pin add -k git nunchaku https://github.com/nunchaku-inria/nunchaku.git#master

then opam should propose to install nunchaku and its dependencies. To upgrade:

opam update
opam upgrade nunchaku

Note that the binary is called 'nunchaku.native' until is it installed.

=== Manually

You need to install the dependencies first, namely:

• http://projects.camlcity.org/projects/findlib.html[ocamlfind]
• https://github.com/c-cube/ocaml-containers/[containers]
• http://gallium.inria.fr/~fpottier/menhir/[menhir]
• https://github.com/c-cube/iter[Iter]
• https://github.com/c-cube/tip-parser[tip-parser] (which requires menhir)
• https://github.com/ocaml/dune/[dune] (build system)

Once you have entered the source directory, type:

make

== License

Free software under the BSD license. See file 'LICENSE' for more details.

[[supported-formats]] == Input/Output/Solvers

Supported input formats are:

• nunchaku's own link:/docs/input_lang.adoc[input format], ML-like (extension .nun)
• TPTP (very partial support, extension .p)
• https://github.com/tip-org/[TIP] (extension .smt2)

Supported solver backends:

• http://cvc4.cs.nyu.edu/web/[CVC4] (at least 1.5, or development versions: we need finite model finding)
• Paradox (https://github.com/c-cube/paradox/[github clone (easy to install)]; http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.cs.chalmers.se/~koen/paradox/[official page])
• https://github.com/emina/kodkod[Kodkod] with its "kodkodi" parser
• https://github.com/c-cube/smbc/[SMBC] (opam install smbc)

=== How to make a release

• udpate the repository itself

  • edit nunchaku.opam to change version number
  • git commit --amend to update the commit
  • git tag 0.42
  • git push origin stable --tags

• make an archive:

  • tar.gz: git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.tar.gz
  • zip: git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.zip

• upload the archive on gforge, write some release notes, send a mail.