Edits

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 7fa33f2459c2d18df7dfc43683f667c4e75b3f81..be4a3a88063882cc05f5cfafca9218724b870f72 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -386,7 +386,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 }
 
 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) {
@@ -408,7 +411,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                constraint = b;
        }
 
-       BooleanEdge be=BooleanEdge(constraint);
+       BooleanEdge be = BooleanEdge(constraint);
        return negate ? be.negate() : be;
 }
 
@@ -470,13 +473,13 @@ int CSolver::solve() {
        DecomposeOrderTransform dot(this);
        dot.doTransform();
 
-       IntegerEncodingTransform iet(this);
-       iet.doTransform();
+       //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);
@@ -504,6 +507,13 @@ void CSolver::printConstraints() {
 
 }
 
+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: