diff options
Diffstat (limited to 'clang/lib/Analysis/Interval.cpp')
-rw-r--r-- | clang/lib/Analysis/Interval.cpp | 496 |
1 files changed, 141 insertions, 355 deletions
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index e643f5e..4b274ed 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -9,8 +9,6 @@ #include "clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp" #include "clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp" -#include "MCFSimplex.h" - #include "llvm/ADT/PostOrderIterator.h" #include "llvm/ADT/DenseMap.h" #include "llvm/Support/Process.h" @@ -22,8 +20,14 @@ #include <set> using namespace clang; +using namespace std; + +template<typename T> +T neg(const T& t) { + return -t; +} -std::string negate_string(const std::string& str) { +string operator-(const string& str) { if (str[0] == '-') return str.substr(1); return '-' + str; @@ -31,28 +35,28 @@ std::string negate_string(const std::string& str) { #include <sstream> template<typename T> -std::string toString(const T& obj) { - std::stringstream stream; +string toString(const T& obj) { + stringstream stream; stream << obj; return stream.str(); } #include <ostream> template<typename K,typename V> -std::ostream& operator<<(std::ostream& cout, const std::pair<K,V>& v) { +ostream& operator<<(ostream& cout, const pair<K,V>& v) { cout << "(" << v.first << ", " << v.second << ")"; return cout; } template<typename V> -std::ostream& operator<<(std::ostream& cout, const std::pair<Variable<Complete<int64_t> >*, V>& v) { +ostream& operator<<(ostream& cout, const pair<Variable<Complete<int64_t> >*, V>& v) { cout << "(" << v.first->name() << ", " << v.second << ")"; return cout; } template<typename V> -std::ostream& operator<<(std::ostream& cout, const std::vector<V>& v) { +ostream& operator<<(ostream& cout, const vector<V>& v) { cout << "["; - for(typename std::vector<V>::const_iterator it = v.begin(), ei = v.end(); + for(typename vector<V>::const_iterator it = v.begin(), ei = v.end(); it != ei; ++it) { if (it != v.begin()) @@ -64,9 +68,9 @@ std::ostream& operator<<(std::ostream& cout, const std::vector<V>& v) { } template<typename K,typename V> -std::ostream& operator<<(std::ostream& cout, const std::map<K,V>& v) { +ostream& operator<<(ostream& cout, const map<K,V>& v) { cout << "{"; - for (typename std::map<K,V>::const_iterator it = v.begin(), ei = v.end(); + for (typename map<K,V>::const_iterator it = v.begin(), ei = v.end(); it != ei; ++it) { if (it != v.begin()) @@ -91,219 +95,89 @@ template<> ZBar infinity() { return ZBar(1, true); } -//typedef std::map<std::string, ZBar> Vector; -struct Vector : public std::map<std::string, ZBar> { + + + + +struct Vector : public map<string, ZBar> { Vector(const ZBar& val=0) : _val(val) { } - ZBar operator[](const std::string& key) const { - if (this->find(key) != this->end()) - return this->find(key)->second; + ZBar operator[](const string& key) const { + const_iterator it = this->find(key); + if (it != this->end()) + return it->second; return _val; } - ZBar& operator[](const std::string& key) { - if (this->find(key) != this->end()) - return this->find(key)->second; - std::pair<iterator,bool> p = this->insert(std::pair<const std::string, ZBar>(key, _val)); + ZBar& operator[](const string& key) { + iterator it = this->find(key); + if (it != this->end()) + return it->second; + pair<iterator,bool> p = this->insert(pair<const string, ZBar>(key, _val)); return p.first->second; } ZBar _val; }; -Vector negate_vector(const Vector& v) { +Vector operator-(const Vector& v) { Vector result; for (Vector::const_iterator it = v.begin(), ei = v.end(); it != ei; ++it) { - result[negate_string(it->first)] = it->second; + result[-it->first] = it->second; } return result; } -typedef std::pair<Vector, ZBar> Result; // a "slice" of an equation - -Result negate_result(const Result& r) { - return Result(negate_vector(r.first), -r.second); -} - -//typedef std::map<std::string, Result> LinearEquation; // one `Result` per variable -struct LinearEquation : public std::map<std::string, Result> { - Result operator[](const std::string& key) const { - if (this->find(key) != this->end()) - return this->find(key)->second; - Result r; - r.first[key] = 1; - r.second = 0; - return r; - } - Result& operator[](const std::string& key) { - if (this->find(key) != this->end()) - return this->find(key)->second; - Result r; - r.first[key] = 1; - r.second = 0; - std::pair<iterator,bool> p = this->insert(std::pair<const std::string, Result>(key, r)); - return p.first->second; - } -}; - -typedef Vector Condition; - -typedef EquationSystem<ZBar> EqnSys; -typedef Expression<ZBar> EqnExpr; -typedef Variable<ZBar> EqnVar; - - -struct LinearOperator : public Operator<Vector> { - LinearOperator(const LinearEquation* result) - : _values(result) {} - - Vector eval(const std::vector<Vector>& vector) const { - assert(vector.size() == 1); - const Vector& v = vector[0]; - Vector result = v; - for (LinearEquation::const_iterator it = _values->begin(), - ei = _values->end(); - it != ei; - ++it) { - ZBar subresult = 0; - for (Vector::const_iterator jt = it->second.first.begin(), - ej = it->second.first.end(); - jt != ej; - ++jt) { - subresult += jt->second * v[jt->first]; +Vector operator+(const Vector& left, const Vector& right) { + Vector::const_iterator + left_iter = left.begin(), + left_end = left.end(), + right_iter = right.begin(), + right_end = right.end(); + + Vector result(left._val + right._val); + while (left_iter != left_end && right_iter != right_end) { + if (left_iter->first == right_iter->first) { + result[left_iter->first] = left_iter->second + right_iter->second; + left_iter++; + right_iter++; + } else { + if (left_iter->first < right_iter->first) { + result[left_iter->first] = left_iter->second; + left_iter++; + } else { + result[right_iter->first] = right_iter->second; + right_iter++; } - subresult += it->second.second; - result[it->first] = subresult; } - return result; } + Vector::const_iterator it = (right_iter == right_end ? left_iter : right_iter); + Vector::const_iterator end = (right_iter == right_end ? left_end : right_end); + for (; it != end; ++it) + result[it->first] = it->second; - void print(std::ostream& cout) const { - cout << "linear[" << *_values << "]"; - } - - const LinearEquation* _values; -}; - - - -template<class F, class M> -void transform_values(const F& f, M& map) { - for (typename M::iterator it = map.begin(), - ei = map.end(); - it != ei; - ++it) { - it->second = f(it->second); - } -} - -template<class M, class F> -M merge_maps_with(const F& f, const M& left, const M& right) { - M result; - typename M::const_iterator first1 = left.begin(), last1 = left.end(), - first2 = right.begin(), last2 = right.end(); - for (; first1 != last1 && first2 != last2;) { - if (first2->first < first1->first) { - result[first2->first] = first2->second; - ++first2; - } else if (first1->first == first2->first) { - result[first1->first] = f(first1->second, first2->second); - ++first1; - ++first2; - } else { - result[first1->first] = first1->second; - ++first1; - } - } - while (first1 != last1) { - result[first1->first] = first1->second; - ++first1; - } - while (first2 != last2) { - result[first2->first] = first2->second; - ++first2; - } return result; } +Vector operator*(const ZBar& left, const Vector& right) { + Vector result(left * right._val); -template<class T> -T max(const T& l, const T& r) { - return (l < r ? l : r); -} -template<class T> -T negate(const T& v) { - return -v; -} -template<class T> -T addValues(const T& l, const T& r) { - return l + r; -} - -Vector operator-(const Vector& vector) { - Vector result(-vector._val); - for (Vector::const_iterator it = vector.begin(), - ei = vector.end(); - it != ei; + for (Vector::const_iterator + it = right.begin(), + end = right.end(); + it != end; ++it) { - result[it->first] = -it->second; + result[it->first] = left * it->second; } - return result; -} - -Vector operator+(const Vector& left, const Vector& right) { - return merge_maps_with(addValues<ZBar>, left, right); -} - -Vector operator-(const Vector& left, const Vector& right) { - return merge_maps_with(addValues<ZBar>, left, -right); -} -Vector operator*(const Vector& left, const ZBar& right) { - Vector result; - for (Vector::const_iterator it = left.begin(), - ei = left.end(); - it != ei; - ++it) { - result[it->first] = (it->second * right); - } return result; } -Vector operator*(const ZBar& left, const Vector& right) { +Vector operator*(const Vector& left, const ZBar& right) { return right * left; } -bool operator<(const Vector& left, const Vector& right) { - bool equal = true; - for (Vector::const_iterator it = left.begin(), - ei = left.end(); - it != ei; - ++it) { - if (it->second < right[it->first]) { - equal = false; - } else if (it->second > right[it->first]) { - return false; - } - } - for (Vector::const_iterator it = right.begin(), - ei = right.end(); - it != ei; - ++it) { - if (left[it->first] < it->second) { - equal = false; - } else if (left[it->first] > it->second) { - return false; - } - } - return equal ? left._val < right._val : true; -} - -template<> -Vector infinity<Vector>() { - return Vector(infinity<ZBar>()); -} -std::ostream& operator<<(std::ostream& cout, const Vector& v) { +ostream& operator<<(ostream& cout, const Vector& v) { cout << "{"; for (Vector::const_iterator it = v.begin(), ei = v.end(); it != ei; @@ -317,6 +191,22 @@ std::ostream& operator<<(std::ostream& cout, const Vector& v) { +typedef pair<Vector, ZBar> Result; // a "slice" of an equation +Result operator-(const Result& r) { + return Result(-r.first, -r.second); +} + +typedef Vector Condition; + +typedef EquationSystem<ZBar> EqnSys; +typedef Expression<ZBar> EqnExpr; +typedef Variable<ZBar> EqnVar; + + + + + + @@ -329,7 +219,7 @@ Result fromInteger(const IntegerLiteral* expr) { } Result fromDeclExpr(const DeclRefExpr* expr) { - Vector val; + Vector val(0); val[expr->getNameInfo().getAsString()] = 1; return Result(val, 0); } @@ -356,14 +246,13 @@ Result fromBinary(const BinaryOperator* op) { case BO_Assign: return right; case BO_Sub: - right = negate_result(right); + right = -right; //transform_values(negate<ZBar>, right.first); //right.second *= -1; case BO_Add: { Result result; - result.first = merge_maps_with(addValues<ZBar>, - left.first, right.first); + result.first = left.first + right.first; result.second = left.second + right.second; return result; } @@ -384,7 +273,7 @@ Result fromBinary(const BinaryOperator* op) { if (scalar >= 0) { return scalar * value; } else { - return -scalar * negate_result(value); + return scalar * -value; } } case BO_LT: @@ -405,15 +294,13 @@ Result fromExpr(const Expr* stmt) { return fromInteger(static_cast<const IntegerLiteral*>(stmt)); case Stmt::DeclRefExprClass: return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt)); - case Stmt::UnaryOperatorClass: - return fromUnary(static_cast<const UnaryOperator*>(stmt)); case Stmt::BinaryOperatorClass: return fromBinary(static_cast<const BinaryOperator*>(stmt)); } const Expr* expr = stmt->IgnoreParenCasts(); if (stmt != expr) return fromExpr(expr); - llvm::errs() << "we shouldn't get here...\n"; + assert(false); return Result(); } @@ -433,7 +320,7 @@ Condition fromComparison(const BinaryOperator* op, bool negate) { const Expr* right = op->getRHS()->IgnoreParenCasts(); bool flip = false; - std::string name; + string name; int64_t value; if (left->getStmtClass() == Stmt::DeclRefExprClass) { name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString(); @@ -465,13 +352,13 @@ Condition fromComparison(const BinaryOperator* op, bool negate) { switch (operation) { case BO_LT: if (negate) - cond[negate_string(name)] = -value; + cond[-name] = -value; else cond[name] = value - 1; break; case BO_LE: if (negate) - cond[negate_string(name)] = -(value + 1); + cond[-name] = -(value + 1); else cond[name] = value; break; @@ -479,13 +366,13 @@ Condition fromComparison(const BinaryOperator* op, bool negate) { if (negate) cond[name] = value - 1; else - cond[negate_string(name)] = -value; + cond[-name] = -value; break; case BO_GT: if (negate) cond[name] = value; else - cond['-' + name] = -(value + 1); + cond[-name] = -(value + 1); break; } } @@ -493,97 +380,20 @@ Condition fromComparison(const BinaryOperator* op, bool negate) { } -struct MinCostFlow : public Operator<ZBar> { - MinCostFlow(const std::vector<std::pair<EqnVar*, ZBar> >& supplies) - : solver(0, 0) { - assert(supplies.size() % 2 == 0); - - if (supplies.size() == 0) - return; - - MCFClass::FNumber* deficits = new MCFClass::FNumber[supplies.size()]; - MCFClass::Index* starts = new MCFClass::Index[supplies.size()]; - MCFClass::Index* ends = new MCFClass::Index[supplies.size()]; - - for (int i = 0, size = supplies.size(); i < size; i += 2) { - deficits[i] = -supplies[i].second.as<MCFClass::FNumber>(); - deficits[i+1] = -supplies[i+1].second.as<MCFClass::FNumber>(); - - starts[i] = i+1; - ends[i] = i+2; - - starts[i+1] = i+2; - ends[i+1] = i+1; - - printableSupply.push_back(supplies[i].second); - printableSupply.push_back(supplies[i+1].second); - } - - solver.LoadNet(supplies.size(), supplies.size(), // max nodes/arcs - supplies.size(), supplies.size(), // current nodes/arcs - NULL, NULL, // arcs have inf cap, zero cost (to begin) - deficits, // deficits for each node - starts, ends); // start/end of each edge - - delete[] deficits; - delete[] starts; - delete[] ends; - } - - ZBar eval(const std::vector<ZBar>& args) const { - if (args.size() == 0) - return 0; - for (int i = 0, size = args.size(); i < size; ++i) { - //if (args[i] == infinity<ZBar>()) { - // if (!solver.IsClosedArc(i)) - // solver.CloseArc(i); - //} else { - // if (solver.IsClosedArc(i)) - // solver.OpenArc(i); - solver.ChgCost(i, args[i].as<MCFClass::CNumber>()); - //} - } - std::cerr << "MCF" << this << "<" << printableSupply << ">(" << args << ")" << " = "; - solver.SolveMCF(); - if (solver.MCFGetStatus() == MCFClass::kUnfeasible){ - std::cerr << -infinity<ZBar>() << std::endl; - return -infinity<ZBar>(); - } else { - if (solver.MCFGetFO() == MCFClass::Inf<MCFClass::FONumber>()) { - std::cerr << infinity<ZBar>() << std::endl; - return infinity<ZBar>(); - } else if (solver.MCFGetFO() == -MCFClass::Inf<MCFClass::FONumber>()) { - std::cerr << -infinity<ZBar>() << std::endl; - return -infinity<ZBar>(); - } else { - ZBar result = solver.MCFGetFO(); - std::cerr << result << std::endl; - return result; - } - } - } - - virtual void print(std::ostream& cout) const { - cout << "MCF" << this << "<" << printableSupply << ">"; - } - - mutable MCFSimplex solver; - std::vector<ZBar> printableSupply; -}; /* Blocks */ -typedef std::map<std::string, unsigned int> Counters; -typedef std::map<std::string, EqnVar*> VarMap; -typedef std::map<const CFGBlock*, std::set<std::string> > BlockVars; +typedef map<string, unsigned int> Counters; +typedef map<string, EqnVar*> VarMap; +typedef map<const CFGBlock*, set<string> > BlockVars; void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { Counters counters; - std::string block_id = toString(block->getBlockID()); + string block_id = toString(block->getBlockID()); VarMap vars; - for (std::set<std::string>::iterator it = block_vars[block].begin(), + for (set<string>::iterator it = block_vars[block].begin(), ei = block_vars[block].end(); it != ei; ++it) { @@ -597,7 +407,7 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { const CFGStmt* cfg_stmt = it->getAs<CFGStmt>(); const Stmt* stmt = cfg_stmt->getStmt(); - std::string name = ""; + string name = ""; Result result; if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) { const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt); @@ -630,41 +440,55 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { if (name == "") continue; - std::string count = toString(counters[name]); + string count = toString(counters[name]); EqnVar* var = &system.variable(name + '-' + block_id + '[' + count + ']'); - EqnVar* negative_var = &system.variable(negate_string(name) + '-' + block_id + '[' + count + ']'); + EqnVar* negative_var = &system.variable(-name + '-' + block_id + '[' + count + ']'); counters[name]++; for (int negative = 0; negative < 2; ++negative) { // one loop for positive, the other for negative if (negative) { - result = negate_result(result); + result = -result; } EqnExpr* expression; if (result.first.size() > 0) { - // set up the min-cost stuff - std::vector<EqnExpr*> minCostArgs; - std::vector<std::pair<EqnVar*, ZBar> > varCosts; - for (Vector::iterator it = result.first.begin(), + // make sure all our variables exist in vars + for (Vector::iterator + it = result.first.begin(), ei = result.first.end(); it != ei; ++it) { if (!vars[it->first]) vars[it->first] = &system.variable(it->first + '-' + block_id + "-pre"); + } - EqnVar& var = *vars[it->first]; - EqnVar& negVar = *vars[negate_string(it->first)]; - - varCosts.push_back(std::pair<EqnVar*, ZBar>(&var, it->second)); - varCosts.push_back(std::pair<EqnVar*, ZBar>(&negVar, -it->second)); - - minCostArgs.push_back(&var); - minCostArgs.push_back(&negVar); + // set up the min-cost-flow operator + vector<ZBar> supplies; + vector<pair<int,int> > arcs; + vector<EqnExpr*> minCostArgs; + ZBar dummy_value = 0; + supplies.push_back(dummy_value); // dummy node to suck up flow + int index = 1; // the solver uses 1-indexing, for some reason + for (map<std::string,EqnVar*>::iterator + it = vars.begin(), + ei = vars.end(); + it != ei; + it++) { + index++; + supplies.push_back(result.first[it->first]); + dummy_value -= result.first[it->first]; + if (it->first[0] == '-') + arcs.push_back(pair<int,int>(1,index)); + else + arcs.push_back(pair<int,int>(index,1)); + minCostArgs.push_back(vars[it->first]); } - EqnExpr* minCostExpr = &system.expression(new MinCostFlow(varCosts), minCostArgs); + supplies[0] = dummy_value; + + EqnExpr* minCostExpr = &system.expression(new MinCostFlow<ZBar>(supplies, arcs), minCostArgs); // add the constant factor to the min-cost bit - std::vector<EqnExpr*> additionArgs; + vector<EqnExpr*> additionArgs; additionArgs.push_back(&system.constant(result.second)); additionArgs.push_back(minCostExpr); expression = &system.expression(new Addition<ZBar>(), additionArgs); @@ -673,7 +497,7 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { } // max(-inf, expr), so strategy iteration will work - std::vector<EqnExpr*> maxArgs; + vector<EqnExpr*> maxArgs; maxArgs.push_back(&system.constant(-infinity<ZBar>())); maxArgs.push_back(expression); if (negative) @@ -682,9 +506,9 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { system[*var] = &system.maxExpression(maxArgs); } vars[name] = var; - vars[negate_string(name)] = negative_var; + vars[-name] = negative_var; block_vars[block].insert(name); - block_vars[block].insert(negate_string(name)); + block_vars[block].insert(-name); } // add to our successor entry values @@ -704,7 +528,7 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { ZBar val = cond[jt->first]; EqnVar* var = &system.variable(jt->first + '-' + toString((*it)->getBlockID()) + "-pre"); if (system[*var] == NULL) { - std::vector<EqnExpr*> maxArgs; + vector<EqnExpr*> maxArgs; maxArgs.push_back(&system.constant(-infinity<ZBar>())); system[*var] = &system.maxExpression(maxArgs); } @@ -718,51 +542,13 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { expr = jt->second; } else { // need a min here - std::vector<EqnExpr*> minArgs; + vector<EqnExpr*> minArgs; minArgs.push_back(&system.constant(val)); minArgs.push_back(jt->second); expr = &system.expression(new Minimum<ZBar>(), minArgs); } system[*var]->arguments().push_back(expr); - - /*if (expr) { - std::set<std::string> ignore; - for (VarMap::iterator - variables = vars.begin(), - variables_end = vars.end(); - variables != variables_end; - ++variables) { - if (ignore.find(variables->first) != ignore.end()) - continue; - ignore.insert(negate_string(variables->first)); - - std::vector<EqnExpr*> plusArgs; - for (int negate = 0; negate < 2; ++negate) { - std::string var_name = negate ? negate_string(variables->first) : variables->first; - if (cond[var_name] == infinity<ZBar>()) { - // min(x, inf) = x - plusArgs.push_back(vars[var_name]); - } else if (cond[var_name] == -infinity<ZBar>()) { - // min(x, -inf) = -inf - plusArgs.push_back(&system.constant(-infinity<ZBar>())); - } else { - // min(x, y) = ? - std::vector<EqnExpr*> minArgs; - minArgs.push_back(vars[var_name]); - minArgs.push_back(&system.constant(cond[var_name])); - plusArgs.push_back(&system.expression(new Minimum<ZBar>(), minArgs)); - } - } - - std::vector<EqnExpr*> guard_args; - guard_args.push_back(&system.expression(new Addition<ZBar>(), plusArgs)); // value - guard_args.push_back(&system.constant(0)); // lower-bound (so value must be >= this) - guard_args.push_back(expr); // result - expr = &system.expression(new Guard<ZBar>(), guard_args); - } - system[*var]->arguments().push_back(expr); - }*/ } } } @@ -788,27 +574,27 @@ void IntervalAnalysis::runOnAllBlocks(const Decl& decl) { EqnSys system; BlockVars block_vars; - std::vector<EqnExpr*> infArg; + vector<EqnExpr*> infArg; infArg.push_back(&system.constant(-infinity<ZBar>())); // left-most argument has to be -infinity infArg.push_back(&system.constant(infinity<ZBar>())); - std::set<std::string>& function_arguments = block_vars[&cfg->getEntry()]; - std::string block_id = toString(cfg->getEntry().getBlockID()); + set<string>& function_arguments = block_vars[&cfg->getEntry()]; + string block_id = toString(cfg->getEntry().getBlockID()); if (const FunctionDecl* func = dyn_cast<const FunctionDecl>(&decl)) { for (unsigned int i = func->getNumParams(); i > 0; i--) { - std::string name = func->getParamDecl(i-1)->getNameAsString(); + string name = func->getParamDecl(i-1)->getNameAsString(); // add the variables to the first block function_arguments.insert(name); - function_arguments.insert(negate_string(name)); + function_arguments.insert(neg(name)); // set the vars to infinity (unconstrained) system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg); - system[system.variable(negate_string(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg); + system[system.variable(neg(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg); } } - std::set<const CFGBlock*> seen; - std::deque<const CFGBlock*> todo; + set<const CFGBlock*> seen; + deque<const CFGBlock*> todo; todo.push_back(&cfg->getEntry()); while (!todo.empty()) { @@ -835,7 +621,7 @@ void IntervalAnalysis::runOnAllBlocks(const Decl& decl) { Solver<ZBar> solver(system); for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { - EqnVar& var = system.variable(size - i - 1); + EqnVar& var = system.variable(i); llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n"; } } |