#include "csolver.h"
void computePolarities(CSolver *This) {
+ if(This->isUnSAT()){
+ return;
+ }
SetIteratorBooleanEdge *iterator = This->getConstraints();
while (iterator->hasNext()) {
BooleanEdge boolean = iterator->next();
Boolean *bdst = dst.getBoolean();
bool isNegated = dst.isNegated();
if (isNegated)
- p=negatePolarity(p);
+ p = negatePolarity(p);
updatePolarity(bdst, p);
}
switch (This->type) {
case BOOLEANVAR:
case ORDERCONST:
+ case BOOLCONST:
return;
case PREDICATEOP:
return computePredicatePolarity((BooleanPredicate *)This);
if (This->undefStatus) {
computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
}
- for(uint i=0; i < This->inputs.getSize(); i++) {
- Element * e = This->inputs.get(i);
+ for (uint i = 0; i < This->inputs.getSize(); i++) {
+ Element *e = This->inputs.get(i);
computeElement(e);
}
}
computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
}
- for(uint i=0; i < ef->inputs.getSize(); i++) {
- Element * echild = ef->inputs.get(i);
+ for (uint i = 0; i < ef->inputs.getSize(); i++) {
+ Element *echild = ef->inputs.get(i);
computeElement(echild);
- }
+ }
}
}