return BooleanEdge(boolean);
} else {
delete boolean;
- return BooleanEdge(boolean);
+ return BooleanEdge(b);
}
}
BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
- ASSERT(first != second);
+ // ASSERT(first != second);
+ if (first == second)
+ return getBooleanFalse();
+
+ bool negate = false;
+ if (order->type == SATC_TOTAL) {
+ if (first > second) {
+ uint64_t tmp = first;
+ first = second;
+ second = tmp;
+ negate = true;
+ }
+ }
Boolean *constraint = new BooleanOrder(order, first, second);
- allBooleans.push(constraint);
- return BooleanEdge(constraint);
+ Boolean *b = boolMap.get(constraint);
+
+ if (b == NULL) {
+ allBooleans.push(constraint);
+ boolMap.put(constraint, constraint);
+ constraint->updateParents();
+ } else {
+ delete constraint;
+ constraint = b;
+ }
+
+ BooleanEdge be = BooleanEdge(constraint);
+ return negate ? be.negate() : be;
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (constraint.isNegated())
- model_print("!");
- constraint.getBoolean()->print();
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
DecomposeOrderTransform dot(this);
dot.doTransform();
- IntegerEncodingTransform iet(this);
- iet.doTransform();
-
- EncodingGraph eg(this);
- eg.buildGraph();
- eg.encode();
+ //IntegerEncodingTransform iet(this);
+ //iet.doTransform();
+ //EncodingGraph eg(this);
+ //eg.buildGraph();
+ //eg.encode();
+ //printConstraints();
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
return result;
}
+void CSolver::printConstraints() {
+ SetIteratorBooleanEdge *it = getConstraints();
+ while (it->hasNext()) {
+ BooleanEdge b = it->next();
+ if (b.isNegated())
+ model_print("!");
+ b->print();
+ model_print("\n");
+ }
+ delete it;
+
+}
+
+void CSolver::printConstraint(BooleanEdge b) {
+ if (b.isNegated())
+ model_print("!");
+ b->print();
+ model_print("\n");
+}
+
uint64_t CSolver::getElementValue(Element *element) {
switch (element->type) {
case ELEMSET: