GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/valuation.cpp Lines: 70 108 64.8 %
Date: 2021-03-22 Branches: 51 323 15.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file valuation.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
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 "valuation" proxy for TheoryEngine
13
 **
14
 ** Implementation of Valuation class.
15
 **/
16
17
#include "theory/valuation.h"
18
19
#include "expr/node.h"
20
#include "options/theory_options.h"
21
#include "prop/prop_engine.h"
22
#include "theory/assertion.h"
23
#include "theory/rewriter.h"
24
#include "theory/theory_engine.h"
25
#include "theory/theory_model.h"
26
27
namespace CVC4 {
28
namespace theory {
29
30
std::ostream& operator<<(std::ostream& os, EqualityStatus s)
31
{
32
  switch (s)
33
  {
34
    case EQUALITY_TRUE_AND_PROPAGATED:
35
      os << "EQUALITY_TRUE_AND_PROPAGATED";
36
      break;
37
    case EQUALITY_FALSE_AND_PROPAGATED:
38
      os << "EQUALITY_FALSE_AND_PROPAGATED";
39
      break;
40
    case EQUALITY_TRUE: os << "EQUALITY_TRUE"; break;
41
    case EQUALITY_FALSE: os << "EQUALITY_FALSE"; break;
42
    case EQUALITY_TRUE_IN_MODEL: os << "EQUALITY_TRUE_IN_MODEL"; break;
43
    case EQUALITY_FALSE_IN_MODEL: os << "EQUALITY_FALSE_IN_MODEL"; break;
44
    case EQUALITY_UNKNOWN: os << "EQUALITY_UNKNOWN"; break;
45
    default: Unhandled(); break;
46
  }
47
  return os;
48
}
49
50
bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) {
51
  switch (s1) {
52
  case EQUALITY_TRUE:
53
  case EQUALITY_TRUE_IN_MODEL:
54
  case EQUALITY_TRUE_AND_PROPAGATED:
55
    switch (s2) {
56
    case EQUALITY_TRUE:
57
    case EQUALITY_TRUE_IN_MODEL:
58
    case EQUALITY_TRUE_AND_PROPAGATED:
59
      return true;
60
    default:
61
      return false;
62
    }
63
    break;
64
  case EQUALITY_FALSE:
65
  case EQUALITY_FALSE_IN_MODEL:
66
  case EQUALITY_FALSE_AND_PROPAGATED:
67
    switch (s2) {
68
    case EQUALITY_FALSE:
69
    case EQUALITY_FALSE_IN_MODEL:
70
    case EQUALITY_FALSE_AND_PROPAGATED:
71
      return true;
72
    default:
73
      return false;
74
    }
75
    break;
76
  default:
77
    return false;
78
  }
79
}
80
81
731516
bool Valuation::isSatLiteral(TNode n) const {
82
731516
  Assert(d_engine != nullptr);
83
731516
  return d_engine->getPropEngine()->isSatLiteral(n);
84
}
85
86
49224
Node Valuation::getSatValue(TNode n) const {
87
49224
  Assert(d_engine != nullptr);
88
49224
  if(n.getKind() == kind::NOT) {
89
    Node atomRes = d_engine->getPropEngine()->getValue(n[0]);
90
    if(atomRes.getKind() == kind::CONST_BOOLEAN) {
91
      return NodeManager::currentNM()->mkConst(!atomRes.getConst<bool>());
92
    } else {
93
      Assert(atomRes.isNull());
94
      return atomRes;
95
    }
96
  } else {
97
49224
    return d_engine->getPropEngine()->getValue(n);
98
  }
99
}
100
101
141582
bool Valuation::hasSatValue(TNode n, bool& value) const {
102
141582
  Assert(d_engine != nullptr);
103
141582
  if (d_engine->getPropEngine()->isSatLiteral(n)) {
104
141526
    return d_engine->getPropEngine()->hasValue(n, value);
105
  } else {
106
56
    return false;
107
  }
108
}
109
110
1558001
EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) {
111
1558001
  Assert(d_engine != nullptr);
112
1558001
  return d_engine->getEqualityStatus(a, b);
113
}
114
115
7091
Node Valuation::getModelValue(TNode var) {
116
7091
  Assert(d_engine != nullptr);
117
7091
  return d_engine->getModelValue(var);
118
}
119
120
167706
TheoryModel* Valuation::getModel() {
121
167706
  if (d_engine == nullptr)
122
  {
123
    // no theory engine, thus we don't have a model object
124
    return nullptr;
125
  }
126
167706
  return d_engine->getModel();
127
}
128
4720
SortInference* Valuation::getSortInference()
129
{
130
4720
  if (d_engine == nullptr)
131
  {
132
    // no theory engine, thus we don't have a sort inference object
133
    return nullptr;
134
  }
135
4720
  return d_engine->getSortInference();
136
}
137
138
94783
void Valuation::setUnevaluatedKind(Kind k)
139
{
140
94783
  TheoryModel* m = getModel();
141
94783
  if (m != nullptr)
142
  {
143
94783
    m->setUnevaluatedKind(k);
144
  }
145
  // If no model is available, this command has no effect. This is the case
146
  // when e.g. calling Theory::finishInit for theories that are using a
147
  // Valuation with no model.
148
94783
}
149
150
17990
void Valuation::setSemiEvaluatedKind(Kind k)
151
{
152
17990
  TheoryModel* m = getModel();
153
17990
  if (m != nullptr)
154
  {
155
17990
    m->setSemiEvaluatedKind(k);
156
  }
157
17990
}
158
159
8995
void Valuation::setIrrelevantKind(Kind k)
160
{
161
8995
  TheoryModel* m = getModel();
162
8995
  if (m != nullptr)
163
  {
164
8995
    m->setIrrelevantKind(k);
165
  }
166
8995
}
167
168
181732
Node Valuation::ensureLiteral(TNode n) {
169
181732
  Assert(d_engine != nullptr);
170
181732
  return d_engine->getPropEngine()->ensureLiteral(n);
171
}
172
173
1337
Node Valuation::getPreprocessedTerm(TNode n)
174
{
175
1337
  Assert(d_engine != nullptr);
176
1337
  return d_engine->getPropEngine()->getPreprocessedTerm(n);
177
}
178
179
1731
Node Valuation::getPreprocessedTerm(TNode n,
180
                                    std::vector<Node>& skAsserts,
181
                                    std::vector<Node>& sks)
182
{
183
1731
  Assert(d_engine != nullptr);
184
1731
  return d_engine->getPropEngine()->getPreprocessedTerm(n, skAsserts, sks);
185
}
186
187
209424
bool Valuation::isDecision(Node lit) const {
188
209424
  Assert(d_engine != nullptr);
189
209424
  return d_engine->getPropEngine()->isDecision(lit);
190
}
191
192
8604
unsigned Valuation::getAssertionLevel() const{
193
8604
  Assert(d_engine != nullptr);
194
8604
  return d_engine->getPropEngine()->getAssertionLevel();
195
}
196
197
5250
std::pair<bool, Node> Valuation::entailmentCheck(options::TheoryOfMode mode,
198
                                                 TNode lit)
199
{
200
5250
  Assert(d_engine != nullptr);
201
5250
  return d_engine->entailmentCheck(mode, lit);
202
}
203
204
379474
bool Valuation::needCheck() const{
205
379474
  Assert(d_engine != nullptr);
206
379474
  return d_engine->needCheck();
207
}
208
209
1096
bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
210
211
6526
context::CDList<Assertion>::const_iterator Valuation::factsBegin(TheoryId tid)
212
{
213
6526
  Theory* theory = d_engine->theoryOf(tid);
214
6526
  Assert(theory != nullptr);
215
6526
  return theory->facts_begin();
216
}
217
6526
context::CDList<Assertion>::const_iterator Valuation::factsEnd(TheoryId tid)
218
{
219
6526
  Theory* theory = d_engine->theoryOf(tid);
220
6526
  Assert(theory != nullptr);
221
6526
  return theory->facts_end();
222
}
223
224
}/* CVC4::theory namespace */
225
26676
}/* CVC4 namespace */