This commit is contained in:
chriseth 2022-02-23 19:06:35 +01:00
parent 29be0d23f6
commit 797651c74b
2 changed files with 3 additions and 3 deletions

View File

@ -86,7 +86,7 @@ void BooleanLPSolver::pop()
void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _sort)
{
// Internal variables are '$<number>', or '$c<numeber>' so escape `$` to `$$`.
// Internal variables are '$<number>', or '$c<number>' 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<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> 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, {}};
}

View File

@ -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<size_t> lowerReasons;