This project is read-only.

\exists quantifier

Aug 9, 2012 at 2:43 AM
Edited Aug 9, 2012 at 2:47 AM

Hi,

I am tring to verify some case with \exists quantifier. But I always get the error infor. I even get the error message for the simplest case. What can I do to handle this?

I tried to add some triggers like: \match_ulong(t) to get rid of the warnings. But it doesn't work for error message.

Thanks very much!

#include<vcc.h>

void test(){
    _(assert \exists unsigned t; \true)
}

/*
=== VCC started. ===
Command Line: "C:\Program Files (x86)\Microsoft Research\Vcc\Binaries\vcc.exe"  /bvd /loc:"c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h":4  "c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h" /p:/D_MBCS  /clpath:"C:\PROGRAM FILES (X86)\MICROSOFT VISUAL STUDIO 10.0\VC\bin\cl.exe"

c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h(4,14) : warning VC9121: failed to infer triggers for '\exists unsigned t; \true)'
Verification of test failed. [0.64]
Prover warning: failed to find a pattern for quantifier (quantifier id: testh.4:14)
c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h(4,14) : error VC9500: Assertion '\exists unsigned t; \true)' did not verify.
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)

=== Verification failed. ===
*/
Aug 9, 2012 at 2:24 PM
Edited Aug 9, 2012 at 2:25 PM

Hi Hare,

I don't have any answers to offer you right now, but you (and any devs looking into this) may be interested in the follwing facts:

  • The following succeeds.

    #include<vcc.h>
    
    void test(){
        _(assert \exists \integer t; \true)
    }
  • The following fails.

    #include<vcc.h>
    
    void test(){
    _(assert \exists \natural t; \true)
    } 
    
  • The following succeeds (with the usual trigger warning).

    #include<vcc.h>
    
    void test(){
        _(assert \exists \integer t; 0 <= t ==> \true)
    } 

In the meantime, I would advise using \integer variables in everything spec, and casting where appropriate. If you need the fact that it's non-negative, you can easily switch between \natural and \integer with a side-condition, although you'll have to add explicit casts where appropriate.

Cheers,

Francois

Aug 9, 2012 at 5:43 PM

Hi Francois,

Thanks very much!

Shu Cheng

Aug 9, 2012 at 6:58 PM
Edited Aug 9, 2012 at 7:01 PM

Hi Francois,

When I go back to my case, it seems \integer also can't help. For instance,

#include<vcc.h>

void test(){
    _(assert \exists \integer t; t == 5)
}

void test1(){
    int x = 25;
    
    _(assert \exists \integer t; t == 5 ==> x == t * t)
    _(assert \exists \integer t; x == t * t)
    _(assert \exists \integer t; t == 5)
}

void test2(){
    int x = 25;

    _(assert \forall \integer t; t == 5 ==> x == t * t)
    _(assert \exists \integer t; t == 5 ==> x == t * t)
}
In these cases, all assertion with \exists are fail to verify. It seems the prover can't solve quantifier \exists correctly.
Is this an bug with vcc or prover? If not, what should I do to avoid these problems.
Thanks very much!
Sep 11, 2012 at 5:39 PM
Edited Sep 11, 2012 at 5:43 PM

It's important to understand how VCC (and more generally, SMT solvers) treat quantifiers. When VCC needs to prove a formula, it first negates and Skolemizes it, and tries to prove \false. It will have two kinds of formulas to use: ground formulas and formulas with quantifiers. It reasons only with the ground formulas, using (essentially) logic and linear arithmetic. A quantified formula is used only by matching its trigger(s) using ground subterms in its formulas to obtain a ground instance, and adding this instance to the collection of ground formulas.

So, for example, if you want to prove (\exists \integer t; t == 5), it will actually have the formula

(\forall \integer t; t != 5)

which it will use to try to prove \false. Even if you had given the existential formula a trigger, to obtain a formula like

(\forall \integer t; {\match_long(t)} t != 5)

it will still fail to prove this because it has no ground term of the form \match_long(a) with which to instantiate the formula. To get it to trigger, you have to provide a ground instance, for example as follows (which verifies):

#include <vcc.h>

_(def \bool match(\integer t) { return \true; })

void test(){
    _(assert match(5))
    _(assert \exists \integer t; {match(t)} t == 5)
}

void test1(){
    int x = 25;
    _(assert match(5))
    _(assert \exists \integer t; {match(t)} t == 5 ==> x == t * t)
    _(assert \exists \integer t; {match(t)} x == t * t)
    _(assert \exists \integer t; {match(t)} t == 5)
}

void test2(){
    int x = 25;
    _(assert match(5))
    _(assert \forall \integer t; {match(t)} t == 5 ==> x == t * t)
    _(assert \exists \integer t; {match(t)} t == 5 ==> x == t * t)
}