Adding IntegerEncodingResolver ...

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 411ddc9ddafeab489c9ce3e0b368c8d67847562a..f1b99199c802efca86045282238e3799a41bc9c4 100644 (file)
--- 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 42175b30f9e40c0db0fc578970c6760297825244..3bfb2895c1eb4f09270ca1e7b39aa0eb6e57065a 100644 (file)
--- 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 7085cf7f9c5e7d916d2c92d941122f28dc6ba133..abd763fe7db988e9ebf35b95d8cd14ade955da92 100644 (file)
--- 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 2b2f1902b7faf94b192015241f3ebd4fd00941f2..a85e98a27d95c0a4787888941fea90b65918246f 100644 (file)
--- 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 (file)
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 (file)
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 */
+