Hi, Sorry, I forgot to mention that I used why3 v0.88.3 with theorem provers: z3(v4.6.0), alt-ergo (v2.0.0) and cvc4 (v1.5).
I also tried z3(4.4.0) but it still doesn't work for me. Thanks for telling me that provers have problems with "existential" goals. Ziqing Luo University of Delaware On Sat, Feb 10, 2018 at 5:57 PM, <why3-club-requ...@lists.gforge.inria.fr> wrote: > Send Why3-club mailing list submissions to > why3-club@lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > or, via email, send a message with subject or body 'help' to > why3-club-requ...@lists.gforge.inria.fr > > You can reach the person managing the list at > why3-club-ow...@lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Why3-club digest..." > > > Today's Topics: > > 1. A predicate that cannot be proved by why3 (Ziqing Luo) > 2. Re: A predicate that cannot be proved by why3 > (Jean-Christophe Filliatre) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 10 Feb 2018 09:42:26 +0800 > From: Ziqing Luo <ziq...@udel.edu> > To: why3-club@lists.gforge.inria.fr > Subject: [Why3-club] A predicate that cannot be proved by why3 > Message-ID: > <CAJsrCF2eMibSpZPXDttpCQ4C0OY1ce4d3D7TnVoWfujGSQ1hAQ@mail. > gmail.com> > Content-Type: text/plain; charset="utf-8" > > Dear Why3 Club, > > I have a why3 script that I think is relatively simple but why3 cannot > prove it. I wander if I did anything wrong. > > *constant X : (map int int)* > > *context: > * > > * X[4] = X[6] && X[5] = X[6] && X[6] < X[7] > * > > *predicate: > * > > * exists k : int. 0 <= k && k <= 3 && not(X[k+4] = X[k+5])* > > It is obvious that there exists such a k = 2. If I modify the predicate a > lilltle bit to : > > *predicate: > * > > * exists k : int. 0 <= k && k <= 3 && k = 2 && not(X[k+4] = X[k+5])* > > > why3 then has no problem to prove it. So I'm confused that why why3 cannot > prove the original case. > > Thanks, > Ziqing Luo > University of Delaware > > The following is the whole why3 script: > > theory Why3Query_408 > > use import int.Int > > use import map.Map > > constant _X : (map int int) > > > (* > > > > > > context: > > > X[4] = X[6] > > > X[5] = X[6] > > > X[6] < X[7] > > > > > > predicate: > > > exists k : int. 0 <= k && k <= 3 && not(X[k+4] = X[k+5]) > > > > > > *) > > > predicate context = (((0) = ((get _X (4)) + ((-1) * (get _X (6))))) > && > > ((0) = ((get _X (5)) + ((-1) * (get _X (6))))) > && > > (((get _X (6)) + ((-1) * (get _X (7))) + (1)) > <= (0))) > > > goal G0: context -> ((exists k : int. (((k + (-3)) <= (0)) && ((0) > <= k) && > > (not ((0) = ((get _X (k + (4))) + ((-1) * > (get _X (k + (5))))))))) ) > > > end > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://lists.gforge.inria.fr/pipermail/why3-club/ > attachments/20180210/8bf8edcd/attachment-0001.html> > > ------------------------------ > > Message: 2 > Date: Sat, 10 Feb 2018 10:57:42 +0100 > From: Jean-Christophe Filliatre <jean-christophe.fillia...@lri.fr> > To: why3-club@lists.gforge.inria.fr > Subject: Re: [Why3-club] A predicate that cannot be proved by why3 > Message-ID: <5a7ec216.6030...@lri.fr> > Content-Type: text/plain; charset=utf-8 > > Hi, > > When you say "why3 cannot prove it", it means "the provers installed on > my machine and called from Why3 cannot prove it". So listing the provers > you've tried on this example would be helpful. > > Indeed, ATPs have trouble proving existential goals, especially when > combined with arithmetic (SMT solvers struggle with arithmetic triggers, > and TPTP provers sometimes simply do not have support for arithmetic). > > But at least Z3 4.4.0 was able to prove your goal on my machine. > > Hope this helps, > -- > Jean-Christophe > > > On 10/02/2018 02:42, Ziqing Luo wrote: > > Dear Why3 Club, > > > > I have a why3 script that I think is relatively simple but why3 cannot > > prove it. I wander if I did anything wrong. > > > > *constant X : (map int int)* > > > > *context: > > * > > > > * X[4] = X[6] && X[5] = X[6] && X[6] < X[7] > > * > > > > *predicate: > > * > > > > * exists k : int. 0 <= k && k <= 3 && not(X[k+4] = X[k+5])* > > > > > > It is obvious that there exists such a k = 2. If I modify the > > predicate a lilltle bit to : > > > > *predicate: > > * > > > > * exists k : int. 0 <= k && k <= 3 && k = 2 && not(X[k+4] = X[k+5])* > > > > * > > * > > > > why3 then has no problem to prove it. So I'm confused that why why3 > > cannot prove the original case. > > > > Thanks, > > Ziqing Luo > > University of Delaware > > > > The following is the whole why3 script: > > > > theoryWhy3Query_408 > > > > useimport int.Int > > > > useimport map.Map > > > > constant_X : (mapintint) > > > > > > (* > > > > > > > > > > > > context: > > > > > > X[4] = X[6] > > > > > > X[5] = X[6] > > > > > > X[6] < X[7] > > > > > > > > > > > > predicate: > > > > > > exists k : int. 0 <= k && k <= 3 && not(X[k+4] = X[k+5]) > > > > > > > > > > > > *) > > > > > > predicatecontext = (((0) = ((get _X (4)) + ((-1) * (get _X > (6))))) && > > > > ((0) = ((get _X (5)) + ((-1) * (get _X > (6))))) && > > > > (((get _X (6)) + ((-1) * (get _X (7))) + (1)) > > <= (0))) > > > > > > goalG0: context -> ((existsk : int. (((k + (-3)) <= (0)) && ((0) > > <= k) && > > > > (not ((0) = ((get _X (k + (4))) + ((-1) > > * (get _X (k + (5))))))))) ) > > > > > > end > > > > > > > > > > > > _______________________________________________ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ------------------------------ > > End of Why3-club Digest, Vol 86, Issue 4 > **************************************** >
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
