Model validator: failed unittest and Real values.

[jhoenicke]

The unit test ("QF_LIRA", "LCTES_smtopt.smt2", "model.LCTES_smtopt.cvc4-broken.smt2") now reports VALID instead of UNKNOWN. The problem seems to be that pySMT has automatic Int to Real casts beyond what the SMT-LIB standard allows.

We may also want to make more unit-tests, e.g.

(define-fun x () Real (- 1))                           ; invalid in QF_LIRA, model value in QF_LRA
(define-fun x () Real (- 1.0))                         ; model value in QF_LIRA, valid in QF_LRA
(define-fun x () Real (/ (- 1) 2))                     ; valid in QF_LIRA (automatic cast), model value in QF_LRA
(define-fun x () Real (/ (- (to_real 1)) (to_real 2))) ; model value in QF_LIRA, not valid in QF_LRA
(define-fun x () Real (/ (- 1.0) 2.0))                 ; valid in QF_LIRA and QF_LRA (but not model value)
(define-fun x () Real (- (/ 1 2)))                     ; valid in QF_LIRA and QF_LRA (but not model value)
(define-fun x () Real (- 0.5))                         ; valid in QF_LIRA and QF_LRA (but not model value)

If you interpret the standard strictly, the constants should be defined by model values, not arbitrary valid expressions. But IMHO we shouldn't be too strict here, especially since the model values vary from logic to logic and that is not very intuitive.

[jhoenicke]

As I understand it, the new SMT-LIB 3 standard will use (- 1.0) and (/ (- 1) 2) as model values for Reals in all linear logics.

[jhoenicke]

It looks like pySMT currently doesn't do any type-checking on parsing. We would need to add type-checking at least for model defined functions. Also the type-checking needs to be dependent on the logic.

[jhoenicke]

@mikand, thanks for your pull-request. I now added new unit-tests of which a few fail. Would you be willing to help on this?

1. Most importantly, model variables with the same name and different type should be allowed. The model variables must only be accessed by (as @xyz Type), so the type is always clear from the context. I think changing the environment to keep model variables separate from normal symbols should help here (and this also fixes that @xyz must not be used later without as). Invoking = on model variables of different types gives a type error, so it's not really necessary to check the type on equal comparison.
2. There seems to be some automatic Int/Real conversion that goes beyond what SMT-LIB allows. Declaring a real constant in LIRA with a numeral should be a type error. However, one has to be careful as numerals in LRA logic are of type Real and therefore completely fine.
3. In the SMT-LIB parser, builtin functions seem to be always defined, even if the logic doesn't have them. In particular invoking to_real in LRA should be a syntax error.

Point 1. is most important to us, as it flags valid output as invalid.

I added unit tests to the master branch (https://github.com/SMT-COMP/postprocessors/blob/master/model-validation-track/ModelValidator_test.py), the ones that are problematic are commented out at the moment.

[mikand]

@jhoenicke Sure! I'll have a look later today or tomorrow!

[mikand]

@jhoenicke Sorry for the latency, it's a busy period. I made a simple workaround for the point 1 in https://github.com/pysmt/pysmt/pull/691.

For the other two points, when do you need them? They seem harder to address as the current pysmt parser does not really care about the declared logic, it does its best to interpret the input even if it is not 100% SMTLib compatible. We explicitly disregard the possibility of using reserved, interpreted names (e.g. to_real) as variables or UFs in logics other than LIRA even if this is allowed by SMTLib.

[jhoenicke]

Thanks, I will add some comments to the pull request.

As for the other points, I said that this is not so important. I can probably add some simple checks to at least avoid integer constant in real definitions on our model-validator side. It's easy to add additional checks to the validator.

Name clashes like a script defining to_real as an uninterpreted function should not occur in SMT-LIB and even if it did, the scrambler would remove these.