From: Hamed <hamed.gorjiara@gmail.com> Date: Tue, 18 Jul 2017 01:07:24 +0000 (-0700) Subject: Modify API to work for partial order as well + adding order test case X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7013b7621b5e9efc22d99d066d52bd2fb40d688a;p=satune.git Modify API to work for partial order as well + adding order test case --- diff --git a/src/AST/ops.h b/src/AST/ops.h index 5a7f092..32febff 100644 --- a/src/AST/ops.h +++ b/src/AST/ops.h @@ -12,7 +12,7 @@ typedef enum CompOp CompOp; enum OrderType {PARTIAL, TOTAL}; typedef enum OrderType OrderType; -enum HappenedBefore {UNORDERED, FIRST, SECOND}; +enum HappenedBefore {FIRST, SECOND, UNORDERED}; typedef enum HappenedBefore HappenedBefore; /** diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c index 5ab5355..4d6f639 100644 --- a/src/Backend/satorderencoder.c +++ b/src/Backend/satorderencoder.c @@ -79,7 +79,10 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){ ASSERT(pair->first!= pair->second); - Edge constraint = getOrderPair(table, pair)->constraint; + OrderPair* value = getOrderPair(table, pair); + if(value == NULL) + return E_NULL; + Edge constraint = value->constraint; if(pair->first > pair->second || edgeIsNull(constraint)) return constraint; else diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c index a72617f..3bfc06b 100644 --- a/src/Backend/sattranslator.c +++ b/src/Backend/sattranslator.c @@ -80,10 +80,10 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){ return This->satEncoder->cnf->solver->solution[index] == true; } -HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, BooleanOrder* boolOrder){ - ASSERT(boolOrder->order->orderPairTable!= NULL); - OrderPair pair={boolOrder->first, boolOrder->second, E_NULL}; - Edge var = getOrderConstraint(boolOrder->order->orderPairTable, & pair); +HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){ + ASSERT(order->orderPairTable!= NULL); + OrderPair pair={first, second, E_NULL}; + Edge var = getOrderConstraint(order->orderPairTable, & pair); if(edgeIsNull(var)) return UNORDERED; int index = getEdgeVar( var ); diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h index aad1c29..0b1a996 100644 --- a/src/Backend/sattranslator.h +++ b/src/Backend/sattranslator.h @@ -13,7 +13,7 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean); -HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, BooleanOrder* boolOrder); +HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second); uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc); diff --git a/src/Test/testorder.c b/src/Test/testorder.c new file mode 100644 index 0000000..37217f0 --- /dev/null +++ b/src/Test/testorder.c @@ -0,0 +1,22 @@ + +#include "csolver.h" + +int main(int numargs, char ** argv) { + CSolver * solver=allocCSolver(); + uint64_t set1[]={5, 1, 4}; + Set * s=createSet(solver, 0, set1, 3); + Order* order = createOrder(solver, TOTAL, s); + Boolean* b1= orderConstraint(solver, order, 1, 4); + Boolean* b2= orderConstraint(solver, order, 5, 4); + addConstraint(solver, b1); + addConstraint(solver, b2); + if (startEncoding(solver)==1) + printf("O(1,4)=%d O(5,4)=%d O(4,5)=%d O(1,5)=%d\n", + getOrderConstraintValue(solver, order, 1, 4), + getOrderConstraintValue(solver, order, 5, 4), + getOrderConstraintValue(solver, order, 4, 5), + getOrderConstraintValue(solver, order, 1, 5)); + else + printf("UNSAT\n"); + deleteSolver(solver); +} \ No newline at end of file diff --git a/src/csolver.c b/src/csolver.c index 67e2589..c92aee6 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -213,13 +213,7 @@ bool getBooleanValue( CSolver* This , Boolean* boolean){ exit(-1); } -HappenedBefore getOrderConstraintValue(CSolver* This, Boolean* orderConstr){ - switch(GETBOOLEANTYPE(orderConstr)){ - case ORDERCONST: - return getOrderConstraintValueSATTranslator(This, (BooleanOrder*)orderConstr); - default: - ASSERT(0); - } - exit(-1); +HappenedBefore getOrderConstraintValue(CSolver* This, Order * order, uint64_t first, uint64_t second){ + return getOrderConstraintValueSATTranslator(This, order, first, second); } diff --git a/src/csolver.h b/src/csolver.h index 1e69794..23c35e0 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -125,6 +125,6 @@ uint64_t getElementValue(CSolver*, Element* element); /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/ bool getBooleanValue( CSolver* , Boolean* boolean); -HappenedBefore getOrderConstraintValue(CSolver*, Boolean* orderConstr); +HappenedBefore getOrderConstraintValue(CSolver*, Order * order, uint64_t first, uint64_t second); #endif