GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node.cpp Lines: 38 46 82.6 %
Date: 2021-03-23 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
72758235
bool NodeTemplate<ref_count>::isConst() const {
83
72758235
  assertTNodeNotExpired();
84
72758235
  Debug("isConst") << "Node::isConst() for: " << *this << std::endl;
85
72758235
  if(isNull()) {
86
32249
    return false;
87
  }
88
72725986
  switch(getMetaKind()) {
89
18200220
  case kind::metakind::CONSTANT:
90
18200220
    Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
91
18200220
    return true;
92
8703708
  case kind::metakind::VARIABLE:
93
8703708
    Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
94
8703708
    return false;
95
45822058
  default:
96
45822058
    if(getAttribute(IsConstComputedAttr())) {
97
40952408
      bool bval = getAttribute(IsConstAttr());
98
40952408
      Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
99
40952408
      return bval;
100
    } else {
101
4869650
      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
102
4869650
      Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
103
4869650
      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
104
4869650
      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
105
4869650
      return bval;
106
    }
107
  }
108
}
109
110
template bool NodeTemplate<true>::isConst() const;
111
template bool NodeTemplate<false>::isConst() const;
112
113
26685
}/* CVC4 namespace */