GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_context.cpp Lines: 21 53 39.6 %
Date: 2021-03-22 Branches: 22 54 40.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_context.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Implementation of term context utilities.
13
 **/
14
15
#include "expr/term_context.h"
16
17
namespace CVC4 {
18
19
uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const
20
{
21
  // default is no change
22
  return tval;
23
}
24
25
557838
uint32_t RtfTermContext::initialValue() const
26
{
27
  // by default, not in a term context or a quantifier
28
557838
  return 0;
29
}
30
31
4112460
uint32_t RtfTermContext::computeValue(TNode t,
32
                                      uint32_t tval,
33
                                      size_t child) const
34
{
35
4112460
  if (t.isClosure())
36
  {
37
    if (tval % 2 == 0)
38
    {
39
      return tval + 1;
40
    }
41
  }
42
4112460
  else if (hasNestedTermChildren(t))
43
  {
44
2667436
    if (tval < 2)
45
    {
46
1525766
      return tval + 2;
47
    }
48
  }
49
2586694
  return tval;
50
}
51
52
uint32_t RtfTermContext::getValue(bool inQuant, bool inTerm)
53
{
54
  return (inQuant ? 1 : 0) + 2 * (inTerm ? 1 : 0);
55
}
56
57
1193570
void RtfTermContext::getFlags(uint32_t val, bool& inQuant, bool& inTerm)
58
{
59
1193570
  inQuant = val % 2 == 1;
60
1193570
  inTerm = val >= 2;
61
1193570
}
62
63
4112460
bool RtfTermContext::hasNestedTermChildren(TNode t)
64
{
65
4112460
  Kind k = t.getKind();
66
  // dont' worry about FORALL or EXISTS, these are part of inQuant.
67
7970330
  return theory::kindToTheoryId(k) != theory::THEORY_BOOL && k != kind::EQUAL
68
2670474
         && k != kind::SEP_STAR && k != kind::SEP_WAND && k != kind::SEP_LABEL
69
6780368
         && k != kind::BITVECTOR_EAGER_ATOM;
70
}
71
72
2750
uint32_t InQuantTermContext::initialValue() const { return 0; }
73
74
205038
uint32_t InQuantTermContext::computeValue(TNode t,
75
                                          uint32_t tval,
76
                                          size_t index) const
77
{
78
205038
  return t.isClosure() ? 1 : tval;
79
}
80
81
uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; }
82
83
bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant)
84
{
85
  return val == 1;
86
}
87
88
uint32_t PolarityTermContext::initialValue() const
89
{
90
  // by default, we have true polarity
91
  return 2;
92
}
93
94
uint32_t PolarityTermContext::computeValue(TNode t,
95
                                           uint32_t tval,
96
                                           size_t index) const
97
{
98
  switch (t.getKind())
99
  {
100
    case kind::AND:
101
    case kind::OR:
102
    case kind::SEP_STAR:
103
      // polarity preserved
104
      return tval;
105
    case kind::IMPLIES:
106
      // first child reverses, otherwise we preserve
107
      return index == 0 ? (tval == 0 ? 0 : (3 - tval)) : tval;
108
    case kind::NOT:
109
      // polarity reversed
110
      return tval == 0 ? 0 : (3 - tval);
111
    case kind::ITE:
112
      // head has no polarity, branches preserve
113
      return index == 0 ? 0 : tval;
114
    case kind::FORALL:
115
      // body preserves, others have no polarity.
116
      return index == 1 ? tval : 0;
117
    default:
118
      // no polarity
119
      break;
120
  }
121
  return 0;
122
}
123
124
uint32_t PolarityTermContext::getValue(bool hasPol, bool pol)
125
{
126
  return hasPol ? (pol ? 2 : 1) : 0;
127
}
128
129
void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol)
130
{
131
  hasPol = val == 0;
132
  pol = val == 2;
133
}
134
135
26676
}  // namespace CVC4