enum PredicateType {TABLEPRED, OPERATORPRED};
typedef enum PredicateType PredicateType;
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST, BOOLEANEDGE, ORDERTYPE, SETTYPE};
+enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST,
+ BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE};
typedef enum ASTNodeType ASTNodeType;
enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3};
typedef enum BooleanValue BooleanValue;
+enum ElementEncodingType {
+ ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, BINARYVAL
+};
+
+typedef enum ElementEncodingType ElementEncodingType;
+
+
#endif
return;
serializer->addObject(this);
order->serialize(serializer);
+
serializer->mywrite(&type, sizeof(ASTNodeType));
BooleanOrder* This = this;
serializer->mywrite(&This, sizeof(BooleanOrder*));
}
void BooleanPredicate::serialize(Serializer* serializer){
- ASSERT(0);
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ predicate->serialize(serializer);
+ uint size = inputs.getSize();
+ for(uint i=0; i<size; i++){
+ Element* input = inputs.get(i);
+ input->serialize(serializer);
+ }
+ serializeBooleanEdge(serializer, undefStatus);
+
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ BooleanPredicate* This = this;
+ serializer->mywrite(&This, sizeof(BooleanPredicate*));
+ serializer->mywrite(&predicate, sizeof(Predicate *));
+ serializer->mywrite(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ Element *input = inputs.get(i);
+ serializer->mywrite(&input, sizeof(Element *));
+ }
+ Boolean* undefStat = undefStatus!= BooleanEdge(NULL)?undefStatus.getRaw() : NULL;
+ serializer->mywrite(&undefStat, sizeof(Boolean*));
}
void BooleanLogic::serialize(Serializer* serializer){
- ASSERT(0);
-}
\ No newline at end of file
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+ uint size = inputs.getSize();
+ for(uint i=0; i<size; i++){
+ BooleanEdge input = inputs.get(i);
+ serializeBooleanEdge(serializer, input);
+ }
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ BooleanLogic* This = this;
+ serializer->mywrite(&This, sizeof(BooleanLogic*));
+ serializer->mywrite(&op, sizeof(LogicOp));
+ serializer->mywrite(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ Boolean* input = inputs.get(i).getRaw();
+ serializer->mywrite(&input, sizeof(Boolean*));
+ }
+}
+
#include "astnode.h"
#include "functionencoding.h"
#include "constraint.h"
-#include "serializable.h"
#include "serializer.h"
-class Boolean : public ASTNode, public Serializable {
+class Boolean : public ASTNode {
public:
Boolean(ASTNodeType _type);
virtual ~Boolean() {}
public:
BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus);
Boolean *clone(CSolver *solver, CloneMap *map);
+ Predicate *getPredicate() {return predicate;}
+ FunctionEncoding *getFunctionEncoding() {return &encoding;}
+ void updateParents();
void serialize(Serializer *serializer );
+
+ CMEMALLOC;
Predicate *predicate;
FunctionEncoding encoding;
Array<Element *> inputs;
BooleanEdge undefStatus;
- FunctionEncoding *getFunctionEncoding() {return &encoding;}
- void updateParents();
-
- CMEMALLOC;
};
class BooleanLogic : public Boolean {
Set * ElementFunction::getRange() {
return function->getRange();
}
+
+void ElementSet::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ set->serialize(serializer);
+
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ ElementSet *This = this;
+ serializer->mywrite(&This, sizeof(ElementSet*));
+ serializer->mywrite(&set, sizeof(Set*));
+}
+
+void ElementConst::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ set->serialize(serializer);
+
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ ElementSet *This = this;
+ serializer->mywrite(&This, sizeof(ElementSet*));
+ VarType type = set->getType();
+ serializer->mywrite(&type, sizeof(VarType));
+ serializer->mywrite(&value, sizeof(uint64_t));
+}
+
+void ElementFunction::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ function->serialize(serializer);
+ uint size = inputs.getSize();
+ for(uint i=0; i<size; i++){
+ Element *input = inputs.get(i);
+ input->serialize(serializer);
+ }
+ serializeBooleanEdge(serializer, overflowstatus);
+
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ ElementFunction *This = this;
+ serializer->mywrite(&This, sizeof(ElementFunction *));
+ serializer->mywrite(&function, sizeof(Function *));
+ serializer->mywrite(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ Element* input = inputs.get(i);
+ serializer->mywrite(&input, sizeof(Element*));
+ }
+ Boolean* overflowstat = overflowstatus.getRaw();
+ serializer->mywrite(&overflowstat, sizeof(Boolean*));
+}
+
Vector<ASTNode *> parents;
ElementEncoding encoding;
virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
+ virtual void serialize(Serializer* serializer) =0;
virtual void updateParents() {}
virtual Set * getRange() = 0;
CMEMALLOC;
ElementSet(ASTNodeType type, Set *s);
ElementSet(Set *s);
virtual Element *clone(CSolver *solver, CloneMap *map);
+ virtual void serialize(Serializer* serializer);
CMEMALLOC;
Set *getRange() {return set;}
- private:
+ protected:
Set *set;
};
public:
ElementConst(uint64_t value, Set *_set);
uint64_t value;
+ virtual void serialize(Serializer* serializer);
Element *clone(CSolver *solver, CloneMap *map);
CMEMALLOC;
};
BooleanEdge overflowstatus;
FunctionEncoding functionencoding;
Element *clone(CSolver *solver, CloneMap *map);
+ virtual void serialize(Serializer* serializer);
Set * getRange();
void updateParents();
Function * getFunction() {return function;}
#include "table.h"
#include "set.h"
#include "csolver.h"
+#include "serializer.h"
FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) :
Function(OPERATORFUNC),
Set * FunctionTable::getRange() {
return table->getRange();
}
+
+void FunctionTable::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ table->serialize(serializer);
+
+ ASTNodeType type = FUNCTABLETYPE;
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ FunctionTable* This = this;
+ serializer->mywrite(&This, sizeof(FunctionTable*));
+ serializer->mywrite(&table, sizeof(Table *));
+ serializer->mywrite(&undefBehavior, sizeof(UndefinedBehavior));
+
+}
+
+void FunctionOperator::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ uint size = domains.getSize();
+ for(uint i=0; i<size; i++){
+ Set* domain = domains.get(i);
+ domain->serialize(serializer);
+ }
+ range->serialize(serializer);
+
+ ASTNodeType nodeType = FUNCOPTYPE;
+ serializer->mywrite(&nodeType, sizeof(ASTNodeType));
+ FunctionOperator* This = this;
+ serializer->mywrite(&This, sizeof(FunctionOperator*));
+ serializer->mywrite(&op, sizeof(ArithOp));
+ serializer->mywrite(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ Set *domain = domains.get(i);
+ serializer->mywrite(&domain, sizeof(Set *));
+ }
+ serializer->mywrite(&range, sizeof(Set *));
+ serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior));
+}
\ No newline at end of file
FunctionType type;
virtual ~Function() {}
virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
+ virtual void serialize(Serializer* serialiezr) =0;
virtual Set * getRange() = 0;
CMEMALLOC;
};
uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
bool isInRangeFunction(uint64_t val);
Function *clone(CSolver *solver, CloneMap *map);
+ virtual void serialize(Serializer* serialiezr);
Set * getRange() {return range;}
CMEMALLOC;
};
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
Function *clone(CSolver *solver, CloneMap *map);
+ virtual void serialize(Serializer* serialiezr);
Set * getRange();
CMEMALLOC;
};
#include "orderencoding.h"
#include "boolean.h"
#include "orderpair.h"
-#include "serializable.h"
-class Order : public Serializable {
+class Order{
public:
Order(OrderType type, Set *set);
virtual ~Order();
#include "table.h"
#include "csolver.h"
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) {
+PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), domains(domain, numDomain), op(_op) {
}
PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
map->put(this, p);
return p;
}
+
+void PredicateTable::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ table->serialize(serializer);
+
+ ASTNodeType type = PREDTABLETYPE;
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ PredicateTable* This = this;
+ serializer->mywrite(&This, sizeof(PredicateTable*));
+ serializer->mywrite(&table, sizeof(Table *));
+ serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior));
+}
+
+void PredicateOperator::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ uint size = domains.getSize();
+ for(uint i=0; i<size; i++){
+ Set* domain = domains.get(i);
+ domain->serialize(serializer);
+ }
+
+ ASTNodeType type = PREDOPERTYPE;
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ PredicateOperator* This = this;
+ serializer->mywrite(&This, sizeof(PredicateOperator*));
+ serializer->mywrite(&op, sizeof(CompOp));
+ serializer->mywrite(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ Set* domain = domains.get(i);
+ serializer->mywrite(&domain, sizeof(Set*));
+ }
+}
+
Predicate(PredicateType _type) : type(_type) {}
virtual ~Predicate() {}
virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
+ virtual void serialize(Serializer* serializer) = 0;
PredicateType type;
CMEMALLOC;
};
PredicateOperator(CompOp op, Set **domain, uint numDomain);
bool evalPredicateOperator(uint64_t *inputs);
Predicate *clone(CSolver *solver, CloneMap *map);
- CompOp op;
+ virtual void serialize(Serializer* serializer);
Array<Set *> domains;
+ CompOp getOp() {return op;}
CMEMALLOC;
+ private:
+ CompOp op;
};
class PredicateTable : public Predicate {
public:
PredicateTable(Table *table, UndefinedBehavior undefBehavior);
Predicate *clone(CSolver *solver, CloneMap *map);
+ virtual void serialize(Serializer* serializer);
Table *table;
UndefinedBehavior undefinedbehavior;
CMEMALLOC;
#include "classlist.h"
#include "structs.h"
#include "mymemory.h"
-#include "serializable.h"
-class Set : public Serializable {
+class Set {
public:
Set(VarType t);
Set(VarType t, uint64_t *elements, uint num);
#include "set.h"
#include "mutableset.h"
#include "csolver.h"
+#include "serializer.h"
Table::Table(Set **_domains, uint numDomain, Set *_range) :
domains(_domains, numDomain),
delete entries;
}
+
+
+void Table::serialize(Serializer* serializer){
+ if(serializer->isSerialized(this))
+ return;
+ serializer->addObject(this);
+
+ uint size = domains.getSize();
+ for(uint i=0; i<size; i++){
+ Set* domain = domains.get(i);
+ domain->serialize(serializer);
+ }
+ if(range!= NULL)
+ range->serialize(serializer);
+
+ ASTNodeType type = TABLETYPE;
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ Table* This = this;
+ serializer->mywrite(&This, sizeof(Table*));
+ serializer->mywrite(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ Set* domain = domains.get(i);
+ serializer->mywrite(&domain, sizeof(Set*));
+ }
+ serializer->mywrite(&range, sizeof(Set*));
+ size = entries->getSize();
+ serializer->mywrite(&size, sizeof(uint));
+ SetIteratorTableEntry* iterator = getEntries();
+ while(iterator->hasNext()){
+ TableEntry* entry = iterator->next();
+ serializer->mywrite(&entry->output, sizeof(uint64_t));
+ serializer->mywrite(&entry->inputSize, sizeof(uint));
+ serializer->mywrite(entry->inputs, sizeof(uint64_t) * entry->inputSize);
+ }
+ delete iterator;
+}
+
+
void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result);
TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
Table *clone(CSolver *solver, CloneMap *map);
+ void serialize(Serializer *serializer);
~Table();
Set * getRange() {return range;}
#include "iterator.h"
#include "element.h"
#include "function.h"
+#include "predicate.h"
+#include "set.h"
+#include "csolver.h"
+#include "tunable.h"
EncodingGraph::EncodingGraph(CSolver * _solver) :
solver(_solver) {
}
}
+void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
+ EncodingSubGraph *graph1=graphMap.get(first);
+ EncodingSubGraph *graph2=graphMap.get(second);
+ if (graph1 == NULL && graph2 == NULL) {
+ graph1 = new EncodingSubGraph();
+ graphMap.put(first, graph1);
+ graph1->addNode(first);
+ }
+ if (graph1 == NULL && graph2 != NULL) {
+ graph1 = graph2;
+ graph2 = NULL;
+ EncodingNode *tmp = second;
+ second = first;
+ first = tmp;
+ }
+ if (graph1 != NULL && graph2 != NULL) {
+ SetIteratorEncodingNode * nodeit=graph2->nodeIterator();
+ while(nodeit->hasNext()) {
+ EncodingNode *node=nodeit->next();
+ graph1->addNode(node);
+ graphMap.put(node, graph1);
+ }
+ delete nodeit;
+ delete graph2;
+ } else {
+ ASSERT(graph1 != NULL && graph2 == NULL);
+ graph1->addNode(second);
+ graphMap.put(second, graph1);
+ }
+}
+
void EncodingGraph::processElement(Element *e) {
uint size=e->parents.getSize();
for(uint i=0;i<size;i++) {
Function *f=ef->getFunction();
if (f->type==OPERATORFUNC) {
FunctionOperator *fo=(FunctionOperator*)f;
- ArithOp op=fo->op;
+ ASSERT(ef->inputs.getSize() == 2);
+ EncodingNode *left=createNode(ef->inputs.get(0));
+ EncodingNode *right=createNode(ef->inputs.get(1));
+ if (left == NULL && right == NULL)
+ return;
+ EncodingNode *dst=createNode(ef);
+ EncodingEdge *edge=getEdge(left, right, dst);
+ edge->numArithOps++;
}
}
void EncodingGraph::processPredicate(BooleanPredicate *b) {
+ Predicate *p=b->getPredicate();
+ if (p->type==OPERATORPRED) {
+ PredicateOperator *po=(PredicateOperator *)p;
+ ASSERT(b->inputs.getSize()==2);
+ EncodingNode *left=createNode(b->inputs.get(0));
+ EncodingNode *right=createNode(b->inputs.get(1));
+ if (left == NULL || right == NULL)
+ return;
+ EncodingEdge *edge=getEdge(left, right, NULL);
+ CompOp op=po->getOp();
+ switch(op) {
+ case SATC_EQUALS:
+ edge->numEquals++;
+ break;
+ case SATC_LT:
+ case SATC_LTE:
+ case SATC_GT:
+ case SATC_GTE:
+ edge->numComparisons++;
+ break;
+ default:
+ ASSERT(0);
+ }
+ }
+}
+
+static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
+
+EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+ EncodingEdge e(left, right, dst);
+ EncodingEdge *result = edgeMap.get(&e);
+ if (result == NULL) {
+ result=new EncodingEdge(left, right, dst);
+ VarType v1=left->getType();
+ VarType v2=right->getType();
+ if (v1 > v2) {
+ VarType tmp=v2;
+ v2=v1;
+ v1=tmp;
+ }
+ result->setEncoding((EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc));
+ edgeMap.put(result, result);
+ }
+ return result;
+}
+
+EncodingNode::EncodingNode(Set *_s) :
+ s(_s),
+ numElements(0) {
+}
+
+uint EncodingNode::getSize() {
+ return s->getSize();
+}
+VarType EncodingNode::getType() {
+ return s->getType();
}
+static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+
EncodingNode * EncodingGraph::createNode(Element *e) {
+ if (e->type == ELEMCONST)
+ return NULL;
Set *s = e->getRange();
EncodingNode *n = encodingMap.get(s);
if (n == NULL) {
n = new EncodingNode(s);
+ n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
encodingMap.put(s, n);
}
n->addElement(e);
+ if (discovered.add(e))
+ n->numElements++;
return n;
}
EncodingEdge::EncodingEdge(EncodingNode *_l, EncodingNode *_r) :
left(_l),
right(_r),
- dst(NULL)
+ dst(NULL),
+ encoding(EDGE_UNASSIGNED),
+ numArithOps(0),
+ numEquals(0),
+ numComparisons(0)
{
}
EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNode *_dst) :
left(_left),
right(_right),
- dst(_dst)
+ dst(_dst),
+ encoding(EDGE_UNASSIGNED),
+ numArithOps(0),
+ numEquals(0),
+ numComparisons(0)
{
}
bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2) {
return e1->left == e2->left && e1->right == e2->right && e1->dst == e2->dst;
}
+
+EncodingSubGraph::EncodingSubGraph() {
+}
+
+void EncodingSubGraph::addNode(EncodingNode *n) {
+ nodes.add(n);
+ Set *s=n->s;
+ uint size=s->getSize();
+ for(uint i=0; i<size; i++) {
+ uint64_t val=s->getElement(i);
+ values.add(val);
+ }
+}
+
+SetIteratorEncodingNode * EncodingSubGraph::nodeIterator() {
+ return nodes.iterator();
+}
uint hashEncodingEdge(EncodingEdge *edge);
bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
+class EncodingSubGraph;
+
typedef Hashtable<EncodingEdge *, EncodingEdge *, uintptr_t, PTRSHIFT, hashEncodingEdge, equalsEncodingEdge> HashtableEdge;
+typedef Hashset<EncodingNode *, uintptr_t, PTRSHIFT> HashsetEncodingNode;
+typedef SetIterator<EncodingNode *, uintptr_t, PTRSHIFT> SetIteratorEncodingNode;
+typedef Hashtable<EncodingNode *, EncodingSubGraph *, uintptr_t, PTRSHIFT> HashtableNodeToSubGraph;
class EncodingGraph {
public:
CSolver * solver;
HashtableEncoding encodingMap;
HashtableEdge edgeMap;
+ HashsetElement discovered;
+ HashtableNodeToSubGraph graphMap;
+
+
+ void mergeNodes(EncodingNode *first, EncodingNode *second);
void processElement(Element *e);
void processFunction(ElementFunction *f);
void processPredicate(BooleanPredicate *b);
EncodingNode * createNode(Element *e);
-
+ EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
};
class EncodingNode {
public:
EncodingNode(Set *_s);
void addElement(Element *e);
+ uint getSize();
+ VarType getType();
+ void setEncoding(ElementEncodingType e) {encoding=e;}
+
CMEMALLOC;
private:
Set *s;
HashsetElement elements;
+ uint numElements;
+ ElementEncodingType encoding;
+ friend class EncodingGraph;
+ friend class EncodingSubGraph;
};
+class EncodingSubGraph {
+ public:
+ EncodingSubGraph();
+ void addNode(EncodingNode *n);
+ SetIteratorEncodingNode * nodeIterator();
+
+ CMEMALLOC;
+ private:
+ HashsetEncodingNode nodes;
+ Hashset64Int values;
+};
+
+enum EdgeEncodingType { EDGE_UNASSIGNED, EDGE_BREAK, EDGE_MATCH};
+typedef enum EdgeEncodingType EdgeEncodingType;
+
class EncodingEdge {
public:
EncodingEdge(EncodingNode *_l, EncodingNode *_r);
EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
+ void setEncoding(EdgeEncodingType e) {encoding=e;}
CMEMALLOC;
+
private:
EncodingNode *left;
EncodingNode *right;
EncodingNode *dst;
+ EdgeEncodingType encoding;
+ uint numArithOps;
+ uint numEquals;
+ uint numComparisons;
friend uint hashEncodingEdge(EncodingEdge *edge);
friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
-
+ friend class EncodingGraph;
};
+
#endif
return getElementValueUnaryConstraint(elem, value);
case BINARYINDEX:
return getElementValueBinaryIndexConstraint(elem, value);
- case ONEHOTBINARY:
- ASSERT(0);
- break;
case BINARYVAL:
return getElementValueBinaryValueConstraint(elem, value);
break;
case UNARY:
generateUnaryEncodingVars(encoding);
return;
- case ONEHOTBINARY:
- return;
case BINARYVAL:
generateBinaryValueEncodingVars(encoding);
return;
ElementEncoding *ee1 = getElementEncoding(elem1);
ASSERT(ee0->numVars == ee1->numVars);
uint numVars = ee0->numVars;
- switch (predicate->op) {
+ switch (predicate->getOp()) {
case SATC_EQUALS:
return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
case SATC_LT:
typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
+typedef Hashset<uint64_t, uint64_t, 0> Hashset64Int;
+
typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, PTRSHIFT> HashtableNodeToNodeSet;
typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, PTRSHIFT, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
typedef Hashtable<Set *, EncodingNode *, uintptr_t, PTRSHIFT> HashtableEncoding;
+
typedef SetIterator<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
typedef SetIterator<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
typedef SetIterator<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
#include "naiveencoder.h"
#include "constraint.h"
-enum ElementEncodingType {
- ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
-};
-
-typedef enum ElementEncodingType ElementEncodingType;
-
class ElementEncoding {
public:
ElementEncoding(Element *element);
#include "csolver.h"
#include "unistd.h"
#include "fcntl.h"
+#include "predicate.h"
+#include "table.h"
+#include "element.h"
Deserializer::Deserializer(const char* file):
solver(new CSolver())
Deserializer::~Deserializer() {
delete solver;
+
+ if (-1 == close(filedesc)){
+ exit(-1);
+ }
}
ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
case SETTYPE:
deserializeSet();
break;
+ case LOGICOP:
+ deserializeBooleanLogic();
+ break;
+ case PREDICATEOP:
+ deserializeBooleanPredicate();
+ break;
+ case PREDTABLETYPE:
+ deserializePredicateTable();
+ break;
+ case PREDOPERTYPE:
+ deserializePredicateOperator();
+ break;
+ case TABLETYPE:
+ deserializeTable();
+ break;
+ case ELEMSET:
+ deserializeElementSet();
+ break;
+ case ELEMCONST:
+ deserializeElementConst();
+ break;
+ case ELEMFUNCRETURN:
+ deserializeElementFunction();
+ break;
+ case FUNCOPTYPE:
+ deserializeFunctionOperator();
+ break;
+ case FUNCTABLETYPE:
+ deserializeFunctionTable();
+ break;
default:
ASSERT(0);
}
void Deserializer::deserializeBooleanOrder(){
BooleanOrder* bo_ptr;
myread(&bo_ptr, sizeof(BooleanOrder*));
- Order* optr;
- myread(&optr, sizeof(Order*));
+ Order* order;
+ myread(&order, sizeof(Order*));
+ ASSERT(map.contains(order));
+ order = (Order*) map.get(order);
uint64_t first;
myread(&first, sizeof(uint64_t));
uint64_t second;
myread(&second, sizeof(uint64_t));
- ASSERT(map.contains(optr));
- Order* order = (Order*) map.get(optr);
map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
}
solver->createSet(type, members.expose(), size);
map.put(s_ptr, set);
}
+
+void Deserializer::deserializeBooleanLogic(){
+ BooleanLogic *bl_ptr;
+ myread(&bl_ptr, sizeof(BooleanLogic *));
+ LogicOp op;
+ myread(&op, sizeof(LogicOp));
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<BooleanEdge> members;
+ for(uint i=0; i<size; i++){
+ Boolean* member;
+ myread(&member, sizeof(Boolean *));
+ BooleanEdge tmp(member);
+ bool isNegated = tmp.isNegated();
+ ASSERT(map.contains(tmp.getBoolean()));
+ member = (Boolean*) map.get(tmp.getBoolean());
+ BooleanEdge res(member);
+ members.push( isNegated?res.negate():res );
+ }
+ map.put(bl_ptr, solver->applyLogicalOperation(op, members.expose(), size).getBoolean());
+}
+
+void Deserializer::deserializeBooleanPredicate(){
+ BooleanPredicate *bp_ptr;
+ myread(&bp_ptr, sizeof(BooleanPredicate *));
+ Predicate* predicate;
+ myread(&predicate, sizeof(Predicate*));
+ ASSERT(map.contains(predicate));
+ predicate = (Predicate*) map.get(predicate);
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<Element*> members;
+ for(uint i=0; i<size; i++){
+ Element* input;
+ myread(&input, sizeof(Element *));
+ ASSERT(map.contains(input));
+ input = (Element*) map.get(input);
+ members.push(input);
+ }
+
+ Boolean* stat_ptr;
+ myread(&stat_ptr, sizeof(Boolean *));
+ BooleanEdge undefStatus;
+ if(stat_ptr != NULL){
+ BooleanEdge tmp(stat_ptr);
+ bool isNegated = tmp.isNegated();
+ ASSERT(map.contains(tmp.getBoolean()));
+ stat_ptr = (Boolean*) map.get(tmp.getBoolean());
+ BooleanEdge res(stat_ptr);
+ undefStatus = isNegated?res.negate():res;
+ } else {
+ undefStatus = NULL;
+ }
+ map.put(bp_ptr, solver->applyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean());
+}
+
+void Deserializer::deserializePredicateTable(){
+ PredicateTable *pt_ptr;
+ myread(&pt_ptr, sizeof(PredicateTable *));
+ Table* table;
+ myread(&table, sizeof(Table*));
+ ASSERT(map.contains(table));
+ table = (Table*) map.get(table);
+ UndefinedBehavior undefinedbehavior;
+ myread(&undefinedbehavior, sizeof(UndefinedBehavior));
+
+ map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior));
+}
+
+void Deserializer::deserializePredicateOperator(){
+ PredicateOperator *po_ptr;
+ myread(&po_ptr, sizeof(PredicateOperator *));
+ CompOp op;
+ myread(&op, sizeof(CompOp));
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<Set*> domains;
+ for(uint i=0; i<size; i++){
+ Set* domain;
+ myread(&domain, sizeof(Set*));
+ ASSERT(map.contains(domain));
+ domain = (Set*) map.get(domain);
+ domains.push(domain);
+ }
+
+ map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
+}
+
+void Deserializer::deserializeTable(){
+ Table *t_ptr;
+ myread(&t_ptr, sizeof(Table *));
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<Set*> domains;
+ for(uint i=0; i<size; i++){
+ Set* domain;
+ myread(&domain, sizeof(Set*));
+ ASSERT(map.contains(domain));
+ domain = (Set*) map.get(domain);
+ domains.push(domain);
+ }
+ Set* range;
+ myread(&range, sizeof(Set*));
+ if(range != NULL){
+ ASSERT(map.contains(range));
+ range = (Set*) map.get(range);
+ }
+ Table* table = solver->createTable(domains.expose(), size, range);
+ myread(&size, sizeof(uint));
+ for(uint i=0; i<size; i++){
+ uint64_t output;
+ myread(&output, sizeof(uint64_t));
+ uint inputSize;
+ myread(&inputSize, sizeof(uint));
+ Vector<uint64_t> inputs;
+ inputs.setSize(inputSize);
+ myread(inputs.expose(), sizeof(uint64_t)*inputSize);
+ table->addNewTableEntry(inputs.expose(), inputSize, output);
+ }
+
+ map.put(t_ptr, table);
+}
+
+
+void Deserializer::deserializeElementSet(){
+ ElementSet* es_ptr;
+ myread(&es_ptr, sizeof(ElementSet*));
+ Set * set;
+ myread(&set, sizeof(Set *));
+ ASSERT(map.contains(set));
+ set = (Set*) map.get(set);
+ map.put(es_ptr, solver->getElementVar(set));
+}
+
+void Deserializer::deserializeElementConst(){
+ ElementSet* es_ptr;
+ myread(&es_ptr, sizeof(ElementSet*));
+ VarType type;
+ myread(&type, sizeof(VarType));
+ uint64_t value;
+ myread(&value, sizeof(uint64_t));
+ map.put(es_ptr, solver->getElementConst(type, value));
+}
+
+void Deserializer::deserializeElementFunction(){
+ ElementFunction *ef_ptr;
+ myread(&ef_ptr, sizeof(ElementFunction *));
+ Function *function;
+ myread(&function, sizeof(Function*));
+ ASSERT(map.contains(function));
+ function = (Function*) map.get(function);
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<Element*> members;
+ for(uint i=0; i<size; i++){
+ Element* input;
+ myread(&input, sizeof(Element *));
+ ASSERT(map.contains(input));
+ input = (Element*) map.get(input);
+ members.push(input);
+ }
+
+ Boolean* overflowstatus;
+ myread(&overflowstatus, sizeof(Boolean *));
+ BooleanEdge tmp(overflowstatus);
+ bool isNegated = tmp.isNegated();
+ ASSERT(map.contains(tmp.getBoolean()));
+ overflowstatus = (Boolean*) map.get(tmp.getBoolean());
+ BooleanEdge res(overflowstatus);
+ BooleanEdge undefStatus = isNegated?res.negate():res;
+
+ map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
+}
+
+
+void Deserializer::deserializeFunctionOperator(){
+ FunctionOperator *fo_ptr;
+ myread(&fo_ptr, sizeof(FunctionOperator *));
+ ArithOp op;
+ myread(&op, sizeof(ArithOp));
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<Set*> domains;
+ for(uint i=0; i<size; i++){
+ Set* domain;
+ myread(&domain, sizeof(Set*));
+ ASSERT(map.contains(domain));
+ domain = (Set*) map.get(domain);
+ domains.push(domain);
+ }
+ Set* range;
+ myread(&range, sizeof(Set*));
+ ASSERT(map.contains(range));
+ range = (Set*) map.get(range);
+ OverFlowBehavior overflowbehavior;
+ myread(&overflowbehavior, sizeof(OverFlowBehavior));
+ map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
+}
+
+void Deserializer::deserializeFunctionTable(){
+ FunctionTable *ft_ptr;
+ myread(&ft_ptr, sizeof(FunctionTable *));
+ Table* table;
+ myread(&table, sizeof(Table*));
+ ASSERT(map.contains(table));
+ table = (Table*) map.get(table);
+ UndefinedBehavior undefinedbehavior;
+ myread(&undefinedbehavior, sizeof(UndefinedBehavior));
+
+ map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
+}
\ No newline at end of file
void deserializeBooleanOrder();
void deserializeOrder();
void deserializeSet();
+ void deserializeBooleanLogic();
+ void deserializeBooleanPredicate();
+ void deserializePredicateTable();
+ void deserializePredicateOperator();
+ void deserializeTable();
+ void deserializeElementSet();
+ void deserializeElementConst();
+ void deserializeElementFunction();
+ void deserializeFunctionOperator();
+ void deserializeFunctionTable();
CSolver *solver;
int filedesc;
CloneMap map;
+++ /dev/null
-
-/*
- * File: serializable.h
- * Author: hamed
- *
- * Created on September 7, 2017, 3:39 PM
- */
-
-#ifndef SERIALIZABLE_H
-#define SERIALIZABLE_H
-
-class Serializable{
- virtual void serialize(Serializer* ) = 0;
-};
-
-#endif /* SERIALIZABLE_H */
-
#include "boolean.h"
Serializer::Serializer(const char *file) {
- filedesc = open(file, O_WRONLY | O_CREAT, 0666);
+ filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
if (filedesc < 0) {
exit(-1);
}
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be){
+void serializeBooleanEdge(Serializer* serializer, BooleanEdge be){
+ if(be == BooleanEdge(NULL))
+ return;
be.getBoolean()->serialize(serializer);
ASTNodeType type = BOOLEANEDGE;
serializer->mywrite(&type, sizeof(ASTNodeType));
#ifndef SERIALIZER_H
#define SERIALIZER_H
#include "mymemory.h"
+#include "classlist.h"
#include "structs.h"
+
class Serializer {
public:
Serializer(const char *file);
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be);
+void serializeBooleanEdge(Serializer* serializer, BooleanEdge be);
#endif /* SERIALIZER_H */
Element *inputs2 [] = {e4, e3};
BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
solver->addConstraint(pred);
-// solver->serialize();
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
else
Element *inputs[] = {e1, e2};
BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
solver->addConstraint(b);
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
Element *inputs[] = {e1, e2};
BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
solver->addConstraint(b);
-
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
else
Element *inputs2 [] = {e7, e6};
BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);
solver->addConstraint(pred);
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
BooleanEdge barray5[] = {b1, b4};
solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
+ solver->serialize();
if (solver->solve() == 1)
printf("b1=%d b2=%d b3=%d b4=%d\n",
solver->getBooleanValue(b1), solver->getBooleanValue(b2),
Element *inputs2[] = {e1, e2};
BooleanEdge b = solver->applyPredicate(lt, inputs2, 2);
solver->addConstraint(b);
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
else
BooleanEdge array12[] = {o58, o81};
solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
-
+ solver->serialize();
/* if (solver->solve() == 1)
printf("SAT\n");
else
Element *inputs2 [] = {e4, e3};
BooleanEdge pred = solver->applyPredicate(lte, inputs2, 2);
solver->addConstraint(pred);
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " e4=%" PRIu64 " overFlow:%d\n",
Element *tmparray2[] = {e1, e2};
BooleanEdge pred2 = solver->applyPredicate(eq, tmparray2, 2);
solver->addConstraint(pred2);
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " undefFlag:%d\n",
return getElementValueUnarySATTranslator(This, elemEnc);
case BINARYINDEX:
return getElementValueBinaryIndexSATTranslator(This, elemEnc);
- case ONEHOTBINARY:
- ASSERT(0);
break;
case BINARYVAL:
ASSERT(0);
TunableSetting::TunableSetting(VarType _type, TunableParam _param) :
hasVar(true),
- type(_type),
+ type1(_type),
+ type2(0),
+ param(_param) {
+}
+
+TunableSetting::TunableSetting(VarType _type1, VarType _type2, TunableParam _param) :
+ hasVar(true),
+ type1(_type1),
+ type2(_type2),
param(_param) {
}
TunableSetting::TunableSetting(TunableParam _param) :
hasVar(false),
- type(0),
+ type1(0),
+ type2(0),
param(_param) {
}
TunableSetting::TunableSetting(TunableSetting *ts) :
hasVar(ts->hasVar),
- type(ts->type),
+ type1(ts->type1),
+ type2(ts->type2),
param(ts->param),
lowValue(ts->lowValue),
highValue(ts->highValue),
void TunableSetting::print() {
if (hasVar) {
- model_print("Type %" PRIu64 ", ", type);
+ model_print("Type1 %" PRIu64 ", ", type1);
+ model_print("Type2 %" PRIu64 ", ", type2);
}
model_print("Param %u = %u\n", param, selectedValue);
}
unsigned int tunableSettingHash(TunableSetting *setting) {
- return setting->hasVar ^ setting->type ^ setting->param;
+ return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
}
bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
return setting1->hasVar == setting2->hasVar &&
- setting1->type == setting2->type &&
- setting1->param == setting2->param;
+ setting1->type1 == setting2->type1 &&
+ setting1->type2 == setting2->type2 &&
+ setting1->param == setting2->param;
}
SearchTuner::SearchTuner() {
}
int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
- TunableSetting setting(vartype, param);
+ return getVarTunable(vartype, 0, param, descriptor);
+}
+
+int SearchTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+ TunableSetting setting(vartype1, vartype2, param);
TunableSetting *result = usedSettings.get(&setting);
if (result == NULL) {
result = settings.get(&setting);
if ( result == NULL) {
- result = new TunableSetting(vartype, param);
+ result = new
+ TunableSetting(vartype1, vartype2, param);
uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
settings.add(result);
class TunableSetting {
public:
TunableSetting(VarType type, TunableParam param);
+ TunableSetting(VarType type1, VarType type2, TunableParam param);
TunableSetting(TunableParam param);
TunableSetting(TunableSetting *ts);
void setDecision(int _low, int _high, int _default, int _selection);
CMEMALLOC;
private:
bool hasVar;
- VarType type;
+ VarType type1;
+ VarType type2;
TunableParam param;
int lowValue;
int highValue;
~SearchTuner();
int getTunable(TunableParam param, TunableDesc *descriptor);
int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+ int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
SearchTuner *copyUsed();
void randomMutate();
uint getSize() { return usedSettings.getSize();}
int DefaultTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
return descriptor->defaultValue;
}
+
int DefaultTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
return descriptor->defaultValue;
}
+
+int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+ return descriptor->defaultValue;
+}
public:
virtual int getTunable(TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
+ virtual int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
virtual ~Tuner() {}
CMEMALLOC;
};
DefaultTuner();
int getTunable(TunableParam param, TunableDesc *descriptor);
int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+ int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
CMEMALLOC;
};
static TunableDesc onoff(0, 1, 1);
static TunableDesc offon(0, 1, 0);
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING};
typedef enum Tunables Tunables;
#endif
}
BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
- return applyPredicateTable(predicate, inputs, numInputs, NULL);
+ return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
}
BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
projects / satune.git / commitdiff