src/expr/node.cpp

   1 /*********************                                                        */
   2 /*! \file node.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Yoni Zohar
   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 Reference-counted encapsulation of a pointer to node information.
  13  **
  14  ** Reference-counted encapsulation of a pointer to node information.
  15  **/
  16 #include "expr/node.h"
  17
  18 #include <cstring>
  19 #include <iostream>
  20 #include <sstream>
  21
  22 #include "base/exception.h"
  23 #include "base/output.h"
  24 #include "expr/attribute.h"
  25 #include "expr/type_checker.h"
  26
  27 using namespace std;
  28
  29 namespace CVC4 {
  30
  31 TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
  32                                                            std::string message)
  33     : Exception(message), d_node(new Node(node))
  34 {
  35 #ifdef CVC4_DEBUG
  36   std::stringstream ss;
  37   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
  38   if(current != NULL){
  39     // Since this node is malformed, we cannot use toString().
  40     // Instead, we print the kind and the children.
  41     ss << "node kind: " << node.getKind() << ". children: ";
  42     int i = 0;
  43     for (const TNode& child : node)
  44     {
  45       ss << "child[" << i << "]: " << child << ". ";
  46       i++;
  47     }
  48     string ssstring = ss.str();
  49     current->setContents(ssstring.c_str());
  50   }
  51 #endif /* CVC4_DEBUG */
  52 }
  53
  54 TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; }
  55
  56 void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const
  57 {
  58   os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node;
  59 }
  60
  61 NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const
  62 {
  63   return *d_node;
  64 }
  65
  66 UnknownTypeException::UnknownTypeException(TNode n)
  67     : TypeCheckingExceptionPrivate(
  68           n,
  69           "this expression contains an element of unknown type (such as an "
  70           "abstract value);"
  71           " its type cannot be computed until it is substituted away")
  72 {
  73 }
  74
  75 /** Is this node constant? (and has that been computed yet?) */
  76 struct IsConstTag { };
  77 struct IsConstComputedTag { };
  78 typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
  79 typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
  80
  81 template <bool ref_count>
  82 bool NodeTemplate<ref_count>::isConst() const {
  83   assertTNodeNotExpired();
  84   Debug("isConst") << "Node::isConst() for: " << *this << std::endl;
  85   if(isNull()) {
  86     return false;
  87   }
  88   switch(getMetaKind()) {
  89   case kind::metakind::CONSTANT:
  90     Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
  91     return true;
  92   case kind::metakind::VARIABLE:
  93     Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
  94     return false;
  95   default:
  96     if(getAttribute(IsConstComputedAttr())) {
  97       bool bval = getAttribute(IsConstAttr());
  98       Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
  99       return bval;
 100     } else {
 101       bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
 102       Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
 103       const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
 104       const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
 105       return bval;
 106     }
 107   }
 108 }
 109
 110 template bool NodeTemplate<true>::isConst() const;
 111 template bool NodeTemplate<false>::isConst() const;
 112
 113 }/* CVC4 namespace */