src/theory/sets/rels_utils.h

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