GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node.cpp Lines: 38 46 82.6 %
Date: 2021-03-22 Branches: 115 226 50.9 %

Line Exec Source
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
440
TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
32
440
                                                           std::string message)
33
440
    : Exception(message), d_node(new Node(node))
34
{
35
#ifdef CVC4_DEBUG
36
880
  std::stringstream ss;
37
440
  LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
38
440
  if(current != NULL){
39
    // Since this node is malformed, we cannot use toString().
40
    // Instead, we print the kind and the children.
41
4
    ss << "node kind: " << node.getKind() << ". children: ";
42
4
    int i = 0;
43
9
    for (const TNode& child : node)
44
    {
45
5
      ss << "child[" << i << "]: " << child << ". ";
46
5
      i++;
47
    }
48
8
    string ssstring = ss.str();
49
4
    current->setContents(ssstring.c_str());
50
  }
51
#endif /* CVC4_DEBUG */
52
440
}
53
54
440
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
72729037
bool NodeTemplate<ref_count>::isConst() const {
83
72729037
  assertTNodeNotExpired();
84
72729037
  Debug("isConst") << "Node::isConst() for: " << *this << std::endl;
85
72729037
  if(isNull()) {
86
32249
    return false;
87
  }
88
72696788
  switch(getMetaKind()) {
89
18188829
  case kind::metakind::CONSTANT:
90
18188829
    Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
91
18188829
    return true;
92
8701754
  case kind::metakind::VARIABLE:
93
8701754
    Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
94
8701754
    return false;
95
45806205
  default:
96
45806205
    if(getAttribute(IsConstComputedAttr())) {
97
40942366
      bool bval = getAttribute(IsConstAttr());
98
40942366
      Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
99
40942366
      return bval;
100
    } else {
101
4863839
      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
102
4863839
      Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
103
4863839
      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
104
4863839
      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
105
4863839
      return bval;
106
    }
107
  }
108
}
109
110
template bool NodeTemplate<true>::isConst() const;
111
template bool NodeTemplate<false>::isConst() const;
112
113
26676
}/* CVC4 namespace */