set(_set),
orderPairTable(NULL),
graph(NULL),
- order(this)
+ encoding(this)
{
}
}
void Order::setOrderEncodingType(OrderEncodingType type) {
- order.type = type;
+ encoding.type = type;
}
Order *Order::clone(CSolver *solver, CloneMap *map) {
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);
}
}
-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;
}
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;
}
~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);
#include "mutableset.h"
#include "ordergraph.h"
#include "csolver.h"
+#include "decomposeorderresolver.h"
DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver)
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);
+++ /dev/null
-#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;
-}
-
+++ /dev/null
-/*
- * 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 */
-
class OrderEncoding {
public:
OrderEncoding(Order *order);
-
+
+ OrderResolver* resolver;
OrderEncodingType type;
Order *order;
CMEMALLOC;
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
${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
--- /dev/null
+
+/*
+ * 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);
+}
+
--- /dev/null
+
+/*
+ * 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 */
+
--- /dev/null
+#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
--- /dev/null
+
+/*
+ * 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 */
+
--- /dev/null
+#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;
+}
+
--- /dev/null
+/*
+ * 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 */
+
#include "mymemory.h"
#include <inttypes.h>
#include "classes.h"
+#include "AST/astnode.h"
class BooleanOrder;
class TunableDesc;
+class OrderResolver;
+class DecomposeOrderResolver;
+
struct IncrementalSolver;
typedef struct IncrementalSolver IncrementalSolver;
struct TableEntry;
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);
#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) { \
projects / satune.git / commitdiff