src/theory/sets/rels_utils.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   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 relations.
  14  */
  15
  16 #ifndef SRC_THEORY_SETS_RELS_UTILS_H_
  17 #define SRC_THEORY_SETS_RELS_UTILS_H_
  18
  19 #include "expr/node.h"
  20
  21 namespace cvc5 {
  22 namespace theory {
  23 namespace sets {
  24
  25 class RelsUtils
  26 {
  27  public:
  28   /**
  29    * compute the transitive closure of a binary relation
  30    * @param members constant nodes of type (Tuple E E) that are known to in the
  31    * relation rel
  32    * @param rel a binary relation of type (Set (Tuple E E))
  33    * @pre all members need to be constants
  34    * @return the transitive closure of the relation
  35    */
  36   static std::set<Node> computeTC(const std::set<Node>& members, Node rel);
  37
  38   /**
  39    * add all pairs (a, c) to the transitive closures where c is reachable from b
  40    * in the transitive relation in a depth first search manner.
  41    * @param rel a binary relation of type (Set (Tuple E E))
  42    * @param members constant nodes of type (Tuple E E) that are known to be in
  43    * the relation rel
  44    * @param a a node of type E where (a,b) is an element in the transitive
  45    * closure
  46    * @param b a node of type E where (a,b) is an element in the transitive
  47    * closure
  48    * @param traversed the set of members that have been visited so far
  49    * @param transitiveClosureMembers members of the transitive closure computed
  50    * so far
  51    */
  52   static void computeTC(Node rel,
  53                         const std::set<Node>& members,
  54                         Node a,
  55                         Node b,
  56                         std::set<Node>& traversed,
  57                         std::set<Node>& transitiveClosureMembers);
  58
  59   /**
  60    * construct a pair from two elements
  61    * @param rel a node of type (Set (Tuple E E))
  62    * @param a a node of type E
  63    * @param b a node of type E
  64    * @return  a tuple (tuple a b)
  65    */
  66   static Node constructPair(Node rel, Node a, Node b);
  67 };
  68 }  // namespace sets
  69 }  // namespace theory
  70 }  // namespace cvc5
  71
  72 #endif