diff options
| author | Paul Meng <baolmeng@gmail.com> | 2017-04-20 14:04:24 -0500 |
|---|---|---|
| committer | Paul Meng <baolmeng@gmail.com> | 2017-04-20 14:04:24 -0500 |
| commit | 7152d6136fc8bd4701d9440ba3eee6bb7bf3a16c (patch) | |
| tree | 9012cc085fcde111d5a0609441415cdbb1a7b460 /src/theory/sets/kinds | |
| parent | c110fa8d07b5650c671b99797c17822e757bc52f (diff) | |
Support for relational operators identity and join image
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index cfe7eb632..34fef7d64 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -50,6 +50,8 @@ operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" operator TCLOSURE 1 "set transitive closure" +operator JOIN_IMAGE 2 "set join image" +operator IDEN 1 "set identity" typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -67,6 +69,8 @@ typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +typerule JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule +typerule IDEN ::CVC4::theory::sets::RelIdenTypeRule construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -80,5 +84,7 @@ construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +construle JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule +construle IDEN ::CVC4::theory::sets::RelIdenTypeRule endtheory |