[YICES] Extrange result

Bruno Dutertre bruno at csl.sri.com
Fri Oct 7 10:52:20 PDT 2011

cristia at cifasis-conicet.gov.ar wrote:
> Hi!
> I've posted a similar email on September 19 but I had no answer.
> I tried to reduce the problem as much as I can so it would be easier for
> you to help me.
> I'm using Yices 1.0.29 on a Linux machine.
> When I load the following script:
> (define-type MDATA)
> (define mdp::int)
> (define memp::(tuple (-> int bool) (-> int MDATA)))
> (define r1::(-> int bool) (lambda (i::int) (and (<= 1 i) (<= i 5))))
> (assert (= r1 (select memp 1)))
> (set-evidence! true)
> (check)
> I get the following result:
> sat
> (= (mk-tuple (select memp 1) (select memp 2)) memp)
> Is this a complete model? I thought the model should include a "value" for
> memp, but the value given by Yices is "circular", isn't it? According to
> the assertion "(select memp 1)" should be equal to r1 which in turn is
> true of [1..5]. Shouldn't the model include what is the value of "(select
> memp 1)" on [1..5]?
> Is there something I'm not getting right?


You're expecting too much. If you have a function f defined over
the integers, then it's not clear how Yices would display what
(f x) is for all x, because there are infinitely many 'x's.
In your example, Yices can't figure out that (r1 x) is true
for finitely many 'x's and false otherwise. So in general,
Yices can't display the value of a function in the model, if
that function is defined by a lambda expression.


More information about the YICES mailing list