GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/rels_utils.h Lines: 44 44 100.0 %
Date: 2021-03-23 Branches: 73 146 50.0 %

Line Exec Source
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-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.\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
#include "expr/dtype.h"
21
#include "expr/dtype_cons.h"
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace sets {
27
28
class RelsUtils {
29
30
public:
31
32
  // Assumption: the input rel_mem contains all constant pairs
33
8
  static std::set< Node > computeTC( std::set< Node > rel_mem, Node rel ) {
34
8
    std::set< Node >::iterator mem_it = rel_mem.begin();
35
16
    std::map< Node, int > ele_num_map;
36
8
    std::set< Node > tc_rel_mem;
37
38
48
    while( mem_it != rel_mem.end() ) {
39
40
      Node fst = nthElementOfTuple( *mem_it, 0 );
40
40
      Node snd = nthElementOfTuple( *mem_it, 1 );
41
40
      std::set< Node > traversed;
42
20
      traversed.insert(fst);
43
20
      computeTC(rel, rel_mem, fst, snd, traversed, tc_rel_mem);
44
20
      mem_it++;
45
    }
46
16
    return tc_rel_mem;
47
  }
48
49
39
  static void computeTC( Node rel, std::set< Node >& rel_mem, Node fst,
50
                         Node snd, std::set< Node >& traversed, std::set< Node >& tc_rel_mem ) {
51
39
    tc_rel_mem.insert(constructPair(rel, fst, snd));
52
39
    if( traversed.find(snd) == traversed.end() ) {
53
35
      traversed.insert(snd);
54
    } else {
55
4
      return;
56
    }
57
58
35
    std::set< Node >::iterator mem_it = rel_mem.begin();
59
275
    while( mem_it != rel_mem.end() ) {
60
240
      Node new_fst = nthElementOfTuple( *mem_it, 0 );
61
240
      Node new_snd = nthElementOfTuple( *mem_it, 1 );
62
120
      if( snd == new_fst ) {
63
19
        computeTC(rel, rel_mem, fst, new_snd, traversed, tc_rel_mem);
64
      }
65
120
      mem_it++;
66
    }
67
  }
68
69
590184
  static Node nthElementOfTuple( Node tuple, int n_th ) {
70
590184
    if( tuple.getKind() == kind::APPLY_CONSTRUCTOR ) {
71
587218
      return tuple[n_th];
72
    }
73
5932
    TypeNode tn = tuple.getType();
74
2966
    const DType& dt = tn.getDType();
75
    return NodeManager::currentNM()->mkNode(
76
2966
        kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
77
  }
78
79
6458
  static Node reverseTuple( Node tuple ) {
80
6458
    Assert(tuple.getType().isTuple());
81
12916
    std::vector<Node> elements;
82
12916
    std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
83
6458
    std::reverse( tuple_types.begin(), tuple_types.end() );
84
12916
    TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
85
6458
    const DType& dt = tn.getDType();
86
6458
    elements.push_back(dt[0].getConstructor());
87
19406
    for(int i = tuple_types.size() - 1; i >= 0; --i) {
88
12948
      elements.push_back( nthElementOfTuple(tuple, i) );
89
    }
90
12916
    return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
91
  }
92
1450
  static Node constructPair(Node rel, Node a, Node b) {
93
1450
    const DType& dt = rel.getType().getSetElementType().getDType();
94
    return NodeManager::currentNM()->mkNode(
95
1450
        kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
96
  }
97
98
};
99
}/* CVC4::theory::sets namespace */
100
}/* CVC4::theory namespace */
101
}/* CVC4 namespace */
102
103
#endif