[YICES-HELP] Re: Yices behavior
bruno at csl.sri.com
Mon Aug 11 11:08:12 PDT 2008
david.cok at kodak.com wrote:
> 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))
(assert (/= (f x) (f y)))
(= x 1)
(= y 3)
(= (f 1) 2)
(= (f 3) 4)
(assert (= z (f (+ 1 x))))
(= x 1)
(= y 4)
(= z 6)
(= (f 1) 3)
(= (f 4) 5)
(= (f 2) 6)
More information about the YICES-HELP