Adding DecomposeOrderResolver
authorHamed <hamed.gorjiara@gmail.com>
Fri, 1 Sep 2017 19:39:40 +0000 (12:39 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Fri, 1 Sep 2017 19:39:40 +0000 (12:39 -0700)
17 files changed:
src/AST/order.cc
src/AST/order.h
src/ASTAnalyses/ordergraph.cc
src/ASTAnalyses/ordergraph.h
src/ASTTransform/decomposeordertransform.cc
src/Backend/sattranslator.cc [deleted file]
src/Backend/sattranslator.h [deleted file]
src/Encoders/orderencoding.h
src/Makefile
src/Translator/decomposeorderresolver.cc [new file with mode: 0644]
src/Translator/decomposeorderresolver.h [new file with mode: 0644]
src/Translator/orderresolver.cc [new file with mode: 0644]
src/Translator/orderresolver.h [new file with mode: 0644]
src/Translator/sattranslator.cc [new file with mode: 0644]
src/Translator/sattranslator.h [new file with mode: 0644]
src/classlist.h
src/mymemory.h

index d359ee6..908d691 100644 (file)
@@ -10,7 +10,7 @@ Order::Order(OrderType _type, Set *_set) :
        set(_set),
        orderPairTable(NULL),
        graph(NULL),
-       order(this)
+       encoding(this)
 {
 }
 
@@ -24,7 +24,7 @@ void Order::addOrderConstraint(BooleanOrder *constraint) {
 }
 
 void Order::setOrderEncodingType(OrderEncodingType type) {
-       order.type = type;
+       encoding.type = type;
 }
 
 Order *Order::clone(CSolver *solver, CloneMap *map) {
index ed82695..65291aa 100644 (file)
@@ -18,7 +18,8 @@ public:
        OrderGraph *graph;
        Order *clone(CSolver *solver, CloneMap *map);
        Vector<BooleanOrder *> constraints;
-       OrderEncoding order;
+       OrderEncoding encoding;
+       void setOrderResolver(OrderResolver* _resolver) { encoding.resolver = _resolver;};
        void initializeOrderHashtable();
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);
index fcc9eda..62d4846 100644 (file)
@@ -105,14 +105,17 @@ void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrd
        }
 }
 
-OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
+OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id, bool create) {
        OrderNode *node = new OrderNode(id);
        OrderNode *tmp = nodes->get(node);
        if ( tmp != NULL) {
                delete node;
                node = tmp;
-       } else {
+       } else if(create) {
                nodes->add(node);
+       } else{
+               delete node;
+               return NULL;
        }
        return node;
 }
@@ -123,14 +126,17 @@ OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
        return tmp;
 }
 
-OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end, bool create) {
        OrderEdge *edge = new OrderEdge(begin, end);
        OrderEdge *tmp = edges->get(edge);
        if ( tmp != NULL ) {
                delete edge;
                edge = tmp;
-       } else {
+       } else if (create) {
                edges->add(edge);
+       } else {
+               delete edge;
+               return NULL;
        }
        return edge;
 }
index 5f10c1f..d508d03 100644 (file)
@@ -17,8 +17,8 @@ public:
        ~OrderGraph();
        void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
        void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder);
-       OrderNode *getOrderNodeFromOrderGraph(uint64_t id);
-       OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+       OrderNode *getOrderNodeFromOrderGraph(uint64_t id, bool create = true);
+       OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end, bool create = true);
        OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id);
        OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
        void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
index 262497e..6be7bea 100644 (file)
@@ -13,6 +13,7 @@
 #include "mutableset.h"
 #include "ordergraph.h"
 #include "csolver.h"
+#include "decomposeorderresolver.h"
 
 
 DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver)
@@ -77,7 +78,7 @@ void DecomposeOrderTransform::doTransform(){
                        neworder->addOrderConstraint(orderconstraint);
                }
        }
-
+       currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
                Order *neworder = partialcandidatevec.get(i);
diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc
deleted file mode 100644 (file)
index 766c5c7..0000000
+++ /dev/null
@@ -1,96 +0,0 @@
-#include "sattranslator.h"
-#include "element.h"
-#include "csolver.h"
-#include "satencoder.h"
-#include "set.h"
-#include "order.h"
-#include "orderpair.h"
-
-uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
-       uint index = 0;
-       for (int i = elemEnc->numVars - 1; i >= 0; i--) {
-               index = index << 1;
-               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
-                       index |= 1;
-       }
-       if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
-               model_print("WARNING: Element has undefined value!\n");
-       return elemEnc->encodingArray[index];
-}
-
-uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
-       uint64_t value = 0;
-       for (int i = elemEnc->numVars - 1; i >= 0; i--) {
-               value = value << 1;
-               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) )
-                       value |= 1;
-       }
-       if (elemEnc->isBinaryValSigned &&
-                       This->getSATEncoder()->getCNF()->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
-               //Do sign extension of negative number
-               uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
-               value += highbits;
-       }
-       value += elemEnc->offset;
-       return value;
-}
-
-uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
-       uint index = 0;
-       for (uint i = 0; i < elemEnc->numVars; i++) {
-               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
-                       index = i;
-       }
-       ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
-       return elemEnc->encodingArray[index];
-}
-
-uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
-       uint i;
-       for (i = 0; i < elemEnc->numVars; i++) {
-               if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
-                       break;
-               }
-       }
-
-       return elemEnc->encodingArray[i];
-}
-
-uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
-       ElementEncoding *elemEnc = getElementEncoding(element);
-       if (elemEnc->numVars == 0)//case when the set has only one item
-               return getElementSet(element)->getElement(0);
-       switch (elemEnc->type) {
-       case ONEHOT:
-               return getElementValueOneHotSATTranslator(This, elemEnc);
-       case UNARY:
-               return getElementValueUnarySATTranslator(This, elemEnc);
-       case BINARYINDEX:
-               return getElementValueBinaryIndexSATTranslator(This, elemEnc);
-       case ONEHOTBINARY:
-               ASSERT(0);
-               break;
-       case BINARYVAL:
-               ASSERT(0);
-               break;
-       default:
-               ASSERT(0);
-               break;
-       }
-       return -1;
-}
-
-bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
-       int index = getEdgeVar( ((BooleanVar *) boolean)->var );
-       return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
-}
-
-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 SATC_UNORDERED;
-       return getValueCNF(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
-}
-
diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h
deleted file mode 100644 (file)
index 1d9964f..0000000
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * File:   sattranslator.h
- * Author: hamed
- *
- * Created on July 11, 2017, 5:27 PM
- */
-
-#ifndef SATTRANSLATOR_H
-#define SATTRANSLATOR_H
-
-#include "classlist.h"
-#include "ops.h"
-
-
-bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean);
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second);
-/**
- * most significant bit is represented by variable index 0
- */
-uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc);
-uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc);
-uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc);
-uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc);
-uint64_t getElementValueSATTranslator(CSolver *This, Element *element);
-
-#endif/* SATTRANSLATOR_H */
-
index 4d71805..90a97eb 100644 (file)
@@ -11,7 +11,8 @@ typedef enum OrderEncodingType OrderEncodingType;
 class OrderEncoding {
 public:
        OrderEncoding(Order *order);
-
+       
+       OrderResolver* resolver;
        OrderEncodingType type;
        Order *order;
        CMEMALLOC;
index 5adb178..e6699e6 100644 (file)
@@ -4,16 +4,16 @@ PHONY += directories
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
 
-C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c)
+C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c)
 
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 CFLAGS := -Wall -g -O0
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -ICollections -IBackend -I. -IEncoders -ITuner
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner
 LDFLAGS := -ldl -lrt -rdynamic
 SHARED := -shared
 
@@ -34,6 +34,7 @@ ${OBJ_DIR}:
        ${MKDIR_P} ${OBJ_DIR}/AST
        ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses
        ${MKDIR_P} ${OBJ_DIR}/ASTTransform
+       ${MKDIR_P} ${OBJ_DIR}/Translator
        ${MKDIR_P} ${OBJ_DIR}/Tuner
        ${MKDIR_P} ${OBJ_DIR}/Collections
        ${MKDIR_P} ${OBJ_DIR}/Backend
diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
new file mode 100644 (file)
index 0000000..49d8855
--- /dev/null
@@ -0,0 +1,32 @@
+
+/* 
+ * File:   DecomposeOrderResolver.cc
+ * Author: hamed
+ * 
+ * Created on September 1, 2017, 10:36 AM
+ */
+
+#include "decomposeorderresolver.h"
+#include "order.h"
+#include "ordernode.h"
+#include "ordergraph.h"
+
+DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*>& _orders):
+       OrderResolver(_graph),
+       orders(_orders.getSize(), _orders.expose())
+{
+}
+
+DecomposeOrderResolver::~DecomposeOrderResolver() {
+       delete graph;
+}
+
+HappenedBefore DecomposeOrderResolver::getOrder(OrderNode* from, OrderNode* to){
+       ASSERT(from->id == to->id);
+       // We should ask this query from the suborder ....
+       Order *suborder = NULL;
+       suborder = orders.get(from->sccNum);
+       ASSERT(suborder != NULL);
+       return suborder->encoding.resolver->resolveOrder(from->id, to->id);
+}
+
diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
new file mode 100644 (file)
index 0000000..6a7d735
--- /dev/null
@@ -0,0 +1,28 @@
+
+/* 
+ * File:   DecomposeOrderResolver.h
+ * Author: hamed
+ *
+ * Created on September 1, 2017, 10:36 AM
+ */
+
+#ifndef DECOMPOSEORDERRESOLVER_H
+#define DECOMPOSEORDERRESOLVER_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "orderresolver.h"
+
+class DecomposeOrderResolver : public OrderResolver{
+public:
+       DecomposeOrderResolver(OrderGraph* graph, Vector<Order *> & orders);
+       virtual ~DecomposeOrderResolver();
+private:
+       OrderGraph* graph;
+       Vector<Order*> orders;
+       
+       HappenedBefore getOrder(OrderNode* from, OrderNode* to);
+};
+
+#endif /* DECOMPOSEORDERRESOLVER_H */
+
diff --git a/src/Translator/orderresolver.cc b/src/Translator/orderresolver.cc
new file mode 100644 (file)
index 0000000..5ed3a5e
--- /dev/null
@@ -0,0 +1,39 @@
+#include "orderresolver.h"
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "orderedge.h"
+
+OrderResolver::OrderResolver(OrderGraph* _graph)
+       :graph(_graph)
+{
+}
+
+OrderResolver::~OrderResolver(){
+       delete graph;
+}
+
+HappenedBefore OrderResolver::resolveOrder(uint64_t first, uint64_t second){
+       OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
+       if(from == NULL){
+               return SATC_UNORDERED;
+       }
+       OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
+       if(from == NULL){
+               return SATC_UNORDERED;
+       }
+       if (from->sccNum != to->sccNum) {
+               OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
+               if (edge != NULL && edge->mustPos){
+                       return SATC_FIRST;
+               } else if( edge != NULL && edge->mustNeg){
+                       return SATC_SECOND;
+               }else {
+                       ASSERT(0);
+                       //It's a case that either there's no edge, or there is an edge
+                       // but we don't know the value! (This case shouldn't happen)
+                       //return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND;
+               }
+       } else {
+               return getOrder(from, to);
+       }
+}
\ No newline at end of file
diff --git a/src/Translator/orderresolver.h b/src/Translator/orderresolver.h
new file mode 100644 (file)
index 0000000..9f248af
--- /dev/null
@@ -0,0 +1,27 @@
+
+/* 
+ * File:   orderresolver.h
+ * Author: hamed
+ *
+ * Created on August 31, 2017, 7:16 PM
+ */
+
+#ifndef ORDERRESOLVER_H
+#define ORDERRESOLVER_H
+#include "classlist.h"
+#include "structs.h"
+#include "mymemory.h"
+
+class OrderResolver {
+public:
+       OrderResolver(OrderGraph* _graph);
+       HappenedBefore resolveOrder(uint64_t first, uint64_t second);
+       virtual ~OrderResolver();
+       CMEMALLOC;
+protected:
+       OrderGraph* graph;
+       virtual HappenedBefore getOrder(OrderNode* from, OrderNode* to) = 0;
+};
+
+#endif /* ORDERRESOLVER_H */
+
diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
new file mode 100644 (file)
index 0000000..766c5c7
--- /dev/null
@@ -0,0 +1,96 @@
+#include "sattranslator.h"
+#include "element.h"
+#include "csolver.h"
+#include "satencoder.h"
+#include "set.h"
+#include "order.h"
+#include "orderpair.h"
+
+uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint index = 0;
+       for (int i = elemEnc->numVars - 1; i >= 0; i--) {
+               index = index << 1;
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
+                       index |= 1;
+       }
+       if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
+               model_print("WARNING: Element has undefined value!\n");
+       return elemEnc->encodingArray[index];
+}
+
+uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint64_t value = 0;
+       for (int i = elemEnc->numVars - 1; i >= 0; i--) {
+               value = value << 1;
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) )
+                       value |= 1;
+       }
+       if (elemEnc->isBinaryValSigned &&
+                       This->getSATEncoder()->getCNF()->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
+               //Do sign extension of negative number
+               uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+               value += highbits;
+       }
+       value += elemEnc->offset;
+       return value;
+}
+
+uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint index = 0;
+       for (uint i = 0; i < elemEnc->numVars; i++) {
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
+                       index = i;
+       }
+       ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
+       return elemEnc->encodingArray[index];
+}
+
+uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint i;
+       for (i = 0; i < elemEnc->numVars; i++) {
+               if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+                       break;
+               }
+       }
+
+       return elemEnc->encodingArray[i];
+}
+
+uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
+       ElementEncoding *elemEnc = getElementEncoding(element);
+       if (elemEnc->numVars == 0)//case when the set has only one item
+               return getElementSet(element)->getElement(0);
+       switch (elemEnc->type) {
+       case ONEHOT:
+               return getElementValueOneHotSATTranslator(This, elemEnc);
+       case UNARY:
+               return getElementValueUnarySATTranslator(This, elemEnc);
+       case BINARYINDEX:
+               return getElementValueBinaryIndexSATTranslator(This, elemEnc);
+       case ONEHOTBINARY:
+               ASSERT(0);
+               break;
+       case BINARYVAL:
+               ASSERT(0);
+               break;
+       default:
+               ASSERT(0);
+               break;
+       }
+       return -1;
+}
+
+bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
+       int index = getEdgeVar( ((BooleanVar *) boolean)->var );
+       return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+}
+
+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 SATC_UNORDERED;
+       return getValueCNF(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
+}
+
diff --git a/src/Translator/sattranslator.h b/src/Translator/sattranslator.h
new file mode 100644 (file)
index 0000000..1d9964f
--- /dev/null
@@ -0,0 +1,27 @@
+/*
+ * File:   sattranslator.h
+ * Author: hamed
+ *
+ * Created on July 11, 2017, 5:27 PM
+ */
+
+#ifndef SATTRANSLATOR_H
+#define SATTRANSLATOR_H
+
+#include "classlist.h"
+#include "ops.h"
+
+
+bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean);
+HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second);
+/**
+ * most significant bit is represented by variable index 0
+ */
+uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc);
+uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc);
+uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc);
+uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc);
+uint64_t getElementValueSATTranslator(CSolver *This, Element *element);
+
+#endif/* SATTRANSLATOR_H */
+
index e8ab113..d56a650 100644 (file)
@@ -13,6 +13,7 @@
 #include "mymemory.h"
 #include <inttypes.h>
 #include "classes.h"
+#include "AST/astnode.h"
 
 
 class BooleanOrder;
@@ -59,6 +60,9 @@ class TunableSetting;
 
 class TunableDesc;
 
+class OrderResolver;
+class DecomposeOrderResolver;
+
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
index 09ea7cd..8ad874b 100644 (file)
@@ -24,7 +24,8 @@
    void ourfree(void *ptr);
    void * ourcalloc(size_t count, size_t size);
    void * ourrealloc(void *ptr, size_t size);
- */
+*/
+ /* 
 void * model_malloc(size_t size);
 void model_free(void *ptr);
 void * model_calloc(size_t count, size_t size);
@@ -35,11 +36,12 @@ void * model_realloc(void *ptr, size_t size);
 #define ourfree model_free
 #define ourrealloc model_realloc
 #define ourcalloc model_calloc
-/*
+*/
+
 static inline void *ourmalloc(size_t size) { return malloc(size); }
 static inline void ourfree(void *ptr) { free(ptr); }
 static inline void *ourcalloc(size_t count, size_t size) { return calloc(count, size); }
-static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }*/
+static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
 
 #define CMEMALLOC                           \
        void *operator new(size_t size) {       \