src/theory/sep/theory_sep_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_sep_type_rules.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 #include "theory/type_enumerator.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace sep {
  27
  28 class SepEmpTypeRule {
  29 public:
  30   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  31     throw (TypeCheckingExceptionPrivate, AssertionException) {
  32     Assert(n.getKind() == kind::SEP_EMP);
  33     return nodeManager->booleanType();
  34   }
  35 };
  36
  37 struct SepPtoTypeRule {
  38   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  39     throw (TypeCheckingExceptionPrivate, AssertionException) {
  40     Assert(n.getKind() == kind::SEP_PTO);
  41     if( check ) {
  42       TypeNode refType = n[0].getType(check);
  43       TypeNode ptType = n[1].getType(check);
  44     }
  45     return nodeManager->booleanType();
  46   }
  47 };/* struct SepSelectTypeRule */
  48
  49 struct SepStarTypeRule {
  50   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  51     throw (TypeCheckingExceptionPrivate, AssertionException) {
  52     TypeNode btype = nodeManager->booleanType();
  53     Assert(n.getKind() == kind::SEP_STAR);
  54     if( check ){
  55       for( unsigned i=0; i<n.getNumChildren(); i++ ){
  56         TypeNode ctype = n[i].getType( check );
  57         if( ctype!=btype ){
  58           throw TypeCheckingExceptionPrivate(n, "child of sep star is not Boolean");
  59         }
  60       }
  61     }
  62     return btype;
  63   }
  64 };/* struct SepStarTypeRule */
  65
  66 struct SepWandTypeRule {
  67   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  68     throw (TypeCheckingExceptionPrivate, AssertionException) {
  69     TypeNode btype = nodeManager->booleanType();
  70     Assert(n.getKind() == kind::SEP_WAND);
  71     if( check ){
  72       for( unsigned i=0; i<n.getNumChildren(); i++ ){
  73         TypeNode ctype = n[i].getType( check );
  74         if( ctype!=btype ){
  75           throw TypeCheckingExceptionPrivate(n, "child of sep magic wand is not Boolean");
  76         }
  77       }
  78     }
  79     return btype;
  80   }
  81 };/* struct SepWandTypeRule */
  82
  83 struct SepLabelTypeRule {
  84   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  85     throw (TypeCheckingExceptionPrivate, AssertionException) {
  86     TypeNode btype = nodeManager->booleanType();
  87     Assert(n.getKind() == kind::SEP_LABEL);
  88     if( check ){
  89       TypeNode ctype = n[0].getType( check );
  90       if( ctype!=btype ){
  91         throw TypeCheckingExceptionPrivate(n, "child of sep label is not Boolean");
  92       }
  93       TypeNode stype = n[1].getType( check );
  94       if( !stype.isSet() ){
  95         throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set");
  96       }
  97     }
  98     return btype;
  99   }
 100 };/* struct SepLabelTypeRule */
 101
 102 struct SepNilTypeRule {
 103   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 104     throw (TypeCheckingExceptionPrivate, AssertionException) {
 105     Assert(n.getKind() == kind::SEP_NIL);
 106     Assert(check);
 107     TypeNode type = n.getType();
 108     return type;
 109   }
 110 };/* struct SepLabelTypeRule */
 111
 112
 113 }/* CVC4::theory::sep namespace */
 114 }/* CVC4::theory namespace */
 115 }/* CVC4 namespace */
 116
 117 #endif /* __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */