GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/normal_form.h Lines: 65 67 97.0 %
Date: 2021-03-22 Branches: 170 342 49.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file normal_form.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed
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 Normal form for set constants.
13
 **
14
 ** Normal form for set constants.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__SETS__NORMAL_FORM_H
20
#define CVC4__THEORY__SETS__NORMAL_FORM_H
21
22
namespace CVC4 {
23
namespace theory {
24
namespace sets {
25
26
class NormalForm {
27
 public:
28
  /**
29
   * Constructs a set of the form:
30
   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
31
   * from the set { c1 ... cn }, also handles empty set case, which is why
32
   * setType is passed to this method.
33
   */
34
  template <bool ref_count>
35
644
  static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements,
36
                            TypeNode setType)
37
  {
38
    typedef typename std::set<NodeTemplate<ref_count> >::const_iterator
39
        ElementsIterator;
40
644
    NodeManager* nm = NodeManager::currentNM();
41
644
    if (elements.size() == 0)
42
    {
43
49
      return nm->mkConst(EmptySet(setType));
44
    }
45
    else
46
    {
47
1190
      TypeNode elementType = setType.getSetElementType();
48
595
      ElementsIterator it = elements.begin();
49
1190
      Node cur = nm->mkSingleton(elementType, *it);
50
3865
      while (++it != elements.end())
51
      {
52
3270
        Node singleton = nm->mkSingleton(elementType, *it);
53
1635
        cur = nm->mkNode(kind::UNION, singleton, cur);
54
      }
55
595
      return cur;
56
    }
57
  }
58
59
  /**
60
   * Returns true if n is considered a to be a (canonical) constant set value.
61
   * A canonical set value is one whose AST is:
62
   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
63
   * where c1 ... cn are constants and the node identifier of these constants
64
   * are such that:
65
   *   c1 > ... > cn.
66
   * Also handles the corner cases of empty set and singleton set.
67
   */
68
4287
  static bool checkNormalConstant(TNode n) {
69
8574
    Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :"
70
4287
                              << std::endl;
71
4287
    if (n.getKind() == kind::EMPTYSET) {
72
      return true;
73
4287
    } else if (n.getKind() == kind::SINGLETON) {
74
      return n[0].isConst();
75
4287
    } else if (n.getKind() == kind::UNION) {
76
      // assuming (union {SmallestNodeID} ... (union {BiggerNodeId} ...
77
78
4477
      Node orig = n;
79
4477
      TNode prvs;
80
      // check intermediate nodes
81
16703
      while (n.getKind() == kind::UNION)
82
      {
83
8981
        if (n[0].getKind() != kind::SINGLETON || !n[0][0].isConst())
84
        {
85
          // not a constant
86
5154
          Trace("sets-isconst") << "sets::isConst: " << orig << " not due to "
87
2577
                                << n[0] << std::endl;
88
2577
          return false;
89
        }
90
12808
        Debug("sets-checknormal")
91
12808
            << "[sets-checknormal]              element = " << n[0][0] << " "
92
6404
            << n[0][0].getId() << std::endl;
93
6404
        if (!prvs.isNull() && n[0][0] >= prvs)
94
        {
95
392
          Trace("sets-isconst")
96
392
              << "sets::isConst: " << orig << " not due to compare " << n[0][0]
97
196
              << std::endl;
98
196
          return false;
99
        }
100
6208
        prvs = n[0][0];
101
6208
        n = n[1];
102
      }
103
104
      // check SmallestNodeID is smallest
105
1514
      if (n.getKind() != kind::SINGLETON || !n[0].isConst())
106
      {
107
212
        Trace("sets-isconst") << "sets::isConst: " << orig
108
106
                              << " not due to final " << n << std::endl;
109
106
        return false;
110
      }
111
2816
      Debug("sets-checknormal")
112
2816
          << "[sets-checknormal]              lst element = " << n[0] << " "
113
1408
          << n[0].getId() << std::endl;
114
      // compare last ID
115
1408
      if (n[0] < prvs)
116
      {
117
1218
        return true;
118
      }
119
380
      Trace("sets-isconst")
120
380
          << "sets::isConst: " << orig << " not due to compare final " << n[0]
121
190
          << std::endl;
122
    }
123
190
    return false;
124
  }
125
126
  /**
127
   * Converts a set term to a std::set of its elements. This expects a set of
128
   * the form:
129
   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
130
   * Also handles the corner cases of empty set and singleton set.
131
   */
132
1336
  static std::set<Node> getElementsFromNormalConstant(TNode n) {
133
1336
    Assert(n.isConst());
134
1336
    std::set<Node> ret;
135
1336
    if (n.getKind() == kind::EMPTYSET) {
136
82
      return ret;
137
    }
138
5230
    while (n.getKind() == kind::UNION) {
139
1988
      Assert(n[0].getKind() == kind::SINGLETON);
140
1988
      ret.insert(ret.begin(), n[0][0]);
141
1988
      n = n[1];
142
    }
143
1254
    Assert(n.getKind() == kind::SINGLETON);
144
1254
    ret.insert(n[0]);
145
1254
    return ret;
146
  }
147
148
5979
  static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){
149
5979
    if( index>=els.size() ){
150
455
      return NodeManager::currentNM()->mkConst(EmptySet(tn));
151
5524
    }else if( index==els.size()-1 ){
152
4480
      return els[index];
153
    }else{
154
1044
      return NodeManager::currentNM()->mkNode( k, els[index], mkBop( k, els, tn, index+1 ) );
155
    }
156
  }
157
158
};
159
}
160
}
161
}
162
163
#endif