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-2019 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
computeTC(std::set<Node> rel_mem,Node rel)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 
computeTC(Node rel,std::set<Node> & rel_mem,Node fst,Node snd,std::set<Node> & traversed,std::set<Node> & tc_rel_mem)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 
nthElementOfTuple(Node tuple,int n_th)65   static Node nthElementOfTuple( Node tuple, int n_th ) {
66     if( tuple.getKind() == kind::APPLY_CONSTRUCTOR ) {
67       return tuple[n_th];
68     }
69     TypeNode tn = tuple.getType();
70     Datatype dt = tn.getDatatype();
71     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple);
72   }
73 
reverseTuple(Node tuple)74   static Node reverseTuple( Node tuple ) {
75     Assert( tuple.getType().isTuple() );
76     std::vector<Node> elements;
77     std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
78     std::reverse( tuple_types.begin(), tuple_types.end() );
79     TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
80     Datatype dt = tn.getDatatype();
81     elements.push_back( Node::fromExpr(dt[0].getConstructor() ) );
82     for(int i = tuple_types.size() - 1; i >= 0; --i) {
83       elements.push_back( nthElementOfTuple(tuple, i) );
84     }
85     return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
86   }
constructPair(Node rel,Node a,Node b)87   static Node constructPair(Node rel, Node a, Node b) {
88     Datatype dt = rel.getType().getSetElementType().getDatatype();
89     return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
90   }
91 
92 };
93 }/* CVC4::theory::sets namespace */
94 }/* CVC4::theory namespace */
95 }/* CVC4 namespace */
96 
97 #endif
98