src/theory/sets/rels_utils.h

   1 /*********************                                                        */
   2 /*! \file rels_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Sets theory implementation.
  13  **
  14  ** Extension to Sets theory.
  15  **/
  16
  17 #ifndef SRC_THEORY_SETS_RELS_UTILS_H_
  18 #define SRC_THEORY_SETS_RELS_UTILS_H_
  19
  20 #include "expr/dtype.h"
  21 #include "expr/node.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace sets {
  26
  27 class RelsUtils {
  28
  29 public:
  30
  31   // Assumption: the input rel_mem contains all constant pairs
  32   static std::set< Node > computeTC( std::set< Node > rel_mem, Node rel ) {
  33     std::set< Node >::iterator mem_it = rel_mem.begin();
  34     std::map< Node, int > ele_num_map;
  35     std::set< Node > tc_rel_mem;
  36
  37     while( mem_it != rel_mem.end() ) {
  38       Node fst = nthElementOfTuple( *mem_it, 0 );
  39       Node snd = nthElementOfTuple( *mem_it, 1 );
  40       std::set< Node > traversed;
  41       traversed.insert(fst);
  42       computeTC(rel, rel_mem, fst, snd, traversed, tc_rel_mem);
  43       mem_it++;
  44     }
  45     return tc_rel_mem;
  46   }
  47
  48   static void computeTC( Node rel, std::set< Node >& rel_mem, Node fst,
  49                          Node snd, std::set< Node >& traversed, std::set< Node >& tc_rel_mem ) {
  50     tc_rel_mem.insert(constructPair(rel, fst, snd));
  51     if( traversed.find(snd) == traversed.end() ) {
  52       traversed.insert(snd);
  53     } else {
  54       return;
  55     }
  56
  57     std::set< Node >::iterator mem_it = rel_mem.begin();
  58     while( mem_it != rel_mem.end() ) {
  59       Node new_fst = nthElementOfTuple( *mem_it, 0 );
  60       Node new_snd = nthElementOfTuple( *mem_it, 1 );
  61       if( snd == new_fst ) {
  62         computeTC(rel, rel_mem, fst, new_snd, traversed, tc_rel_mem);
  63       }
  64       mem_it++;
  65     }
  66   }
  67
  68   static Node nthElementOfTuple( Node tuple, int n_th ) {
  69     if( tuple.getKind() == kind::APPLY_CONSTRUCTOR ) {
  70       return tuple[n_th];
  71     }
  72     TypeNode tn = tuple.getType();
  73     const DType& dt = tn.getDType();
  74     return NodeManager::currentNM()->mkNode(
  75         kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
  76   }
  77
  78   static Node reverseTuple( Node tuple ) {
  79     Assert(tuple.getType().isTuple());
  80     std::vector<Node> elements;
  81     std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
  82     std::reverse( tuple_types.begin(), tuple_types.end() );
  83     TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
  84     const DType& dt = tn.getDType();
  85     elements.push_back(dt[0].getConstructor());
  86     for(int i = tuple_types.size() - 1; i >= 0; --i) {
  87       elements.push_back( nthElementOfTuple(tuple, i) );
  88     }
  89     return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
  90   }
  91   static Node constructPair(Node rel, Node a, Node b) {
  92     const DType& dt = rel.getType().getSetElementType().getDType();
  93     return NodeManager::currentNM()->mkNode(
  94         kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
  95   }
  96
  97 };
  98 }/* CVC4::theory::sets namespace */
  99 }/* CVC4::theory namespace */
 100 }/* CVC4 namespace */
 101
 102 #endif