1 /********************* */
4 ** Original author: Paul Meng
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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_
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
;
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
);
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
);
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
);
65 static Node
nthElementOfTuple( Node tuple
, int n_th
) {
66 if(tuple
.isConst() || (!tuple
.isVar() && !tuple
.isConst()))
68 Datatype dt
= tuple
.getType().getDatatype();
69 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL
, dt
[0][n_th
].getSelector(), tuple
);
72 static Node
reverseTuple( Node tuple
) {
73 Assert( tuple
.getType().isTuple() );
74 std::vector
<Node
> elements
;
75 std::vector
<TypeNode
> tuple_types
= tuple
.getType().getTupleTypes();
76 std::reverse( tuple_types
.begin(), tuple_types
.end() );
77 TypeNode tn
= NodeManager::currentNM()->mkTupleType( tuple_types
);
78 Datatype dt
= tn
.getDatatype();
79 elements
.push_back( Node::fromExpr(dt
[0].getConstructor() ) );
80 for(int i
= tuple_types
.size() - 1; i
>= 0; --i
) {
81 elements
.push_back( nthElementOfTuple(tuple
, i
) );
83 return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR
, elements
);
85 static Node
constructPair(Node rel
, Node a
, Node b
) {
86 Datatype dt
= rel
.getType().getSetElementType().getDatatype();
87 return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR
, Node::fromExpr(dt
[0].getConstructor()), a
, b
);
91 }/* CVC4::theory::sets namespace */
92 }/* CVC4::theory namespace */