Re: [Why3-club] A predicate that cannot be proved by why3

[Jean-Christophe Filliatre]

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
> 
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] A predicate that cannot be proved by why3

[Ziqing Luo]

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
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club