Closed cheshire closed 8 years ago
I also strongly suspect that the code for function values in model was never actually run, as we don't actually use functions of boolean sort in cpachecker.
Oh wait, sorry, I was wrong, the visitor extracts all variables and UFs from the asserted formulas first... OK that should be easy to implement than.
Should be also more efficient, if we do that only in the iterator, so the model creation will not have this cost.
SMTInterpol's
Model
interface only exposes anevaluate
method, and does not support iterating over model values. The current code somewhat arbitrary decides to populate the dict with the values of the boolean constraints which were pushed to the solver stack. I think we should:UnsupportedOperationException
for now, as it is dead-easy to get the values for those boolean terms usingevaluate
, and such an incomplete model might be misleading (null-s should be "don't-matter's", not "everything else")