blob: 75f4834eaeef69636e1ae91c12f66974c00dff17 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
/********************* */
/*! \file idl_model.cpp
** \verbatim
** Original author: Dejan Jovanovic
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "theory/idl/idl_model.h"
using namespace CVC4;
using namespace theory;
using namespace idl;
IDLModel::IDLModel(context::Context* context)
: d_model(context)
, d_reason(context)
{}
Integer IDLModel::getValue(TNode var) const {
model_value_map::const_iterator find = d_model.find(var);
if (find != d_model.end()) {
return (*find).second;
} else {
return 0;
}
}
void IDLModel::setValue(TNode var, Integer value, IDLReason reason) {
Assert(!reason.constraint.isNull());
d_model[var] = value;
d_reason[var] = reason;
}
void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) {
TNode current = var;
do {
Debug("theory::idl::model") << "processing: " << var << std::endl;
Assert(d_reason.find(current) != d_reason.end());
IDLReason reason = d_reason[current];
Debug("theory::idl::model") << "adding reason: " << reason.constraint << std::endl;
reasons.push_back(reason.constraint);
current = reason.x;
} while (current != var);
}
void IDLModel::toStream(std::ostream& out) const {
model_value_map::const_iterator it = d_model.begin();
model_value_map::const_iterator it_end = d_model.end();
out << "Model[" << std::endl;
for (; it != it_end; ++ it) {
out << (*it).first << " -> " << (*it).second << std::endl;
}
out << "]";
}
|
