- uint newindex=0;
- for(uint i=0;i<asize;i++) {
- Boolean *b=array[i];
- if (b->type == BOOLCONST) {
- if (b->isTrue())
- return b;
- else
- continue;
- } else
- newarray[newindex++]=b;
- }
- if (newindex==1)
- return newarray[0];
- else if (newindex == 2) {
- bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
- bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
-
- if (isNot0 != isNot1) {
- if (isNot0) {
- newarray[0] = ((BooleanLogic *) newarray[0])->inputs.get(0);
- } else {
- Boolean *tmp = ((BooleanLogic *) array[1])->inputs.get(0);
- array[1] = array[0];
- array[0] = tmp;
- }
- return applyLogicalOperation(SATC_IMPLIES, newarray, 2);
- }
- } else {
- array = newarray;
- asize = newindex;
+ for (uint i =0; i <asize; i++) {
+ newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);