From: Hamed <hamed.gorjiara@gmail.com>
Date: Wed, 28 Jun 2017 18:50:41 +0000 (-0700)
Subject: Generating constraints for BooleanOrder
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=494125ae2742bcc5c1acd2d617a8533c5506ba97;p=satune.git

Generating constraints for BooleanOrder
---

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 0432b43..9d37723 100644
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -18,6 +18,7 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
 	tmp->order=order;
 	tmp->first=first;
 	tmp->second=second;
+	tmp->var=NULL;
 	allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp));
 	return & tmp -> base;
 }
diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index a59aff1..cf807c6 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -24,6 +24,7 @@ struct BooleanOrder {
 	Order* order;
 	uint64_t first;
 	uint64_t second;
+	Constraint* var;
 };
 
 struct BooleanVar {
diff --git a/src/AST/order.c b/src/AST/order.c
index 1e39b38..cbfeac3 100644
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -13,6 +13,14 @@ Order* allocOrder(OrderType type, Set * set){
 	return order;
 }
 
+void addOrderConstraint(Order* order, BooleanOrder* constraint){
+	pushVectorBoolean( &order->constraints, (Boolean) constraint);
+}
+
+void setOrderEncodingType(Order* order, OrderEncodingType type){
+	order->order.type = type;
+}
+
 void deleteOrder(Order* order){
 	deleteVectorArrayBoolean(& order->constraints);
 	deleteOrderEncoding(& order->order);
diff --git a/src/AST/order.h b/src/AST/order.h
index 0229982..935787f 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -5,6 +5,7 @@
 #include "structs.h"
 #include "ops.h"
 #include "orderencoding.h"
+#include "boolean.h"
 
 struct Order {
 	OrderType type;
@@ -14,5 +15,7 @@ struct Order {
 };
 
 Order* allocOrder(OrderType type, Set * set);
+void addOrderConstraint(Order* order, BooleanOrder* constraint);
+void setOrderEncodingType(Order* order, OrderEncodingType type);
 void deleteOrder(Order* order);
 #endif
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 325b614..fa385ae 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -8,6 +8,7 @@
 #include "function.h"
 #include "tableentry.h"
 #include "table.h"
+#include "order.h"
 
 
 SATEncoder * allocSATEncoder() {
@@ -113,8 +114,10 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint)
 }
 
 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
-	//TO IMPLEMENT
-	return NULL;
+	if(constraint->var== NULL){
+		constraint->var = getNewVarSATEncoder(This);
+	}
+	return constraint->var;
 }
 
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
@@ -132,7 +135,6 @@ Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction
 		default:
 			ASSERT(0);
 	}
-	//FIXME
 	return NULL;
 }
 
@@ -144,7 +146,6 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun
 		default:
 			ASSERT(0);
 	}
-	//FIXME
 	return NULL;
 }
 
@@ -157,6 +158,7 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
 	ArrayElement* elements= &This->inputs;
 	Table* table = ((FunctionTable*) (This->function))->table;
 	uint size = getSizeVectorTableEntry(&table->entries);
+	Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 	for(uint i=0; i<size; i++){
 		TableEntry* entry = getVectorTableEntry(&table->entries, i);
 		uint inputNum =getSizeArrayElement(elements);
@@ -167,8 +169,9 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
 		}
 		Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 			getElementValueConstraint((Element*)This, entry->output));
-		pushVectorConstraint( getSATEncoderAllConstraints(encoder), row);
+		constraints[i]=row;
 	}
-	//FIXME
-	return NULL;
+	Constraint* result = allocArrayConstraint(OR, size, constraints);
+	pushVectorConstraint( getSATEncoderAllConstraints(encoder), result);
+	return result;
 }
\ No newline at end of file
diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 1ea5857..4f9db3e 100644
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -10,6 +10,7 @@
 #include "boolean.h"
 #include "table.h"
 #include "tableentry.h"
+#include "order.h"
 #include <strings.h>
 
 
@@ -36,12 +37,15 @@ void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){
 	
 	size = getSizeVectorBoolean(csolver->allBooleans);
 	for(uint i=0; i<size; i++){
-		Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
-		switch(GETBOOLEANTYPE(predicate)){
+		Boolean* boolean = getVectorBoolean(csolver->allBooleans, i);
+		switch(GETBOOLEANTYPE(boolean)){
 			case PREDICATEOP:
-				setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)predicate),
+				setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean),
 					ENUMERATEIMPLICATIONS);
 				break;
+			case ORDERCONST:
+				setOrderEncodingType( ((BooleanOrder*)boolean)->order, PAIRWISE );
+				break;
 			default:
 				continue;
 		}