GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sep/theory_sep_rewriter.cpp Lines: 84 95 88.4 %
Date: 2021-03-23 Branches: 180 401 44.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sep_rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed, Andres Noetzli
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "expr/attribute.h"
19
#include "theory/sep/theory_sep_rewriter.h"
20
#include "theory/quantifiers/quant_util.h"
21
#include "options/sep_options.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace sep {
26
27
399
void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){
28
399
  Assert(n.getKind() == kind::SEP_STAR);
29
798
  Node tr = NodeManager::currentNM()->mkConst( true );
30
1351
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
31
952
    if( n[i].getKind()==kind::SEP_EMP ){
32
14
      s_children.push_back( n[i] );
33
938
    }else if( n[i].getKind()==kind::SEP_STAR ){
34
19
      getStarChildren( n[i], s_children, ns_children );
35
919
    }else if( n[i].getKind()==kind::SEP_PTO ){
36
677
      s_children.push_back( n[i] );
37
    }else{
38
484
      std::vector< Node > temp_s_children;
39
242
      getAndChildren( n[i], temp_s_children, ns_children );
40
484
      Node to_add;
41
242
      if( temp_s_children.size()==0 ){
42
60
        if( std::find( s_children.begin(), s_children.end(), tr )==s_children.end() ){
43
59
          to_add = tr;
44
        }
45
182
      }else if( temp_s_children.size()==1 ){
46
182
        to_add = temp_s_children[0];
47
      }else{
48
        to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children );
49
      }
50
242
      if( !to_add.isNull() ){
51
        //flatten star
52
241
        if( to_add.getKind()==kind::SEP_STAR ){
53
          getStarChildren( to_add, s_children, ns_children );
54
241
        }else if( to_add.getKind()!=kind::SEP_EMP || s_children.empty() ){  //remove sep emp
55
225
          s_children.push_back( to_add );
56
        }
57
      }
58
    }
59
  }
60
399
}
61
62
282
void TheorySepRewriter::getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ) {
63
282
  if( n.getKind()==kind::AND ){
64
60
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
65
40
      getAndChildren( n[i], s_children, ns_children );
66
    }
67
  }else{
68
524
    std::map< Node, bool > visited;
69
262
    if( isSpatial( n, visited ) ){
70
182
      if( std::find( s_children.begin(), s_children.end(), n )==s_children.end() ){
71
182
        s_children.push_back( n );
72
      }
73
    }else{
74
80
      if( std::find( ns_children.begin(), ns_children.end(), n )==ns_children.end() ){
75
80
        if( n!=NodeManager::currentNM()->mkConst(true) ){
76
22
          ns_children.push_back( n );
77
        }
78
      }
79
    }
80
  }
81
282
}
82
83
469
bool TheorySepRewriter::isSpatial( Node n, std::map< Node, bool >& visited ) {
84
469
  if( visited.find( n )==visited.end() ){
85
469
    visited[n] = true;
86
469
    if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP || n.getKind()==kind::SEP_LABEL ){
87
182
      return true;
88
287
    }else if( n.getType().isBoolean() ){
89
288
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
90
207
        if( isSpatial( n[i], visited ) ){
91
162
          return true;
92
        }
93
      }
94
    }
95
  }
96
125
  return false;
97
}
98
99
2977
RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
100
2977
  Trace("sep-postrewrite") << "Sep::postRewrite start " << node << std::endl;
101
5954
  Node retNode = node;
102
2977
  switch (node.getKind()) {
103
1529
    case kind::SEP_LABEL: {
104
1529
      if( node[0].getKind()==kind::SEP_PTO ){
105
        // TODO(project##230): Find a safe type for the singleton operator
106
2244
        Node s = NodeManager::currentNM()->mkSingleton(node[0][0].getType(),
107
4488
                                                       node[0][0]);
108
1122
        if( node[1]!=s ){
109
1020
          Node c1 = node[1].eqNode( s );
110
1020
          Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s );
111
510
          retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 );
112
        }
113
      }
114
1529
      if( node[0].getKind()==kind::SEP_EMP ){
115
129
        retNode = node[1].eqNode(
116
86
            NodeManager::currentNM()->mkConst(EmptySet(node[1].getType())));
117
      }
118
1529
      break;
119
    }
120
698
    case kind::SEP_PTO: {
121
698
      break;
122
    }
123
380
    case kind::SEP_STAR: {
124
      //flatten
125
760
      std::vector< Node > s_children;
126
760
      std::vector< Node > ns_children;
127
380
      getStarChildren( node, s_children, ns_children );
128
380
      if( !s_children.empty() ){
129
760
        Node schild;
130
380
        if( s_children.size()==1 ) {
131
9
          schild = s_children[0];
132
        }else{
133
371
          schild = NodeManager::currentNM()->mkNode( kind::SEP_STAR, s_children );
134
        }
135
380
        ns_children.push_back( schild );
136
      }
137
380
      Assert(!ns_children.empty());
138
380
      if( ns_children.size()==1 ){
139
367
        retNode = ns_children[0];
140
      }else{
141
13
        retNode = NodeManager::currentNM()->mkNode( kind::AND, ns_children );
142
      }
143
380
      break;
144
    }
145
    case kind::EQUAL: {
146
      if(node[0] == node[1]) {
147
        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
148
      }
149
      else if (node[0].isConst() && node[1].isConst()) {
150
        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
151
      }
152
      if (node[0] > node[1]) {
153
        Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
154
        return RewriteResponse(REWRITE_DONE, newNode);
155
      }
156
      break;
157
    }
158
370
    default:
159
370
      break;
160
  }
161
2977
  if( node!=retNode ){
162
585
    Trace("sep-rewrite") << "Sep::rewrite : " << node << " -> " << retNode << std::endl;
163
  }
164
2977
  return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
165
}
166
167
}/* CVC4::theory::sep namespace */
168
}/* CVC4::theory namespace */
169
26685
}/* CVC4 namespace */