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
