GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sep/theory_sep_type_rules.h Lines: 39 43 90.7 %
Date: 2021-03-22 Branches: 44 192 22.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sep_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Mathias Preiner
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 Typing and cardinality rules for the theory of sep
13
 **
14
 ** Typing and cardinality rules for the theory of sep.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
20
#define CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
21
22
namespace CVC4 {
23
namespace theory {
24
namespace sep {
25
26
class SepEmpTypeRule {
27
public:
28
51
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
29
  {
30
51
    Assert(n.getKind() == kind::SEP_EMP);
31
51
    return nodeManager->booleanType();
32
  }
33
};
34
35
struct SepPtoTypeRule {
36
311
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
37
  {
38
311
    Assert(n.getKind() == kind::SEP_PTO);
39
311
    if( check ) {
40
622
      TypeNode refType = n[0].getType(check);
41
311
      TypeNode ptType = n[1].getType(check);
42
    }
43
311
    return nodeManager->booleanType();
44
  }
45
};/* struct SepSelectTypeRule */
46
47
struct SepStarTypeRule {
48
211
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
49
  {
50
211
    TypeNode btype = nodeManager->booleanType();
51
211
    Assert(n.getKind() == kind::SEP_STAR);
52
211
    if( check ){
53
706
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
54
990
        TypeNode ctype = n[i].getType( check );
55
495
        if( ctype!=btype ){
56
          throw TypeCheckingExceptionPrivate(n, "child of sep star is not Boolean");
57
        }
58
      }
59
    }
60
211
    return btype;
61
  }
62
};/* struct SepStarTypeRule */
63
64
struct SepWandTypeRule {
65
28
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
66
  {
67
28
    TypeNode btype = nodeManager->booleanType();
68
28
    Assert(n.getKind() == kind::SEP_WAND);
69
28
    if( check ){
70
84
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
71
112
        TypeNode ctype = n[i].getType( check );
72
56
        if( ctype!=btype ){
73
          throw TypeCheckingExceptionPrivate(n, "child of sep magic wand is not Boolean");
74
        }
75
      }
76
    }
77
28
    return btype;
78
  }
79
};/* struct SepWandTypeRule */
80
81
struct SepLabelTypeRule {
82
885
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
83
  {
84
885
    TypeNode btype = nodeManager->booleanType();
85
885
    Assert(n.getKind() == kind::SEP_LABEL);
86
885
    if( check ){
87
1770
      TypeNode ctype = n[0].getType( check );
88
885
      if( ctype!=btype ){
89
        throw TypeCheckingExceptionPrivate(n, "child of sep label is not Boolean");
90
      }
91
1770
      TypeNode stype = n[1].getType( check );
92
885
      if( !stype.isSet() ){
93
        throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set");
94
      }
95
    }
96
885
    return btype;
97
  }
98
};/* struct SepLabelTypeRule */
99
100
struct SepNilTypeRule {
101
1388
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
102
  {
103
1388
    Assert(n.getKind() == kind::SEP_NIL);
104
1388
    Assert(check);
105
1388
    TypeNode type = n.getType();
106
1388
    return type;
107
  }
108
};/* struct SepLabelTypeRule */
109
110
111
}/* CVC4::theory::sep namespace */
112
}/* CVC4::theory namespace */
113
}/* CVC4 namespace */
114
115
#endif /* CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */