Nunchaku

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 CVC4 1.5 or later. Alternatively, it can use other backends:

• smbc, a solver written in OCaml, for computational logic

• kodkod with its kodkodi frontend

• Paradox (snapshot here)

We have 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.

Table of Contents

• Basic Usage
• Contact
• Documentation
• Build/Install
  • Released versions
  • Opam
  • Manually
• License
• Input/Output/Solvers
  • How to make a release

Basic Usage

After installing nunchaku (see Build/Install) and at least one backend, call the tool on problem files written in one of the accepted syntaxes (Input/Output/Solvers) 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 nunchaku-users@lists.gforge.inria.fr (register). The issue tracker can be used for reporting bugs.

Documentation

See the website https://nunchaku-inria.github.io/nunchaku/ and the documentation sources.

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 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:

• ocamlfind

• containers

• menhir

• Iter

• tip-parser (which requires menhir)

• 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.

Input/Output/Solvers

Supported input formats are:

• nunchaku’s own input format, ML-like (extension .nun)

• TPTP (very partial support, extension .p)

• TIP (extension .smt2)

Supported solver backends:

• CVC4 (at least 1.5, or development versions: we need finite model finding)

• Paradox (github clone (easy to install); official page)

• Kodkod with its "kodkodi" parser

• 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.