search

doyougnu / VSmt

Variational Satisfiability Solver
3 stars 0 forks source link

Remove duplicates in variational models #5

Closed doyougnu closed 3 years ago

doyougnu commented 4 years ago

Consider this propositions:

bChc "AA" (bRef "Aleft") (bRef "Aright") ||| bRef "one" &&& bRef "two"

In this proposition the value of one is effectively variational because it depends on the result of confguring the AA choice, whereas two is plain because it is independent of the choice completely. Thus we would expect that would result model would show a variational context for one but a constant for two. Yet we are returned this:

model := 
Aleft   -->   (ite ~AA (False :: Bool) ite AA (False :: Bool) Undefined)
Aright   -->   ite ~AA (True :: Bool) Undefined
two   -->   (ite ~AA (True :: Bool) ite AA (True :: Bool) Undefined)
one   -->   (ite ~AA (False :: Bool) ite AA (True :: Bool) Undefined)
AA   -->   (ite ~AA (False :: Bool) ite AA (False :: Bool) Undefined)

Sat_Model := 
(~AA or AA)

where both one and two have results in a context even though two's value never changes, which is correct, it is constant. Thus, during construction of the result we should check to ensure we are not adding duplicate values.

doyougnu commented 4 years ago

This can't be fixed until sbv resets bindings created in the assertion levels. That is, if I resetAssertion then all bindings in the stack are still maintained, including those defined inside a push->foo->pop call.

doyougnu commented 3 years ago

This is fixed as of 78a13fee796fdef5691cb39c87a0a75e570a3511 in the move from sbv to z3 only. However there is a subtle difference in z3 semantics. Z3 get-model returns a minimal model, thus if you have a ||| b ||| c ||| only one variable will be returned in the model as the other's won't even be checked. This is default behavior from z3 (I checked rise4fun) and so I won't change it. Note that this makes variational models much much smaller and can lead to some un-intuitive resutls:

consider:

bChc "AA" (bRef "a") (bRef "b" ||| bRef "c") ||| bRef "d"

with this formula the returned model is:

=: Model :=
a   -->   (ite AA (True) Undefined)
b   -->   (ite ~AA (True) Undefined)

=: Sat_Model :=
(~AA or AA)

which is missing bindings for c and d but is a perfectly reasonable model to be returned by the definition of satisfiability.