#include "csolver.h"
void computePolarities(CSolver *This) {
- HSIteratorBoolean *iterator=This->constraints.iterator();
- while(iterator->hasNext()) {
- Boolean *boolean = iterator->next();
- updatePolarity(boolean, P_TRUE);
- updateMustValue(boolean, BV_MUSTBETRUE);
- computePolarityAndBooleanValue(boolean);
+ SetIteratorBooleanEdge *iterator = This->getConstraints();
+ while (iterator->hasNext()) {
+ BooleanEdge boolean = iterator->next();
+ Boolean *b = boolean.getBoolean();
+ bool isNegated = boolean.isNegated();
+ if (isNegated) {
+ updatePolarity(b, P_FALSE);
+ } else {
+ updatePolarity(b, P_TRUE);
+ }
+ computePolarity(b);
}
delete iterator;
}
This->boolVal = (BooleanValue) (This->boolVal | value);
}
-void computePolarityAndBooleanValue(Boolean *This) {
- switch (GETBOOLEANTYPE(This)) {
+void computePolarity(Boolean *This) {
+ switch (This->type) {
case BOOLEANVAR:
case ORDERCONST:
return;
case PREDICATEOP:
- return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
+ return computePredicatePolarity((BooleanPredicate *)This);
case LOGICOP:
- return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
+ return computeLogicOpPolarity((BooleanLogic *)This);
default:
ASSERT(0);
}
}
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
- if (This->undefStatus != NULL) {
- updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
- computePolarityAndBooleanValue(This->undefStatus);
+void computePredicatePolarity(BooleanPredicate *This) {
+ if (This->undefStatus) {
+ updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
+ computePolarity(This->undefStatus.getBoolean());
}
}
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
- computeLogicOpBooleanValue(This);
- computeLogicOpPolarity(This);
+void computeLogicOpPolarity(BooleanLogic *This) {
+ computeLogicOpPolarityChildren(This);
uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- computePolarityAndBooleanValue(This->inputs.get(i));
+ computePolarity(This->inputs.get(i).getBoolean());
}
}
}
}
-void computeLogicOpPolarity(BooleanLogic *This) {
- Polarity parentpolarity = GETBOOLEANPOLARITY(This);
+void computeLogicOpPolarityChildren(BooleanLogic *This) {
+ Polarity parentpolarity = This->polarity;
switch (This->op) {
- case L_AND:
- case L_OR: {
+ case SATC_AND: {
uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- Boolean *tmp = This->inputs.get(i);
- updatePolarity(tmp, parentpolarity);
+ BooleanEdge tmp = This->inputs.get(i);
+ Boolean *btmp = tmp.getBoolean();
+ updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity);
}
break;
}
- case L_NOT: {
- Boolean *tmp = This->inputs.get(0);
- updatePolarity(tmp, negatePolarity(parentpolarity));
- break;
- }
- case L_XOR: {
- updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
- updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
- break;
- }
- case L_IMPLIES: {
- Boolean *left = This->inputs.get(0);
- updatePolarity(left, negatePolarity( parentpolarity));
- Boolean *right = This->inputs.get(1);
- updatePolarity(right, parentpolarity);
+ case SATC_IFF: {
+ updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE);
+ updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE);
break;
}
default:
ASSERT(0);
}
}
-
-void computeLogicOpBooleanValue(BooleanLogic *This) {
- BooleanValue parentbv = GETBOOLEANVALUE(This);
- switch (This->op) {
- case L_AND: {
- if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
- uint size = This->inputs.getSize();
- for (uint i = 0; i < size; i++) {
- updateMustValue(This->inputs.get(i), parentbv);
- }
- }
- return;
- }
- case L_OR: {
- if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
- uint size = This->inputs.getSize();
- for (uint i = 0; i < size; i++) {
- updateMustValue(This->inputs.get(i), parentbv);
- }
- }
- return;
- }
- case L_NOT:
- updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
- return;
- case L_IMPLIES:
- //implies is really an or with the first term negated
- if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
- uint size = This->inputs.getSize();
- updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
- updateMustValue(This->inputs.get(1), parentbv);
- }
- return;
- case L_XOR:
- return;
- default:
- ASSERT(0);
- }
-}