#include "orderedge.h"
#include "orderanalysis.h"
#include <time.h>
+#include <stdarg.h>
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
return element;
}
+void CSolver::mustHaveValue(Element *element){
+ element->getElementEncoding()->anyValue = true;
+}
+
Set *CSolver::getElementRange (Element *element) {
return element->getRange();
}
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;
+static int booleanEdgeCompares(const void *p1, const void *p2) {
+ BooleanEdge be1 = *(BooleanEdge const *) p1;
+ BooleanEdge be2 = *(BooleanEdge const *) p2;
+ uint64_t b1 = be1->id;
+ uint64_t b2 = be2->id;
if (b1 < b2)
return -1;
else if (b1 == b2)
} else if (newindex == 1) {
return newarray[0];
} else {
- bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
+ bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
array = newarray;
asize = newindex;
}
}
delete orderit;
}
-
computePolarities(this);
long long time2 = getTimeNano();
model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
int result = unsat ? IS_UNSAT : satEncoder->solve();
- model_print("Result Computed in CSolver: %d\n", result);
+ model_print("Result Computed in SAT solver: %d\n", result);
if (deleteTuner) {
delete tuner;
autotuner->tune();
delete autotuner;
}
+
+//Set* CSolver::addItemsToRange(Element* element, uint num, ...){
+// va_list args;
+// va_start(args, num);
+// element->getRange()
+// uint setSize = set->getSize();
+// uint newSize = setSize+ num;
+// uint64_t members[newSize];
+// for(uint i=0; i<setSize; i++){
+// members[i] = set->getElement(i);
+// }
+// for( uint i=0; i< num; i++){
+// uint64_t arg = va_arg(args, uint64_t);
+// members[setSize+i] = arg;
+// }
+// va_end(args);
+// return createSet(set->getType(), members, newSize);
+//}
\ No newline at end of file