1

Closed

get-value side effect

description

Hi Leo,

Just wanted to let you know that (get-value …) has a side effect, because it permanently enables model completion. So,

(get-value (x))
(get-model)

Will report a model that is different from

; (get-value (x))
(get-model)

Because model::eval at model.cpp:131 permanently sets model completion to true.

This is not really a problem, but could potentially confuse users a bit. So, doesn’t really need a fix, I just wanted to point this out to you in case you’d like to change the behavior. I guess we could work around it by creating a temporary copy of the model before it is completed…

Cheers,
Christoph
Closed Jun 7, 2013 at 1:41 AM by leodemoura
This is not a bug.

comments

leodemoura wrote Jun 7, 2013 at 1:36 AM

Creating a temporary model is not an option since some users make thousands of calls to get-value, and the model can be quite big.
It is also not correct to erase the value assigned to x by model completion. If we do that, we can get a different value when we invoke "(get-value (x))" again.

leodemoura wrote Jun 7, 2013 at 1:41 AM

This is not a bug. This is the intended behavior.
Here is an example:

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (> x 0))
(check-sat)
(get-model)
(eval y)
(eval z)
(get-value (y))
(eval z)
(get-model)