nunchaku-inria / nunchaku Goto Github PK
View Code? Open in Web Editor NEWModel finder for higher-order logic
Home Page: https://nunchaku-inria.github.io/nunchaku/
License: BSD 2-Clause "Simplified" License
Model finder for higher-order logic
Home Page: https://nunchaku-inria.github.io/nunchaku/
License: BSD 2-Clause "Simplified" License
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?
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.
in encoding of functions, add the prototype (perhaps with a flag to enable/disable it).
with a path relative to the current file.
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 π
Need to deal with composite types (like (list foo)
) when looking for domains. Take mangling in consideration (separate with _
).
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.
Error message "Alarm clock 14" when timeout.
fmf.card
in CVC4The meaning of (fmf.card t n) is "the cardinality of the type of t is at most n.
We need to be able to rename constructors (such as Some
) upon monomorphization.
in Elim_multi_eqns
, emit warning if some cases are undefined (and print corresponding input pattern)
A syntax for builtins such as =
or =>
, seen as functions:
@= A a
fun x. a = x
Versions:
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?
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).
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.
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.
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
transformation for inlining non-recursive defined functions
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.
see bugs/better_card_kodkod.nun
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.
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.
file is a symlink, need to upload the .exe itself
both:
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.
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.
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.
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?
Fatal error: exception invalid term ?ty_b/73
: remaining meta-variable
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.
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.
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.
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
π Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. πππ
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google β€οΈ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.