More edits

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 0988a574aca4bd26bbe073db41d02cf739910762..7fa33f2459c2d18df7dfc43683f667c4e75b3f81 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -381,21 +381,38 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                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);
+       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)) {
@@ -459,7 +476,7 @@ int CSolver::solve() {
        EncodingGraph eg(this);
        eg.buildGraph();
        eg.encode();
-
+       printConstraints();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
@@ -474,6 +491,19 @@ int CSolver::solve() {
        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;
+
+}
+
 uint64_t CSolver::getElementValue(Element *element) {
        switch (element->type) {
        case ELEMSET: