Dafny times out

Feb 11, 2013 at 7:33 AM

Hi --- The following code seems to put Z3 into a hard loop (both on my machine and at rise4fun.) Even stranger, if the unused predicate definitions are removed, it does not loop: instead it gives an assertion violation.

function Id<T> (z: T): T {z}

predicate UpSequence (ss: seq<int>, us: seq<int>, l: int)
{ |ss|>=|us|==l && forall i,j:: 0<=i<j<l ==> 0<=us[i]<us[j]<|ss| && ss[us[i]]<ss[us[j]]}

predicate isLongestUpSequence (ss: seq<int>, us: seq<int>, l: int)
{ UpSequence(ss,us,l) && (forall vs,m:: UpSequence(ss,vs,m) ==> m<=l) }

predicate isLeastLastUpSequence (ss: seq<int>, us: seq<int>, l: int, s: int)
{ l>=1 && UpSequence(ss,us,l) && 0<=us[l-1]<|ss| && ss[us[l-1]]==s &&
(forall vs,t:: UpSequence(ss,vs,l) && 0<=vs[l-1]<|ss| && ss[vs[l-1]]==t ==> s<=t)

method TestPredicates () {
var ss: seq<int>, us: seq<int>, l: int, s: int;
assert (forall i,j:: 0<=i<j<|us|<=|ss| ==> 0<=us[Id(i)]<us[Id(j)]<|ss| && ss[us[Id(i)]]<ss[us[Id(j)]])
    ==> forall i,j:: 0<=i<j<|us|<=|ss|+1 ==> 0<=us[Id(i)]<us[Id(j)]<|ss| && ss[us[Id(i)]]<ss[us[Id(j)]];
Feb 13, 2013 at 4:30 PM
Time-outs are often caused by matching loops, but I don't see such an issue in this example. (I did not try the Z3AxiomProfiler to try to figure out why Z3 gets stuck.)

As you mentioned, by removing the unused predicates, the time-out no longer happens (and instead you get an error message that complains about not being able to prove the assertion). I also found the same if you remove the uses of Id in this example. Thus, what I said about fickleness in this discussion may be useful. As I said there, it would be good not to rely on the /r option, but it perfectly fine to routinely use something like /vcsMaxKeepGoingSplits:2 (which does in fact work for this example).

By the way, in many cases, these sorts of issues happen while your program and specifications are incorrect (that is, you might get time-out instead of an error report then), but once you've corrected the program and specifications, the time-outs no longer happen and Z3 quickly finds the proof. Since Z3 is usually very fast on Dafny programs, I usually never let Z3 run more than a small number of seconds (maybe 10, which you can specify with /timeLimit). If it doesn't verify within that limit, I know I want to change something in the program (and I hope I will figure out what, since Z3's output didn't help).


PS. I'm wondering if I have done the wrong thing by mentioning the Id trick before. Usually (and also in this example), there is enough structure (not counting built-in operators like + and < and ==>) in the body of quantifiers that you don't need to use something like Id to produce triggers.
Feb 14, 2013 at 11:48 PM
Hi Rustan ---

Further on time-outs: I have a short program (below) that verifies; but if you un-comment an assumption, it loops. Thus it -is- correct (since an assumption can only make it "correcter"), but I cannot proceed any further with this approach unless I can experiment with the assumption.

--- So is there any way I can get guidance (from Dafny or Z3) about why it is looping, and how to avoid that?

The background is that the assertion I need has a very particular conjunct in its antecedent, an existential quantifier, and I will eventually need to prove that with a lemma. (It has an inductive assertion, basically that if there is a solution to something at all, then there is a least one.) But --in the spirit of your remarks about lemmas-- I would like to make sure that the lemma is what I need before I go and prove it. Hence the assumption --- but, because of the loop, I am stuck.

So --- to summarise --- the code below verifies in rise4fun; but if you remove the comment symbols, it times out.


function LastElement(bs: seq<int>): int requires bs!=[]; { bs[|bs|-1] }
function Front(bs: seq<int>): seq<int> requires bs!=[]; { bs[..|bs|-1] }
function LastValue(bs: seq<int>, cs: seq<int>): int requires cs!=[] && selectsUpsequence(bs,cs);
{ bs[LastElement(cs)] }

predicate isStrictlySorted (bs: seq<int>)
{ forall i,j:: 0<=i<j<|bs| ==> bs[i]<bs[j] }

predicate selectsSubsequence (bs: seq<int>, cs: seq<int>)
{ isStrictlySorted(cs) && forall i:: 0<=i<|cs| ==> 0<=cs[i]<|bs| }

predicate selectsUpsequence (bs: seq<int>, cs: seq<int>)
{ selectsSubsequence(bs,cs) && forall i,j:: 0<=i<j<|cs| ==> bs[cs[i]]<bs[cs[j]] }

predicate selectsLowestUpsequence (bs: seq<int>, cs: seq<int>, c: int)
{ selectsUpsequence(bs,cs) &&
(cs!=[] ==> c==bs[LastElement(cs)]
          &&  forall ds:: selectsUpsequence(bs,ds)
          &&  |cs|==|ds|
          ==> c<=bs[LastElement(ds)]) }
method Test() {/*
assume forall bs,cs,ds,d::
       (exists ds,d:: |ds|==|cs| && selectsLowestUpsequence(bs,ds,d))

assert forall bs,n,cs,c,ds,d:: 0<=n && n+1<|bs| &&
       selectsLowestUpsequence(bs[..n],cs,c) &&
       selectsLowestUpsequence(bs[..n],ds,d) &&
       |ds|==|cs|+1 &&
       |cs|>=1 &&
     (exists es,e::
         selectsLowestUpsequence(bs[..n+1],es,e) &&
         |es|==|ds| &&
         (c<=LastValue(bs[..n+1],Front(es))<bs[n] ==> c<bs[n]) // Pointless truth supplies a trigger?
     ) &&
       if (c<bs[n]<=d) then selectsLowestUpsequence(bs[..n+1],cs+[n],bs[n])
       else if bs[n]<=c then selectsLowestUpsequence(bs[..n+1],ds,d)
       else if d<bs[n] then selectsLowestUpsequence(bs[..n+1],ds,d)
       else false