GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/theory_quantifiers_type_rules.h Lines: 40 49 81.6 %
Date: 2021-03-23 Branches: 114 354 32.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_quantifiers_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Tim King
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 Theory of quantifiers
13
 **
14
 ** Theory of quantifiers.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
20
#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
21
22
#include "expr/node.h"
23
#include "expr/type_node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
struct QuantifierForallTypeRule {
30
98852
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
31
  {
32
98852
    Debug("typecheck-q") << "type check for fa " << n << std::endl;
33
98852
    Assert(n.getKind() == kind::FORALL && n.getNumChildren() > 0);
34
98852
    if( check ){
35
98852
      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
36
        throw TypeCheckingExceptionPrivate(n, "first argument of universal quantifier is not bound var list");
37
      }
38
98852
      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
39
        throw TypeCheckingExceptionPrivate(n, "body of universal quantifier is not boolean");
40
      }
41
98852
      if( n.getNumChildren()==3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
42
        throw TypeCheckingExceptionPrivate(n, "third argument of universal quantifier is not instantiation pattern list");
43
      }
44
    }
45
98852
    return nodeManager->booleanType();
46
  }
47
};/* struct QuantifierForallTypeRule */
48
49
struct QuantifierExistsTypeRule {
50
9170
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
51
  {
52
9170
    Debug("typecheck-q") << "type check for ex " << n << std::endl;
53
9170
    Assert(n.getKind() == kind::EXISTS && n.getNumChildren() > 0);
54
9170
    if( check ){
55
9170
      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
56
        throw TypeCheckingExceptionPrivate(n, "first argument of existential quantifier is not bound var list");
57
      }
58
9170
      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
59
        throw TypeCheckingExceptionPrivate(n, "body of existential quantifier is not boolean");
60
      }
61
9170
      if( n.getNumChildren()==3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
62
        throw TypeCheckingExceptionPrivate(n, "third argument of existential quantifier is not instantiation pattern list");
63
      }
64
    }
65
9170
    return nodeManager->booleanType();
66
  }
67
};/* struct QuantifierExistsTypeRule */
68
69
struct QuantifierBoundVarListTypeRule {
70
66871
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
71
  {
72
66871
    Assert(n.getKind() == kind::BOUND_VAR_LIST);
73
66871
    if( check ){
74
228134
      for( int i=0; i<(int)n.getNumChildren(); i++ ){
75
161263
        if( n[i].getKind()!=kind::BOUND_VARIABLE ){
76
          throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not bound variable");
77
        }
78
      }
79
    }
80
66871
    return nodeManager->boundVarListType();
81
  }
82
};/* struct QuantifierBoundVarListTypeRule */
83
84
struct QuantifierInstPatternTypeRule {
85
7669
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
86
  {
87
7669
    Assert(n.getKind() == kind::INST_PATTERN);
88
7669
    if( check ){
89
15338
      TypeNode tn = n[0].getType(check);
90
      // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x))
91
7669
      if( n[0].isVar() && n[0].getKind()!=kind::BOUND_VARIABLE && tn.isFunction() ){
92
        throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms.");
93
      }
94
    }
95
7669
    return nodeManager->instPatternType();
96
  }
97
};/* struct QuantifierInstPatternTypeRule */
98
99
struct QuantifierInstNoPatternTypeRule {
100
16
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
101
  {
102
16
    Assert(n.getKind() == kind::INST_NO_PATTERN);
103
16
    return nodeManager->instPatternType();
104
  }
105
};/* struct QuantifierInstNoPatternTypeRule */
106
107
struct QuantifierInstAttributeTypeRule {
108
953
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
109
  {
110
953
    Assert(n.getKind() == kind::INST_ATTRIBUTE);
111
953
    return nodeManager->instPatternType();
112
  }
113
};/* struct QuantifierInstAttributeTypeRule */
114
115
struct QuantifierInstPatternListTypeRule {
116
8319
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
117
  {
118
8319
    Assert(n.getKind() == kind::INST_PATTERN_LIST);
119
8319
    if( check ){
120
17023
      for( int i=0; i<(int)n.getNumChildren(); i++ ){
121
8704
        if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN && n[i].getKind()!=kind::INST_ATTRIBUTE ){
122
          throw TypeCheckingExceptionPrivate(n, "argument of inst pattern list is not inst pattern");
123
        }
124
      }
125
    }
126
8319
    return nodeManager->instPatternListType();
127
  }
128
};/* struct QuantifierInstPatternListTypeRule */
129
130
}/* CVC4::theory::quantifiers namespace */
131
}/* CVC4::theory namespace */
132
}/* CVC4 namespace */
133
134
#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */