Parsing error on unary clause

[rainoftime]

Hi, for the following formula,

(set-logic QF_LRA)
(declare-const v0 Bool)
(assert (or v0))
(check-sat)

smtinterpol commit 0610d35 issues a warning/error

success
success
(error "xx.smt2:3:9: Undeclared function symbol (or Bool)")

The input satisfies the SMT-Lib2 standard. Unary clauses can also exist in real cases.

[rainoftime]

@tanjaschindler Can you check this?

[jhoenicke]

@rainoftime, The smt-lib standard defines left-assoc operators only for at least two arguments. This is on page 34 of the SMT-LIB language document. For n > 2, (or f1 ... fn) is an abbreviation, but for n=1, (or f1) is not defined. Instead one has to write simply f1.

Some other solvers may accept this syntax, but it doesn't follow the standard.

[rainoftime]

@jhoenicke Thanks for the explanation! Is it possible to support this? It could be useful for some practical scenarios. For example, as shown in the pseudocode below, when the user creates a disjunction of several assertions, he/she does not need to check the size of somewhrere or list.

list = []
for i in somewhere:
   list.append(i)
assert = to_or(list)
solver.add(assert)

[jhoenicke]

we have a small wrapper function

buildor(list) {
  if (list.size() == 0) {
    return term("false");
  } else if (list.size() == 1) {
    return list.getFirst();
  } else {
    return term("or", list);
  }
}

[rainoftime]

Do you mean there is a wrapper as the level of Java API? Is there any plan for supporting the extension in SMT-lib frontend? A user may interact SMTInterpol with the SMT-Lib. E.g., https://github.com/LeventErkok/sbv

[jhoenicke]

As this is not allowed by the SMT-LIB standard, I would say that an SMT library that creates such output is buggy. If the library can create such terms it should internally fix them by converting unary or/and/+/..., before creating the text representation for SMT-LIB.

Allowing these unary operators is problematic, as the question is for which operators we should allow this. Cleary unary "-" is a different operator. What about unary "/", unary "=>", which are also declared as :left-assoc or :right-assoc? I would like to strictly follow the SMT-LIB standard here.