nunchaku-inria / nunchaku Goto Github PK

View Code? Open in Web Editor NEW

41.0 6.0 3.0 4.08 MB

Model finder for higher-order logic

Home Page: https://nunchaku-inria.github.io/nunchaku/

License: BSD 2-Clause "Simplified" License

Makefile 0.12% OCaml 99.88%

model-finding sat cvc4 higher-order logic proof-assistant isabelle hol

nunchaku's Introduction

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

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.

nunchaku's People

Stargazers

Watchers

Forkers

fxfactorial rafoo bryjikov

nunchaku's Issues

add prototypes

in encoding of functions, add the prototype (perhaps with a flag to enable/disable it).

call CVC4 with --fmf-empty-sorts to avoid refining recursive functions that are not used. We need to force it to fill other sorts though, by declaring p : sort -> bool, c : sort, and p(c) if we want to ensure that sort is not empty.

polymorphic constants

val monoid: type -> type.
val inst_monoid: forall a. a -> (a -> a -> a) -> monoid a.

currently results in:

Error: ill-formed term: no quantifiers in types
  at file 'foo.nun': line 3, col 17 to 57

I suppose we should monomorphize such undefined symbols properly.

Release page returns 403 error, and compiling nunchaku fails with numerous errors

Hello, couldn't install nunchaku on my system because the release page https://gforge.inria.fr/projects/nunchaku returns a 403 error and installing with opam (or compiling manually) fails with:

#=== ERROR while compiling nunchaku.0.6 =======================================#
# context     2.1.2 | linux/x86_64 | ocaml.4.13.1 | pinned(git+https://github.com/nunchaku-inria/nunchaku.git#master#91e62687)
# path        ~/.opam/default/.opam-switch/build/nunchaku.0.6
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p nunchaku -j 19
# exit-code   1
# env-file    ~/.opam/log/nunchaku-147734-090624.env
# output-file ~/.opam/log/nunchaku-147734-090624.out
### output ###
# [...]
# Alert deprecated: module CCOpt
# use CCOption instead
# File "src/transformations/TypeInference.ml", line 965, characters 8-17:
# 965 |         CCOpt.map
#               ^^^^^^^^^
# Alert deprecated: module CCOpt
# use CCOption instead
# File "src/transformations/TypeInference.ml", line 1129, characters 22-32:
# 1129 |                       CCOpt.iter (check_prenex_types_ ~loc) g;
#                              ^^^^^^^^^^
# Alert deprecated: module CCOpt
# use CCOption instead

Fixing that with a simple search and replace uncovers more deprecation errors.

nunchaku fails to find a counterexample for a simple list-based map implementation

Versions:

nunchaku 0.5.1 70e5101
CVC4 version 1.5 (shipped with Isabelle 2017)

The following example

val K : type.
val V : type.

data tuple := pair K V.

data list :=
  nil
| cons tuple list.

data option :=
  None
| Some V.

rec get : list -> K -> option :=
  forall k. get nil k = None;
  forall ki vi k rest. get (cons (pair ki vi) rest) k =
    (if (ki = k) then Some vi else get rest k).

rec filter : (tuple -> prop) -> list -> list :=
  forall f. filter f nil = nil;
  forall f h t. filter f (cons h t) =
    (if (f h) then (cons h (filter f t)) else (filter f t)).

rec remove : list -> K -> list :=
  forall l k. remove l k = filter (fun t.
     match t with
     | pair ki vi -> ki != k
     end)
     l.

rec put : list -> K -> V -> list :=
  put = (fun l k v. cons (pair k v) (remove l k)).

val l: list.
val k1: K.
val k2: K.
val v: V.

# Missing hypothesis:
# axiom k1 != k2.

goal ~ (get (put l k1 v) k2 = get l k2).

returns UNKNOWN, even though a simple counterexample exists, as shown by nitpick in Isabelle2017:

theory ListMapTests
  imports Main
begin

typedecl K
typedecl V

datatype tuple = pair K V

datatype list = nil | cons tuple list

datatype option = None | Some V

fun get :: "list ⇒ K ⇒ option" where
  "get nil k = None" |
  "get (cons (pair ki vi) rest) k = 
    (if (ki = k) then Some vi else get rest k)"

fun filter :: "(tuple ⇒ bool) ⇒ list ⇒ list" where
  "filter f nil = nil" |
  "filter f (cons h t) =
     (if (f h) then (cons h (filter f t)) else (filter f t))"

fun remove :: "list ⇒ K ⇒ list" where
  "remove l k = filter (λ t. case t of pair ki vi ⇒ ki ≠ k) l"

fun put :: "list ⇒ K ⇒ V ⇒ list" where
  "put l k v = cons (pair k v) (remove l k)"

lemma "get (put l k1 v) k2 = get l k2"
  nitpick

which returns

Nitpick found a counterexample for card K = 2 and card V = 2:

  Free variables:
    k1 = K⇩1
    k2 = K⇩1
    l = nil
    v = V⇩1

I understand that nunchaku has not yet received as much development time as nitpick and the tools powering it, but do you have an estimate of how far nunchaku is away from being able to solve examples like this one? Or is there a simple change I can make to the input file so that it works?

(co)inductive predicates

keyword: pred/copred (?)

copred a : foo -> prop :=
  a x & b (f x) => a (s x);
  a 0
and b : bar -> prop := ....

Each rhs should start with the defined predicate and contain no other occurrence of the predicates being defined.

Flag well-founded (or variant wf-pred / wf-copred) as an option/attribute.
For well-founded predicates, encoding straightforward (turn into a rec definition, then encoding of rec functions).

not well-founded: add an argument (of type nat) that decreases at each call:

pred even n :=
  even 0;
  even n => even n;
  even n => even (s (s n)).

# use even
p (even n0).

becomes, with an approximation of depth k:

wf-pred even k n :=
  even 0 _ = false;  # we start at 1
  even (s k) 0;
  even k n => even (s k) n;
  even k n => even (s k) (s (s n)).

val k0: nat.

# use even:
p (even k0 n0).

and then we can reverse the definition and turn it into a recursive function.

inlining pass

transformation for inlining non-recursive defined functions

transformation for introducing destructors

transform exists x. y = s x & p[x] into is-s y && p[select-s-0 y]

note: would apply to backends CVC4 and smbc, at least?

Parse error on TIP input

Whenever I try to use a TIP file as input i get a parse error. For example, if I run nunchaku --input tip cfg5_unambig.smt2 on this file from the TIP-benchmarks repository, I get the error:

could not parse cfg5_unambig.smt2: parsing error: expected statement at file 'cfg5_unambig.smt2': line 1, col 1 to 17

This seems to happen for any TIP I give as input.

add an `include` statement

with a path relative to the current file.

in skolem, ignore `let`-bound variables

README references missing files

The README references the file docs/examples/first_order.nun, which is not actually present in the repository.

I think either the missing file should be added, or, the README should be updated to correctly reference the (I assume identical?) file here.

approximate quantifiers in `ElimData` on incomplete types

For a datatype τ approximated in an incomplete way but with finite cardinal (say, 16), we need to encode ∀x:τ. p x into card(α_τ) ≥ 16 ∧ ∀x:α_τ. p x.

See: bugs/quantifier_kodkod.nun

keep definition of alpha_u even when unused

La définition de a_u est virée au moment de la monorphisation.

Error: elim_infinite:
universal type u does not have an approximation

test.txt

Can't find nun-file after using nunchaku in isabelle

Hello,

I have used nunchaku on an isabelle lemma, and I get an error because of an ill-formed term (probably caused by using an own datatype, more specifically a domain). It also shows the directory where the .nun-file (nunchaku2832584.nun) of the process should be.
However, I couldn't find the file there, so my question is how to get the information of the file, as it could be helpful for using nunchaku for such a datatype.

Thanks in advance.

cleanup duplicates in models

both:

sets of equations that occur multiple times (after merging)
variables bound in several equations

CVC4 1.7 support

I tried to run nunchaku on nunchaku-problems/tests/first_order.nun:

nunchaku tests/first_order.nun

but got

Error: in the interface to CVC4: non first-order list

Output of cvc4 --version:

This is CVC4 version 1.7-prerelease [git master 9168f325]
compiled with GCC version 8.1.1 20180712 (Red Hat 8.1.1-5)
on Oct 10 2018 01:26:41

With CVC4 version 1.5 it worked, though.

cardinality bounds

syntax (attribute?) to specify bounds on cardinality of uninterpreted types
Use fmf.card in CVC4

The meaning of (fmf.card t n) is "the cardinality of the type of t is at most n.

Could nunchaku be used for Coq (which allows empty types)?

As pointed out by @blanchette, nunchaku is based on a theory where all types are inhabited.
In Coq, however, empty types are allowed, and it's more than a theoretical curiosity required to define False, but it's actually a feature I use in my work: I'm writing a compiler which does not yet support function calls, while my colleague is writing a separation logic framework for its input language which already supports function calls, and in order to share the same ASTs, we generalize the AST over function names, and he instantiates them with string, while I instantiate them with the empty type, as illustrated in this minimized example:

Require Import Coq.Lists.List. Import ListNotations.

Inductive stmt{varname funcname: Type}: Type :=
| SAdd(res arg1 arg2: varname)
| SSet(x: varname)(v: nat)
| SCall(f: funcname)(res: varname)(args: list varname).

Definition collect_varnames{V F}(s: stmt (varname:=V) (funcname:=F)): list V :=
  match s with
  | SAdd res arg1 arg2 => [res; arg1; arg2]
  | SSet x v => [x]
  | SCall f res args => res :: args
  end.

Inductive empty_funcname: Type := .

Definition simple_stmt := stmt (varname:=nat) (funcname:=empty_funcname).

Lemma number_of_vars_bound: forall (s: simple_stmt),
    length (collect_varnames s) <= 2.
Proof.
  (* call counterexample generator here *)

Here, a counterexample generator should report a counterexample for the SAdd case (because 3 <= 2 does not hold), and it should not report a counterexample based on the SCall case, because that's impossible for simple_stmt.

Now I wonder wether/how this could be encoded in nunchaku.

data empty_funcname := .

doesn't work because it results in a parsing error.

val empty_funcname: type.

axiom forall (fn: empty_funcname). false.

doesn't work either because nunchaku considers it UNSAT.

Given that a Coq plugin for nunchaku was started, I guess it was assumed that this could be made working somehow? If so, how?

I'm not restricted to sound and complete solutions, I'd also be interested in "practical" solutions 😉

Unclear error if backend solver is not installed

E.g.

nunchaku --solvers cvc4 foo.nun

if cvc4 is not installed.

Edit: more precisely, should fail if no solver is installed among these which are specified.

warning for partially defined functions

in Elim_multi_eqns, emit warning if some cases are undefined (and print corresponding input pattern)

support partially applied builtins

A syntax for builtins such as = or =>, seen as functions:

either something like @= A a
or force the user to write fun x. a = x

support for dependent types

no universes
must be accepted in typechecking (without inference for term parameters)
do the encoding (hatt 2016)

CVC4 bug NodeValue

bug.txt

Type error : remaining meta-variable

Fatal error: exception invalid term ?ty_b/73: remaining meta-variable

bug.txt

better parsing of CVC4

Need to deal with composite types (like (list foo)) when looking for domains. Take mangling in consideration (separate with _).

precedence-based printers

Use a numeric precedence for every construct (including each builtin) and give to every printer the current precedence, to put exactly the correct amount of parenthesis.

nunchaku on continuous functions on codatatypes in Isabelle

Hello,

I have another question about the Isabelle plugin. Maybe you can answer it, even though the plugin is not ready yet, or @blanchette if he is currently working on the plugin.

While testing nunchaku on a codatatype, I found out that it doesn't work on continuous functions (or functions which use continuous functions). Instead, it gives the following error: Error: env: undefined ID 'anon_fun_7' (code 1).
We looked for possible ways to define ID in the documentation (in this section: https://nunchaku-inria.github.io/nunchaku/0.6/nunchaku/Nunchaku_core/Env/index.html) and, unfortunately, didn't have any idea how to do it. Maybe you know if that was the right approach, or what we may actually have to do in order to make nunchaku work for continuous function.

Thank you in advance.

improve cardinality analysis for kodkod

see bugs/better_card_kodkod.nun

Type error without line number

Version: nunchaku 0.5.1 70e5101

The following example

val K : type.
val V : type.

data tuple := pair K V.

data list :=
  nil
| cons tuple list.

data option :=
  None
| Some V.

rec put : list -> K -> V -> list :=
  fun l k v. cons (pair k v) l.

# correct version:
# rec put : list -> K -> V -> list :=
#   put = (fun l k v. cons (pair k v) l).

yields

Error: type error:
  unification error: incompatible types:
  trying to unify `list -> K -> V -> list` and `prop`

It would be good if a line number was reported.

opam installation failed for OCaml 4.03.0

On an opam switch with OCaml 4.03.0, I ran

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

but I got the following error:

nunchaku is now git-pinned to https://github.com/nunchaku-inria/nunchaku.git#master

[nunchaku] https://github.com/nunchaku-inria/nunchaku.git#master updated

nunchaku needs to be installed.
The following actions will be performed:
  - install jbuilder   1.0+beta20                       [required by nunchaku]
  - install ocamlbuild 0.12.0                           [required by menhir, sequence]
  - install result     1.3                              [required by containers]
  - install uchar      0.0.2                            [required by containers]
  - install sequence   0.5.4                            [required by nunchaku]
  - install menhir     20180905                         [required by nunchaku]
  - install containers 2.3                              [required by nunchaku]
  - install nunchaku   0.5.1*    
===== 8 to install =====
Do you want to continue ? [Y/n] y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[default] https://opam.ocaml.org/1.2.2/archives/containers.2.3+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/jbuilder.1.0+beta20+opam.tar.gz downloaded
[ocamlbuild] Archive in cache
[nunchaku] https://github.com/nunchaku-inria/nunchaku.git#master already up-to-date
[default] https://opam.ocaml.org/1.2.2/archives/menhir.20180905+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/result.1.3+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/sequence.0.5.4+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/uchar.0.0.2+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-> installed ocamlbuild.0.12.0
-> installed uchar.0.0.2
-> installed jbuilder.1.0+beta20
-> installed result.1.3
-> installed sequence.0.5.4
-> installed containers.2.3
-> installed menhir.20180905
[ERROR] The compilation of nunchaku failed at "jbuilder build -p nunchaku -j 4".

#=== ERROR while installing nunchaku.0.5.1 ====================================#
# opam-version 1.2.2
# os           linux
# command      jbuilder build -p nunchaku -j 4
# path         /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1
# compiler     4.03.0
# exit-code    1
# env-file     /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1/nunchaku-25480-722625.env
# stdout-file  /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1/nunchaku-25480-722625.out
# stderr-file  /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1/nunchaku-25480-722625.err
### stderr ###
# Warning: the token SECTION is unused.
# [...]
# (cd _build/default && /home/sam/.opam/smtcoq_cvc4/bin/ocamlc.opt -w -40 -w +a-4-42-44-48-50-58-32-60-29@8 -color always -g -bin-annot -I src/core/.nunchaku_core.objs -I /home/sam/.opam/smtcoq_cvc4/lib/bytes -I /home/sam/.opam/smtcoq_cvc4/lib/containers -I /home/sam/.opam/smtcoq_cvc4/lib/containers/data -I /home/sam/.opam/smtcoq_cvc4/lib/containers/monomorphic -I /home/sam/.opam/smtcoq_cvc4/lib/num -I /home/sam/.opam/smtcoq_cvc4/lib/ocaml/threads -I /home/sam/.opam/smtcoq_cvc4/lib/result -I /home/sam/.opam/smtcoq_cvc4/lib/sequence -I /home/sam/.opam/smtcoq_cvc4/lib/uchar -no-alias-deps -open Nunchaku_core -o src/core/.nunchaku_core.objs/nunchaku_core__FO.cmo -c -impl src/core/FO.ml)
# File "src/core/FO.ml", line 318, characters 7-26:
# Error: Unbound value Sequence.flat_map_l
# Hint: Did you mean flat_map?
#     ocamlopt src/core/.nunchaku_core.objs/nunchaku_core__FO.{cmx,o} (exit 2)
# (cd _build/default && /home/sam/.opam/smtcoq_cvc4/bin/ocamlopt.opt -w -40 -w +a-4-42-44-48-50-58-32-60-29@8 -color always -g -bin-annot -O2 -I src/core/.nunchaku_core.objs -I /home/sam/.opam/smtcoq_cvc4/lib/bytes -I /home/sam/.opam/smtcoq_cvc4/lib/containers -I /home/sam/.opam/smtcoq_cvc4/lib/containers/data -I /home/sam/.opam/smtcoq_cvc4/lib/containers/monomorphic -I /home/sam/.opam/smtcoq_cvc4/lib/num -I /home/sam/.opam/smtcoq_cvc4/lib/ocaml/threads -I /home/sam/.opam/smtcoq_cvc4/lib/result -I /home/sam/.opam/smtcoq_cvc4/lib/sequence -I /home/sam/.opam/smtcoq_cvc4/lib/uchar -no-alias-deps -open Nunchaku_core -o src/core/.nunchaku_core.objs/nunchaku_core__FO.cmx -c -impl src/core/FO.ml)
# File "src/core/FO.ml", line 318, characters 7-26:
# Error: Unbound value Sequence.flat_map_l
# Hint: Did you mean flat_map?



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install nunchaku 0.5.1
The following changes have been performed
  - install containers 2.3       
  - install jbuilder   1.0+beta20
  - install menhir     20180905  
  - install ocamlbuild 0.12.0    
  - install result     1.3       
  - install sequence   0.5.4     
  - install uchar      0.0.2     

=-=- containers.2.3 installed successfully =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
=> Containers 2.3 is a small release with a few more functions in existing modules,
   some bugfixes, and many performance improvements.

   Changelog: https://github.com/c-cube/ocaml-containers/blob/2.3/CHANGELOG.adoc
[NOTE] Pinning command successful, but your installed packages may be out of sync.

The former state can be restored with:
    opam switch import "~/.opam/smtcoq_cvc4/backup/state-20180912230059.export"

This is surprising because according to this travis build, OCaml 4.03.0 should be supported.

Any advice on how to get this to build?

fix release 0.4 for win32

file is a symlink, need to upload the .exe itself

modify syntax for `spec`

spec head : pi a. list a -> a and tail : pi a. list a -> list a := <axioms>
instead of separate declarations.

Should only have to modify parser + type inference.

bug: match cases need type arguments

We need to be able to rename constructors (such as Some) upon monomorphization.

Alarm clock 14

Error message "Alarm clock 14" when timeout.

bug.txt

Better error message when pred not well funded.

Error message when pred not well funded.

File "src/transformations/Unroll.ml", line 111, characters 8-14: Assertion failed

Eg.

val u : type.
val setminus : u -> u -> u.
pred is_in : u -> u -> prop :=
forall a b x. ((is_in a x) && (~(is_in b x))) => (is_in (setminus a b) x).
goal exists x a b. ~(is_in a x) && (is_in b x).

nunchaku-inria / nunchaku Goto Github PK

nunchaku's Introduction

Nunchaku

Basic Usage

Contact

Documentation

Build/Install

Released versions

Opam

Manually

License

Input/Output/Solvers

How to make a release

nunchaku's People

Stargazers

Watchers

Forkers

nunchaku's Issues

Recommend Projects

Recommend Topics

Recommend Org