Dear Jean-Christophe,
Thank you for your message. I will read the paper that you pointed out.
I have however a modified driver for Z3 that when used proves one of the
results in the presence of set.Set, and it proves both if set.Set is
removed. I will try to send the modified driver tomorrow. The time taken
to prove both results in absence of set.Set is about 0.01s. This has
worked for us in the past as well, but not after changing to the latest
version of why3. It seems that set.Set has been significantly refactored
in recent versions.
Best regards,
Viorel
On 1/5/2021 5:48 PM, Jean-Christophe Filliatre wrote:
Dear Viorel,
Those goals involving a lot of nonlinear arithmetic are giving trouble
to SMT solvers. I could not verify your two goals on my machine either,
even without importing set.Set.
You might be interested in this paper by Guillaume and Raphaël. It
precisely describes a technique to solve such nonlinear arithmetic goals
in Why3:
https://www.lri.fr/~melquion/doc/18-ijcar-article.pdf
Best regards,
--
Jean-Christophe
On 01/01/2021 09:14 PM, Viorel Preoteasa wrote:
Hello,
I have the following theory:
theory TestPower
use real.RealInfix
use real.PowerInt
use real.Square
(*
use set.Set
*)
constant _a: real
constant _b: real
goal task6:
(((power (_a +. _b) 6)) =
power _a 6)
+. ((6.0 *. (power _a 5)) *. _b))
+. ((15.0 *. (power _a 4)) *. (sqr _b)))
+. ((2E+1 *. (power _a 3)) *. (power _b 3)))
+. ((15.0 *. (sqr _a)) *. (power _b 4)))
+. ((6.0 *. _a) *. (power _b 5)))
+. (power _b 6
goal task9:
(((power (_a +. _b) 9)) =
(((power _a 9)
+. ((9.0 *. _a) *. (power _b 8)))
+. ((36.0 *. (sqr _a)) *. (power _b 7)))
+. ((84.0 *. (power _a 3)) *. (power _b 6)))
+. ((126.0 *. (power _a 4)) *. (power _b 5)))
+. ((126.0 *. (power _a 5)) *. (power _b 4)))
+. ((84.0 *. (power _a 6)) *. (power _b 3)))
+. ((36.0 *. (power _a 7)) *. (sqr _b)))
+. ((9.0 *. (power _a 8)) *. (power _b 1)))
+. (power _b 9
end
This cannot be proved by the default z3 driver, but it can be proved by
a customized driver which removes many results. However, even the
customized driver fails if the theory includes set.Set. Then task6 times
out, and task9 succeeds. I tried to add to the custom driver the
following declaration:
theory set.Set
remove allprops
end
But it does not help. The problem is that I cannot avoid having set.Set
in the theory, but I want to disable it somehow from the driver.
I am using why3 1.3.3 and z3 4.8.9. I know that this version of z3 is
not supported, but the latest supported version seems to have a bug
related to powers.
Any help would by appreciated.
Best regards,
Viorel Preoteasa
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
