From 1491d52574950c4a2d013e626b9b4ece05d6790e Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 1 Sep 2017 18:35:58 -0700
Subject: [PATCH] Adding IntegerEncodingResolver ...

---
 src/ASTTransform/integerencoding.cc       | 10 +++++--
 src/ASTTransform/integerencoding.h        |  1 +
 src/ASTTransform/integerencodingrecord.cc | 10 ++++---
 src/ASTTransform/integerencodingrecord.h  |  2 +-
 src/Translator/integerencorderresolver.cc | 34 +++++++++++++++++++++++
 src/Translator/integerencorderresolver.h  | 24 ++++++++++++++++
 6 files changed, 74 insertions(+), 7 deletions(-)
 create mode 100644 src/Translator/integerencorderresolver.cc
 create mode 100644 src/Translator/integerencorderresolver.h

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 411ddc9..f1b9919 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -5,6 +5,7 @@
 #include "satencoder.h"
 #include "csolver.h"
 #include "integerencodingrecord.h"
+#include "integerencorderresolver.h"
 
 
 IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver) 
@@ -22,14 +23,19 @@ bool IntegerEncodingTransform::canExecuteTransform(){
 }
 
 void IntegerEncodingTransform::doTransform(){
+	IntegerEncodingRecord* encodingRecord = NULL;
 	if (!orderIntEncoding->contains(currOrder)) {
-		orderIntEncoding->put(currOrder, new IntegerEncodingRecord(
-		solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize()-1)));
+		encodingRecord = new IntegerEncodingRecord(
+			solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize()-1));
+		orderIntEncoding->put(currOrder, encodingRecord);
+	} else {
+		encodingRecord = orderIntEncoding->get(currOrder);
 	}
 	uint size = currOrder->constraints.getSize();
 	for(uint i=0; i<size; i++){
 		orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
 	}
+	currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
 }
 
 
diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index 42175b3..3bfb289 100644
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -21,6 +21,7 @@ public:
 	virtual ~IntegerEncodingTransform();
 private:
 	Order* currOrder;
+	//FIXME:We can remove it, because we don't need it for translating anymore... -HG
 	HashTableOrderIntEncoding* orderIntEncoding;
 };
 
diff --git a/src/ASTTransform/integerencodingrecord.cc b/src/ASTTransform/integerencodingrecord.cc
index 7085cf7..abd763f 100644
--- a/src/ASTTransform/integerencodingrecord.cc
+++ b/src/ASTTransform/integerencodingrecord.cc
@@ -21,13 +21,15 @@ IntegerEncodingRecord::~IntegerEncodingRecord(){
 	}
 }
 
-Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item) {
+Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) {
 	OrderElement oelement(item, NULL);
-	if ( !elementTable->contains(&oelement)) {
+	if ( elementTable->contains(&oelement)) {
+		return elementTable->get(&oelement)->getElement();
+	} else if (create) {
 		Element *elem = This->getElementVar(secondarySet);
 		elementTable->add(new OrderElement(item, elem));
 		return elem;
-	} else
-		return elementTable->get(&oelement)->getElement();
+	}
+	return NULL;
 }
 
diff --git a/src/ASTTransform/integerencodingrecord.h b/src/ASTTransform/integerencodingrecord.h
index 2b2f190..a85e98a 100644
--- a/src/ASTTransform/integerencodingrecord.h
+++ b/src/ASTTransform/integerencodingrecord.h
@@ -15,7 +15,7 @@ class IntegerEncodingRecord {
 public:
 	IntegerEncodingRecord(Set* set);
 	~IntegerEncodingRecord();
-	Element* getOrderIntegerElement(CSolver *This, uint64_t item);
+	Element* getOrderIntegerElement(CSolver *This, uint64_t item, bool create = true);
 	inline Set* getSecondarySet() { return secondarySet; }
 	CMEMALLOC;
 	
diff --git a/src/Translator/integerencorderresolver.cc b/src/Translator/integerencorderresolver.cc
new file mode 100644
index 0000000..a9048ef
--- /dev/null
+++ b/src/Translator/integerencorderresolver.cc
@@ -0,0 +1,34 @@
+
+/* 
+ * File:   integerencorderresolver.cpp
+ * Author: hamed
+ * 
+ * Created on September 1, 2017, 4:58 PM
+ */
+
+#include "integerencorderresolver.h"
+#include "integerencodingrecord.h"
+#include "sattranslator.h"
+
+IntegerEncOrderResolver::IntegerEncOrderResolver(CSolver* _solver, IntegerEncodingRecord* _ierecord):
+	solver(_solver),
+	ierecord(_ierecord)
+{
+}
+
+IntegerEncOrderResolver::~IntegerEncOrderResolver() {
+}
+
+
+HappenedBefore IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second){
+	Element* elem1 = ierecord->getOrderIntegerElement(solver, first, false);
+	if(elem1 == NULL)
+		return SATC_UNORDERED;
+	Element* elem2 = ierecord->getOrderIntegerElement(solver, second, false);
+	if(elem2 == NULL)
+		return SATC_UNORDERED;
+	
+	uint64_t val1 = getElementValueSATTranslator(solver, elem1);
+	uint64_t val2 = getElementValueSATTranslator(solver, elem2);
+	return val1 < val2? SATC_FIRST : val1> val2? SATC_SECOND: SATC_UNORDERED;
+}
diff --git a/src/Translator/integerencorderresolver.h b/src/Translator/integerencorderresolver.h
new file mode 100644
index 0000000..e517881
--- /dev/null
+++ b/src/Translator/integerencorderresolver.h
@@ -0,0 +1,24 @@
+
+/* 
+ * File:   integerencorderresolver.h
+ * Author: hamed
+ *
+ * Created on September 1, 2017, 4:58 PM
+ */
+
+#ifndef INTEGERENCORDERRESOLVER_H
+#define INTEGERENCORDERRESOLVER_H
+#include "orderresolver.h"
+
+class IntegerEncOrderResolver : public OrderResolver{
+public:
+	IntegerEncOrderResolver(CSolver* _solver, IntegerEncodingRecord* _ierecord);
+	HappenedBefore resolveOrder(uint64_t first, uint64_t second);
+	virtual ~IntegerEncOrderResolver();
+private:
+	CSolver* solver;
+	IntegerEncodingRecord* ierecord;
+};
+
+#endif /* INTEGERENCORDERRESOLVER_H */
+
-- 
2.34.1