src/theory/bags/bags_utils.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed
   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  * Utility functions for bags.
  14  */
  15
  16 #include <expr/node.h>
  17
  18 #include "cvc5_private.h"
  19
  20 #ifndef CVC5__THEORY__BAGS__UTILS_H
  21 #define CVC5__THEORY__BAGS__UTILS_H
  22
  23 namespace cvc5 {
  24 namespace theory {
  25 namespace bags {
  26
  27 class BagsUtils
  28 {
  29  public:
  30   /**
  31    * @param bagType type of bags
  32    * @param bags a vector of bag nodes
  33    * @return disjoint union of these bags
  34    */
  35   static Node computeDisjointUnion(TypeNode bagType,
  36                                    const std::vector<Node>& bags);
  37   /**
  38    * Returns true if n is considered a to be a (canonical) constant bag value.
  39    * A canonical bag value is one whose AST is:
  40    *   (bag.union_disjoint (bag e1 c1) ...
  41    *      (bag.union_disjoint (bag e_{n-1} c_{n-1}) (bag e_n c_n))))
  42    * where c1 ... cn are positive integers, e1 ... en are constants, and the
  43    * node identifier of these constants are such that: e1 < ... < en.
  44    * Also handles the corner cases of empty bag and bag constructed by bag
  45    */
  46   static bool isConstant(TNode n);
  47   /**
  48    * check whether all children of the given node are constants
  49    */
  50   static bool areChildrenConstants(TNode n);
  51   /**
  52    * evaluate the node n to a constant value.
  53    * As a precondition, children of n should be constants.
  54    */
  55   static Node evaluate(TNode n);
  56
  57   /**
  58    * get the elements along with their multiplicities in a given bag
  59    * @param n a constant node whose type is a bag
  60    * @return a map whose keys are constant elements and values are
  61    * multiplicities
  62    */
  63   static std::map<Node, Rational> getBagElements(TNode n);
  64
  65   /**
  66    * construct a constant bag from constant elements
  67    * @param t the type of the returned bag
  68    * @param elements a map whose keys are constant elements and values are
  69    *        multiplicities
  70    * @return a constant bag that contains
  71    */
  72   static Node constructConstantBagFromElements(
  73       TypeNode t, const std::map<Node, Rational>& elements);
  74
  75   /**
  76    * construct a constant bag from node elements
  77    * @param t the type of the returned bag
  78    * @param elements a map whose keys are constant elements and values are
  79    *        multiplicities
  80    * @return a constant bag that contains
  81    */
  82   static Node constructBagFromElements(TypeNode t,
  83                                        const std::map<Node, Node>& elements);
  84
  85   /**
  86    * @param n has the form (bag.fold f t A) where A is a constant bag
  87    * @return a single value which is the result of the fold
  88    */
  89   static Node evaluateBagFold(TNode n);
  90
  91   /**
  92    * @param n has the form (bag.filter p A) where A is a constant bag
  93    * @return A filtered with predicate p
  94    */
  95   static Node evaluateBagFilter(TNode n);
  96
  97   /**
  98    * @param n of the form (table.product A B) where A , B of types (Bag T1),
  99    * (Bag T2) respectively.
 100    * @param e1 a tuple of type T1 of the form (tuple a1 ... an)
 101    * @param e2 a tuple of type T2 of the form (tuple b1 ... bn)
 102    * @return  (tuple a1 ... an b1 ... bn)
 103    */
 104   static Node constructProductTuple(TNode n, TNode e1, TNode e2);
 105
 106   /**
 107    * @param n of the form (table.product A B) where A, B are constants
 108    * @return the evaluation of the cross product of A B
 109    */
 110   static Node evaluateProduct(TNode n);
 111
 112  private:
 113   /**
 114    * a high order helper function that return a constant bag that is the result
 115    * of (op A B) where op is a binary operator and A, B are constant bags.
 116    * The result is computed from the elements of A (elementsA with iterator itA)
 117    * and elements of B (elementsB with iterator itB).
 118    * The arguments below specify how these iterators are used to generate the
 119    * elements of the result (elements).
 120    * @param n a node whose kind is a binary operator (bag.union_disjoint,
 121    * union_max, intersection_min, difference_subtract, difference_remove) and
 122    * whose children are constant bags.
 123    * @param equal a lambda expression that receives (elements, itA, itB) and
 124    * specify the action that needs to be taken when the elements of itA, itB are
 125    * equal.
 126    * @param less a lambda expression that receives (elements, itA, itB) and
 127    * specify the action that needs to be taken when the element itA is less than
 128    * the element of itB.
 129    * @param greaterOrEqual less a lambda expression that receives (elements,
 130    * itA, itB) and specify the action that needs to be taken when the element
 131    * itA is greater than or equal than the element of itB.
 132    * @param remainderOfA a lambda expression that receives (elements, elementsA,
 133    * itA) and specify the action that needs to be taken to the remaining
 134    * elements of A when all elements of B are visited.
 135    * @param remainderOfB a lambda expression that receives (elements, elementsB,
 136    * itB) and specify the action that needs to be taken to the remaining
 137    * elements of B when all elements of A are visited.
 138    * @return a constant bag that the result of (op n[0] n[1])
 139    */
 140   template <typename T1, typename T2, typename T3, typename T4, typename T5>
 141   static Node evaluateBinaryOperation(const TNode& n,
 142                                       T1&& equal,
 143                                       T2&& less,
 144                                       T3&& greaterOrEqual,
 145                                       T4&& remainderOfA,
 146                                       T5&& remainderOfB);
 147   /**
 148    * evaluate n as follows:
 149    * - (bag a 0) = (as bag.empty T) where T is the type of the original bag
 150    * - (bag a (-c)) = (as bag.empty T) where T is the type the original bag,
 151    *                                and c > 0 is a constant
 152    */
 153   static Node evaluateMakeBag(TNode n);
 154
 155   /**
 156    * returns the multiplicity in a constant bag
 157    * @param n has the form (bag.count x A) where x, A are constants
 158    * @return the multiplicity of element x in bag A.
 159    */
 160   static Node evaluateBagCount(TNode n);
 161
 162   /**
 163    * @param n has the form (bag.duplicate_removal A) where A is a constant bag
 164    * @return a constant bag constructed from the elements in A where each
 165    * element has multiplicity one
 166    */
 167   static Node evaluateDuplicateRemoval(TNode n);
 168
 169   /**
 170    * evaluates union disjoint node such that the returned node is a canonical
 171    * bag that has the form
 172    * (bag.union_disjoint (bag e1 c1) ...
 173    *   (bag.union_disjoint  * (bag e_{n-1} c_{n-1}) (bag e_n c_n)))) where
 174    *   c1... cn are positive integers, e1 ... en are constants, and the node
 175    * identifier of these constants are such that: e1 < ... < en.
 176    * @param n has the form (bag.union_disjoint A B) where A, B are constant bags
 177    * @return the union disjoint of A and B
 178    */
 179   static Node evaluateUnionDisjoint(TNode n);
 180   /**
 181    * @param n has the form (bag.union_max A B) where A, B are constant bags
 182    * @return the union max of A and B
 183    */
 184   static Node evaluateUnionMax(TNode n);
 185   /**
 186    * @param n has the form (bag.inter_min A B) where A, B are constant bags
 187    * @return the intersection min of A and B
 188    */
 189   static Node evaluateIntersectionMin(TNode n);
 190   /**
 191    * @param n has the form (bag.difference_subtract A B) where A, B are constant
 192    * bags
 193    * @return the difference subtract of A and B
 194    */
 195   static Node evaluateDifferenceSubtract(TNode n);
 196   /**
 197    * @param n has the form (bag.difference_remove A B) where A, B are constant
 198    * bags
 199    * @return the difference remove of A and B
 200    */
 201   static Node evaluateDifferenceRemove(TNode n);
 202   /**
 203    * @param n has the form (bag.choose A) where A is a constant bag
 204    * @return x if n has the form (bag.choose (bag x c)). Otherwise an error is
 205    * thrown.
 206    */
 207   static Node evaluateChoose(TNode n);
 208   /**
 209    * @param n has the form (bag.card A) where A is a constant bag
 210    * @return the number of elements in bag A
 211    */
 212   static Node evaluateCard(TNode n);
 213   /**
 214    * @param n has the form (bag.is_singleton A) where A is a constant bag
 215    * @return whether the bag A has cardinality one.
 216    */
 217   static Node evaluateIsSingleton(TNode n);
 218   /**
 219    * @param n has the form (bag.from_set A) where A is a constant set
 220    * @return a constant bag that contains exactly the elements in A.
 221    */
 222   static Node evaluateFromSet(TNode n);
 223   /**
 224    * @param n has the form (bag.to_set A) where A is a constant bag
 225    * @return a constant set constructed from the elements in A.
 226    */
 227   static Node evaluateToSet(TNode n);
 228   /**
 229    * @param n has the form (bag.map f A) where A is a constant bag
 230    * @return a constant bag constructed from the images of elements in A.
 231    */
 232   static Node evaluateBagMap(TNode n);
 233 };
 234 }  // namespace bags
 235 }  // namespace theory
 236 }  // namespace cvc5
 237
 238 #endif /* CVC5__THEORY__BAGS__UTILS_H */