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 |
|
* Extension to Sets theory. |
14 |
|
*/ |
15 |
|
|
16 |
|
#ifndef SRC_THEORY_SETS_RELS_UTILS_H_ |
17 |
|
#define SRC_THEORY_SETS_RELS_UTILS_H_ |
18 |
|
|
19 |
|
#include "expr/dtype.h" |
20 |
|
#include "expr/dtype_cons.h" |
21 |
|
#include "expr/node.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
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 |
7 |
static std::set< Node > computeTC( std::set< Node > rel_mem, Node rel ) { |
33 |
7 |
std::set< Node >::iterator mem_it = rel_mem.begin(); |
34 |
14 |
std::map< Node, int > ele_num_map; |
35 |
7 |
std::set< Node > tc_rel_mem; |
36 |
|
|
37 |
43 |
while( mem_it != rel_mem.end() ) { |
38 |
36 |
Node fst = nthElementOfTuple( *mem_it, 0 ); |
39 |
36 |
Node snd = nthElementOfTuple( *mem_it, 1 ); |
40 |
36 |
std::set< Node > traversed; |
41 |
18 |
traversed.insert(fst); |
42 |
18 |
computeTC(rel, rel_mem, fst, snd, traversed, tc_rel_mem); |
43 |
18 |
mem_it++; |
44 |
|
} |
45 |
14 |
return tc_rel_mem; |
46 |
|
} |
47 |
|
|
48 |
35 |
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 |
35 |
tc_rel_mem.insert(constructPair(rel, fst, snd)); |
51 |
35 |
if( traversed.find(snd) == traversed.end() ) { |
52 |
33 |
traversed.insert(snd); |
53 |
|
} else { |
54 |
2 |
return; |
55 |
|
} |
56 |
|
|
57 |
33 |
std::set< Node >::iterator mem_it = rel_mem.begin(); |
58 |
265 |
while( mem_it != rel_mem.end() ) { |
59 |
232 |
Node new_fst = nthElementOfTuple( *mem_it, 0 ); |
60 |
232 |
Node new_snd = nthElementOfTuple( *mem_it, 1 ); |
61 |
116 |
if( snd == new_fst ) { |
62 |
17 |
computeTC(rel, rel_mem, fst, new_snd, traversed, tc_rel_mem); |
63 |
|
} |
64 |
116 |
mem_it++; |
65 |
|
} |
66 |
|
} |
67 |
|
|
68 |
596036 |
static Node nthElementOfTuple( Node tuple, int n_th ) { |
69 |
596036 |
if( tuple.getKind() == kind::APPLY_CONSTRUCTOR ) { |
70 |
591947 |
return tuple[n_th]; |
71 |
|
} |
72 |
8178 |
TypeNode tn = tuple.getType(); |
73 |
4089 |
const DType& dt = tn.getDType(); |
74 |
|
return NodeManager::currentNM()->mkNode( |
75 |
4089 |
kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple); |
76 |
|
} |
77 |
|
|
78 |
6636 |
static Node reverseTuple( Node tuple ) { |
79 |
6636 |
Assert(tuple.getType().isTuple()); |
80 |
13272 |
std::vector<Node> elements; |
81 |
13272 |
std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes(); |
82 |
6636 |
std::reverse( tuple_types.begin(), tuple_types.end() ); |
83 |
13272 |
TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types ); |
84 |
6636 |
const DType& dt = tn.getDType(); |
85 |
6636 |
elements.push_back(dt[0].getConstructor()); |
86 |
19948 |
for(int i = tuple_types.size() - 1; i >= 0; --i) { |
87 |
13312 |
elements.push_back( nthElementOfTuple(tuple, i) ); |
88 |
|
} |
89 |
13272 |
return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements ); |
90 |
|
} |
91 |
1486 |
static Node constructPair(Node rel, Node a, Node b) { |
92 |
1486 |
const DType& dt = rel.getType().getSetElementType().getDType(); |
93 |
|
return NodeManager::currentNM()->mkNode( |
94 |
1486 |
kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b); |
95 |
|
} |
96 |
|
|
97 |
|
}; |
98 |
|
} // namespace sets |
99 |
|
} // namespace theory |
100 |
|
} // namespace cvc5 |
101 |
|
|
102 |
|
#endif |