diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-06-05 16:35:37 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-06-06 14:51:32 -0400 |
commit | 482167cc10c5df25e107e0b44a24c125f7b18bd2 (patch) | |
tree | b3a132657bbe28c4af493c0152e634ffedf28c3f /src/theory/idl/idl_model.cpp | |
parent | 6edae99ca2d1af88ebe82256132d0d058913a13c (diff) |
IDL example theory (to be used with --use-theory=idl).
Diffstat (limited to 'src/theory/idl/idl_model.cpp')
-rw-r--r-- | src/theory/idl/idl_model.cpp | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp new file mode 100644 index 000000000..2feabd700 --- /dev/null +++ b/src/theory/idl/idl_model.cpp @@ -0,0 +1,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 << "]"; +} |