GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_state.cpp Lines: 71 71 100.0 %
Date: 2021-03-22 Branches: 79 190 41.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 A theory state for Theory
13
 **/
14
15
#include "theory/theory_state.h"
16
17
#include "theory/uf/equality_engine.h"
18
19
namespace CVC4 {
20
namespace theory {
21
22
98987
TheoryState::TheoryState(context::Context* c,
23
                         context::UserContext* u,
24
98987
                         Valuation val)
25
    : d_context(c),
26
      d_ucontext(u),
27
      d_valuation(val),
28
      d_ee(nullptr),
29
98987
      d_conflict(c, false)
30
{
31
98987
}
32
33
98945
void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
34
35
167982
context::Context* TheoryState::getSatContext() const { return d_context; }
36
37
233596
context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
38
39
29050399
bool TheoryState::hasTerm(TNode a) const
40
{
41
29050399
  Assert(d_ee != nullptr);
42
29050399
  return d_ee->hasTerm(a);
43
}
44
45
13188004
TNode TheoryState::getRepresentative(TNode t) const
46
{
47
13188004
  Assert(d_ee != nullptr);
48
13188004
  if (d_ee->hasTerm(t))
49
  {
50
13026486
    return d_ee->getRepresentative(t);
51
  }
52
161518
  return t;
53
}
54
55
8211973
bool TheoryState::areEqual(TNode a, TNode b) const
56
{
57
8211973
  Assert(d_ee != nullptr);
58
8211973
  if (a == b)
59
  {
60
2471809
    return true;
61
  }
62
5740164
  else if (hasTerm(a) && hasTerm(b))
63
  {
64
5700377
    return d_ee->areEqual(a, b);
65
  }
66
39787
  return false;
67
}
68
69
615164
bool TheoryState::areDisequal(TNode a, TNode b) const
70
{
71
615164
  Assert(d_ee != nullptr);
72
615164
  if (a == b)
73
  {
74
297623
    return false;
75
  }
76
77
317541
  bool isConst = true;
78
317541
  bool hasTerms = true;
79
317541
  if (hasTerm(a))
80
  {
81
317108
    a = d_ee->getRepresentative(a);
82
317108
    isConst = a.isConst();
83
  }
84
433
  else if (!a.isConst())
85
  {
86
    // if not constant and not a term in the ee, it cannot be disequal
87
259
    return false;
88
  }
89
  else
90
  {
91
174
    hasTerms = false;
92
  }
93
94
317282
  if (hasTerm(b))
95
  {
96
316881
    b = d_ee->getRepresentative(b);
97
316881
    isConst = isConst && b.isConst();
98
  }
99
401
  else if (!b.isConst())
100
  {
101
    // same as above, it cannot be disequal
102
77
    return false;
103
  }
104
  else
105
  {
106
324
    hasTerms = false;
107
  }
108
109
317205
  if (isConst)
110
  {
111
    // distinct constants are disequal
112
49931
    return a != b;
113
  }
114
267274
  else if (!hasTerms)
115
  {
116
252
    return false;
117
  }
118
  // otherwise there may be an explicit disequality in the equality engine
119
267022
  return d_ee->areDisequal(a, b, false);
120
}
121
122
8626
void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
123
{
124
8626
  if (d_ee->hasTerm(a))
125
  {
126
15936
    Node rep = d_ee->getRepresentative(a);
127
7968
    eq::EqClassIterator eqc_iter(rep, d_ee);
128
108066
    while (!eqc_iter.isFinished())
129
    {
130
50049
      eqc.push_back(*eqc_iter);
131
50049
      eqc_iter++;
132
    }
133
  }
134
  else
135
  {
136
658
    eqc.push_back(a);
137
  }
138
  // a should be in its equivalence class
139
8626
  Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
140
8626
}
141
142
6312922
eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
143
144
186635
void TheoryState::notifyInConflict() { d_conflict = true; }
145
146
45158503
bool TheoryState::isInConflict() const { return d_conflict; }
147
148
456824
bool TheoryState::isSatLiteral(TNode lit) const
149
{
150
456824
  return d_valuation.isSatLiteral(lit);
151
}
152
153
1825
TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
154
155
4720
SortInference* TheoryState::getSortInference()
156
{
157
4720
  return d_valuation.getSortInference();
158
}
159
160
223
bool TheoryState::hasSatValue(TNode n, bool& value) const
161
{
162
223
  return d_valuation.hasSatValue(n, value);
163
}
164
165
6526
context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
166
{
167
6526
  return d_valuation.factsBegin(tid);
168
}
169
6526
context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
170
{
171
6526
  return d_valuation.factsEnd(tid);
172
}
173
174
189877
Valuation& TheoryState::getValuation() { return d_valuation; }
175
176
}  // namespace theory
177
26676
}  // namespace CVC4