for (uint i = 0; i < size; i++) {
delete allOrders.get(i);
}
-
size = allFunctions.getSize();
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
Deserializer deserializer("dump");
deserializer.deserialize();
}
-
}
Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
}
}
+
Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
Element *e = elemMap.get(element);
}
case SATC_IFF: {
for (uint i = 0; i < 2; i++) {
- if (array[i]->type == BOOLCONST) {
- if (isTrue(array[i])) { // It can be undefined
- return array[1 - i];
- } else if (isFalse(array[i])) {
- newarray[0] = array[1 - i];
- return applyLogicalOperation(SATC_NOT, newarray, 1);
- }
+ if (isTrue(array[i])) { // It can be undefined
+ return array[1 - i];
+ } else if (isFalse(array[i])) {
+ newarray[0] = array[1 - i];
+ return applyLogicalOperation(SATC_NOT, newarray, 1);
} else if (array[i]->type == LOGICOP) {
BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
if (b->replaced) {
if (((BooleanLogic *)b.getBoolean())->replaced)
return rewriteLogicalOperation(op, array, asize);
}
- if (b->type == BOOLCONST) {
- if (isTrue(b))
- continue;
- else {
- return boolFalse;
- }
+ if (isTrue(b))
+ continue;
+ else if (isFalse(b)) {
+ return boolFalse;
} else
newarray[newindex++] = b;
}
// ASSERT(first != second);
if (first == second)
return getBooleanFalse();
-
+
bool negate = false;
if (order->type == SATC_TOTAL) {
if (first > second) {