why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-04-08T13:40:36Zhttps://gitlab.inria.fr/why3/why3/-/issues/567wish: provide monomorphic, clonable modules for references and arrays2021-04-08T13:40:36ZMARCHE Claudewish: provide monomorphic, clonable modules for references and arraysPolymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexample features are essentially broken in presence of polymorphism. In the current implementation of "jessie3" in collaboration with TIS, I had to suggest to avoid producing WhyML code involving polymorphism, both for proving efficiency and counterexamples. Recently, Quentin came up with the following trivial example
```
use int.Int
use array.Array
let update a i (v:int)
requires { 0 <= i < length a }
ensures { a[i] = v }
= a[i] <- v
```
which is easily solved by Alt-Ergo, but not by CVC4 nor Z3.
I suggest:
- to provide monomorphic clonable versions of ref.Ref and array.Array in the stdlib, which would allow to program without polymorphism unless needed elsewhere
- to review to current support of polymorphism in Why3: are the drivers appropriate? it seems that in Why3 0.xx, using modules ref.Ref or array.Array was *not* enforcing polymorphism in the generated tasks, but since Why3 1.0 tasks generated are always polymorphic because of type `ref'mk 'a` or `array'mk 'a`Polymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexample features are essentially broken in presence of polymorphism. In the current implementation of "jessie3" in collaboration with TIS, I had to suggest to avoid producing WhyML code involving polymorphism, both for proving efficiency and counterexamples. Recently, Quentin came up with the following trivial example
```
use int.Int
use array.Array
let update a i (v:int)
requires { 0 <= i < length a }
ensures { a[i] = v }
= a[i] <- v
```
which is easily solved by Alt-Ergo, but not by CVC4 nor Z3.
I suggest:
- to provide monomorphic clonable versions of ref.Ref and array.Array in the stdlib, which would allow to program without polymorphism unless needed elsewhere
- to review to current support of polymorphism in Why3: are the drivers appropriate? it seems that in Why3 0.xx, using modules ref.Ref or array.Array was *not* enforcing polymorphism in the generated tasks, but since Why3 1.0 tasks generated are always polymorphic because of type `ref'mk 'a` or `array'mk 'a`1.5.0https://gitlab.inria.fr/why3/why3/-/issues/550Add support for recent versions of Z32021-02-11T10:34:46ZMARCHE ClaudeAdd support for recent versions of Z3Add support for Z3 4.8.7 to 4.8.10 :
https://github.com/Z3Prover/z3/releasesAdd support for Z3 4.8.7 to 4.8.10 :
https://github.com/Z3Prover/z3/releases1.4.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/535Add srem and sdiv operations on bitvectors2021-02-06T11:44:28ZGuillaume CluzelAdd srem and sdiv operations on bitvectorsIt looks like there exists, in both CVC4 and Z3, operations on 2's complement signed integer for division (BVSDIV) and modulo on bitvectors. For modulo BVSMOD follows the semantic of the modulo in programming language.
I would appreciate if these two operations could be added in the theory of bitvector in addition to the `urem` and `udiv` operation that are already existing.It looks like there exists, in both CVC4 and Z3, operations on 2's complement signed integer for division (BVSDIV) and modulo on bitvectors. For modulo BVSMOD follows the semantic of the modulo in programming language.
I would appreciate if these two operations could be added in the theory of bitvector in addition to the `urem` and `udiv` operation that are already existing.1.4.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/533Add support for Alt-Ergo 2.4.02021-02-05T13:46:12ZMARCHE ClaudeAdd support for Alt-Ergo 2.4.0Beware that the command line options have changed.
https://discuss.ocaml.org/t/ann-alt-ergo-2-4-0-release/7134Beware that the command line options have changed.
https://discuss.ocaml.org/t/ann-alt-ergo-2-4-0-release/71341.4.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/512Useless axioms for min and max in SMT output2020-11-05T09:39:14ZJohannes KanigUseless axioms for min and max in SMT outputThe axioms in theory `int.MinMax` should not be used by SMT solvers. So the following snippet should be added to `smt-libv2.gen`, similar to what is already done for `real.MinMax`:
```
theory int.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
```
We have already put this in our Why3 repo, @bbecker could you take care of merging this in the INRIA repo if Why3 team agrees? The commit in AdaCore repo is 6cf79069ee96d8162c8d63031b21772f021f0b7b.The axioms in theory `int.MinMax` should not be used by SMT solvers. So the following snippet should be added to `smt-libv2.gen`, similar to what is already done for `real.MinMax`:
```
theory int.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
```
We have already put this in our Why3 repo, @bbecker could you take care of merging this in the INRIA repo if Why3 team agrees? The commit in AdaCore repo is 6cf79069ee96d8162c8d63031b21772f021f0b7b.Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/502support for CVC4 1.82021-02-12T16:36:52ZMARCHE Claudesupport for CVC4 1.81.4.0Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/491Invalid XML file generated for Isabelle 2019 for a VC in micro-C2020-10-28T15:33:40ZFrédéric BoulangerInvalid XML file generated for Isabelle 2019 for a VC in micro-CI have a micro-C file [pgcd.c](/uploads/85f32884f8142024e0fe378ec1cf65f8/pgcd.c) with two lemmas for provings the VCs. When trying to prove lemma gcd_ab in Isabelle 2019, I get errors in the .thy file [pgcd_Pgcd_gcd_ab_2.thy](/uploads/a42f56c45fb388386292b6384e8d7a5a/pgcd_Pgcd_gcd_ab_2.thy) that come from an issue in the generated .xml file [pgcd_Pgcd_gcd_ab_2.xml](/uploads/c34c9ddb97018f0b35b6fc1a5d4c9462/pgcd_Pgcd_gcd_ab_2.xml).
The first error (in the .xml file) gives:
Malformed global fact "pgcd_Pgcd_gcd_ab_2.gcd_ab.facts.mixfix_lblsmnrbqtspec(1)" Illegal fixed variable: "'a"I have a micro-C file [pgcd.c](/uploads/85f32884f8142024e0fe378ec1cf65f8/pgcd.c) with two lemmas for provings the VCs. When trying to prove lemma gcd_ab in Isabelle 2019, I get errors in the .thy file [pgcd_Pgcd_gcd_ab_2.thy](/uploads/a42f56c45fb388386292b6384e8d7a5a/pgcd_Pgcd_gcd_ab_2.thy) that come from an issue in the generated .xml file [pgcd_Pgcd_gcd_ab_2.xml](/uploads/c34c9ddb97018f0b35b6fc1a5d4c9462/pgcd_Pgcd_gcd_ab_2.xml).
The first error (in the .xml file) gives:
Malformed global fact "pgcd_Pgcd_gcd_ab_2.gcd_ab.facts.mixfix_lblsmnrbqtspec(1)" Illegal fixed variable: "'a"https://gitlab.inria.fr/why3/why3/-/issues/461CVC4 1.7 hates predefined symbols2020-03-18T17:47:34ZGuillaume MelquiondCVC4 1.7 hates predefined symbols```
function exp int: int
goal G: true
```
```
$ bin/why3 prove -P CVC4,1.7 foo.mlw
foo.mlw Top G: HighFailure (0.02s)
Prover exit status: killed by signal 11
Prover output:
(error "Parse Error: /tmp/why_72ac78_foo-T-G.smt2:9.16: Symbol `exp' is shadowing a theory function symbol
(declare-fun exp (Int) Int)
^
")
CVC4 suffered a segfault.
Offending address is 0x8
Looks like a NULL pointer was dereferenced.
```
The `exp` case is fixed by 290333ce, but there might be other cases.```
function exp int: int
goal G: true
```
```
$ bin/why3 prove -P CVC4,1.7 foo.mlw
foo.mlw Top G: HighFailure (0.02s)
Prover exit status: killed by signal 11
Prover output:
(error "Parse Error: /tmp/why_72ac78_foo-T-G.smt2:9.16: Symbol `exp' is shadowing a theory function symbol
(declare-fun exp (Int) Int)
^
")
CVC4 suffered a segfault.
Offending address is 0x8
Looks like a NULL pointer was dereferenced.
```
The `exp` case is fixed by 290333ce, but there might be other cases.1.3.1MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/450Wrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC42020-03-04T09:36:51ZGhost UserWrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC4On the following example:
```why3
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
```
The following command fails:
```
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover exit status: exited with status 1
Prover output:
(error "expecting an integer subterm")
...
```
Apparently, `in_range` is transformed into `abs 0.0` which requires an int. Note that on Why3 1.2.1, the file contains a definition `abs1` for real numbers, but the generated goal uses `abs` (leading to the same error). If `in_range` is used in a lemma or an axiom, the same bug happens.On the following example:
```why3
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
```
The following command fails:
```
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover exit status: exited with status 1
Prover output:
(error "expecting an integer subterm")
...
```
Apparently, `in_range` is transformed into `abs 0.0` which requires an int. Note that on Why3 1.2.1, the file contains a definition `abs1` for real numbers, but the generated goal uses `abs` (leading to the same error). If `in_range` is used in a lemma or an axiom, the same bug happens.1.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/438Add floating-point support by Alt-Ergo FPA and mathsat2021-02-05T13:44:35ZMARCHE ClaudeAdd floating-point support by Alt-Ergo FPA and mathsatTitle says all. For mathsat see also #437Title says all. For mathsat see also #4371.5.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/437SMT support for solvers which do not support quantifiers2021-01-22T14:24:00ZMARCHE ClaudeSMT support for solvers which do not support quantifiersWe should support SMT solvers even if they do not support quantifiers, like Yices 2 and mathsat.
This can be done by applying a transformation that removes quantified hypotheses, like it is done already for Colibri I think (see !112)We should support SMT solvers even if they do not support quantifiers, like Yices 2 and mathsat.
This can be done by applying a transformation that removes quantified hypotheses, like it is done already for Colibri I think (see !112)1.5.0François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/404Theory "string.String" is unsound2019-11-12T10:12:27ZGuillaume MelquiondTheory "string.String" is unsoundBut more likely, it should really be disabled for some provers:
```
use string.String
goal g : false
```
```
$ bin/why3 prove foo.mlw -P Z3,4.6.0
foo.mlw Top g: Valid (0.04s, 24607 steps)
```But more likely, it should really be disabled for some provers:
```
use string.String
goal g : false
```
```
$ bin/why3 prove foo.mlw -P Z3,4.6.0
foo.mlw Top g: Valid (0.04s, 24607 steps)
```1.3.0Claudio Belo LourencoClaudio Belo Lourencohttps://gitlab.inria.fr/why3/why3/-/issues/386Support for Z3 4.8.5 and 4.8.62019-10-25T09:45:23ZDAILLER SylvainSupport for Z3 4.8.5 and 4.8.61.2.1MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/362overly generic logics declaration causes slowdown of cvc4 proof2020-10-28T13:06:53ZJohannes Kanigoverly generic logics declaration causes slowdown of cvc4 proofFlorian had identified a long time ago an issue where cvc4 would take
much longer to prove a given VC if a non-linear arithmetic was specified
compared to a linear one. See this ticket and the example in the ticket:
https://github.com/CVC4/CVC4/issues/1276
On my machine, there is a factor of 10 (0.6s vs 6s) between UFBVDTLIRA
and UFBVDTNIRA when using cvc4 on the example in the issue.
We were wondering if Why3 could be more precise, e.g. detecting when
only linear operators are used. Given the potentially large speedups it
seems worthwhile. The other idea mentioned in the TN to specify
--inst-when-strict-interleave isn't an option for us.Florian had identified a long time ago an issue where cvc4 would take
much longer to prove a given VC if a non-linear arithmetic was specified
compared to a linear one. See this ticket and the example in the ticket:
https://github.com/CVC4/CVC4/issues/1276
On my machine, there is a factor of 10 (0.6s vs 6s) between UFBVDTLIRA
and UFBVDTNIRA when using cvc4 on the example in the issue.
We were wondering if Why3 could be more precise, e.g. detecting when
only linear operators are used. Given the potentially large speedups it
seems worthwhile. The other idea mentioned in the TN to specify
--inst-when-strict-interleave isn't an option for us.https://gitlab.inria.fr/why3/why3/-/issues/272CVC4 for smtlib 2.62021-01-22T14:47:23ZDAILLER SylvainCVC4 for smtlib 2.6Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```1.5.0https://gitlab.inria.fr/why3/why3/-/issues/271Add support for Vampire (SMT-LIB2 input)2020-02-12T08:02:25ZGuillaume MelquiondAdd support for Vampire (SMT-LIB2 input)1.3.0Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/268possible improvements in SMT-LIB driver2019-04-11T15:12:46ZMARCHE Claudepossible improvements in SMT-LIB driverAdaCore is using the following additional mappings in drivers for CVC4. We should try to evaluate if these are interesting for improvement proof automation in our bench
```
theory real.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove allprops
end
```
[EDIT]
```
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- 1 (to_int (- 1.0 %1)))"
remove allprops
end
```
AdaCore is using the following additional mappings in drivers for CVC4. We should try to evaluate if these are interesting for improvement proof automation in our bench
```
theory real.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove allprops
end
```
[EDIT]
```
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- 1 (to_int (- 1.0 %1)))"
remove allprops
end
```
DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/263Removing Inline_trivial2019-02-12T16:55:13ZDAILLER SylvainRemoving Inline_trivialHello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.Hello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/250Support Z3 4.8.1 and 4.8.32019-02-07T10:26:18ZMARCHE ClaudeSupport Z3 4.8.1 and 4.8.3feature wish: add support for Z3 4.8.1 (released oct 16) and 4.8.3 (released nov 20)feature wish: add support for Z3 4.8.1 (released oct 16) and 4.8.3 (released nov 20)1.2.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/242Division and comparison in SMT and Alt-ergo2021-02-11T09:40:57ZFrançois BobotDivision and comparison in SMT and Alt-ergoIt seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because `/.` is defined with `inv` and `*.`, and because `*.` is said monotone.It seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because `/.` is defined with `inv` and `*.`, and because `*.` is said monotone.