src/theory/sets/kinds

   1 # kinds                                                               -*- sh -*-
   2 #
   3 # For documentation on this file format, please refer to
   4 # src/theory/builtin/kinds.
   5 #
   6
   7 theory THEORY_SETS \
   8     ::CVC4::theory::sets::TheorySets \
   9     "theory/sets/theory_sets.h"
  10 typechecker "theory/sets/theory_sets_type_rules.h"
  11 rewriter ::CVC4::theory::sets::TheorySetsRewriter \
  12     "theory/sets/theory_sets_rewriter.h"
  13
  14 properties parametric
  15 properties check propagate presolve
  16
  17 # constants
  18 constant EMPTYSET \
  19     ::CVC4::EmptySet \
  20     ::CVC4::EmptySetHashFunction \
  21     "expr/emptyset.h" \
  22     "the empty set constant; payload is an instance of the CVC4::EmptySet class"
  23
  24 # the type
  25 operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
  26 cardinality SET_TYPE \
  27     "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
  28     "theory/sets/theory_sets_type_rules.h"
  29 well-founded SET_TYPE \
  30     "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
  31     "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
  32     "theory/sets/theory_sets_type_rules.h"
  33 enumerator SET_TYPE \
  34     "::CVC4::theory::sets::SetEnumerator" \
  35     "theory/sets/theory_sets_type_enumerator.h"
  36
  37 # operators
  38 operator UNION         2  "set union"
  39 operator INTERSECTION  2  "set intersection"
  40 operator SETMINUS      2  "set subtraction"
  41 operator SUBSET        2  "subset predicate; first parameter a subset of second"
  42 operator MEMBER        2  "set membership predicate; first parameter a member of second"
  43 operator SINGLETON     1  "the set of the single element given as a parameter"
  44 operator INSERT        2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
  45 operator CARD          1  "set cardinality operator"
  46
  47 typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
  48 typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
  49 typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
  50 typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
  51 typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
  52 typerule SINGLETON      ::CVC4::theory::sets::SingletonTypeRule
  53 typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
  54 typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
  55 typerule CARD           ::CVC4::theory::sets::CardTypeRule
  56
  57 construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
  58 construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
  59 construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
  60 construle SINGLETON     ::CVC4::theory::sets::SingletonTypeRule
  61 construle INSERT        ::CVC4::theory::sets::InsertTypeRule
  62 construle CARD          ::CVC4::theory::sets::CardTypeRule
  63
  64 endtheory