From: Hamed <hamed.gorjiara@gmail.com> Date: Tue, 18 Jul 2017 18:52:13 +0000 (-0700) Subject: bug fix for the order test case ... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3e27c15520a179e1107547685fa69fc53e0c307e;p=satune.git bug fix for the order test case ... --- diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c index dee9b26..36c16f2 100644 --- a/src/Backend/satorderencoder.c +++ b/src/Backend/satorderencoder.c @@ -20,7 +20,7 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair * pair) { bool negate = false; OrderPair flipped; - if (pair->first > pair->second) { + if (pair->first < pair->second) { negate=true; flipped.first=pair->second; flipped.second=pair->first; @@ -79,17 +79,20 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){ ASSERT(pair->first!= pair->second); - OrderPair* value = getOrderPair(table, pair); - if(value == NULL) + bool negate = false; + OrderPair flipped; + if (pair->first < pair->second) { + negate=true; + flipped.first=pair->second; + flipped.second=pair->first; + pair = &flipped; + } + if (!containsOrderPair(table, pair)) { return E_NULL; - Edge constraint = value->constraint; - model_print("Constraint:\n"); - printCNF(constraint); - model_print("\n***********\n"); - if(pair->first > pair->second || edgeIsNull(constraint)) - return constraint; - else - return constraintNegate(constraint); + } + Edge constraint= getOrderPair(table, pair)->constraint; + ASSERT(!edgeIsNull(constraint)); + return negate ? constraintNegate(constraint) : constraint; } Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){ diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c index ee22879..a3245d8 100644 --- a/src/Backend/sattranslator.c +++ b/src/Backend/sattranslator.c @@ -82,9 +82,8 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){ HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){ ASSERT(order->orderPairTable!= NULL); - model_print("Frist:%llu\tSecond:%llu\n", first, second); OrderPair pair={first, second, E_NULL}; - Edge var = getOrderConstraint(order->orderPairTable, & pair); + Edge var = getOrderConstraint(order->orderPairTable, &pair); if(edgeIsNull(var)) return UNORDERED; return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND; diff --git a/src/Test/testorder.c b/src/Test/testorder.c index 0ebd5e2..4970cac 100644 --- a/src/Test/testorder.c +++ b/src/Test/testorder.c @@ -11,11 +11,12 @@ int main(int numargs, char ** argv) { addConstraint(solver, b1); addConstraint(solver, b2); if (startEncoding(solver)==1) - printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", + printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n", getOrderConstraintValue(solver, order, 5, 1), getOrderConstraintValue(solver, order, 1, 4), getOrderConstraintValue(solver, order, 5, 4), - getOrderConstraintValue(solver, order, 1, 5)); + getOrderConstraintValue(solver, order, 1, 5), + getOrderConstraintValue(solver, order, 1111, 5)); else printf("UNSAT\n"); deleteSolver(solver);