diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 52adc329f..3f9d5ed94 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -86,7 +86,7 @@ void BooleanLPSolver::pop() void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _sort) { - // Internal variables are '$', or '$c' so escape `$` to `$$`. + // Internal variables are '$', or '$c' so escape `$` to `$$`. string name = (_name.empty() || _name.at(0) != '$') ? _name : "$$" + _name; // TODO This will not be an integer variable in our model. // Introduce a new kind? @@ -244,7 +244,7 @@ pair> BooleanLPSolver::check(vector cons } else { - //cout << "==============> CDCL final result: SATisfiable / UNKNON." << endl; + //cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl; // TODO should be "unknown" later on return {CheckResult::SATISFIABLE, {}}; } diff --git a/libsolutil/LP.h b/libsolutil/LP.h index a586ef0e3..bbd0d2cac 100644 --- a/libsolutil/LP.h +++ b/libsolutil/LP.h @@ -63,7 +63,7 @@ struct SolvingState bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); } bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); } - // TOOD this is currently not used + // TODO this is currently not used /// Set of literals the conjunction of which implies the lower bonud. std::set lowerReasons;