size = allElements.getSize();
for (uint i = 0; i < size; i++) {
- delete allElements.get(i);
+ Element* el = allElements.get(i);
+ delete el;
}
size = allTables.getSize();
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);
return copy;
}
+CSolver* CSolver::deserialize(const char * file){
+ model_print("deserializing ...\n");
+ Deserializer deserializer(file);
+ return deserializer.deserialize();
+}
+
void CSolver::serialize() {
model_print("serializing ...\n");
- {
- Serializer serializer("dump");
- SetIteratorBooleanEdge *it = getConstraints();
- while (it->hasNext()) {
- BooleanEdge b = it->next();
- serializeBooleanEdge(&serializer, b);
- }
- delete it;
- }
- model_print("deserializing ...\n");
- {
- Deserializer deserializer("dump");
- deserializer.deserialize();
+ printConstraints();
+ Serializer serializer("dump");
+ SetIteratorBooleanEdge *it = getConstraints();
+ while (it->hasNext()) {
+ BooleanEdge b = it->next();
+ serializeBooleanEdge(&serializer, b, true);
}
-
+ delete it;
}
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) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
+#ifdef TRACE_DEBUG
+ model_println("****New Constraint******");
+#endif
+ if(constraint.isNegated())
+ model_print("!");
+ constraint.getBoolean()->print();
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
//IntegerEncodingTransform iet(this);
//iet.doTransform();
- //EncodingGraph eg(this);
- //eg.buildGraph();
- //eg.encode();
- //printConstraints();
+ EncodingGraph eg(this);
+ eg.buildGraph();
+ eg.encode();
+// printConstraints();
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
model_print("\n");
}
delete it;
-
}
void CSolver::printConstraint(BooleanEdge b) {