1 /********************* */
4 ** Top contributors (to current version):
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
12 ** \brief Sets theory implementation.
14 ** Extension to Sets theory.
17 #ifndef SRC_THEORY_SETS_RELS_UTILS_H_
18 #define SRC_THEORY_SETS_RELS_UTILS_H_
20 #include "expr/dtype.h"
21 #include "expr/node.h"
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
;
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
);
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
);
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
);
68 static Node
nthElementOfTuple( Node tuple
, int n_th
) {
69 if( tuple
.getKind() == kind::APPLY_CONSTRUCTOR
) {
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
);
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
) );
89 return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR
, elements
);
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
);
98 }/* CVC4::theory::sets namespace */
99 }/* CVC4::theory namespace */
100 }/* CVC4 namespace */