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.
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:
-
--helpfor 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>(wheren=1,2,…5) to enable debug printing. The maximal verbosity level is 5, and it is very verbose. Consider usingnunchaku --debug 5 foo.nun | less -Rto not drown in pages of text. -
--pp-all(and each--pp-<pass>) for printing the problem after each transformation. -
-ncto disable colored output if your terminal does not support it..
Contact
There is a dedicated mailing list at [email protected] (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:
-
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.opamto change version number -
git commit --amendto 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.