Adding IntegerEncodingResolver ...
authorHamed <hamed.gorjiara@gmail.com>
Sat, 2 Sep 2017 01:35:58 +0000 (18:35 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Sat, 2 Sep 2017 01:35:58 +0000 (18:35 -0700)
src/ASTTransform/integerencoding.cc
src/ASTTransform/integerencoding.h
src/ASTTransform/integerencodingrecord.cc
src/ASTTransform/integerencodingrecord.h
src/Translator/integerencorderresolver.cc [new file with mode: 0644]
src/Translator/integerencorderresolver.h [new file with mode: 0644]

index 411ddc9..f1b9919 100644 (file)
@@ -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));
 }
 
 
index 42175b3..3bfb289 100644 (file)
@@ -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;
 };
 
index 7085cf7..abd763f 100644 (file)
@@ -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;
 }
 
index 2b2f190..a85e98a 100644 (file)
@@ -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
@@ -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
@@ -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 */
+