[YICES-HELP] Re: Yices behavior

[Bruno Dutertre]

david.cok at kodak.com wrote:
> Bruno,
> 
> Suppose I assert some statements to Yices, call (check) and get back a 
> satisfying model.
> 
> Then I assert some additional statements which are known not to change the 
> satisfiability.  For example they are of the form   X == expr where X is a 
> new variable.
> 
> And then I call (check) again.
> 
> I'd like to be sure that I will get back the same satisfying assignment, 
> augmented with the new variables.  Will I?  Or does (check) restart the 
> whole search for an assignment over again?
> 

Yices will search for a new assignment and there's no guarantee
that the new assignment will agree the previous one on the old variables.
Because of the way models are constructed, the new assertion (X == expr) may
interfere with the previous model and cause Yices to change the assignment.

Here's an example:

(define f::(-> int int))
(define x::int)
(define y::int)
(assert (/= (f x) (f y)))
(check)
sat
(= x 1)
(= y 3)
(= (f 1) 2)
(= (f 3) 4)

(define z::int)
(assert (= z (f (+ 1 x))))
(check)
sat
(= x 1)
(= y 4)
(= z 6)
(= (f 1) 3)
(= (f 4) 5)
(= (f 2) 6)


Bruno