-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
- Boolean * newarray[asize];
- switch(op) {
- case SATC_NOT: {
- if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) {
- return ((BooleanLogic *) array[0])->inputs.get(0);
- } else if (array[0]->type == BOOLCONST) {
- return array[0]->isTrue() ? boolFalse : boolTrue;
+BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
+ BooleanEdge array[] = {arg1, arg2};
+ return applyLogicalOperation(op, array, 2);
+}
+
+BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
+ BooleanEdge array[] = {arg};
+ return applyLogicalOperation(op, array, 1);
+}
+
+static int ptrcompares(const void *p1, const void *p2) {
+ uintptr_t b1 = *(uintptr_t const *) p1;
+ uintptr_t b2 = *(uintptr_t const *) p2;
+ if (b1 < b2)
+ return -1;
+ else if (b1 == b2)
+ return 0;
+ else
+ return 1;
+}
+
+BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) {
+ BooleanEdge newarray[asize];
+ memcpy(newarray, array, asize * sizeof(BooleanEdge));
+ for(uint i=0; i < asize; i++) {
+ BooleanEdge b=newarray[i];
+ if (b->type == LOGICOP) {
+ if (((BooleanLogic *) b.getBoolean())->replaced) {
+ newarray[i] = doRewrite(newarray[i]);
+ i--;//Check again
+ }