Почему оператор продукта CVC4 не применяется к наборам?

Я работаю с поддержкой наборов и отношений CVC4 и ожидаю, что смогу использовать оператор product для построения декартова произведения двух наборов. Однако этот оператор применяется только к отношениям.

Это пример ввода, подаваемого на CVC4:

(set-logic ALL_SUPPORTED)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun es1 () (Set S1))
(declare-fun es2 () (Set S2))
(declare-fun es1s2 () (Set (Tuple S1 S2)))
(assert (= es1s2 (product es1 es2)))

Это приводит к следующему сообщению об ошибке:

(error " Relational operator operates on non-relations (sets of tuples)")

Затем я обнаружил, что CVC4 ожидает, что оператор product будет применяться к наборам кортежей. Успешно обрабатывается следующее:

(set-logic ALL_SUPPORTED)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun e1 () (Set (Tuple S1)))
(declare-fun e2 () (Set (Tuple S2)))
(declare-fun es1s2 () (Set (Tuple S1 S2)))
(assert (= es1s2 (product e1 e2)))

CVC4 может рассматривать здесь набор как набор 1-кортежей с элементами этого набора.

• Есть ли какая-то фундаментальная проблема, которая препятствует такому поведению?