Support for get-assignment

[bclement-ocp]

Dolmen accepts the following files ga.smt2 and ga.rsmt2 without complaining:

; ga.smt2
(set-option :produce-models true)
(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-const p Bool)
(assert (=> (! (not p) :named not_p) (= p false)))
(check-sat)
(get-model)
(get-assignment)

; ga.rsmt2
sat
(
  (define-fun p () Bool true)
)
((not_p true))

with

$ dolmen ga.smt2 -r ga.rsmt2 --check-model true 

$

This is surprising because the assignment is incorrect: not_p is defined as (not p) and can't be true when p is true. However Dolmen clearly knows some stuff about not_p because if I use the following for ga.rsmt2:

sat
(
  (define-fun p () Bool true)
  (define-fun not_p () Bool true)
)
((not_p true))

I get the following error:

File "ga.rsmt2", line 5, character 2-33:
5 |   (define-fun not_p () Bool true)
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error Trying to define a model value for symbol `not_p`,
      but the symbol was already implicitly introduced in the term at line 5, character 12-36

Either correctly parsing (get-assignment) or having an error/warning that it is not supported would be less confusing.

[Gbury]

So, the current situation, is that the response to the (get-assignment) is simply never read and checked.

In this very particular instance, where the (get-assignment) follows a (get-model), dolmen could indeed verify that the values agree, however, it cannot be done for all (get-assignment) statements in general, in which case we'd need to emit a warning/error.

There are thus two solutions: 1) as said above, try and check (get-assignment) when it is possible (and emit a warning/error otherwise), or 2) simply always emit a warning stating that these are not checked.

I won't have much time to work on that unfortunately, so I can do option 2 (but I don't know when), and if you want/need optin 1), you'll probably need to open a PR.

[bclement-ocp]

I opened this issue mostly for tracking purposes, I don't need a fix for it currently.

Long term I think option 2 is acceptable; it would remove the ambiguity/surprises (especially since dolmen does writes warning for invalid models but does not seem to produce any output for valid models). Option 1 would be useful but I don't see myself implementing it in the near future either.