Многоэлементное вычитание в Z3

Question

Я использую Z3 для решения проблемы, требующей вычитания, и столкнулся с тем фактом, что вычитание в Z3 допускает несколько аргументов. Это кажется мне странным, поскольку вычитание не является ассоциативной операцией. Это видно из следующего сценария:

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= a (- 1 2 3)))
(assert (= b (- 1 (- 2 3))))
(assert (= c (- (- 1 2) 3)))

, который удовлетворяется a=c=-4 и b=2 Так что это означает, что вычитание в Z3 определяется путем применения двоичной операции слева направо?

Answer 1

Это на самом деле особенность SMT-Lib, z3 просто реализует это. Смотрите здесь: http://smtlib.cs.uiowa.edu/theories-Ints.shtml

И да, если у вас есть несколько элементов, он просто ассоциируется слева. То есть:

 (- 1 2 3 4)

означает то же самое, что и:

 (- (- (- 1 2) 3) 4)

Это действительно сбивает с толку, поскольку мы хотим сделать только для ассоциативных операторов, где скобки не имеют значения (например, + и *), но SMTLib либерален в этом смысле. Это не означает, что вычитание является ассоциативным в SMT-Lib, это просто означает, что если у вас есть несколько аргументов, он анализируется, как описано выше. Надеюсь, это поможет!