blob: 2feabd70014da90aa4eb2c3cbe1301162c263687 (
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
|
#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 << "]";
}
|