Boolean *parent = bexpr->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
switch (logicop->op) {
- case L_AND:
+ case SATC_AND:
handleANDTrue(logicop, bexpr);
break;
- case L_OR:
+ case SATC_OR:
replaceBooleanWithTrue(parent);
break;
- case L_NOT:
+ case SATC_NOT:
replaceBooleanWithFalse(parent);
break;
- case L_XOR:
+ case SATC_XOR:
handleXORTrue(logicop, bexpr);
break;
- case L_IMPLIES:
+ case SATC_IMPLIES:
handleIMPLIESTrue(logicop, bexpr);
break;
}
Boolean *b = bexpr->inputs.get(0);
uint childindex = (b == child) ? 0 : 1;
bexpr->inputs.remove(childindex);
- bexpr->op = L_NOT;
+ bexpr->op = SATC_NOT;
}
void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
} else {
//Make into negation of first term
bexpr->inputs.get(1);
- bexpr->op = L_NOT;
+ bexpr->op = SATC_NOT;
}
}
Boolean *parent = bexpr->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
switch (logicop->op) {
- case L_AND:
+ case SATC_AND:
replaceBooleanWithFalse(parent);
break;
- case L_OR:
+ case SATC_OR:
handleORFalse(logicop, bexpr);
break;
- case L_NOT:
+ case SATC_NOT:
replaceBooleanWithTrue(parent);
break;
- case L_XOR:
+ case SATC_XOR:
handleXORFalse(logicop, bexpr);
break;
- case L_IMPLIES:
+ case SATC_IMPLIES:
handleIMPLIESFalse(logicop, bexpr);
break;
}