src/theory/bags/theory_bags_type_rules.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Bags theory type rules.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
  19 #define CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
  20
  21 #include "expr/node.h"
  22
  23 namespace cvc5 {
  24
  25 class NodeManager;
  26 class TypeNode;
  27
  28 namespace theory {
  29 namespace bags {
  30
  31 /**
  32  * Type rule for binary operators (bag.union_max, bag.union_disjoint,
  33  * bag.inter_min bag.difference_subtract, bag.difference_remove) to check
  34  * if the two arguments are bags of the same sort.
  35  */
  36 struct BinaryOperatorTypeRule
  37 {
  38   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
  39   static bool computeIsConst(NodeManager* nodeManager, TNode n);
  40 }; /* struct BinaryOperatorTypeRule */
  41
  42 /**
  43  * Type rule for binary operator bag.subbag to check if the two arguments are
  44  * bags of the same sort.
  45  */
  46 struct SubBagTypeRule
  47 {
  48   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
  49 }; /* struct SubBagTypeRule */
  50
  51 /**
  52  * Type rule for binary operator bag.count to check the sort of the first
  53  * argument matches the element sort of the given bag.
  54  */
  55 struct CountTypeRule
  56 {
  57   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
  58 }; /* struct CountTypeRule */
  59
  60 /**
  61  * Type rule for binary operator bag.member to check the sort of the first
  62  * argument matches the element sort of the given bag.
  63  */
  64 struct MemberTypeRule
  65 {
  66   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
  67 };
  68
  69 /**
  70  * Type rule for bag.duplicate_removal to check the argument is of a bag.
  71  */
  72 struct DuplicateRemovalTypeRule
  73 {
  74   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
  75 }; /* struct DuplicateRemovalTypeRule */
  76
  77 /**
  78  * Type rule for (bag op e) operator to check the sort of e matches the sort
  79  * stored in op.
  80  */
  81 struct BagMakeTypeRule
  82 {
  83   static TypeNode computeType(NodeManager* nm, TNode n, bool check);
  84   static bool computeIsConst(NodeManager* nodeManager, TNode n);
  85 }; /* struct BagMakeTypeRule */
  86
  87 /**
  88  * Type rule for (bag.is_singleton B) to check the argument B is a bag.
  89  */
  90 struct IsSingletonTypeRule
  91 {
  92   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
  93 }; /* struct IsSingletonTypeRule */
  94
  95 /**
  96  * Type rule for (as bag.empty (Bag T)) where T is a type
  97  */
  98 struct EmptyBagTypeRule
  99 {
 100   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 101 }; /* struct EmptyBagTypeRule */
 102
 103 /**
 104  * Type rule for (bag.card B) to check the argument B is a bag.
 105  */
 106 struct CardTypeRule
 107 {
 108   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 109 }; /* struct CardTypeRule */
 110
 111 /**
 112  * Type rule for (bag.choose B) to check the argument B is a bag.
 113  */
 114 struct ChooseTypeRule
 115 {
 116   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 117 }; /* struct ChooseTypeRule */
 118
 119 /**
 120  * Type rule for (bag.from_set ..) to check the argument is of a set.
 121  */
 122 struct FromSetTypeRule
 123 {
 124   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 125 }; /* struct FromSetTypeRule */
 126
 127 /**
 128  * Type rule for (bag.to_set ..) to check the argument is of a bag.
 129  */
 130 struct ToSetTypeRule
 131 {
 132   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 133 }; /* struct ToSetTypeRule */
 134
 135 /**
 136  * Type rule for (bag.map f B) to make sure f is a unary function of type
 137  * (-> T1 T2) where B is a bag of type (Bag T1)
 138  */
 139 struct BagMapTypeRule
 140 {
 141   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 142 }; /* struct BagMapTypeRule */
 143
 144 /**
 145  * Type rule for (bag.filter p B) to make sure p is a unary predicate of type
 146  * (-> T Bool) where B is a bag of type (Bag T)
 147  */
 148 struct BagFilterTypeRule
 149 {
 150   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 151 }; /* struct BagFilterTypeRule */
 152
 153 /**
 154  * Type rule for (bag.fold f t A) to make sure f is a binary operation of type
 155  * (-> T1 T2 T2), t of type T2, and B is a bag of type (Bag T1)
 156  */
 157 struct BagFoldTypeRule
 158 {
 159   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 160 }; /* struct BagFoldTypeRule */
 161
 162 struct BagsProperties
 163 {
 164   static Cardinality computeCardinality(TypeNode type);
 165
 166   static bool isWellFounded(TypeNode type);
 167
 168   static Node mkGroundTerm(TypeNode type);
 169 }; /* struct BagsProperties */
 170
 171 }  // namespace bags
 172 }  // namespace theory
 173 }  // namespace cvc5
 174
 175 #endif /* CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */