diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-03-27 11:33:07 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-07-01 15:52:40 +0100 |
commit | a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 (patch) | |
tree | 878d75da74e7a6ae4a917c41ed482fc5c0ffe3e0 /lib/Expr/Assignment.cpp | |
parent | f56c7aa2a7200ece5d074651b9839eb917f910f5 (diff) | |
download | klee-a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0.tar.gz |
Separate constraint set and constraint manager
Diffstat (limited to 'lib/Expr/Assignment.cpp')
-rw-r--r-- | lib/Expr/Assignment.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp index 2fc569cc..98b92337 100644 --- a/lib/Expr/Assignment.cpp +++ b/lib/Expr/Assignment.cpp @@ -25,20 +25,20 @@ void Assignment::dump() { } } -void Assignment::createConstraintsFromAssignment( - std::vector<ref<Expr> > &out) const { - assert(out.size() == 0 && "out should be empty"); - for (bindings_ty::const_iterator it = bindings.begin(), ie = bindings.end(); - it != ie; ++it) { - const Array *array = it->first; - const std::vector<unsigned char> &values = it->second; +ConstraintSet Assignment::createConstraintsFromAssignment() const { + ConstraintSet result; + for (const auto &binding : bindings) { + const auto &array = binding.first; + const auto &values = binding.second; + for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) { unsigned char value = values[arrayIndex]; - out.push_back(EqExpr::create( + result.push_back(EqExpr::create( ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(arrayIndex, array->getDomain())), ConstantExpr::alloc(value, array->getRange()))); } } + return result; } } |