GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_state.cpp Lines: 71 71 100.0 %
Date: 2021-03-23 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
99009
TheoryState::TheoryState(context::Context* c,
23
                         context::UserContext* u,
24
99009
                         Valuation val)
25
    : d_context(c),
26
      d_ucontext(u),
27
      d_valuation(val),
28
      d_ee(nullptr),
29
99009
      d_conflict(c, false)
30
{
31
99009
}
32
33
98967
void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
34
35
168014
context::Context* TheoryState::getSatContext() const { return d_context; }
36
37
233651
context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
38
39
29050575
bool TheoryState::hasTerm(TNode a) const
40
{
41
29050575
  Assert(d_ee != nullptr);
42
29050575
  return d_ee->hasTerm(a);
43
}
44
45
13188149
TNode TheoryState::getRepresentative(TNode t) const
46
{
47
13188149
  Assert(d_ee != nullptr);
48
13188149
  if (d_ee->hasTerm(t))
49
  {
50
13026631
    return d_ee->getRepresentative(t);
51
  }
52
161518
  return t;
53
}
54
55
8212086
bool TheoryState::areEqual(TNode a, TNode b) const
56
{
57
8212086
  Assert(d_ee != nullptr);
58
8212086
  if (a == b)
59
  {
60
2471835
    return true;
61
  }
62
5740251
  else if (hasTerm(a) && hasTerm(b))
63
  {
64
5700462
    return d_ee->areEqual(a, b);
65
  }
66
39789
  return false;
67
}
68
69
615176
bool TheoryState::areDisequal(TNode a, TNode b) const
70
{
71
615176
  Assert(d_ee != nullptr);
72
615176
  if (a == b)
73
  {
74
297614
    return false;
75
  }
76
77
317562
  bool isConst = true;
78
317562
  bool hasTerms = true;
79
317562
  if (hasTerm(a))
80
  {
81
317129
    a = d_ee->getRepresentative(a);
82
317129
    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
317303
  if (hasTerm(b))
95
  {
96
316902
    b = d_ee->getRepresentative(b);
97
316902
    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
317226
  if (isConst)
110
  {
111
    // distinct constants are disequal
112
49941
    return a != b;
113
  }
114
267285
  else if (!hasTerms)
115
  {
116
252
    return false;
117
  }
118
  // otherwise there may be an explicit disequality in the equality engine
119
267033
  return d_ee->areDisequal(a, b, false);
120
}
121
122
8630
void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
123
{
124
8630
  if (d_ee->hasTerm(a))
125
  {
126
15944
    Node rep = d_ee->getRepresentative(a);
127
7972
    eq::EqClassIterator eqc_iter(rep, d_ee);
128
108130
    while (!eqc_iter.isFinished())
129
    {
130
50079
      eqc.push_back(*eqc_iter);
131
50079
      eqc_iter++;
132
    }
133
  }
134
  else
135
  {
136
658
    eqc.push_back(a);
137
  }
138
  // a should be in its equivalence class
139
8630
  Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
140
8630
}
141
142
6313215
eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
143
144
186657
void TheoryState::notifyInConflict() { d_conflict = true; }
145
146
45160380
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
6530
context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
166
{
167
6530
  return d_valuation.factsBegin(tid);
168
}
169
6530
context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
170
{
171
6530
  return d_valuation.factsEnd(tid);
172
}
173
174
189883
Valuation& TheoryState::getValuation() { return d_valuation; }
175
176
}  // namespace theory
177
26685
}  // namespace CVC4