samvv/bolt
1
0
Fork 0
Code Issues 24 Pull requests Projects Releases Packages Wiki Activity Actions

Allow more constraints to be eagerly solved

Browse source
This commit is contained in:
Sam Vervaeck 2023-05-23 21:50:00 +02:00
parent ebc51539ad
commit 3bc77b1bb6
Signed by: samvv
SSH key fingerprint: SHA256:dIg0ywU1OP+ZYifrYxy8c5esO72cIKB+4/9wkZj1VaY
1 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Checker.cc
View file

@ -120,14 +120,23 @@ namespace bolt {
{
auto Y = static_cast<CEqual*>(C);
std::size_t MaxLevel = 0;
std::size_t MaxLevelLeft = 0;
for (std::size_t I = Contexts.size(); I-- > 0; ) {
auto Ctx = Contexts[I];
if (hasTypeVar(*Ctx->TVs, Y->Left) || hasTypeVar(*Ctx->TVs, Y->Right)) {
MaxLevel = I;
if (hasTypeVar(*Ctx->TVs, Y->Left)) {
MaxLevelLeft = I;
break;
}
}
std::size_t MaxLevelRight = 0;
for (std::size_t I = Contexts.size(); I-- > 0; ) {
auto Ctx = Contexts[I];
if (hasTypeVar(*Ctx->TVs, Y->Right)) {
MaxLevelRight = I;
break;
}
}
auto MaxLevel = std::max(MaxLevelLeft, MaxLevelRight);
std::size_t MinLevel = MaxLevel;
for (std::size_t I = 0; I < Contexts.size(); I++) {
@ -139,7 +148,7 @@ namespace bolt {
}
// TODO detect if MaxLevelLeft == 0 or MaxLevelRight == 0
if (MaxLevel == MinLevel) {
if (MaxLevel == MinLevel || MaxLevelLeft == 0 || MaxLevelRight == 0) {
solveCEqual(Y);
} else {
Contexts[MaxLevel]->Constraints->push_back(C);