summaryrefslogtreecommitdiff
path: root/src/theory/sets/kinds
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-03-07 11:17:34 -0600
committerajreynol <andrew.j.reynolds@gmail.com>2017-03-07 11:17:34 -0600
commitab68adfc44049598ee79a3c8b4379694d786d9aa (patch)
tree1609ecda726c535466b4f7501d4dba5b72409ba9 /src/theory/sets/kinds
parent105cae4ed94f0ce13b0525a348b29d2fc7d5af72 (diff)
More fixes for printing/parsing sets, fix kind name.
Diffstat (limited to 'src/theory/sets/kinds')
-rw-r--r--src/theory/sets/kinds6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 53905e47f..ab0ca3428 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -43,7 +43,7 @@ operator MEMBER 2 "set membership predicate; first parameter a member of
operator SINGLETON 1 "the set of the single element given as a parameter"
operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
operator CARD 1 "set cardinality operator"
-operator COMPLIMENT 1 "set compliment (with respect to finite universe)"
+operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
operator JOIN 2 "set join"
operator PRODUCT 2 "set cartesian product"
@@ -59,7 +59,7 @@ typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
typerule INSERT ::CVC4::theory::sets::InsertTypeRule
typerule CARD ::CVC4::theory::sets::CardTypeRule
-typerule COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule
+typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule
typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
@@ -74,7 +74,7 @@ construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule
construle INSERT ::CVC4::theory::sets::InsertTypeRule
construle CARD ::CVC4::theory::sets::CardTypeRule
-construle COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule
+construle COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule
construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback