Open bclement-ocp opened 4 months ago
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.
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.
Dolmen accepts the following files
ga.smt2
andga.rsmt2
without complaining:with
This is surprising because the assignment is incorrect:
not_p
is defined as(not p)
and can't betrue
whenp
istrue
. However Dolmen clearly knows some stuff aboutnot_p
because if I use the following forga.rsmt2
:I get the following error:
Either correctly parsing
(get-assignment)
or having an error/warning that it is not supported would be less confusing.