CODEWITHSUNDEEP
smtcvc4
dde
dde

Reputation: 192

Why is CVC4 product operator not applying to sets?

I am tinkering with CVC4 support for sets and relations and expected to be able to use the product operator to build the Cartesian product of two sets. However, this operator only applies to relations.

This is a sample input fed to 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)))

This results in the following error message:

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

I then found that CVC4 expects the product operator to apply to sets of tuples. The following is processed successfully:

(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 could consider here that a set as the set of 1-tuples with elements of that set.

Upvotes: 1

Views: 61

Answers (1)

Vladi
Vladi

Reputation: 1

This is just how the syntax works in CVC4. I am using it for work, and we specifically deal with the Theory of Sets. For most of the operations on sets with Finite relations, CVC4 expects to have tuples.

This link may be helpful: https://cvc4.github.io/sets-and-relations So, the operations with Finite Sets generally can be operated without tuples, while finite relations need tuples.

Also, I found this paper helps to understand the theory behind the implementation of set in CVC4: https://homepage.cs.uiowa.edu/~tinelli/papers/MenEtAl-CADE-17.pdf

Upvotes: 0

Related Questions