Question

The equality operator in SMT-LIB generally requires, unsurprisingly, that its operands be of the same type. For example, this is an error:

(set-logic QF_LIRA)
(declare-fun a () Bool)
(declare-fun b () Real)
(assert (= a b))
(check-sat)

However, I expected this to be likewise an error:

(set-logic QF_LIRA)
(declare-fun a () Int)
(declare-fun b () Real)
(assert (= a b))
(check-sat)

But Yices and Z3 both accept it without complaint.

What am I missing?

Answer 1

Strictly speaking, such mixing-and-matching is not allowed by SMTLib. (See page 37 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf, where it clearly states = must take two arguments of the same sort.)

However, most solvers are "lenient" in their processing; i.e., they introduce coercions when they think it "makes sense." I personally find that problematic: Coercions are hardly ever useful (especially in a language that s meant to be generated by tools in general), and sometimes they can hide bugs where the user wanted to say one thing but said the wrong thing, and the system somehow assigned a meaning to it. (You can compare this to mixing and matching of arithmetic with different types in many programming languages. But I digress.)

Having said that, cvc5 does better, if you ask it to:

$ cvc5 --strict-parsing a.smt2
(error "Parse Error: a.smt2:4.15: Subexpressions must have the same type:
Equation: (= a b)
Type 1: Int
Type 2: Real
")

Note that I explicitly had to pass --strict-parsing argument, as it also inserts the coercion without that flag.

My personal opinion is that they should all do this sort of strict parsing; but the state of the affairs is that most solvers introduce these coercions leading to confusion at best, and hiding bugs at worst.

友情链接