Почему оператор продукта CVC4 не применяется к сетам? - PullRequest
Новая
       28

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

1 голос
/ 02 мая 2019

Я возился с поддержкой 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 кортежей с элементами этого набора.

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