typedef enum PredicateType PredicateType;
enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST,
- BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE};
+ 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;
+extern const char *elemEncTypeNames[];
+
enum ElementEncodingType {
ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, BINARYVAL
};
}
BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) {
- bool isnegated=e.isNegated();
- Boolean *b=e->clone(solver, map);
- BooleanEdge be=BooleanEdge(b);
+ bool isnegated = e.isNegated();
+ Boolean *b = e->clone(solver, map);
+ BooleanEdge be = BooleanEdge(b);
return isnegated ? be.negate() : be;
}
if (b != NULL)
return b;
BooleanEdge bvar = solver->getBooleanVar(type);
- Boolean * base=bvar.getRaw();
+ Boolean *base = bvar.getRaw();
map->put(this, base);
return base;
}
}
void BooleanPredicate::updateParents() {
- for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+ for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
}
void BooleanLogic::updateParents() {
- for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+ for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
}
-void BooleanVar::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void BooleanVar::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
serializer->mywrite(&type, sizeof(ASTNodeType));
- BooleanVar* This = this;
- serializer->mywrite(&This, sizeof(BooleanVar*));
+ BooleanVar *This = this;
+ serializer->mywrite(&This, sizeof(BooleanVar *));
serializer->mywrite(&vtype, sizeof(VarType));
}
-void BooleanVar::print(){
- model_println("BooleanVar:%lu", (uintptr_t)this);
+void BooleanVar::print() {
+ model_print("BooleanVar:%lu\n", (uintptr_t)this);
}
-void BooleanConst::print(){
- model_println("BooleanConst:%s", istrue?"TRUE" :"FALSE");
+void BooleanConst::print() {
+ model_print("BooleanConst:%s\n", istrue ? "TRUE" : "FALSE");
}
-void BooleanOrder::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void BooleanOrder::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
order->serialize(serializer);
-
+
serializer->mywrite(&type, sizeof(ASTNodeType));
- BooleanOrder* This = this;
- serializer->mywrite(&This, sizeof(BooleanOrder*));
- serializer->mywrite(&order, sizeof(Order*));
+ BooleanOrder *This = this;
+ serializer->mywrite(&This, sizeof(BooleanOrder *));
+ serializer->mywrite(&order, sizeof(Order *));
serializer->mywrite(&first, sizeof(uint64_t));
serializer->mywrite(&second, sizeof(uint64_t));
}
-void BooleanOrder::print(){
- model_println("{BooleanOrder: First= %lu, Second = %lu on Order:", first, second);
+void BooleanOrder::print() {
+ model_print("{BooleanOrder: First= %lu, Second = %lu on Order:\n", first, second);
order->print();
- model_println("}\n");
+ model_print("}\n");
}
-void BooleanPredicate::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void BooleanPredicate::serialize(Serializer *serializer) {
+ 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);
+ 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*));
+ 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++){
+ 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*));
+ Boolean *undefStat = undefStatus != BooleanEdge(NULL) ? undefStatus.getRaw() : NULL;
+ serializer->mywrite(&undefStat, sizeof(Boolean *));
}
-void BooleanPredicate::print(){
- model_println("{BooleanPredicate:");
- predicate->print();
- model_println("elements:");
- uint size = inputs.getSize();
- for(uint i=0; i<size; i++){
+void BooleanPredicate::print() {
+ model_print("{BooleanPredicate:\n");
+ predicate->print();
+ model_print("elements:\n");
+ uint size = inputs.getSize();
+ for (uint i = 0; i < size; i++) {
Element *input = inputs.get(i);
input->print();
}
- model_println("}\n");
+ model_print("}\n");
}
-void BooleanLogic::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void BooleanLogic::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
uint size = inputs.getSize();
- for(uint i=0; i<size; i++){
+ 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*));
+ 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*));
+ for (uint i = 0; i < size; i++) {
+ Boolean *input = inputs.get(i).getRaw();
+ serializer->mywrite(&input, sizeof(Boolean *));
}
}
-void BooleanLogic::print(){
- model_println("{BooleanLogic: %s",
- op ==SATC_AND? "AND": op == SATC_OR? "OR": op==SATC_NOT? "NOT":
- op == SATC_XOR? "XOR" : op==SATC_IFF? "IFF" : "IMPLIES");
- uint size = inputs.getSize();
- for(uint i=0; i<size; i++){
+void BooleanLogic::print() {
+ model_print("{BooleanLogic: %s\n",
+ op == SATC_AND ? "AND" : op == SATC_OR ? "OR" : op == SATC_NOT ? "NOT" :
+ op == SATC_XOR ? "XOR" : op == SATC_IFF ? "IFF" : "IMPLIES");
+ uint size = inputs.getSize();
+ for (uint i = 0; i < size; i++) {
BooleanEdge input = inputs.get(i);
- if(input.isNegated())
- model_print("!");
- input.getBoolean()->print();
+ if (input.isNegated())
+ model_print("!");
+ input.getBoolean()->print();
}
- model_println("}\n");
+ model_print("}\n");
}
Boolean(ASTNodeType _type);
virtual ~Boolean() {}
virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
- virtual void serialize(Serializer* ) = 0;
- virtual void print() =0;
+ virtual void serialize(Serializer * ) = 0;
+ virtual void print() = 0;
virtual bool isTrue() {return boolVal == BV_MUSTBETRUE;}
virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
Polarity polarity;
BooleanValue boolVal;
Vector<Boolean *> parents;
virtual void updateParents() {}
-
+
CMEMALLOC;
};
Boolean *clone(CSolver *solver, CloneMap *map);
bool isTrue() {return istrue;}
bool isFalse() {return !istrue;}
- void serialize(Serializer *serializer ){};
- virtual void print();
+ void serialize(Serializer *serializer ) {};
+ virtual void print();
bool istrue;
CMEMALLOC;
};
BooleanVar(VarType t);
Boolean *clone(CSolver *solver, CloneMap *map);
void serialize(Serializer *serializer );
- virtual void print();
+ virtual void print();
VarType vtype;
Edge var;
CMEMALLOC;
BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
Boolean *clone(CSolver *solver, CloneMap *map);
void serialize(Serializer *serializer );
- virtual void print();
+ virtual void print();
Order *order;
uint64_t first;
FunctionEncoding *getFunctionEncoding() {return &encoding;}
void updateParents();
void serialize(Serializer *serializer );
- virtual void print();
+ virtual void print();
CMEMALLOC;
Predicate *predicate;
BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize);
Boolean *clone(CSolver *solver, CloneMap *map);
void serialize(Serializer *serializer );
- virtual void print();
+ virtual void print();
LogicOp op;
bool replaced;
Array<BooleanEdge> inputs;
void updateParents();
-
+
CMEMALLOC;
};
BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
}
void ElementFunction::updateParents() {
- for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+ for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
}
-Set * ElementFunction::getRange() {
+Set *ElementFunction::getRange() {
return function->getRange();
}
-void ElementSet::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+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*));
+ serializer->mywrite(&This, sizeof(ElementSet *));
+ serializer->mywrite(&set, sizeof(Set *));
}
-void ElementSet::print(){
- model_println("{ElementSet:");
+void ElementSet::print() {
+ model_print("{ElementSet:");
set->print();
- model_println("}\n");
+ model_print(" %p ", this);
+ getElementEncoding()->print();
+ model_print("}");
}
-void ElementConst::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+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*));
+ serializer->mywrite(&This, sizeof(ElementSet *));
VarType type = set->getType();
serializer->mywrite(&type, sizeof(VarType));
serializer->mywrite(&value, sizeof(uint64_t));
}
-void ElementConst::print(){
- model_println("{ElementConst: %lu}", value);
+void ElementConst::print() {
+ model_print("{ElementConst: %lu}\n", value);
}
-void ElementFunction::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+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++){
+ 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*));
+ 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*));
+ Boolean *overflowstat = overflowstatus.getRaw();
+ serializer->mywrite(&overflowstat, sizeof(Boolean *));
}
-void ElementFunction::print(){
- model_println("{ElementFunction:");
+void ElementFunction::print() {
+ model_print("{ElementFunction:\n");
function->print();
- model_println("Elements:");
+ model_print("Elements:\n");
uint size = inputs.getSize();
- for(uint i=0; i<size; i++){
+ for (uint i = 0; i < size; i++) {
Element *input = inputs.get(i);
input->print();
}
- model_println("}\n");
+ model_print("}\n");
}
virtual ~Element() {}
Vector<ASTNode *> parents;
ElementEncoding encoding;
- inline ElementEncoding *getElementEncoding(){ return &encoding; }
+ inline ElementEncoding *getElementEncoding() { return &encoding; }
virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
- virtual void serialize(Serializer* serializer) =0;
- virtual void print() = 0;
+ virtual void serialize(Serializer *serializer) = 0;
+ virtual void print() = 0;
virtual void updateParents() {}
- virtual Set * getRange() = 0;
+ virtual Set *getRange() = 0;
CMEMALLOC;
};
virtual ~ElementSet(){}
ElementSet(Set *s);
virtual Element *clone(CSolver *solver, CloneMap *map);
- virtual void serialize(Serializer* serializer);
- virtual void print();
+ virtual void serialize(Serializer *serializer);
+ virtual void print();
CMEMALLOC;
Set *getRange() {return set;}
- protected:
+protected:
Set *set;
};
ElementConst(uint64_t value, Set *_set);
virtual ~ElementConst(){}
uint64_t value;
- virtual void serialize(Serializer* serializer);
- virtual void print();
+ virtual void serialize(Serializer *serializer);
+ virtual void print();
Element *clone(CSolver *solver, CloneMap *map);
CMEMALLOC;
};
BooleanEdge overflowstatus;
FunctionEncoding functionencoding;
Element *clone(CSolver *solver, CloneMap *map);
- virtual void serialize(Serializer* serializer);
- virtual void print();
- Set * getRange();
+ virtual void serialize(Serializer *serializer);
+ virtual void print();
+ Set *getRange();
void updateParents();
- Function * getFunction() {return function;}
+ Function *getFunction() {return function;}
inline FunctionEncoding *getElementFunctionEncoding() {return &functionencoding;}
CMEMALLOC;
- private:
+private:
Function *function;
};
return f;
}
-Set * FunctionTable::getRange() {
+Set *FunctionTable::getRange() {
return table->getRange();
}
-void FunctionTable::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void FunctionTable::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
-
+
table->serialize(serializer);
-
- ASTNodeType type = FUNCTABLETYPE;
+
+ ASTNodeType type = FUNCTABLETYPE;
serializer->mywrite(&type, sizeof(ASTNodeType));
- FunctionTable* This = this;
- serializer->mywrite(&This, sizeof(FunctionTable*));
+ FunctionTable *This = this;
+ serializer->mywrite(&This, sizeof(FunctionTable *));
serializer->mywrite(&table, sizeof(Table *));
serializer->mywrite(&undefBehavior, sizeof(UndefinedBehavior));
-
+
}
-void FunctionTable::print(){
- model_println("{FunctionTable:");
- table->print();
- model_println("}\n");
-
+void FunctionTable::print() {
+ model_print("{FunctionTable:\n");
+ table->print();
+ model_print("}\n");
}
-void FunctionOperator::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+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);
+ for (uint i = 0; i < size; i++) {
+ Set *domain = domains.get(i);
domain->serialize(serializer);
}
range->serialize(serializer);
-
- ASTNodeType nodeType = FUNCOPTYPE;
+
+ ASTNodeType nodeType = FUNCOPTYPE;
serializer->mywrite(&nodeType, sizeof(ASTNodeType));
- FunctionOperator* This = this;
- serializer->mywrite(&This, sizeof(FunctionOperator*));
+ 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++){
+ for (uint i = 0; i < size; i++) {
Set *domain = domains.get(i);
serializer->mywrite(&domain, sizeof(Set *));
}
serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior));
}
-void FunctionOperator::print(){
- model_println("{FunctionOperator: %s}", op == SATC_ADD? "ADD": "SUB" );
-}
\ No newline at end of file
+void FunctionOperator::print() {
+ model_print("{FunctionOperator: %s}\n", op == SATC_ADD ? "ADD" : "SUB" );
+}
FunctionType type;
virtual ~Function() {}
virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
- virtual void serialize(Serializer* serialiezr) =0;
- virtual void print() = 0;
- virtual Set * getRange() = 0;
+ virtual void serialize(Serializer *serialiezr) = 0;
+ virtual void print() = 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);
- virtual void print();
- Set * getRange() {return range;}
+ virtual void serialize(Serializer *serialiezr);
+ virtual void print();
+ Set *getRange() {return range;}
CMEMALLOC;
};
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
Function *clone(CSolver *solver, CloneMap *map);
- virtual void serialize(Serializer* serialiezr);
- virtual void print();
- Set * getRange();
+ virtual void serialize(Serializer *serialiezr);
+ virtual void print();
+ Set *getRange();
CMEMALLOC;
};
#include "element.h"
#include "csolver.h"
-BooleanIterator::BooleanIterator(CSolver * _solver) :
+BooleanIterator::BooleanIterator(CSolver *_solver) :
solverit(_solver->getConstraints()) {
updateNext();
}
boolean.pop();
index.pop();
}
-
- while(true) {
+
+ while (true) {
if (boolean.getSize() == 0) {
if (solverit->hasNext()) {
- Boolean *b=solverit->next().getBoolean();
+ Boolean *b = solverit->next().getBoolean();
if (discovered.add(b)) {
boolean.push(b);
index.push(0);
} else
return;
}
- Boolean *topboolean=boolean.last();
- uint topindex=index.last();
- switch(topboolean->type) {
+ Boolean *topboolean = boolean.last();
+ uint topindex = index.last();
+ switch (topboolean->type) {
case ORDERCONST:
case BOOLEANVAR:
case PREDICATEOP:
case BOOLCONST:
return;
case LOGICOP: {
- BooleanLogic * logicop=(BooleanLogic*) topboolean;
- uint size=logicop->inputs.getSize();
+ BooleanLogic *logicop = (BooleanLogic *) topboolean;
+ uint size = logicop->inputs.getSize();
if (topindex == size)
return;
index.pop();
- index.push(topindex+1);
- Boolean *newchild=logicop->inputs.get(topindex).getBoolean();
+ index.push(topindex + 1);
+ Boolean *newchild = logicop->inputs.get(topindex).getBoolean();
if (discovered.add(newchild)) {
boolean.push(newchild);
index.push(0);
}
}
-Boolean * BooleanIterator::next() {
- Boolean * b = boolean.last();
+Boolean *BooleanIterator::next() {
+ Boolean *b = boolean.last();
updateNext();
return b;
}
element.pop();
index.pop();
}
-
- while(true) {
+
+ while (true) {
if (element.getSize() == 0) {
if (base != NULL) {
if (baseindex == base->inputs.getSize()) {
base = NULL;
continue;
} else {
- Element * e = base->inputs.get(baseindex);
+ Element *e = base->inputs.get(baseindex);
baseindex++;
if (discovered.add(e)) {
element.push(e);
}
} else {
if (bit.hasNext()) {
- Boolean *b=bit.next();
+ Boolean *b = bit.next();
if (b->type == PREDICATEOP) {
base = (BooleanPredicate *)b;
- baseindex=0;
+ baseindex = 0;
}
continue;
} else
return;
}
}
- Element *topelement=element.last();
- uint topindex=index.last();
- switch(topelement->type) {
+ Element *topelement = element.last();
+ uint topindex = index.last();
+ switch (topelement->type) {
case ELEMSET:
case ELEMCONST:
return;
case ELEMFUNCRETURN: {
- ElementFunction * func=(ElementFunction*) topelement;
- uint size=func->inputs.getSize();
+ ElementFunction *func = (ElementFunction *) topelement;
+ uint size = func->inputs.getSize();
if (topindex == size)
return;
index.pop();
- index.push(topindex+1);
- Element *newchild=func->inputs.get(topindex);
+ index.push(topindex + 1);
+ Element *newchild = func->inputs.get(topindex);
if (discovered.add(newchild)) {
element.push(newchild);
index.push(0);
}
}
-Element * ElementIterator::next() {
- Element * e = element.last();
+Element *ElementIterator::next() {
+ Element *e = element.last();
updateNext();
return e;
}
#include "structs.h"
class BooleanIterator {
- public:
- BooleanIterator(CSolver * _solver);
+public:
+ BooleanIterator(CSolver *_solver);
~BooleanIterator();
bool hasNext();
- Boolean * next();
+ Boolean *next();
CMEMALLOC;
- private:
- SetIteratorBooleanEdge * solverit;
+private:
+ SetIteratorBooleanEdge *solverit;
HashsetBoolean discovered;
Vector<Boolean *> boolean;
Vector<uint> index;
};
class ElementIterator {
- public:
+public:
ElementIterator(CSolver *_solver);
~ElementIterator();
bool hasNext();
- Element * next();
+ Element *next();
CMEMALLOC;
- private:
+private:
BooleanIterator bit;
BooleanPredicate *base;
uint baseindex;
s = solver->createMutableSet(type);
for (uint i = 0; i < members->getSize(); i++) {
((MutableSet *)s)->addElementMSet(members->get(i));
- solver->addItem((MutableSet *) s, members->get(i));
+ solver->addItem((MutableSet *) s, members->get(i));
}
- ((MutableSet*)s)->finalize();
+ ((MutableSet *)s)->finalize();
map->put(this, s);
return s;
}
-void MutableSet::finalize(){
+void MutableSet::finalize() {
bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
}
\ No newline at end of file
return o;
}
-HashtableOrderPair* Order::getOrderPairTable(){
+HashtableOrderPair *Order::getOrderPairTable() {
ASSERT( encoding.resolver != NULL);
- if (OrderPairResolver* t = dynamic_cast<OrderPairResolver*>(encoding.resolver)){
+ if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
return t->getOrderPairTable();
} else {
ASSERT(0);
}
}
-void Order::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void Order::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
set->serialize(serializer);
ASTNodeType asttype = ORDERTYPE;
serializer->mywrite(&asttype, sizeof(ASTNodeType));
- Order* This = this;
- serializer->mywrite(&This, sizeof(Order*));
+ Order *This = this;
+ serializer->mywrite(&This, sizeof(Order *));
serializer->mywrite(&type, sizeof(OrderType));
serializer->mywrite(&set, sizeof(Set *));
}
-void Order::print(){
- model_println("{Order on Set:");
- set->print();
- model_println("}\n");
+void Order::print() {
+ model_print("{Order on Set:\n");
+ set->print();
+ model_print("}\n");
}
#include "boolean.h"
#include "orderpair.h"
-class Order{
+class Order {
public:
Order(OrderType type, Set *set);
virtual ~Order();
void initializeOrderElementsHashtable();
void addOrderConstraint(BooleanOrder *constraint);
void setOrderEncodingType(OrderEncodingType type);
- HashtableOrderPair* getOrderPairTable();
+ HashtableOrderPair *getOrderPairTable();
CMEMALLOC;
};
return p;
}
-void PredicateTable::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void PredicateTable::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
-
+
table->serialize(serializer);
-
- ASTNodeType type = PREDTABLETYPE;
+
+ ASTNodeType type = PREDTABLETYPE;
serializer->mywrite(&type, sizeof(ASTNodeType));
- PredicateTable* This = this;
- serializer->mywrite(&This, sizeof(PredicateTable*));
+ PredicateTable *This = this;
+ serializer->mywrite(&This, sizeof(PredicateTable *));
serializer->mywrite(&table, sizeof(Table *));
serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior));
}
-void PredicateTable::print(){
- model_println("{PredicateTable:");
- table->print();
- model_println("}\n");
+void PredicateTable::print() {
+ model_print("{PredicateTable:\n");
+ table->print();
+ model_print("}\n");
}
-void PredicateOperator::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+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);
+ for (uint i = 0; i < size; i++) {
+ Set *domain = domains.get(i);
domain->serialize(serializer);
}
-
- ASTNodeType type = PREDOPERTYPE;
+
+ ASTNodeType type = PREDOPERTYPE;
serializer->mywrite(&type, sizeof(ASTNodeType));
- PredicateOperator* This = this;
- serializer->mywrite(&This, sizeof(PredicateOperator*));
+ 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*));
+ for (uint i = 0; i < size; i++) {
+ Set *domain = domains.get(i);
+ serializer->mywrite(&domain, sizeof(Set *));
}
}
-void PredicateOperator::print(){
- model_println("{PredicateOperator: %s }", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL");
+void PredicateOperator::print() {
+ const char *names[] = {"==", "<", ">", "<=", ">="};
+
+ model_print("PredicateOperator: %s\n", names[(int)op]);
}
Predicate(PredicateType _type) : type(_type) {}
virtual ~Predicate() {}
virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
- virtual void serialize(Serializer* serializer) = 0;
- virtual void print() =0;
+ virtual void serialize(Serializer *serializer) = 0;
+ virtual void print() = 0;
PredicateType type;
CMEMALLOC;
};
PredicateOperator(CompOp op, Set **domain, uint numDomain);
bool evalPredicateOperator(uint64_t *inputs);
Predicate *clone(CSolver *solver, CloneMap *map);
- virtual void serialize(Serializer* serializer);
- virtual void print();
+ virtual void serialize(Serializer *serializer);
+ virtual void print();
Array<Set *> domains;
CompOp getOp() {return op;}
CMEMALLOC;
- private:
+private:
CompOp op;
};
public:
PredicateTable(Table *table, UndefinedBehavior undefBehavior);
Predicate *clone(CSolver *solver, CloneMap *map);
- virtual void serialize(Serializer* serializer);
- virtual void print();
+ virtual void serialize(Serializer *serializer);
+ virtual void print();
Table *table;
UndefinedBehavior undefinedbehavior;
CMEMALLOC;
void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
if (constraints.contains(bexpr.negate())) {
constraints.remove(bexpr.negate());
-#ifdef TRACE_DEBUG
- model_println("replaceBooleanWithTrue");
-#endif
setUnSAT();
- }
+ }
if (constraints.contains(bexpr)) {
constraints.remove(bexpr);
}
replaceBooleanWithTrueNoRemove(bexpr);
}
-
+
void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
ASSERT(bexpr->boolVal != BV_UNSAT);
-
+
uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
Boolean *parent = bexpr->parents.get(i);
void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
//Canonicalize
if (oldb.isNegated()) {
- oldb=oldb.negate();
- newb=newb.negate();
+ oldb = oldb.negate();
+ newb = newb.negate();
}
if (constraints.contains(oldb)) {
for (uint i = 0; i < size; i++) {
Boolean *parent = oldb->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
- boolMap.remove(parent); //could change parent's hash
-
+ boolMap.remove(parent); //could change parent's hash
+
uint parentsize = logicop->inputs.getSize();
for (uint j = 0; j < parentsize; j++) {
BooleanEdge b = logicop->inputs.get(j);
}
void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
- BooleanEdge childNegate=child.negate();
-
+ BooleanEdge childNegate = child.negate();
+
boolMap.remove(bexpr);
-
+
for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
BooleanEdge b = bexpr->inputs.get(i);
-
+
if (b == child) {
bexpr->inputs.remove(i);
i--;
}
}
- uint size=bexpr->inputs.getSize();
+ uint size = bexpr->inputs.getSize();
if (size == 0) {
bexpr->replaced = true;
replaceBooleanWithTrue(bexpr);
}
BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
- bool isNegated=bexpr.isNegated();
- BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+ bool isNegated = bexpr.isNegated();
+ BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
BooleanEdge result;
if (b->op == SATC_IFF) {
if (isTrue(b->inputs.get(0))) {
} else if (isFalse(b->inputs.get(1))) {
result = b->inputs.get(0).negate();
} else ASSERT(0);
- } else if (b->op==SATC_AND) {
+ } else if (b->op == SATC_AND) {
uint size = b->inputs.getSize();
if (size == 0)
result = boolTrue;
#include "qsort.h"
int intcompare(const void *p1, const void *p2) {
- uint64_t a=*(uint64_t const *) p1;
- uint64_t b=*(uint64_t const *) p2;
+ uint64_t a = *(uint64_t const *) p1;
+ uint64_t b = *(uint64_t const *) p2;
if (a < b)
return -1;
- else if (a==b)
+ else if (a == b)
return 0;
else
return 1;
return element >= low && element <= high;
} else {
//Use Binary Search
- uint low=0;
- uint high=members->getSize()-1;
- while(true) {
- uint middle=(low+high)/2;
- uint64_t val=members->get(middle);
+ uint low = 0;
+ uint high = members->getSize() - 1;
+ while (true) {
+ uint middle = (low + high) / 2;
+ uint64_t val = members->get(middle);
if (element < val) {
- high=middle-1;
- if (middle<=low)
+ high = middle - 1;
+ if (middle <= low)
return false;
} else if (element > val) {
- low=middle+1;
- if (middle>=high)
+ low = middle + 1;
+ if (middle >= high)
return false;
} else {
return true;
uint sum = 0;
uint64_t sValue = s->getElement(sIndex);
uint64_t thisValue = getElement(thisIndex);
- while(thisIndex < thisSize && sIndex < sSize) {
+ while (thisIndex < thisSize && sIndex < sSize) {
if (sValue < thisValue) {
- sValue = s->getElement(++sIndex);
+ sIndex++;
+ if (sIndex < sSize)
+ sValue = s->getElement(sIndex);
sum++;
} else if (thisValue < sValue) {
- thisValue = getElement(++thisIndex);
+ thisIndex++;
+ if (thisIndex < thisSize)
+ thisValue = getElement(thisIndex);
sum++;
} else {
- thisValue = getElement(++thisIndex);
- sValue = s->getElement(++sIndex);
+ thisIndex++;
+ sIndex++;
+ if (sIndex < sSize)
+ sValue = s->getElement(sIndex);
+ if (thisIndex < thisSize)
+ thisValue = getElement(thisIndex);
sum++;
}
}
sum += (thisSize - thisIndex) + (sSize - sIndex);
-
+
return sum;
}
-void Set::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+void Set::serialize(Serializer *serializer) {
+ if (serializer->isSerialized(this))
return;
serializer->addObject(this);
ASTNodeType asttype = SETTYPE;
serializer->mywrite(&asttype, sizeof(ASTNodeType));
- Set* This = this;
- serializer->mywrite(&This, sizeof(Set*));
+ Set *This = this;
+ serializer->mywrite(&This, sizeof(Set *));
serializer->mywrite(&type, sizeof(VarType));
serializer->mywrite(&isRange, sizeof(bool));
bool isMutable = isMutableSet();
}
}
-void Set::print(){
+void Set::print() {
model_print("{Set:");
- if(isRange){
- model_print("Range: low=%lu, high=%lu}\n\n", low, high);
- } else {
- uint size = members->getSize();
- model_print("Members: ");
- for(uint i=0; i<size; i++){
- uint64_t mem = members->get(i);
- model_print("%lu, ", mem);
- }
- model_println("}\n");
- }
+ if (isRange) {
+ model_print("Range: low=%lu, high=%lu}", low, high);
+ } else {
+ uint size = members->getSize();
+ model_print("Members: ");
+ for (uint i = 0; i < size; i++) {
+ uint64_t mem = members->get(i);
+ model_print("%lu, ", mem);
+ }
+ model_print("}");
+ }
}
uint getUnionSize(Set *s);
virtual bool isMutableSet() {return false;}
virtual Set *clone(CSolver *solver, CloneMap *map);
- virtual void serialize(Serializer* serializer);
+ virtual void serialize(Serializer *serializer);
virtual void print();
CMEMALLOC;
protected:
-void Table::serialize(Serializer* serializer){
- if(serializer->isSerialized(this))
+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);
+ for (uint i = 0; i < size; i++) {
+ Set *domain = domains.get(i);
domain->serialize(serializer);
}
- if(range!= NULL)
+ if (range != NULL)
range->serialize(serializer);
-
- ASTNodeType type = TABLETYPE;
+
+ ASTNodeType type = TABLETYPE;
serializer->mywrite(&type, sizeof(ASTNodeType));
- Table* This = this;
- serializer->mywrite(&This, sizeof(Table*));
+ 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*));
+ for (uint i = 0; i < size; i++) {
+ Set *domain = domains.get(i);
+ serializer->mywrite(&domain, sizeof(Set *));
}
- serializer->mywrite(&range, 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();
+ 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);
}
-void Table::print(){
- model_println("{Table:");
- SetIteratorTableEntry* iterator = getEntries();
- while(iterator->hasNext()){
- TableEntry* entry = iterator->next();
- model_print("<");
- for(uint i=0; i<entry->inputSize; i++){
- model_print("%lu, ", entry->inputs[i]);
- }
- model_print(" == %lu>", entry->output);
+void Table::print() {
+ model_print("{Table:\n");
+ SetIteratorTableEntry *iterator = getEntries();
+ while (iterator->hasNext()) {
+ TableEntry *entry = iterator->next();
+ model_print("<");
+ for (uint i = 0; i < entry->inputSize; i++) {
+ model_print("%lu, ", entry->inputs[i]);
+ }
+ model_print(" == %lu>", entry->output);
}
- model_println("}\n");
+ model_print("}\n");
delete iterator;
}
TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
Table *clone(CSolver *solver, CloneMap *map);
void serialize(Serializer *serializer);
- void print();
+ void print();
~Table();
- Set * getRange() {return range;}
-
- Set * getDomain(uint i) {return domains.get(i);}
+ Set *getRange() {return range;}
+
+ Set *getDomain(uint i) {return domains.get(i);}
uint numDomains() {return domains.getSize();}
-
- SetIteratorTableEntry * getEntries() {return entries->iterator();}
+
+ SetIteratorTableEntry *getEntries() {return entries->iterator();}
uint getSize() {return entries->getSize();}
CMEMALLOC;
-
- private:
+
+private:
Array<Set *> domains;
Set *range;
HashsetTableEntry *entries;
#include "subgraph.h"
#include "elementencoding.h"
-EncodingGraph::EncodingGraph(CSolver * _solver) :
+EncodingGraph::EncodingGraph(CSolver *_solver) :
solver(_solver) {
}
-int sortEncodingEdge(const void * p1, const void *p2) {
- const EncodingEdge * e1 = * (const EncodingEdge **) p1;
- const EncodingEdge * e2 = * (const EncodingEdge **) p2;
+EncodingGraph::~EncodingGraph() {
+ subgraphs.resetAndDelete();
+ encodingMap.resetAndDeleteVals();
+ edgeMap.resetAndDeleteVals();
+}
+
+int sortEncodingEdge(const void *p1, const void *p2) {
+ const EncodingEdge *e1 = *(const EncodingEdge **) p1;
+ const EncodingEdge *e2 = *(const EncodingEdge **) p2;
uint64_t v1 = e1->getValue();
uint64_t v2 = e2->getValue();
if (v1 < v2)
void EncodingGraph::buildGraph() {
ElementIterator it(solver);
- while(it.hasNext()) {
- Element * e = it.next();
- switch(e->type) {
+ while (it.hasNext()) {
+ Element *e = it.next();
+ switch (e->type) {
case ELEMSET:
case ELEMFUNCRETURN:
processElement(e);
}
void EncodingGraph::encode() {
- SetIteratorEncodingSubGraph * itesg=subgraphs.iterator();
- while(itesg->hasNext()) {
- EncodingSubGraph *sg=itesg->next();
+ SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
+ while (itesg->hasNext()) {
+ EncodingSubGraph *sg = itesg->next();
sg->encode();
}
delete itesg;
ElementIterator it(solver);
- while(it.hasNext()) {
- Element * e = it.next();
- switch(e->type) {
+ while (it.hasNext()) {
+ Element *e = it.next();
+ switch (e->type) {
case ELEMSET:
case ELEMFUNCRETURN: {
- ElementEncoding *encoding=e->getElementEncoding();
+ ElementEncoding *encoding = e->getElementEncoding();
if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
EncodingNode *n = getNode(e);
if (n == NULL)
continue;
- ElementEncodingType encodetype=n->getEncoding();
+ ElementEncodingType encodetype = n->getEncoding();
encoding->setElementEncodingType(encodetype);
if (encodetype == UNARY || encodetype == ONEHOT) {
encoding->encodingArrayInitialization();
} else if (encodetype == BINARYINDEX) {
- EncodingSubGraph * subgraph = graphMap.get(n);
+ EncodingSubGraph *subgraph = graphMap.get(n);
if (subgraph == NULL)
continue;
- uint encodingSize = subgraph->getEncodingSize(n);
+ uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
encoding->allocInUseArrayElement(paddedSize);
encoding->allocEncodingArrayElement(paddedSize);
- Set * s=e->getRange();
- for(uint i=0;i<s->getSize();i++) {
- uint64_t value=s->getElement(i);
- uint encodingIndex=subgraph->getEncoding(n, value);
+ Set *s = e->getRange();
+ for (uint i = 0; i < s->getSize(); i++) {
+ uint64_t value = s->getElement(i);
+ uint encodingIndex = subgraph->getEncoding(n, value);
encoding->setInUseElement(encodingIndex);
encoding->encodingArray[encodingIndex] = value;
}
}
void EncodingGraph::encodeParent(Element *e) {
- uint size=e->parents.getSize();
- for(uint i=0;i<size;i++) {
- ASTNode * n = e->parents.get(i);
- if (n->type==PREDICATEOP) {
- BooleanPredicate *b=(BooleanPredicate *)n;
- FunctionEncoding *fenc=b->getFunctionEncoding();
+ uint size = e->parents.getSize();
+ for (uint i = 0; i < size; i++) {
+ ASTNode *n = e->parents.get(i);
+ if (n->type == PREDICATEOP) {
+ BooleanPredicate *b = (BooleanPredicate *)n;
+ FunctionEncoding *fenc = b->getFunctionEncoding();
if (fenc->getFunctionEncodingType() != FUNC_UNASSIGNED)
continue;
- 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));
+ 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);
+ EncodingEdge *edge = getEdge(left, right, NULL);
if (edge != NULL && edge->getEncoding() == EDGE_MATCH) {
fenc->setFunctionEncodingType(CIRCUIT);
}
}
void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
- EncodingSubGraph *graph1=graphMap.get(first);
- EncodingSubGraph *graph2=graphMap.get(second);
+ EncodingSubGraph *graph1 = graphMap.get(first);
+ EncodingSubGraph *graph2 = graphMap.get(second);
if (graph1 == NULL)
first->setEncoding(BINARYINDEX);
if (graph2 == NULL)
first = tmp;
}
if (graph1 != NULL && graph2 != NULL) {
- SetIteratorEncodingNode * nodeit=graph2->nodeIterator();
- while(nodeit->hasNext()) {
- EncodingNode *node=nodeit->next();
+ SetIteratorEncodingNode *nodeit = graph2->nodeIterator();
+ while (nodeit->hasNext()) {
+ EncodingNode *node = nodeit->next();
graph1->addNode(node);
graphMap.put(node, graph1);
}
}
void EncodingGraph::processElement(Element *e) {
- uint size=e->parents.getSize();
- for(uint i=0;i<size;i++) {
- ASTNode * n = e->parents.get(i);
- switch(n->type) {
+ uint size = e->parents.getSize();
+ for (uint i = 0; i < size; i++) {
+ ASTNode *n = e->parents.get(i);
+ switch (n->type) {
case PREDICATEOP:
processPredicate((BooleanPredicate *)n);
break;
}
void EncodingGraph::processFunction(ElementFunction *ef) {
- Function *f=ef->getFunction();
- if (f->type==OPERATORFUNC) {
- FunctionOperator *fo=(FunctionOperator*)f;
+ Function *f = ef->getFunction();
+ if (f->type == OPERATORFUNC) {
+ FunctionOperator *fo = (FunctionOperator *)f;
ASSERT(ef->inputs.getSize() == 2);
- EncodingNode *left=createNode(ef->inputs.get(0));
- EncodingNode *right=createNode(ef->inputs.get(1));
+ 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=createEdge(left, right, dst);
+ EncodingNode *dst = createNode(ef);
+ EncodingEdge *edge = createEdge(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));
+ 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=createEdge(left, right, NULL);
- CompOp op=po->getOp();
- switch(op) {
+ EncodingEdge *edge = createEdge(left, right, NULL);
+ CompOp op = po->getOp();
+ switch (op) {
case SATC_EQUALS:
edge->numEquals++;
break;
}
uint convertSize(uint cost) {
- cost = 1.2 * cost; // fudge factor
+ cost = 1.2 * cost;// fudge factor
return NEXTPOW2(cost);
}
void EncodingGraph::decideEdges() {
- uint size=edgeVector.getSize();
- for(uint i=0; i<size; i++) {
+ uint size = edgeVector.getSize();
+ for (uint i = 0; i < size; i++) {
EncodingEdge *ee = edgeVector.get(i);
EncodingNode *left = ee->left;
EncodingNode *right = ee->right;
-
+
if (ee->encoding != EDGE_UNASSIGNED ||
!left->couldBeBinaryIndex() ||
!right->couldBeBinaryIndex())
continue;
-
+
uint64_t eeValue = ee->getValue();
if (eeValue == 0)
return;
EncodingSubGraph *leftGraph = graphMap.get(left);
EncodingSubGraph *rightGraph = graphMap.get(right);
- if (leftGraph == NULL && rightGraph !=NULL) {
- EncodingNode *tmp = left; left=right; right=tmp;
+ if (leftGraph == NULL && rightGraph != NULL) {
+ EncodingNode *tmp = left; left = right; right = tmp;
EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
}
- uint leftSize=0, rightSize=0, newSize=0;
- uint64_t totalCost=0;
+ uint leftSize = 0, rightSize = 0, newSize = 0;
+ uint64_t totalCost = 0;
if (leftGraph == NULL && rightGraph == NULL) {
- leftSize=convertSize(left->getSize());
- rightSize=convertSize(right->getSize());
- newSize=convertSize(left->s->getUnionSize(right->s));
- newSize=(leftSize > newSize) ? leftSize: newSize;
- newSize=(rightSize > newSize) ? rightSize: newSize;
+ leftSize = convertSize(left->getSize());
+ rightSize = convertSize(right->getSize());
+ newSize = convertSize(left->s->getUnionSize(right->s));
+ newSize = (leftSize > newSize) ? leftSize : newSize;
+ newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * left->elements.getSize() +
- (newSize - rightSize) * right->elements.getSize();
+ (newSize - rightSize) * right->elements.getSize();
} else if (leftGraph != NULL && rightGraph == NULL) {
- leftSize=convertSize(leftGraph->encodingSize);
- rightSize=convertSize(right->getSize());
- newSize=convertSize(leftGraph->estimateNewSize(right));
- newSize=(leftSize > newSize) ? leftSize: newSize;
- newSize=(rightSize > newSize) ? rightSize: newSize;
+ leftSize = convertSize(leftGraph->encodingSize);
+ rightSize = convertSize(right->getSize());
+ newSize = convertSize(leftGraph->estimateNewSize(right));
+ newSize = (leftSize > newSize) ? leftSize : newSize;
+ newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * leftGraph->numElements +
- (newSize - rightSize) * right->elements.getSize();
+ (newSize - rightSize) * right->elements.getSize();
} else {
//Neither are null
- leftSize=convertSize(leftGraph->encodingSize);
- rightSize=convertSize(rightGraph->encodingSize);
- newSize=convertSize(leftGraph->estimateNewSize(rightGraph));
- newSize=(leftSize > newSize) ? leftSize: newSize;
- newSize=(rightSize > newSize) ? rightSize: newSize;
+ leftSize = convertSize(leftGraph->encodingSize);
+ rightSize = convertSize(rightGraph->encodingSize);
+ newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
+ newSize = (leftSize > newSize) ? leftSize : newSize;
+ newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * leftGraph->numElements +
- (newSize - rightSize) * rightGraph->numElements;
+ (newSize - rightSize) * rightGraph->numElements;
}
double conversionfactor = 0.5;
if ((totalCost * conversionfactor) < eeValue) {
static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
-EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+EncodingEdge *EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
EncodingEdge e(left, right, dst);
EncodingEdge *result = edgeMap.get(&e);
return result;
}
-EncodingEdge * EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+EncodingEdge *EncodingGraph::createEdge(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();
+ result = new EncodingEdge(left, right, dst);
+ VarType v1 = left->getType();
+ VarType v2 = right->getType();
if (v1 > v2) {
- VarType tmp=v2;
- v2=v1;
- v1=tmp;
+ VarType tmp = v2;
+ v2 = v1;
+ v1 = tmp;
}
if ((left != NULL && left->couldBeBinaryIndex()) &&
(right != NULL) && right->couldBeBinaryIndex()) {
- EdgeEncodingType type=(EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
+ EdgeEncodingType type = (EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
result->setEncoding(type);
if (type == EDGE_MATCH) {
mergeNodes(left, right);
static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
-EncodingNode * EncodingGraph::createNode(Element *e) {
+EncodingNode *EncodingGraph::createNode(Element *e) {
if (e->type == ELEMCONST)
return NULL;
Set *s = e->getRange();
if (n == NULL) {
n = new EncodingNode(s);
n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
-
+
encodingMap.put(s, n);
}
n->addElement(e);
return n;
}
-EncodingNode * EncodingGraph::getNode(Element *e) {
+EncodingNode *EncodingGraph::getNode(Element *e) {
if (e->type == ELEMCONST)
return NULL;
Set *s = e->getRange();
}
uint hashEncodingEdge(EncodingEdge *edge) {
- uintptr_t hash=(((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
+ uintptr_t hash = (((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
return (uint) hash;
}
#include "graphstructs.h"
class EncodingGraph {
- public:
- EncodingGraph(CSolver * solver);
+public:
+ EncodingGraph(CSolver *solver);
+ ~EncodingGraph();
void buildGraph();
void encode();
-
+
CMEMALLOC;
- private:
- CSolver * solver;
+private:
+ CSolver *solver;
HashtableEncoding encodingMap;
HashtableEdge edgeMap;
Vector<EncodingEdge *> edgeVector;
HashsetElement discovered;
HashtableNodeToSubGraph graphMap;
HashsetEncodingSubGraph subgraphs;
-
+
void encodeParent(Element *e);
void decideEdges();
void mergeNodes(EncodingNode *first, EncodingNode *second);
void processElement(Element *e);
void processFunction(ElementFunction *f);
void processPredicate(BooleanPredicate *b);
- EncodingNode * createNode(Element *e);
- EncodingNode * getNode(Element *e);
- EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
- EncodingEdge * createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+ EncodingNode *createNode(Element *e);
+ EncodingNode *getNode(Element *e);
+ EncodingEdge *getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+ EncodingEdge *createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
};
class EncodingNode {
- public:
+public:
EncodingNode(Set *_s);
void addElement(Element *e);
uint getSize() const;
VarType getType() const;
- void setEncoding(ElementEncodingType e) {encoding=e;}
+ void setEncoding(ElementEncodingType e) {encoding = e;}
ElementEncodingType getEncoding() {return encoding;}
bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
CMEMALLOC;
- private:
+private:
Set *s;
HashsetElement elements;
HashsetEncodingEdge edges;
typedef enum EdgeEncodingType EdgeEncodingType;
class EncodingEdge {
- public:
+public:
EncodingEdge(EncodingNode *_l, EncodingNode *_r);
EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
- void setEncoding(EdgeEncodingType e) {encoding=e;}
+ void setEncoding(EdgeEncodingType e) {encoding = e;}
uint64_t getValue() const;
EdgeEncodingType getEncoding() {return encoding;}
CMEMALLOC;
-
- private:
+
+private:
EncodingNode *left;
EncodingNode *right;
EncodingNode *dst;
maxEncodingVal(0) {
}
+EncodingSubGraph::~EncodingSubGraph() {
+ map.resetAndDeleteKeys();
+ values.resetAndDelete();
+}
+
uint hashNodeValuePair(NodeValuePair *nvp) {
return (uint) (nvp->value ^ ((uintptr_t)nvp->node));
}
}
int sortEncodingValue(const void *p1, const void *p2) {
- const EncodingValue * e1 = * (const EncodingValue **) p1;
- const EncodingValue * e2 = * (const EncodingValue **) p2;
- uint se1=e1->notequals.getSize();
- uint se2=e2->notequals.getSize();
+ const EncodingValue *e1 = *(const EncodingValue **) p1;
+ const EncodingValue *e2 = *(const EncodingValue **) p2;
+ uint se1 = e1->notequals.getSize();
+ uint se2 = e2->notequals.getSize();
if (se1 > se2)
return -1;
else if (se2 == se1)
void EncodingSubGraph::solveEquals() {
Vector<EncodingValue *> toEncode;
Vector<bool> encodingArray;
- SetIteratorEncodingValue *valIt=values.iterator();
- while(valIt->hasNext()) {
- EncodingValue *ev=valIt->next();
+ SetIteratorEncodingValue *valIt = values.iterator();
+ while (valIt->hasNext()) {
+ EncodingValue *ev = valIt->next();
if (!ev->inComparison)
toEncode.push(ev);
else
}
delete valIt;
bsdqsort(toEncode.expose(), toEncode.getSize(), sizeof(EncodingValue *), sortEncodingValue);
- uint toEncodeSize=toEncode.getSize();
- for(uint i=0; i<toEncodeSize; i++) {
- EncodingValue * ev=toEncode.get(i);
+ uint toEncodeSize = toEncode.getSize();
+ for (uint i = 0; i < toEncodeSize; i++) {
+ EncodingValue *ev = toEncode.get(i);
encodingArray.clear();
- SetIteratorEncodingValue *conflictIt=ev->notequals.iterator();
- while(conflictIt->hasNext()) {
- EncodingValue * conflict=conflictIt->next();
+ SetIteratorEncodingValue *conflictIt = ev->notequals.iterator();
+ while (conflictIt->hasNext()) {
+ EncodingValue *conflict = conflictIt->next();
if (conflict->assigned) {
encodingArray.setExpand(conflict->encoding, true);
}
}
delete conflictIt;
- uint encoding=0;
- for(;encoding<encodingArray.getSize();encoding++) {
+ uint encoding = 0;
+ for (; encoding < encodingArray.getSize(); encoding++) {
//See if this is unassigned
if (!encodingArray.get(encoding))
break;
void EncodingSubGraph::solveComparisons() {
HashsetEncodingValue discovered;
Vector<EncodingValue *> tovisit;
- SetIteratorEncodingValue *valIt=values.iterator();
- while(valIt->hasNext()) {
- EncodingValue *ev=valIt->next();
+ SetIteratorEncodingValue *valIt = values.iterator();
+ while (valIt->hasNext()) {
+ EncodingValue *ev = valIt->next();
if (discovered.add(ev)) {
tovisit.push(ev);
- while(tovisit.getSize()!=0) {
- EncodingValue * val=tovisit.last(); tovisit.pop();
- SetIteratorEncodingValue *nextIt=val->larger.iterator();
+ while (tovisit.getSize() != 0) {
+ EncodingValue *val = tovisit.last(); tovisit.pop();
+ SetIteratorEncodingValue *nextIt = val->larger.iterator();
uint minVal = val->encoding + 1;
- while(nextIt->hasNext()) {
- EncodingValue *nextVal=nextIt->next();
+ while (nextIt->hasNext()) {
+ EncodingValue *nextVal = nextIt->next();
if (nextVal->encoding < minVal) {
if (minVal > maxEncodingVal)
maxEncodingVal = minVal;
}
uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
- uint newSize=0;
- SetIteratorEncodingNode * nit = sg->nodes.iterator();
- while(nit->hasNext()) {
+ uint newSize = 0;
+ SetIteratorEncodingNode *nit = sg->nodes.iterator();
+ while (nit->hasNext()) {
EncodingNode *en = nit->next();
- uint size=estimateNewSize(en);
+ uint size = estimateNewSize(en);
if (size > newSize)
newSize = size;
}
}
uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
- SetIteratorEncodingEdge * eeit = n->edges.iterator();
- uint newsize=n->getSize();
- while(eeit->hasNext()) {
- EncodingEdge * ee = eeit->next();
+ SetIteratorEncodingEdge *eeit = n->edges.iterator();
+ uint newsize = n->getSize();
+ while (eeit->hasNext()) {
+ EncodingEdge *ee = eeit->next();
if (ee->left != NULL && ee->left != n && nodes.contains(ee->left)) {
uint intersectSize = n->s->getUnionSize(ee->left->s);
if (intersectSize > newsize)
void EncodingSubGraph::addNode(EncodingNode *n) {
nodes.add(n);
- uint newSize=estimateNewSize(n);
+ uint newSize = estimateNewSize(n);
numElements += n->elements.getSize();
if (newSize > encodingSize)
- encodingSize=newSize;
+ encodingSize = newSize;
}
-SetIteratorEncodingNode * EncodingSubGraph::nodeIterator() {
+SetIteratorEncodingNode *EncodingSubGraph::nodeIterator() {
return nodes.iterator();
}
}
void EncodingSubGraph::computeEqualities() {
- SetIteratorEncodingNode *nodeit=nodes.iterator();
- while(nodeit->hasNext()) {
- EncodingNode *node=nodeit->next();
+ SetIteratorEncodingNode *nodeit = nodes.iterator();
+ while (nodeit->hasNext()) {
+ EncodingNode *node = nodeit->next();
generateEquals(node, node);
-
- SetIteratorEncodingEdge *edgeit=node->edges.iterator();
- while(edgeit->hasNext()) {
- EncodingEdge *edge=edgeit->next();
+
+ SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+ while (edgeit->hasNext()) {
+ EncodingEdge *edge = edgeit->next();
//skip over comparisons as we have already handled them
if (edge->numComparisons != 0)
continue;
}
void EncodingSubGraph::computeComparisons() {
- SetIteratorEncodingNode *nodeit=nodes.iterator();
- while(nodeit->hasNext()) {
- EncodingNode *node=nodeit->next();
- SetIteratorEncodingEdge *edgeit=node->edges.iterator();
- while(edgeit->hasNext()) {
- EncodingEdge *edge=edgeit->next();
+ SetIteratorEncodingNode *nodeit = nodes.iterator();
+ while (nodeit->hasNext()) {
+ EncodingNode *node = nodeit->next();
+ SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+ while (edgeit->hasNext()) {
+ EncodingEdge *edge = edgeit->next();
if (edge->numComparisons == 0)
continue;
if (edge->left == NULL || !nodes.contains(edge->left))
}
void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
- Set *lset=left->s;
- Set *rset=right->s;
- uint lSize=lset->getSize(), rSize=rset->getSize();
- for(uint lindex=0; lindex < lSize; lindex++) {
- for(uint rindex=0; rindex < rSize; rindex++) {
- uint64_t lVal=lset->getElement(lindex);
+ Set *lset = left->s;
+ Set *rset = right->s;
+ uint lSize = lset->getSize(), rSize = rset->getSize();
+ for (uint lindex = 0; lindex < lSize; lindex++) {
+ for (uint rindex = 0; rindex < rSize; rindex++) {
+ uint64_t lVal = lset->getElement(lindex);
NodeValuePair nvp1(left, lVal);
EncodingValue *lev = map.get(&nvp1);
- uint64_t rVal=rset->getElement(rindex);
+ uint64_t rVal = rset->getElement(rindex);
NodeValuePair nvp2(right, rVal);
EncodingValue *rev = map.get(&nvp2);
if (lev != rev) {
}
void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *right) {
- Set *lset=left->s;
- Set *rset=right->s;
- uint lindex=0, rindex=0;
- uint lSize=lset->getSize(), rSize=rset->getSize();
- uint64_t lVal=lset->getElement(lindex);
+ Set *lset = left->s;
+ Set *rset = right->s;
+ uint lindex = 0, rindex = 0;
+ uint lSize = lset->getSize(), rSize = rset->getSize();
+ uint64_t lVal = lset->getElement(lindex);
NodeValuePair nvp1(left, lVal);
EncodingValue *lev = map.get(&nvp1);
lev->inComparison = true;
- uint64_t rVal=rset->getElement(rindex);
+ uint64_t rVal = rset->getElement(rindex);
NodeValuePair nvp2(right, rVal);
EncodingValue *rev = map.get(&nvp2);
rev->inComparison = true;
EncodingValue *last = NULL;
- while(lindex < lSize || rindex < rSize) {
+ while (lindex < lSize || rindex < rSize) {
if (last != NULL) {
if (lev != NULL)
orderEV(last, lev);
orderEV(lev, rev);
last = lev;
if (++lindex < lSize) {
- lVal=lset->getElement(lindex);
+ lVal = lset->getElement(lindex);
NodeValuePair nvpl(left, lVal);
lev = map.get(&nvpl);
lev->inComparison = true;
orderEV(rev, lev);
last = rev;
if (++rindex < rSize) {
- rVal=rset->getElement(rindex);
+ rVal = rset->getElement(rindex);
NodeValuePair nvpr(right, rVal);
rev = map.get(&nvpr);
rev->inComparison = true;
} else {
last = lev;
if (++lindex < lSize) {
- lVal=lset->getElement(lindex);
+ lVal = lset->getElement(lindex);
NodeValuePair nvpl(left, lVal);
lev = map.get(&nvpl);
lev->inComparison = true;
lev = NULL;
if (++rindex < rSize) {
- rVal=rset->getElement(rindex);
+ rVal = rset->getElement(rindex);
NodeValuePair nvpr(right, rVal);
rev = map.get(&nvpr);
rev->inComparison = true;
}
void EncodingSubGraph::computeEncodingValue() {
- SetIteratorEncodingNode *nodeit=nodes.iterator();
- while(nodeit->hasNext()) {
- EncodingNode *node=nodeit->next();
- Set * set = node->s;
+ SetIteratorEncodingNode *nodeit = nodes.iterator();
+ while (nodeit->hasNext()) {
+ EncodingNode *node = nodeit->next();
+ Set *set = node->s;
uint setSize = set->getSize();
- for(uint i=0; i<setSize; i++) {
+ for (uint i = 0; i < setSize; i++) {
uint64_t val = set->getElement(i);
NodeValuePair nvp(node, val);
if (!map.contains(&nvp)) {
}
void EncodingSubGraph::traverseValue(EncodingNode *node, uint64_t value) {
- EncodingValue *ecv=new EncodingValue(value);
+ EncodingValue *ecv = new EncodingValue(value);
values.add(ecv);
HashsetEncodingNode discovered;
Vector<EncodingNode *> tovisit;
tovisit.push(node);
discovered.add(node);
- while(tovisit.getSize()!=0) {
- EncodingNode *n=tovisit.last();tovisit.pop();
+ while (tovisit.getSize() != 0) {
+ EncodingNode *n = tovisit.last();tovisit.pop();
//Add encoding node to structures
ecv->nodes.add(n);
- NodeValuePair *nvp=new NodeValuePair(n, value);
+ NodeValuePair *nvp = new NodeValuePair(n, value);
map.put(nvp, ecv);
- SetIteratorEncodingEdge *edgeit=node->edges.iterator();
- while(edgeit->hasNext()) {
- EncodingEdge *ee=edgeit->next();
+ SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+ while (edgeit->hasNext()) {
+ EncodingEdge *ee = edgeit->next();
if (!discovered.contains(ee->left) && nodes.contains(ee->left) && ee->left->s->exists(value)) {
tovisit.push(ee->left);
discovered.add(ee->left);
#include "graphstructs.h"
class NodeValuePair {
- public:
- NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
+public:
+ NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
EncodingNode *node;
uint64_t value;
};
typedef SetIterator<EncodingValue *, uintptr_t, PTRSHIFT> SetIteratorEncodingValue;
class EncodingValue {
- public:
- EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
+public:
+ EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
void merge(EncodingValue *value);
uint64_t value;
uint encoding;
typedef Hashtable<NodeValuePair *, EncodingValue *, uintptr_t, 0, hashNodeValuePair, equalsNodeValuePair> NVPMap;
class EncodingSubGraph {
- public:
+public:
EncodingSubGraph();
+ ~EncodingSubGraph();
void addNode(EncodingNode *n);
- SetIteratorEncodingNode * nodeIterator();
+ SetIteratorEncodingNode *nodeIterator();
void encode();
uint getEncoding(EncodingNode *n, uint64_t val);
- uint getEncodingSize(EncodingNode *n) { return maxEncodingVal;}
-
+ uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;}
+
CMEMALLOC;
- private:
+private:
uint estimateNewSize(EncodingNode *n);
uint estimateNewSize(EncodingSubGraph *sg);
void traverseValue(EncodingNode *node, uint64_t value);
uint encodingSize;
uint numElements;
uint maxEncodingVal;
-
+
friend class EncodingGraph;
};
#include "mutableset.h"
#include "tunable.h"
-void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
- SetIteratorOrderNode *iterator = graph->getNodes();
- while (iterator->hasNext()) {
- OrderNode *node = iterator->next();
- if (node->status == NOTVISITED) {
- node->status = VISITED;
- DFSNodeVisit(node, finishNodes, false, false, 0);
- node->status = FINISHED;
- finishNodes->push(node);
- }
- }
- delete iterator;
-}
-
-void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
- uint size = finishNodes->getSize();
- uint sccNum = 1;
- for (int i = size - 1; i >= 0; i--) {
- OrderNode *node = finishNodes->get(i);
- if (node->status == NOTVISITED) {
- node->status = VISITED;
- DFSNodeVisit(node, NULL, true, false, sccNum);
- node->sccNum = sccNum;
- node->status = FINISHED;
- sccNum++;
- }
- }
-}
-
-void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
- SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
-#ifdef TRACE_DEBUG
- model_print("Node:%lu=>", node->id);
-#endif
- while (iterator->hasNext()) {
- OrderEdge *edge = iterator->next();
-#ifdef TRACE_DEBUG
- model_print("Edge:%lu=>",(uintptr_t) edge);
-#endif
- if (mustvisit) {
- if (!edge->mustPos)
- continue;
- } else
- if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
- continue;
-
- OrderNode *child = isReverse ? edge->source : edge->sink;
-#ifdef TRACE_DEBUG
- model_println("NodeChild:%lu", child->id);
-#endif
- if (child->status == NOTVISITED) {
- child->status = VISITED;
- DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
- child->status = FINISHED;
- if (finishNodes != NULL)
- finishNodes->push(child);
- if (isReverse)
- child->sccNum = sccNum;
- }
- }
- delete iterator;
-}
-
-void resetNodeInfoStatusSCC(OrderGraph *graph) {
- SetIteratorOrderNode *iterator = graph->getNodes();
- while (iterator->hasNext()) {
- iterator->next()->status = NOTVISITED;
- }
- delete iterator;
-}
-
-void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
- Vector<OrderNode *> finishNodes;
- DFS(graph, &finishNodes);
- resetNodeInfoStatusSCC(graph);
- DFSReverse(graph, &finishNodes);
- resetNodeInfoStatusSCC(graph);
-}
-
-bool isMustBeTrueNode(OrderNode *node) {
- SetIteratorOrderEdge *iterator = node->inEdges.iterator();
- while (iterator->hasNext()) {
- OrderEdge *edge = iterator->next();
- if (!edge->mustPos) {
- delete iterator;
- return false;
- }
- }
- delete iterator;
- iterator = node->outEdges.iterator();
- while (iterator->hasNext()) {
- OrderEdge *edge = iterator->next();
- if (!edge->mustPos) {
- delete iterator;
- return false;
- }
- }
- delete iterator;
- return true;
-}
-
-void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
- SetIteratorOrderEdge *iterin = node->inEdges.iterator();
- while (iterin->hasNext()) {
- OrderEdge *inEdge = iterin->next();
- OrderNode *srcNode = inEdge->source;
- srcNode->outEdges.remove(inEdge);
- SetIteratorOrderEdge *iterout = node->outEdges.iterator();
- while (iterout->hasNext()) {
- OrderEdge *outEdge = iterout->next();
- OrderNode *sinkNode = outEdge->sink;
- sinkNode->inEdges.remove(outEdge);
- //Adding new edge to new sink and src nodes ...
- if(srcNode == sinkNode){
-#ifdef TRACE_DEBUG
- model_println("bypassMustBe 1");
-#endif
- This->setUnSAT();
- delete iterout;
- delete iterin;
- return;
- }
- OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
- newEdge->mustPos = true;
- newEdge->polPos = true;
- if (newEdge->mustNeg){
-#ifdef TRACE_DEBUG
- model_println("BypassMustBe 2");
-#endif
- This->setUnSAT();
- }
- srcNode->outEdges.add(newEdge);
- sinkNode->inEdges.add(newEdge);
- }
- delete iterout;
- }
- delete iterin;
-}
-
-void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
- SetIteratorOrderNode *iterator = graph->getNodes();
- while (iterator->hasNext()) {
- OrderNode *node = iterator->next();
- if (isMustBeTrueNode(node)) {
- bypassMustBeTrueNode(This, graph, node);
- }
- }
- delete iterator;
-}
-
-/** This function computes a source set for every nodes, the set of
- nodes that can reach that node via pospolarity edges. It then
- looks for negative polarity edges from nodes in the the source set
- to determine whether we need to generate pseudoPos edges. */
-
-void completePartialOrderGraph(OrderGraph *graph) {
- Vector<OrderNode *> finishNodes;
- DFS(graph, &finishNodes);
- resetNodeInfoStatusSCC(graph);
- HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-
- Vector<OrderNode *> sccNodes;
-
- uint size = finishNodes.getSize();
- uint sccNum = 1;
- for (int i = size - 1; i >= 0; i--) {
- OrderNode *node = finishNodes.get(i);
- HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
- table->put(node, sources);
-
- if (node->status == NOTVISITED) {
- //Need to do reverse traversal here...
- node->status = VISITED;
- DFSNodeVisit(node, &sccNodes, true, false, sccNum);
- node->status = FINISHED;
- node->sccNum = sccNum;
- sccNum++;
- sccNodes.push(node);
-
- //Compute in set for entire SCC
- uint rSize = sccNodes.getSize();
- for (uint j = 0; j < rSize; j++) {
- OrderNode *rnode = sccNodes.get(j);
- //Compute source sets
- SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
- while (iterator->hasNext()) {
- OrderEdge *edge = iterator->next();
- OrderNode *parent = edge->source;
- if (edge->polPos) {
- sources->add(parent);
- HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
- sources->addAll(parent_srcs);
- }
- }
- delete iterator;
- }
- for (uint j = 0; j < rSize; j++) {
- //Copy in set of entire SCC
- OrderNode *rnode = sccNodes.get(j);
- HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
- table->put(rnode, set);
-
- //Use source sets to compute pseudoPos edges
- SetIteratorOrderEdge *iterator = node->inEdges.iterator();
- while (iterator->hasNext()) {
- OrderEdge *edge = iterator->next();
- OrderNode *parent = edge->source;
- ASSERT(parent != rnode);
- if (edge->polNeg && parent->sccNum != rnode->sccNum &&
- sources->contains(parent)) {
- OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
- newedge->pseudoPos = true;
- }
- }
- delete iterator;
- }
-
- sccNodes.clear();
- }
- }
-
- table->resetanddelete();
- delete table;
- resetNodeInfoStatusSCC(graph);
-}
-
-void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
- SetIteratorOrderNode *iterator = graph->getNodes();
- while (iterator->hasNext()) {
- OrderNode *node = iterator->next();
- if (node->status == NOTVISITED) {
- node->status = VISITED;
- DFSNodeVisit(node, finishNodes, false, true, 0);
- node->status = FINISHED;
- finishNodes->push(node);
- }
- }
- delete iterator;
-}
-
void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
uint size = finishNodes->getSize();
HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
SetIteratorOrderNode *srciterator = sources->iterator();
while (srciterator->hasNext()) {
OrderNode *srcnode = srciterator->next();
+ if (srcnode->removed)
+ continue;
OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
newedge->mustPos = true;
newedge->polPos = true;
- if (newedge->mustNeg){
-#ifdef TRACE_DEBUG
- model_println("DFS clear 1");
-#endif
+ if (newedge->mustNeg)
solver->setUnSAT();
- }
srcnode->outEdges.add(newedge);
node->inEdges.add(newedge);
}
if (!edge->mustPos && sources->contains(parent)) {
edge->mustPos = true;
edge->polPos = true;
- if (edge->mustNeg){
-#ifdef TRACE_DEBUG
- model_println("DFS clear 2");
-#endif
- solver->setUnSAT();
- }
+ if (edge->mustNeg)
+ solver->setUnSAT();
}
}
delete iterator;
if (!edge->mustNeg && sources->contains(child)) {
edge->mustNeg = true;
edge->polNeg = true;
- if (edge->mustPos){
-#ifdef TRACE_DEBUG
- model_println("DFS clear 3: NodeFrom:%lu=>edge%lu=>NodeTo:%lu", node->id, (uintptr_t) edge, child->id);
-#endif
- solver->setUnSAT();
- }
+ if (edge->mustPos) {
+ solver->setUnSAT();
+ }
}
}
delete iterator;
}
}
- table->resetanddelete();
+ table->resetAndDeleteVals();
delete table;
}
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
Vector<OrderNode *> finishNodes;
//Topologically sort the mustPos edge graph
- DFSMust(graph, &finishNodes);
- resetNodeInfoStatusSCC(graph);
+ graph->DFSMust(&finishNodes);
+ graph->resetNodeInfoStatusSCC();
//Find any backwards edges that complete cycles and force them to be mustNeg
DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
if (invEdge != NULL) {
if (!invEdge->mustPos) {
invEdge->polPos = false;
- } else {
-#ifdef TRACE_DEBUG
- model_println("localMustAnalysis Total");
-#endif
+ } else
solver->setUnSAT();
- }
invEdge->mustNeg = true;
invEdge->polNeg = true;
}
if (edge->mustPos) {
if (!edge->mustNeg) {
edge->polNeg = false;
- } else{
-#ifdef TRACE_DEBUG
- model_println("Local must analysis partial");
-#endif
+ } else {
solver->setUnSAT();
- }
+ }
OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
if (invEdge != NULL) {
if (!invEdge->mustPos)
invEdge->polPos = false;
- else{
-#ifdef TRACE_DEBUG
- model_println("Local must analysis partial 2");
-#endif
+ else
solver->setUnSAT();
- }
invEdge->mustNeg = true;
invEdge->polNeg = true;
}
#include "structs.h"
#include "mymemory.h"
-void computeStronglyConnectedComponentGraph(OrderGraph *graph);
-void initializeNodeInfoSCC(OrderGraph *graph);
-void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
-void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void completePartialOrderGraph(OrderGraph *graph);
-void resetNodeInfoStatusSCC(OrderGraph *graph);
-bool isMustBeTrueNode(OrderNode *node);
-void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node);
-void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
-void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
#include "order.h"
OrderGraph::OrderGraph(Order *_order) :
- nodes(new HashsetOrderNode()),
- edges(new HashsetOrderEdge()),
order(_order) {
}
OrderGraph *buildOrderGraph(Order *order) {
- ASSERT(order->graph == NULL);
+ ASSERT(order->graph == NULL);
OrderGraph *orderGraph = new OrderGraph(order);
- order->graph = orderGraph;
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
//Builds only the subgraph for the must order graph.
OrderGraph *buildMustOrderGraph(Order *order) {
- ASSERT(order->graph == NULL);
+ ASSERT(order->graph == NULL);
OrderGraph *orderGraph = new OrderGraph(order);
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
}
}
+void OrderGraph::addEdge(uint64_t first, uint64_t second) {
+ OrderNode *node1 = getOrderNodeFromOrderGraph(first);
+ OrderNode *node2 = getOrderNodeFromOrderGraph(second);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
+ _1to2->polPos = true;
+ _1to2->mustPos = true;
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
+}
+
void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
BooleanValue mustval = constr->boolVal;
switch (mustval) {
OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
OrderNode *node = new OrderNode(id);
- OrderNode *tmp = nodes->get(node);
+ OrderNode *tmp = nodes.get(node);
if ( tmp != NULL) {
delete node;
node = tmp;
} else {
- nodes->add(node);
+ nodes.add(node);
}
return node;
}
OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
OrderNode node(id);
- OrderNode *tmp = nodes->get(&node);
+ OrderNode *tmp = nodes.get(&node);
return tmp;
}
OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
OrderEdge *edge = new OrderEdge(begin, end);
- OrderEdge *tmp = edges->get(edge);
+ OrderEdge *tmp = edges.get(edge);
if ( tmp != NULL ) {
delete edge;
edge = tmp;
} else {
- edges->add(edge);
+ edges.add(edge);
}
return edge;
}
OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
OrderEdge edge(begin, end);
- OrderEdge *tmp = edges->get(&edge);
+ OrderEdge *tmp = edges.get(&edge);
return tmp;
}
OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
OrderEdge inverseedge(edge->sink, edge->source);
- OrderEdge *tmp = edges->get(&inverseedge);
+ OrderEdge *tmp = edges.get(&inverseedge);
return tmp;
}
}
OrderGraph::~OrderGraph() {
- SetIteratorOrderNode *iterator = nodes->iterator();
- while (iterator->hasNext()) {
- OrderNode *node = iterator->next();
- delete node;
- }
- delete iterator;
-
- SetIteratorOrderEdge *eiterator = edges->iterator();
- while (eiterator->hasNext()) {
- OrderEdge *edge = eiterator->next();
- delete edge;
- }
- delete eiterator;
- delete nodes;
- delete edges;
+ nodes.resetAndDelete();
+ edges.resetAndDelete();
}
-bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
+bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
HashsetOrderNode visited;
visited.add(source);
SetIteratorOrderEdge *iterator = source->outEdges.iterator();
bool found = false;
- while(iterator->hasNext()){
- OrderEdge* edge = iterator->next();
- if(edge->polPos){
- OrderNode* node = edge->sink;
- if(!visited.contains(node)){
- if( node == destination ){
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (edge->polPos) {
+ OrderNode *node = edge->sink;
+ if (!visited.contains(node)) {
+ if ( node == destination ) {
found = true;
break;
}
visited.add(node);
- found =isTherePathVisit(visited, node, destination);
- if(found){
+ found = isTherePathVisit(visited, node, destination);
+ if (found) {
break;
}
}
return found;
}
-bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
+bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
SetIteratorOrderEdge *iterator = current->outEdges.iterator();
bool found = false;
- while(iterator->hasNext()){
- OrderEdge* edge = iterator->next();
- if(edge->polPos){
- OrderNode* node = edge->sink;
- if(node == destination){
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (edge->polPos) {
+ OrderNode *node = edge->sink;
+ if (node == destination) {
found = true;
break;
}
visited.add(node);
- if(isTherePathVisit(visited, node, destination)){
+ if (isTherePathVisit(visited, node, destination)) {
found = true;
break;
}
delete iterator;
return found;
}
+
+void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
+ SetIteratorOrderNode *iterator = getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = iterator->next();
+ if (node->status == NOTVISITED && !node->removed) {
+ node->status = VISITED;
+ DFSNodeVisit(node, finishNodes, false, false, 0);
+ node->status = FINISHED;
+ finishNodes->push(node);
+ }
+ }
+ delete iterator;
+}
+
+void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
+ SetIteratorOrderNode *iterator = getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = iterator->next();
+ if (node->status == NOTVISITED && !node->removed) {
+ node->status = VISITED;
+ DFSNodeVisit(node, finishNodes, false, true, 0);
+ node->status = FINISHED;
+ finishNodes->push(node);
+ }
+ }
+ delete iterator;
+}
+
+void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
+ uint size = finishNodes->getSize();
+ uint sccNum = 1;
+ for (int i = size - 1; i >= 0; i--) {
+ OrderNode *node = finishNodes->get(i);
+ if (node->status == NOTVISITED) {
+ node->status = VISITED;
+ DFSNodeVisit(node, NULL, true, false, sccNum);
+ node->sccNum = sccNum;
+ node->status = FINISHED;
+ sccNum++;
+ }
+ }
+}
+
+void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
+ SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (mustvisit) {
+ if (!edge->mustPos)
+ continue;
+ } else
+ if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
+ continue;
+
+ OrderNode *child = isReverse ? edge->source : edge->sink;
+ if (child->status == NOTVISITED) {
+ child->status = VISITED;
+ DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
+ child->status = FINISHED;
+ if (finishNodes != NULL) {
+ finishNodes->push(child);
+ }
+ if (isReverse)
+ child->sccNum = sccNum;
+ }
+ }
+ delete iterator;
+}
+
+void OrderGraph::resetNodeInfoStatusSCC() {
+ SetIteratorOrderNode *iterator = getNodes();
+ while (iterator->hasNext()) {
+ iterator->next()->status = NOTVISITED;
+ }
+ delete iterator;
+}
+
+void OrderGraph::computeStronglyConnectedComponentGraph() {
+ Vector<OrderNode *> finishNodes;
+ DFS(&finishNodes);
+ resetNodeInfoStatusSCC();
+ DFSReverse(&finishNodes);
+ resetNodeInfoStatusSCC();
+}
+
+/** This function computes a source set for every nodes, the set of
+ nodes that can reach that node via pospolarity edges. It then
+ looks for negative polarity edges from nodes in the the source set
+ to determine whether we need to generate pseudoPos edges. */
+
+void OrderGraph::completePartialOrderGraph() {
+ Vector<OrderNode *> finishNodes;
+ DFS(&finishNodes);
+ resetNodeInfoStatusSCC();
+ HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
+
+ Vector<OrderNode *> sccNodes;
+
+ uint size = finishNodes.getSize();
+ uint sccNum = 1;
+ for (int i = size - 1; i >= 0; i--) {
+ OrderNode *node = finishNodes.get(i);
+ HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
+ table->put(node, sources);
+
+ if (node->status == NOTVISITED) {
+ //Need to do reverse traversal here...
+ node->status = VISITED;
+ DFSNodeVisit(node, &sccNodes, true, false, sccNum);
+ node->status = FINISHED;
+ node->sccNum = sccNum;
+ sccNum++;
+ sccNodes.push(node);
+
+ //Compute in set for entire SCC
+ uint rSize = sccNodes.getSize();
+ for (uint j = 0; j < rSize; j++) {
+ OrderNode *rnode = sccNodes.get(j);
+ //Compute source sets
+ SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ OrderNode *parent = edge->source;
+ if (edge->polPos) {
+ sources->add(parent);
+ HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
+ sources->addAll(parent_srcs);
+ }
+ }
+ delete iterator;
+ }
+ for (uint j = 0; j < rSize; j++) {
+ //Copy in set of entire SCC
+ OrderNode *rnode = sccNodes.get(j);
+ HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
+ table->put(rnode, set);
+
+ //Use source sets to compute pseudoPos edges
+ SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ OrderNode *parent = edge->source;
+ ASSERT(parent != rnode);
+ if (edge->polNeg && parent->sccNum != rnode->sccNum &&
+ sources->contains(parent)) {
+ OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
+ newedge->pseudoPos = true;
+ }
+ }
+ delete iterator;
+ }
+
+ sccNodes.clear();
+ }
+ }
+
+ table->resetAndDeleteVals();
+ delete table;
+ resetNodeInfoStatusSCC();
+}
OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+ void addEdge(uint64_t first, uint64_t second);
OrderEdge *getInverseOrderEdge(OrderEdge *edge);
- Order *getOrder() {return order;}
- bool isTherePath(OrderNode* source, OrderNode* destination);
- bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
- SetIteratorOrderNode *getNodes() {return nodes->iterator();}
- SetIteratorOrderEdge *getEdges() {return edges->iterator();}
+ Order *getOrder() {return order;}
+ bool isTherePath(OrderNode *source, OrderNode *destination);
+ bool isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination);
+ SetIteratorOrderNode *getNodes() {return nodes.iterator();}
+ SetIteratorOrderEdge *getEdges() {return edges.iterator();}
+ void DFS(Vector<OrderNode *> *finishNodes);
+ void DFSMust(Vector<OrderNode *> *finishNodes);
+ void computeStronglyConnectedComponentGraph();
+ void resetNodeInfoStatusSCC();
+ void completePartialOrderGraph();
CMEMALLOC;
private:
- HashsetOrderNode *nodes;
- HashsetOrderEdge *edges;
+ HashsetOrderNode nodes;
+ HashsetOrderEdge edges;
Order *order;
+ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
+ void DFSReverse(Vector<OrderNode *> *finishNodes);
};
OrderGraph *buildOrderGraph(Order *order);
OrderNode::OrderNode(uint64_t _id) :
id(_id),
status(NOTVISITED),
+ removed(false),
sccNum(0),
inEdges(),
outEdges() {
OrderNode(uint64_t id);
void addNewIncomingEdge(OrderEdge *edge);
void addNewOutgoingEdge(OrderEdge *edge);
+ uint64_t getID() {return id;}
uint64_t id;
NodeStatus status;
+ bool removed;
uint sccNum;
HashsetOrderEdge inEdges;
HashsetOrderEdge outEdges;
}
void computeLogicOpPolarity(BooleanLogic *This) {
- Polarity child=computeLogicOpPolarityChildren(This);
+ Polarity child = computeLogicOpPolarityChildren(This);
uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- BooleanEdge b=This->inputs.get(i);
+ BooleanEdge b = This->inputs.get(i);
computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
}
}
void DecomposeOrderTransform::doTransform() {
HashsetOrder *orders = solver->getActiveOrders()->copy();
- SetIteratorOrder * orderit=orders->iterator();
- while(orderit->hasNext()) {
+ SetIteratorOrder *orderit = orders->iterator();
+ while (orderit->hasNext()) {
Order *order = orderit->next();
if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
continue;
}
+ DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
+ order->setOrderResolver(dor);
+
OrderGraph *graph = buildOrderGraph(order);
if (order->type == SATC_PARTIAL) {
//Required to do SCC analysis for partial order graphs. It
//makes sure we don't incorrectly optimize graphs with negative
//polarity edges
- completePartialOrderGraph(graph);
+ graph->completePartialOrderGraph();
}
bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
-
if (mustReachGlobal)
reachMustAnalysis(solver, graph, false);
bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-
if (mustReachLocal) {
//This pair of analysis is also optional
if (order->type == SATC_PARTIAL) {
}
}
-
bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+ HashsetOrderEdge *edgesRemoved = NULL;
+
+ if (mustReachPrune) {
+ edgesRemoved = new HashsetOrderEdge();
+ removeMustBeTrueNodes(graph, edgesRemoved);
+ }
- if (mustReachPrune)
- removeMustBeTrueNodes(solver, graph);
-
//This is needed for splitorder
- computeStronglyConnectedComponentGraph(graph);
- decomposeOrder(order, graph);
+ graph->computeStronglyConnectedComponentGraph();
+ decomposeOrder(order, graph, edgesRemoved, dor);
+ if (edgesRemoved != NULL)
+ delete edgesRemoved;
+ delete graph;
}
delete orderit;
delete orders;
}
-void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
- Vector<Order *> ordervec;
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
Vector<Order *> partialcandidatevec;
uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
BooleanOrder *orderconstraint = currOrder->constraints.get(i);
OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
+ OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
+ OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
+ if (edgesRemoved != NULL) {
+ if (edgesRemoved->contains(edge)) {
+ dor->mustOrderEdge(from->getID(), to->getID());
+ solver->replaceBooleanWithTrue(orderconstraint);
+ continue;
+ } else if (edgesRemoved->contains(invedge)) {
+ dor->mustOrderEdge(to->getID(), from->getID());
+ solver->replaceBooleanWithFalse(orderconstraint);
+ continue;
+ }
+ }
+
if (from->sccNum != to->sccNum) {
- OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
if (edge != NULL) {
if (edge->polPos) {
+ dor->mustOrderEdge(from->getID(), to->getID());
solver->replaceBooleanWithTrue(orderconstraint);
} else if (edge->polNeg) {
+ if (currOrder->type == SATC_TOTAL)
+ dor->mustOrderEdge(to->getID(), from->getID());
solver->replaceBooleanWithFalse(orderconstraint);
} else {
//This case should only be possible if constraint isn't in AST
;
}
} else {
- OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
if (invedge != NULL) {
if (invedge->polPos) {
+ dor->mustOrderEdge(to->getID(), from->getID());
solver->replaceBooleanWithFalse(orderconstraint);
} else if (edge->polNeg) {
//This case shouldn't happen... If we have a partial order,
} else {
//Build new order and change constraint's order
Order *neworder = NULL;
- if (ordervec.getSize() > from->sccNum)
- neworder = ordervec.get(from->sccNum);
+ neworder = dor->getOrder(from->sccNum);
if (neworder == NULL) {
MutableSet *set = solver->createMutableSet(currOrder->set->getType());
neworder = solver->createOrder(currOrder->type, set);
- ordervec.setExpand(from->sccNum, neworder);
+ dor->setOrder(from->sccNum, neworder);
if (currOrder->type == SATC_PARTIAL)
partialcandidatevec.setExpand(from->sccNum, neworder);
else
((MutableSet *)neworder->set)->addElementMSet(to->id);
}
if (currOrder->type == SATC_PARTIAL) {
- OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polNeg)
partialcandidatevec.setExpand(from->sccNum, NULL);
}
orderconstraint->order = neworder;
+ dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
neworder->addOrderConstraint(orderconstraint);
}
}
- currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
solver->getActiveOrders()->remove(currOrder);
uint pcvsize = partialcandidatevec.getSize();
for (uint i = 0; i < pcvsize; i++) {
}
}
}
+
+bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
+ SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (!edge->mustPos) {
+ delete iterator;
+ return false;
+ }
+ }
+ delete iterator;
+ iterator = node->outEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (!edge->mustPos) {
+ delete iterator;
+ return false;
+ }
+ }
+ delete iterator;
+ return true;
+}
+
+void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+ node->removed = true;
+ SetIteratorOrderEdge *iterin = node->inEdges.iterator();
+ while (iterin->hasNext()) {
+ OrderEdge *inEdge = iterin->next();
+ OrderNode *srcNode = inEdge->source;
+ srcNode->outEdges.remove(inEdge);
+ edgesRemoved->add(inEdge);
+ bool removeOutgoingEdges = !iterin->hasNext();
+
+ SetIteratorOrderEdge *iterout = node->outEdges.iterator();
+ while (iterout->hasNext()) {
+ OrderEdge *outEdge = iterout->next();
+ OrderNode *sinkNode = outEdge->sink;
+ if (removeOutgoingEdges) {
+ sinkNode->inEdges.remove(outEdge);
+ edgesRemoved->add(outEdge);
+ }
+ //Adding new edge to new sink and src nodes ...
+ if (srcNode == sinkNode) {
+ solver->setUnSAT();
+ delete iterout;
+ delete iterin;
+ return;
+ }
+ //Add new order constraint
+ BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+ solver->addConstraint(orderconstraint);
+
+ //Add new edge
+ OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
+ newEdge->mustPos = true;
+ newEdge->polPos = true;
+ if (newEdge->mustNeg)
+ solver->setUnSAT();
+ srcNode->outEdges.add(newEdge);
+ sinkNode->inEdges.add(newEdge);
+ }
+ delete iterout;
+ }
+ delete iterin;
+}
+
+void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
+ SetIteratorOrderNode *iterator = graph->getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = iterator->next();
+ if (isMustBeTrueNode(node)) {
+ bypassMustBeTrueNode(graph, node, edgesRemoved);
+ }
+ }
+ delete iterator;
+}
DecomposeOrderTransform(CSolver *_solver);
~DecomposeOrderTransform();
void doTransform();
- void decomposeOrder (Order *currOrder, OrderGraph *currGraph);
CMEMALLOC;
private:
+ bool isMustBeTrueNode(OrderNode *node);
+ void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved);
+ void decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor);
+ void removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved);
};
+
+
#endif/* ORDERTRANSFORM_H */
void IntegerEncodingTransform::doTransform() {
HashsetOrder *orders = solver->getActiveOrders()->copy();
- SetIteratorOrder * orderit=orders->iterator();
- while(orderit->hasNext()) {
+ SetIteratorOrder *orderit = orders->iterator();
+ while (orderit->hasNext()) {
Order *order = orderit->next();
if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
integerEncode(order);
void Preprocess::doTransform() {
if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
return;
-
+
BooleanIterator bit(solver);
- while(bit.hasNext()) {
- Boolean *b=bit.next();
+ while (bit.hasNext()) {
+ Boolean *b = bit.next();
if (b->type == BOOLEANVAR)
processBooleanVar((BooleanVar *)b);
}
}
void Preprocess::resolveBooleanVars() {
- SetIteratorBoolean * iterator = toremove.iterator();
+ SetIteratorBoolean *iterator = toremove.iterator();
while (iterator->hasNext()) {
BooleanVar *bv = (BooleanVar *) iterator->next();
if (bv->polarity == P_TRUE) {
delete iterator;
}
-void Preprocess::processBooleanVar(BooleanVar * b) {
- if (b->polarity==P_TRUE ||
- b->polarity==P_FALSE) {
+void Preprocess::processBooleanVar(BooleanVar *b) {
+ if (b->polarity == P_TRUE ||
+ b->polarity == P_FALSE) {
toremove.add(b);
}
}
#include "transform.h"
class Preprocess : public Transform {
- public:
+public:
Preprocess(CSolver *_solver);
~Preprocess();
void doTransform();
-
+
CMEMALLOC;
- private:
+private:
HashsetBoolean toremove;
- void processBooleanVar(BooleanVar * b);
+ void processBooleanVar(BooleanVar *b);
void resolveBooleanVars();
};
convertPass(cnf, false);
finishedClauses(cnf->solver);
long long startSolve = getTimeNano();
-#ifdef TRACE_DEBUG
- model_println("Backend: Calling the SAT Solver from CSolver ...");
-#endif
- int result = solve(cnf->solver);
- model_print("Backend: Result got from SATSolver: %d", result);
+ int result = solve(cnf->solver);
long long finishTime = getTimeNano();
cnf->encodeTime = startSolve - startTime;
cnf->solveTime = finishTime - startSolve;
constraint(E_NULL) {
}
-OrderPair::~OrderPair(){
+OrderPair::~OrderPair() {
}
-Edge OrderPair::getConstraint(){
+Edge OrderPair::getConstraint() {
return constraint;
}
-Edge OrderPair::getNegatedConstraint(){
+Edge OrderPair::getNegatedConstraint() {
return constraintNegate(constraint);
}
-bool OrderPair::getConstraintValue(CSolver* solver){
+bool OrderPair::getConstraintValue(CSolver *solver) {
return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
}
-bool OrderPair::getNegatedConstraintValue(CSolver* solver){
+bool OrderPair::getNegatedConstraintValue(CSolver *solver) {
return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
}
OrderPair();
virtual ~OrderPair();
virtual Edge getConstraint();
- virtual bool getConstraintValue(CSolver* solver);
+ virtual bool getConstraintValue(CSolver *solver);
//for the cases that we swap first and second ... For total order is straight forward.
// but for partial order it has some complexity which should be hidden ... -HG
virtual Edge getNegatedConstraint();
- virtual bool getNegatedConstraintValue(CSolver* solver);
+ virtual bool getNegatedConstraintValue(CSolver *solver);
uint64_t first;
uint64_t second;
CMEMALLOC;
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
-// constraint.getBoolean()->print();
Edge c = encodeConstraintSATEncoder(constraint);
addConstraintCNF(cnf, c);
}
Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
Edge result;
- Boolean * constraint = c.getBoolean();
+ Boolean *constraint = c.getBoolean();
if (booledgeMap.contains(constraint)) {
Edge e = {(Node *) booledgeMap.get(constraint)};
case SATC_OR:
case SATC_XOR:
case SATC_IMPLIES:
- //Don't handle, translate these away...
+ //Don't handle, translate these away...
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
exit(-1);
flipped.second = pair->first;
pair = &flipped;
}
- OrderPair* tmp;
+ OrderPair *tmp;
if (!(table->contains(pair))) {
tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
table->put(tmp, tmp);
return gvalue;
HashtableOrderPair *table = order->getOrderPairTable();
-
- OrderPair* tmp;
+
+ OrderPair *tmp;
if (!(table->contains(pair))) {
Edge constraint = getNewVarSATEncoder();
tmp = new OrderPair(pair->first, pair->second, constraint);
boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
if (doOptOrderStructure) {
- ASSERT(boolOrder->order->graph == NULL);
+ ASSERT(boolOrder->order->graph == NULL);
boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
reachMustAnalysis(solver, boolOrder->order->graph, true);
}
Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji));
Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj));
Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki));
-
+
Edge t1[] = {ij, jk, ik};
Edge t2[] = {ji, jk, ik};
Edge t3[] = {ij, kj, ki};
Edge ct4 = constraintAND(cnf, 3, t4);
Edge ct5 = constraintAND(cnf, 3, t5);
Edge ct6 = constraintAND(cnf, 3, t6);
-
+
Edge p1[] = {uoIJ, jk, ik};
Edge p2[] = {ij, kj, uoIK};
Edge p3[] = {ji, uoJK, ki};
Edge cp4 = constraintAND(cnf, 3, p4);
Edge cp5 = constraintAND(cnf, 3, p5);
Edge cp6 = constraintAND(cnf, 3, p6);
-
+
Edge o1[] = {uoIJ, uoJK, ik};
Edge o2[] = {ij, uoJK, uoIK};
Edge o3[] = {uoIK, jk, uoIK};
Edge co4 = constraintAND(cnf, 3, o4);
Edge co5 = constraintAND(cnf, 3, o5);
Edge co6 = constraintAND(cnf, 3, o6);
-
+
Edge unorder [] = {uoIJ, uoJK, uoIK};
Edge cunorder = constraintAND(cnf, 3, unorder);
-
-
+
+
Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
- cp1,cp2,cp3,cp4,cp5,cp6,
- co1,co2,co3,co4,co5,co6,
- cunorder};
+ cp1,cp2,cp3,cp4,cp5,cp6,
+ co1,co2,co3,co4,co5,co6,
+ cunorder};
return constraintOR(cnf, 19, res);
}
Edge constKI = getPartialPairConstraint(order, &pairKI);
Edge constKJ = getPartialPairConstraint(order, &pairKJ);
addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
- constJK, constKJ, constIK, constKI));
+ constJK, constKJ, constIK, constKI));
}
}
}
#define PTRSHIFT 5
class BooleanEdge {
- public:
- BooleanEdge() : b(NULL) {}
- BooleanEdge(Boolean * _b) : b(_b) {}
+public:
+ BooleanEdge() : b(NULL) {}
+ BooleanEdge(Boolean *_b) : b(_b) {}
BooleanEdge negate() {return BooleanEdge((Boolean *)(((uintptr_t) b) ^ 1));}
- bool operator==(BooleanEdge e) { return b==e.b;}
- bool operator!=(BooleanEdge e) { return b!=e.b;}
+ bool operator==(BooleanEdge e) { return b == e.b;}
+ bool operator!=(BooleanEdge e) { return b != e.b;}
bool isNegated() { return ((uintptr_t) b) & 1; }
- Boolean * getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
- Boolean * getRaw() {return b;}
- Boolean * operator->() {return getBoolean();}
+ Boolean *getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
+ Boolean *getRaw() {return b;}
+ Boolean *operator->() {return getBoolean();}
operator bool() const {return b != NULL;}
- private:
+private:
Boolean *b;
};
inline bool boolEdgeEquals(BooleanEdge b1, BooleanEdge b2) {
- return b1==b2;
+ return b1 == b2;
}
inline unsigned int boolEdgeHash(BooleanEdge b) {
- return (unsigned int) (((uintptr_t)b.getRaw())>>PTRSHIFT);
+ return (unsigned int) (((uintptr_t)b.getRaw()) >> PTRSHIFT);
}
-
-typedef Hashset<BooleanEdge, uintptr_t, PTRSHIFT, & boolEdgeHash, & boolEdgeEquals> HashsetBooleanEdge;
+
+typedef Hashset<BooleanEdge, uintptr_t, PTRSHIFT, &boolEdgeHash, &boolEdgeEquals> HashsetBooleanEdge;
typedef Hashset<Order *, uintptr_t, PTRSHIFT> HashsetOrder;
-typedef SetIterator<BooleanEdge, uintptr_t, PTRSHIFT, & boolEdgeHash, & boolEdgeEquals> SetIteratorBooleanEdge;
+typedef SetIterator<BooleanEdge, uintptr_t, PTRSHIFT, &boolEdgeHash, &boolEdgeEquals> SetIteratorBooleanEdge;
typedef SetIterator<Order *, uintptr_t, PTRSHIFT> SetIteratorOrder;
#endif
table->reset();
}
+ void resetAndDelete() {
+ Linknode<_Key> *tmp = list;
+ while (tmp != NULL) {
+ Linknode<_Key> *tmpnext = tmp->next;
+ ourfree(tmp);
+ tmp = tmpnext;
+ }
+ list = tail = NULL;
+ table->resetAndDeleteKeys();
+ }
+
/** @brief Adds a new key to the hashset. Returns false if the key
* is already present. */
}
}
- void resetanddelete() {
+ void resetAndDeleteKeys() {
+ for (unsigned int i = 0; i < capacity; i++) {
+ struct Hashlistnode<_Key, _Val> *bin = &table[i];
+ if (bin->key != NULL) {
+ delete bin->key;
+ bin->key = NULL;
+ if (bin->val != NULL) {
+ bin->val = NULL;
+ }
+ }
+ }
+ if (zero) {
+ ourfree(zero);
+ zero = NULL;
+ }
+ size = 0;
+ }
+
+ void resetAndDeleteVals() {
for (unsigned int i = 0; i < capacity; i++) {
struct Hashlistnode<_Key, _Val> *bin = &table[i];
if (bin->key != NULL) {
size = 0;
}
- void resetandfree() {
+ void resetAndFreeVals() {
for (unsigned int i = 0; i < capacity; i++) {
struct Hashlistnode<_Key, _Val> *bin = &table[i];
if (bin->key != NULL) {
* isn't worth optimizing; the SWAP's get sped up by the cache, and pointer
* arithmetic gets lost in the time required for comparison function calls.
*/
-#define SWAP(a, b, count, size, tmp) { \
- count = size; \
- do { \
- tmp = *a; \
- *a++ = *b; \
- *b++ = tmp; \
- } while (--count); \
+#define SWAP(a, b, count, size, tmp) { \
+ count = size; \
+ do { \
+ tmp = *a; \
+ *a++ = *b; \
+ *b++ = tmp; \
+ } while (--count); \
}
/* Copy one block of size size to another. */
#define COPY(a, b, count, size, tmp1, tmp2) { \
- count = size; \
- tmp1 = a; \
- tmp2 = b; \
- do { \
- *tmp1++ = *tmp2++; \
- } while (--count); \
+ count = size; \
+ tmp1 = a; \
+ tmp2 = b; \
+ do { \
+ *tmp1++ = *tmp2++; \
+ } while (--count); \
}
/*
* j < nmemb, select largest of Ki, Kj and Kj+1.
*/
#define CREATE(initval, nmemb, par_i, child_i, par, child, size, count, tmp) { \
- for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
- par_i = child_i) { \
- child = base + child_i * size; \
- if (child_i < nmemb && compar(child, child + size) < 0) { \
- child += size; \
- ++child_i; \
+ for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
+ par_i = child_i) { \
+ child = base + child_i * size; \
+ if (child_i < nmemb && compar(child, child + size) < 0) { \
+ child += size; \
+ ++child_i; \
+ } \
+ par = base + par_i * size; \
+ if (compar(child, par) <= 0) \
+ break; \
+ SWAP(par, child, count, size, tmp); \
} \
- par = base + par_i * size; \
- if (compar(child, par) <= 0) \
- break; \
- SWAP(par, child, count, size, tmp); \
- } \
}
/*
* XXX Don't break the #define SELECT line, below. Reiser cpp gets upset.
*/
#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \
- for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
- child = base + child_i * size; \
- if (child_i < nmemb && compar(child, child + size) < 0) { \
- child += size; \
- ++child_i; \
+ for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
+ child = base + child_i * size; \
+ if (child_i < nmemb && compar(child, child + size) < 0) { \
+ child += size; \
+ ++child_i; \
+ } \
+ par = base + par_i * size; \
+ COPY(par, child, count, size, tmp1, tmp2); \
} \
- par = base + par_i * size; \
- COPY(par, child, count, size, tmp1, tmp2); \
- } \
- for (;;) { \
- child_i = par_i; \
- par_i = child_i / 2; \
- child = base + child_i * size; \
- par = base + par_i * size; \
- if (child_i == 1 || compar(k, par) < 0) { \
- COPY(child, k, count, size, tmp1, tmp2); \
- break; \
+ for (;; ) { \
+ child_i = par_i; \
+ par_i = child_i / 2; \
+ child = base + child_i * size; \
+ par = base + par_i * size; \
+ if (child_i == 1 || compar(k, par) < 0) { \
+ COPY(child, k, count, size, tmp1, tmp2); \
+ break; \
+ } \
+ COPY(child, par, count, size, tmp1, tmp2); \
} \
- COPY(child, par, count, size, tmp1, tmp2); \
- } \
}
/*
*/
int
bsdheapsort(void *vbase, size_t nmemb, size_t size,
- int (*compar)(const void *, const void *))
+ int (*compar)(const void *, const void *))
{
size_t cnt, i, j, l;
char tmp, *tmp1, *tmp2;
*/
base = (char *)vbase - size;
- for (l = nmemb / 2 + 1; --l;)
+ for (l = nmemb / 2 + 1; --l; )
CREATE(l, nmemb, i, j, t, p, size, cnt, tmp);
/*
}
-static __inline char *med3(char *, char *, char *, int (*)(const void *, const void *));
-static __inline void swapfunc(char *, char *, size_t, int);
+static __inline char *med3(char *, char *, char *, int (*)(const void *, const void *));
+static __inline void swapfunc(char *, char *, size_t, int);
-#define min(a, b) (a) < (b) ? a : b
+#define min(a, b) (a) < (b) ? a : b
/*
* Qsort routine from Bentley & McIlroy's "Engineering a Sort Function".
* 4. Tail recursion is eliminated when sorting the larger of two
* subpartitions to save stack space.
*/
-#define SWAPTYPE_BYTEV 1
-#define SWAPTYPE_INTV 2
-#define SWAPTYPE_LONGV 3
-#define SWAPTYPE_INT 4
-#define SWAPTYPE_LONG 5
+#define SWAPTYPE_BYTEV 1
+#define SWAPTYPE_INTV 2
+#define SWAPTYPE_LONGV 3
+#define SWAPTYPE_INT 4
+#define SWAPTYPE_LONG 5
-#define TYPE_ALIGNED(TYPE, a, es) \
+#define TYPE_ALIGNED(TYPE, a, es) \
(((char *)a - (char *)0) % sizeof(TYPE) == 0 && es % sizeof(TYPE) == 0)
-#define swapcode(TYPE, parmi, parmj, n) { \
- size_t i = (n) / sizeof (TYPE); \
- TYPE *pi = (TYPE *) (parmi); \
- TYPE *pj = (TYPE *) (parmj); \
- do { \
- TYPE t = *pi; \
- *pi++ = *pj; \
- *pj++ = t; \
- } while (--i > 0); \
+#define swapcode(TYPE, parmi, parmj, n) { \
+ size_t i = (n) / sizeof (TYPE); \
+ TYPE *pi = (TYPE *) (parmi); \
+ TYPE *pj = (TYPE *) (parmj); \
+ do { \
+ TYPE t = *pi; \
+ *pi++ = *pj; \
+ *pj++ = t; \
+ } while (--i > 0); \
}
static __inline void
}
}
-#define swap(a, b) do { \
- switch (swaptype) { \
- case SWAPTYPE_INT: { \
- int t = *(int *)(a); \
- *(int *)(a) = *(int *)(b); \
- *(int *)(b) = t; \
- break; \
- } \
- case SWAPTYPE_LONG: { \
- long t = *(long *)(a); \
- *(long *)(a) = *(long *)(b); \
- *(long *)(b) = t; \
- break; \
- } \
- default: \
- swapfunc(a, b, es, swaptype); \
- } \
+#define swap(a, b) do { \
+ switch (swaptype) { \
+ case SWAPTYPE_INT: { \
+ int t = *(int *)(a); \
+ *(int *)(a) = *(int *)(b); \
+ *(int *)(b) = t; \
+ break; \
+ } \
+ case SWAPTYPE_LONG: { \
+ long t = *(long *)(a); \
+ *(long *)(a) = *(long *)(b); \
+ *(long *)(b) = t; \
+ break; \
+ } \
+ default: \
+ swapfunc(a, b, es, swaptype); \
+ } \
} while (0)
-#define vecswap(a, b, n) if ((n) > 0) swapfunc(a, b, n, swaptype)
+#define vecswap(a, b, n) if ((n) > 0) swapfunc(a, b, n, swaptype)
static __inline char *
med3(char *a, char *b, char *c, int (*cmp)(const void *, const void *))
{
return cmp(a, b) < 0 ?
- (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a ))
- :(cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c ));
+ (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a))
+ : (cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c));
}
static void
introsort(char *a, size_t n, size_t es, size_t maxdepth, int swaptype,
- int (*cmp)(const void *, const void *))
+ int (*cmp)(const void *, const void *))
{
char *pa, *pb, *pc, *pd, *pl, *pm, *pn;
int cmp_result;
size_t r, s;
-loop: if (n < 7) {
+loop: if (n < 7) {
for (pm = a + es; pm < a + n * es; pm += es)
for (pl = pm; pl > a && cmp(pl - es, pl) > 0;
- pl -= es)
+ pl -= es)
swap(pl, pl - es);
return;
}
swap(a, pm);
pa = pb = a + es;
pc = pd = a + (n - 1) * es;
- for (;;) {
+ for (;; ) {
while (pb <= pc && (cmp_result = cmp(pb, a)) <= 0) {
if (cmp_result == 0) {
swap(pa, pb);
if (s > es) {
if (r > es) {
introsort(a, r / es, es, maxdepth,
- swaptype, cmp);
+ swaptype, cmp);
}
a = pn - s;
n = s / es;
if (r > es) {
if (s > es) {
introsort(pn - s, s / es, es, maxdepth,
- swaptype, cmp);
+ swaptype, cmp);
}
n = r / es;
goto loop;
#include "ordergraph.h"
#include "orderelement.h"
#include "structs.h"
+#include "decomposeorderresolver.h"
unsigned int table_entry_hash_function(TableEntry *This) {
unsigned int h = 0;
bool order_pair_equals(OrderPair *key1, OrderPair *key2) {
return key1->first == key2->first && key1->second == key2->second;
}
+
+unsigned int doredge_hash_function(DOREdge *key) {
+ return (uint) (key->newfirst << 2) ^ key->newsecond;
+}
+
+bool doredge_equals(DOREdge *key1, DOREdge *key2) {
+ return key1->newfirst == key2->newfirst &&
+ key1->newsecond == key2->newsecond;
+}
unsigned int order_pair_hash_function(OrderPair *This);
bool order_pair_equals(OrderPair *key1, OrderPair *key2);
+unsigned int doredge_hash_function(DOREdge *key);
+bool doredge_equals(DOREdge *key1, DOREdge *key2);
+
typedef Hashset<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
typedef Hashset<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> HashsetOrderNode;
typedef Hashset<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
typedef Hashset<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> HashsetOrderElement;
+typedef Hashset<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> HashsetDOREdge;
typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
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;
typedef SetIterator<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
-
+typedef SetIterator<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> SetIteratorDOREdge;
#endif
void setVector ## name(Vector ## name * vector, uint index, type item) { \
vector->array[index] = item; \
} \
- uint getSizeVector ## name(const Vector ## name * vector) { \
+ uint getSizeVector ## name(const Vector ## name * vector) { \
return vector->size; \
} \
void deleteVector ## name(Vector ## name * vector) { \
#include "satencoder.h"
#include "set.h"
+const char *elemEncTypeNames[] = {"UNASSIGNED", "ONEHOT", "UNARY", "BINARYINDEX", "BINARYVAL"};
+
ElementEncoding::ElementEncoding(Element *_element) :
type(ELEM_UNASSIGNED),
element(_element),
setInUseElement(i);
}
}
+
+void ElementEncoding::print() {
+ model_print("%s ", elemEncTypeNames[type]);
+ if (type == BINARYINDEX) {
+ for (uint i = 0; i < encArraySize; i++) {
+ if (i != 0)
+ model_print(", ");
+ if (isinUseElement(i))
+ model_print("%" PRIu64 "", encodingArray[i]);
+ else
+ model_print("_");
+ }
+ }
+}
}
return -1;
}
-
+ void print();
ElementEncodingType type;
Element *element;
return;
}
case ORDERCONST: {
- if(((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+ if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
return;
}
{
}
-OrderEncoding::~OrderEncoding(){
- if(resolver!= NULL){
+OrderEncoding::~OrderEncoding() {
+ if (resolver != NULL) {
delete resolver;
}
}
-/*
+/*
* File: deserializer.cc
* Author: hamed
- *
+ *
* Created on September 7, 2017, 6:08 PM
*/
#include "element.h"
#include "mutableset.h"
-Deserializer::Deserializer(const char* file):
+Deserializer::Deserializer(const char *file) :
solver(new CSolver())
{
filedesc = open(file, O_RDONLY);
-
+
if (filedesc < 0) {
exit(-1);
}
Deserializer::~Deserializer() {
delete solver;
-
- if (-1 == close(filedesc)){
+
+ if (-1 == close(filedesc)) {
exit(-1);
}
}
-ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
+ssize_t Deserializer::myread(void *__buf, size_t __nbytes) {
return read (filedesc, __buf, __nbytes);
}
-CSolver * Deserializer::deserialize(){
+CSolver *Deserializer::deserialize() {
ASTNodeType nodeType;
- while(myread(&nodeType, sizeof(ASTNodeType) ) >0){
- switch(nodeType){
- case BOOLEANEDGE:
- deserializeBooleanEdge();
- break;
- case BOOLEANVAR:
- deserializeBooleanVar();
- break;
- case ORDERCONST:
- deserializeBooleanOrder();
- break;
- case ORDERTYPE:
- deserializeOrder();
- break;
- 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);
+ while (myread(&nodeType, sizeof(ASTNodeType) ) > 0) {
+ switch (nodeType) {
+ case BOOLEANEDGE:
+ deserializeBooleanEdge();
+ break;
+ case BOOLEANVAR:
+ deserializeBooleanVar();
+ break;
+ case ORDERCONST:
+ deserializeBooleanOrder();
+ break;
+ case ORDERTYPE:
+ deserializeOrder();
+ break;
+ 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);
}
}
return solver;
}
-void Deserializer::deserializeBooleanEdge(){
+void Deserializer::deserializeBooleanEdge() {
Boolean *b;
- myread(&b, sizeof(Boolean*));
+ myread(&b, sizeof(Boolean *));
BooleanEdge tmp(b);
bool isNegated = tmp.isNegated();
ASSERT(map.contains(tmp.getBoolean()));
- b = (Boolean*) map.get(tmp.getBoolean());
+ b = (Boolean *) map.get(tmp.getBoolean());
BooleanEdge res(b);
- solver->addConstraint(isNegated?res.negate():res);
+ solver->addConstraint(isNegated ? res.negate() : res);
}
-void Deserializer::deserializeBooleanVar(){
+void Deserializer::deserializeBooleanVar() {
BooleanVar *b;
- myread(&b, sizeof(BooleanVar*));
+ myread(&b, sizeof(BooleanVar *));
VarType vtype;
myread(&vtype, sizeof(VarType));
map.put(b, solver->getBooleanVar(vtype).getBoolean());
}
-void Deserializer::deserializeBooleanOrder(){
- BooleanOrder* bo_ptr;
- myread(&bo_ptr, sizeof(BooleanOrder*));
- Order* order;
- myread(&order, sizeof(Order*));
+void Deserializer::deserializeBooleanOrder() {
+ BooleanOrder *bo_ptr;
+ myread(&bo_ptr, sizeof(BooleanOrder *));
+ Order *order;
+ myread(&order, sizeof(Order *));
ASSERT(map.contains(order));
- order = (Order*) map.get(order);
+ order = (Order *) map.get(order);
uint64_t first;
myread(&first, sizeof(uint64_t));
uint64_t second;
map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
}
-void Deserializer::deserializeOrder(){
- Order* o_ptr;
- myread(&o_ptr, sizeof(Order*));
+void Deserializer::deserializeOrder() {
+ Order *o_ptr;
+ myread(&o_ptr, sizeof(Order *));
OrderType type;
myread(&type, sizeof(OrderType));
- Set * set_ptr;
+ Set *set_ptr;
myread(&set_ptr, sizeof(Set *));
ASSERT(map.contains(set_ptr));
- Set* set = (Set*) map.get(set_ptr);
+ Set *set = (Set *) map.get(set_ptr);
map.put(o_ptr, solver->createOrder(type, set));
}
-void Deserializer::deserializeSet(){
+void Deserializer::deserializeSet() {
Set *s_ptr;
- myread(&s_ptr, sizeof(Set*));
+ myread(&s_ptr, sizeof(Set *));
VarType type;
myread(&type, sizeof(VarType));
bool isRange;
}
map.put(s_ptr, set);
}
-
}
-void Deserializer::deserializeBooleanLogic(){
+void Deserializer::deserializeBooleanLogic() {
BooleanLogic *bl_ptr;
myread(&bl_ptr, sizeof(BooleanLogic *));
LogicOp op;
uint size;
myread(&size, sizeof(uint));
Vector<BooleanEdge> members;
- for(uint i=0; i<size; i++){
- Boolean* member;
+ 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());
+ member = (Boolean *) map.get(tmp.getBoolean());
BooleanEdge res(member);
- members.push( isNegated?res.negate():res );
+ members.push( isNegated ? res.negate() : res );
}
map.put(bl_ptr, solver->applyLogicalOperation(op, members.expose(), size).getBoolean());
}
-void Deserializer::deserializeBooleanPredicate(){
+void Deserializer::deserializeBooleanPredicate() {
BooleanPredicate *bp_ptr;
myread(&bp_ptr, sizeof(BooleanPredicate *));
- Predicate* predicate;
- myread(&predicate, sizeof(Predicate*));
+ Predicate *predicate;
+ myread(&predicate, sizeof(Predicate *));
ASSERT(map.contains(predicate));
- predicate = (Predicate*) map.get(predicate);
+ predicate = (Predicate *) map.get(predicate);
uint size;
myread(&size, sizeof(uint));
- Vector<Element*> members;
- for(uint i=0; i<size; i++){
- Element* input;
+ 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);
+ input = (Element *) map.get(input);
members.push(input);
}
-
- Boolean* stat_ptr;
+
+ Boolean *stat_ptr;
myread(&stat_ptr, sizeof(Boolean *));
BooleanEdge undefStatus;
- if(stat_ptr != NULL){
+ if (stat_ptr != NULL) {
BooleanEdge tmp(stat_ptr);
bool isNegated = tmp.isNegated();
ASSERT(map.contains(tmp.getBoolean()));
- stat_ptr = (Boolean*) map.get(tmp.getBoolean());
+ stat_ptr = (Boolean *) map.get(tmp.getBoolean());
BooleanEdge res(stat_ptr);
- undefStatus = isNegated?res.negate():res;
+ undefStatus = isNegated ? res.negate() : res;
} else {
undefStatus = NULL;
}
map.put(bp_ptr, solver->applyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean());
}
-void Deserializer::deserializePredicateTable(){
+void Deserializer::deserializePredicateTable() {
PredicateTable *pt_ptr;
myread(&pt_ptr, sizeof(PredicateTable *));
- Table* table;
- myread(&table, sizeof(Table*));
+ Table *table;
+ myread(&table, sizeof(Table *));
ASSERT(map.contains(table));
- table = (Table*) map.get(table);
+ table = (Table *) map.get(table);
UndefinedBehavior undefinedbehavior;
myread(&undefinedbehavior, sizeof(UndefinedBehavior));
-
+
map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior));
}
-void Deserializer::deserializePredicateOperator(){
+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*));
+ 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);
+ domain = (Set *) map.get(domain);
domains.push(domain);
}
map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
}
-void Deserializer::deserializeTable(){
+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*));
+ 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);
+ domain = (Set *) map.get(domain);
domains.push(domain);
}
- Set* range;
- myread(&range, sizeof(Set*));
- if(range != NULL){
+ Set *range;
+ myread(&range, sizeof(Set *));
+ if (range != NULL) {
ASSERT(map.contains(range));
- range = (Set*) map.get(range);
+ range = (Set *) map.get(range);
}
- Table* table = solver->createTable(domains.expose(), size, range);
+ Table *table = solver->createTable(domains.expose(), size, range);
myread(&size, sizeof(uint));
- for(uint i=0; i<size; i++){
+ 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);
+ 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;
+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);
+ set = (Set *) map.get(set);
map.put(es_ptr, solver->getElementVar(set));
}
-void Deserializer::deserializeElementConst(){
- ElementSet* es_ptr;
- myread(&es_ptr, sizeof(ElementSet*));
+void Deserializer::deserializeElementConst() {
+ ElementSet *es_ptr;
+ myread(&es_ptr, sizeof(ElementSet *));
VarType type;
myread(&type, sizeof(VarType));
uint64_t value;
map.put(es_ptr, solver->getElementConst(type, value));
}
-void Deserializer::deserializeElementFunction(){
+void Deserializer::deserializeElementFunction() {
ElementFunction *ef_ptr;
myread(&ef_ptr, sizeof(ElementFunction *));
Function *function;
- myread(&function, sizeof(Function*));
+ myread(&function, sizeof(Function *));
ASSERT(map.contains(function));
- function = (Function*) map.get(function);
+ function = (Function *) map.get(function);
uint size;
myread(&size, sizeof(uint));
- Vector<Element*> members;
- for(uint i=0; i<size; i++){
- Element* input;
+ 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);
+ input = (Element *) map.get(input);
members.push(input);
}
-
- Boolean* overflowstatus;
+
+ Boolean *overflowstatus;
myread(&overflowstatus, sizeof(Boolean *));
BooleanEdge tmp(overflowstatus);
bool isNegated = tmp.isNegated();
ASSERT(map.contains(tmp.getBoolean()));
- overflowstatus = (Boolean*) map.get(tmp.getBoolean());
+ overflowstatus = (Boolean *) map.get(tmp.getBoolean());
BooleanEdge res(overflowstatus);
- BooleanEdge undefStatus = isNegated?res.negate():res;
-
+ BooleanEdge undefStatus = isNegated ? res.negate() : res;
+
map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
}
-void Deserializer::deserializeFunctionOperator(){
+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*));
+ 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);
+ domain = (Set *) map.get(domain);
domains.push(domain);
}
- Set* range;
- myread(&range, sizeof(Set*));
+ Set *range;
+ myread(&range, sizeof(Set *));
ASSERT(map.contains(range));
- range = (Set*) map.get(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(){
+void Deserializer::deserializeFunctionTable() {
FunctionTable *ft_ptr;
myread(&ft_ptr, sizeof(FunctionTable *));
- Table* table;
- myread(&table, sizeof(Table*));
+ Table *table;
+ myread(&table, sizeof(Table *));
ASSERT(map.contains(table));
- table = (Table*) map.get(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
+}
-/*
+/*
* File: deserializer.h
* Author: hamed
*
/**
* Style of serialized file:
* ASTNodeType#Pointer#ObjectDATA
- *
+ *
* @param file
*/
class Deserializer {
public:
- Deserializer(const char* file);
+ Deserializer(const char *file);
CSolver *deserialize();
virtual ~Deserializer();
private:
CloneMap map;
};
-#endif /* DESERIALIZER_H */
+#endif/* DESERIALIZER_H */
-/*
+/*
* File: serializer.cc
* Author: hamed
- *
+ *
* Created on September 7, 2017, 3:38 PM
*/
Serializer::Serializer(const char *file) {
filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
-
+
if (filedesc < 0) {
exit(-1);
}
}
Serializer::~Serializer() {
- if (-1 == close(filedesc)){
+ if (-1 == close(filedesc)) {
exit(-1);
}
}
-void Serializer::mywrite(const void *__buf, size_t __n){
+void Serializer::mywrite(const void *__buf, size_t __n) {
write (filedesc, __buf, __n);
}
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge be){
- if(be == BooleanEdge(NULL))
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be) {
+ if (be == BooleanEdge(NULL))
return;
be.getBoolean()->serialize(serializer);
ASTNodeType type = BOOLEANEDGE;
serializer->mywrite(&type, sizeof(ASTNodeType));
- Boolean* boolean = be.getRaw();
- serializer->mywrite(&boolean, sizeof(Boolean*));
+ Boolean *boolean = be.getRaw();
+ serializer->mywrite(&boolean, sizeof(Boolean *));
}
\ No newline at end of file
-/*
+/*
* File: serializer.h
* Author: hamed
*
CloneMap map;
};
-inline bool Serializer::isSerialized(void* obj){
+inline bool Serializer::isSerialized(void *obj) {
return map.contains(obj);
}
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge be);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be);
-#endif /* SERIALIZER_H */
+#endif/* SERIALIZER_H */
* 8=>9
* 9=>2
* 6=>2
- *
- *
+ *
+ *
*/
int main(int numargs, char **argv) {
CSolver *solver = new CSolver();
Set *s = solver->createSet(0, set1, 10);
Order *order = solver->createOrder(SATC_TOTAL, s);
BooleanEdge b01 = solver->orderConstraint(order, 0, 1);
- solver->addConstraint(b01);
+ solver->addConstraint(b01);
BooleanEdge b12 = solver->orderConstraint(order, 1, 2);
- solver->addConstraint(b12);
+ solver->addConstraint(b12);
BooleanEdge b23 = solver->orderConstraint(order, 2, 3);
- solver->addConstraint(b23);
+ solver->addConstraint(b23);
BooleanEdge b14 = solver->orderConstraint(order, 1, 4);
- solver->addConstraint(b14);
+ solver->addConstraint(b14);
BooleanEdge b45 = solver->orderConstraint(order, 4, 5);
- solver->addConstraint(b45);
+ solver->addConstraint(b45);
BooleanEdge b56 = solver->orderConstraint(order, 5, 6);
- solver->addConstraint(b56);
+ solver->addConstraint(b56);
BooleanEdge b17 = solver->orderConstraint(order, 1, 7);
- solver->addConstraint(b17);
+ solver->addConstraint(b17);
BooleanEdge b78 = solver->orderConstraint(order, 7, 8);
- solver->addConstraint(b78);
+ solver->addConstraint(b78);
BooleanEdge b89 = solver->orderConstraint(order, 8, 9);
- solver->addConstraint(b89);
+ solver->addConstraint(b89);
BooleanEdge b92 = solver->orderConstraint(order, 9, 2);
- solver->addConstraint(b92);
+ solver->addConstraint(b92);
BooleanEdge b62 = solver->orderConstraint(order, 6, 2);
- solver->addConstraint(b62);
+ solver->addConstraint(b62);
- BooleanEdge v1 = solver->getBooleanVar(0);
- solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
- BooleanEdge v2 = solver->getBooleanVar(0);
- solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
- BooleanEdge v3 = solver->getBooleanVar(0);
- BooleanEdge v4 = solver->getBooleanVar(0);
- BooleanEdge v5 = solver->getBooleanVar(0);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_OR,
- solver->applyLogicalOperation(SATC_IFF, v3, v4),
- v5));
- solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
- BooleanEdge v6 = solver->getBooleanVar(0);
- BooleanEdge v7 = solver->getBooleanVar(0);
- BooleanEdge v8 = solver->getBooleanVar(0);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_OR,
- solver->applyLogicalOperation(SATC_IFF, v7, v8),
- v6));
+ BooleanEdge v1 = solver->getBooleanVar(0);
+ solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
+ BooleanEdge v2 = solver->getBooleanVar(0);
+ solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
+ BooleanEdge v3 = solver->getBooleanVar(0);
+ BooleanEdge v4 = solver->getBooleanVar(0);
+ BooleanEdge v5 = solver->getBooleanVar(0);
+ BooleanEdge be = solver->applyLogicalOperation(SATC_IFF, v3, v4);
+ BooleanEdge sor = solver->applyLogicalOperation(SATC_OR, be, v5);
+ solver->addConstraint(sor);
+ solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
+ BooleanEdge v6 = solver->getBooleanVar(0);
+ BooleanEdge v7 = solver->getBooleanVar(0);
+ BooleanEdge v8 = solver->getBooleanVar(0);
+ solver->addConstraint(
+ solver->applyLogicalOperation(SATC_OR,
+ solver->applyLogicalOperation(SATC_IFF, v7, v8),
+ v6));
solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
- BooleanEdge v9 = solver->getBooleanVar(0);
+ BooleanEdge v9 = solver->getBooleanVar(0);
solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
- BooleanEdge v10 = solver->getBooleanVar(0);
- BooleanEdge v11 = solver->getBooleanVar(0);
- BooleanEdge v12 = solver->getBooleanVar(0);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_OR,
- solver->applyLogicalOperation(SATC_OR, v10, v11),
- solver->applyLogicalOperation(SATC_IFF, v1, v12)));
- BooleanEdge b48 = solver->orderConstraint(order, 4, 8);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_OR,
- solver->applyLogicalOperation(SATC_OR, v10, v11),
- b48));
- BooleanEdge v13 = solver->getBooleanVar(0);
- BooleanEdge v14 = solver->getBooleanVar(0);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_OR,
- solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
- solver->applyLogicalOperation(SATC_AND,
- solver->applyLogicalOperation(SATC_IFF, v12, v13),
- solver->applyLogicalOperation(SATC_NOT,b48))
- ));
- solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
- solver->addConstraint(v14);
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
- BooleanEdge v15 = solver->getBooleanVar(0);
- BooleanEdge v16 = solver->getBooleanVar(0);
- BooleanEdge v17 = solver->getBooleanVar(0);
- BooleanEdge v18 = solver->getBooleanVar(0);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_OR,
- solver->applyLogicalOperation(SATC_OR, v15, v16),
- solver->applyLogicalOperation(SATC_IFF, v17, v2)
- ));
- BooleanEdge b57 = solver->orderConstraint(order, 5, 7);
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_IMPLIES,
- b57,
- solver->applyLogicalOperation(SATC_OR, v15, v16)
- ));
- solver->addConstraint(
- solver->applyLogicalOperation(SATC_IMPLIES,
- solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
- solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
- ));
- solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
- solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
- solver->addConstraint(v18);
-
- if (solver->solve() == 1){
+ BooleanEdge v10 = solver->getBooleanVar(0);
+ BooleanEdge v11 = solver->getBooleanVar(0);
+ BooleanEdge v12 = solver->getBooleanVar(0);
+ solver->addConstraint(
+ solver->applyLogicalOperation(SATC_OR,
+ solver->applyLogicalOperation(SATC_OR, v10, v11),
+ solver->applyLogicalOperation(SATC_IFF, v1, v12)));
+ BooleanEdge b48 = solver->orderConstraint(order, 4, 8);
+ BooleanEdge be1 = solver->applyLogicalOperation(SATC_OR, v10, v11);
+ BooleanEdge be2 = solver->applyLogicalOperation(SATC_OR, be1, b48);
+ solver->addConstraint(be2);
+ BooleanEdge v13 = solver->getBooleanVar(0);
+ BooleanEdge v14 = solver->getBooleanVar(0);
+ solver->addConstraint(
+ solver->applyLogicalOperation(SATC_OR,
+ solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
+ solver->applyLogicalOperation(SATC_AND,
+ solver->applyLogicalOperation(SATC_IFF, v12, v13),
+ solver->applyLogicalOperation(SATC_NOT,b48))
+ ));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
+ solver->addConstraint(v14);
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
+ BooleanEdge v15 = solver->getBooleanVar(0);
+ BooleanEdge v16 = solver->getBooleanVar(0);
+ BooleanEdge v17 = solver->getBooleanVar(0);
+ BooleanEdge v18 = solver->getBooleanVar(0);
+ solver->addConstraint(
+ solver->applyLogicalOperation(SATC_OR,
+ solver->applyLogicalOperation(SATC_OR, v15, v16),
+ solver->applyLogicalOperation(SATC_IFF, v17, v2)
+ ));
+ BooleanEdge b57 = solver->orderConstraint(order, 5, 7);
+ solver->addConstraint(
+ solver->applyLogicalOperation(SATC_IMPLIES,
+ b57,
+ solver->applyLogicalOperation(SATC_OR, v15, v16)
+ ));
+ solver->addConstraint(
+ solver->applyLogicalOperation(SATC_IMPLIES,
+ solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
+ solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
+ ));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
+ solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
+ solver->addConstraint(v18);
+
+ if (solver->solve() == 1) {
printf("SAT\n");
- printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
- solver->getOrderConstraintValue(order, 5, 1),
- solver->getOrderConstraintValue(order, 1, 4),
- solver->getOrderConstraintValue(order, 5, 4),
- solver->getOrderConstraintValue(order, 1, 5));
+ printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+ solver->getOrderConstraintValue(order, 5, 1),
+ solver->getOrderConstraintValue(order, 1, 4),
+ solver->getOrderConstraintValue(order, 5, 4),
+ solver->getOrderConstraintValue(order, 1, 5));
} else {
printf("UNSAT\n");
}
* 8=>9
* 9=>2
* 6=>2
- *
- *
+ *
+ *
*/
int main(int numargs, char **argv) {
CSolver *solver = new CSolver();
BooleanEdge b57 = solver->orderConstraint(order, 5, 7);
solver->addConstraint(b57);
-
- if (solver->solve() == 1){
+
+ if (solver->solve() == 1) {
printf("SAT\n");
- printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
- solver->getOrderConstraintValue(order, 5, 1),
+ printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+ solver->getOrderConstraintValue(order, 5, 1),
solver->getOrderConstraintValue(order, 1, 4),
solver->getOrderConstraintValue(order, 5, 4),
solver->getOrderConstraintValue(order, 1, 5));
--- /dev/null
+#include "csolver.h"
+
+int main(int numargs, char **argv) {
+ CSolver *solver = new CSolver();
+ uint64_t elements[] = {0, 1};
+ Set *s = solver->createSet(1, elements, 2);
+ Element *e1 = solver->getElementVar(s);
+ Element *e2 = solver->getElementVar(s);
+ Set *sarray[] = {s, s};
+ Predicate *p = solver->createPredicateOperator(SATC_LT, sarray, 2);
+ Element *earray[] = {e1, e2};
+ BooleanEdge be = solver->applyPredicate(p, earray, 2);
+ solver->addConstraint(be);
+
+ if (solver->solve() == 1) {
+ printf("SAT\n");
+ } else {
+ printf("UNSAT\n");
+ }
+ delete solver;
+}
--- /dev/null
+#include "csolver.h"
+
+int main(int numargs, char **argv) {
+ CSolver *solver = new CSolver();
+ uint64_t set1[] = {1, 2, 3};
+ Set *s = solver->createSet(0, set1, 3);
+ Order *order = solver->createOrder(SATC_TOTAL, s);
+ BooleanEdge b12 = solver->orderConstraint(order, 1, 2);
+ solver->addConstraint(b12);
+ BooleanEdge b23 = solver->orderConstraint(order, 2, 3);
+ solver->addConstraint(b23);
+
+ if (solver->solve() == 1) {
+ printf("SAT\n");
+ } else {
+ printf("UNSAT\n");
+ }
+ delete solver;
+}
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
solver->serialize();
- if (solver->solve() == 1){
+ if (solver->solve() == 1) {
printf("SAT\n");
- printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
- solver->getOrderConstraintValue(order, 5, 1),
- solver->getOrderConstraintValue(order, 1, 4),
- solver->getOrderConstraintValue(order, 5, 4),
- solver->getOrderConstraintValue(order, 1, 5));
+ printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+ solver->getOrderConstraintValue(order, 5, 1),
+ solver->getOrderConstraintValue(order, 1, 4),
+ solver->getOrderConstraintValue(order, 5, 4),
+ solver->getOrderConstraintValue(order, 1, 5));
} else {
printf("UNSAT\n");
}
#include "ordernode.h"
#include "ordergraph.h"
-DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order *> &_orders) :
- graph(_graph),
- orders(_orders.getSize(), _orders.expose())
+DecomposeOrderResolver::DecomposeOrderResolver(Order *_order) :
+ graph(NULL),
+ order(_order)
{
}
DecomposeOrderResolver::~DecomposeOrderResolver() {
+ if (graph != NULL)
+ delete graph;
+ edges.resetAndDelete();
+}
+
+void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
+ DOREdge edge(first, second, 0, first, second);
+ if (!edges.contains(&edge)) {
+ DOREdge *newedge = new DOREdge(first, second, 0, first, second);
+ edges.add(newedge);
+ }
+}
+
+void DecomposeOrderResolver::remapEdge(uint64_t first, uint64_t second, uint64_t newfirst, uint64_t newsecond) {
+ DOREdge edge(first, second, 0, first, second);
+ DOREdge *oldedge = edges.get(&edge);
+ if (oldedge != NULL) {
+ edges.remove(oldedge);
+ oldedge->newfirst = newfirst;
+ oldedge->newsecond = newsecond;
+ edges.add(oldedge);
+ } else {
+ DOREdge *newedge = new DOREdge(first, second, 0, newfirst, newsecond);
+ edges.add(newedge);
+ }
+}
+
+void DecomposeOrderResolver::setEdgeOrder(uint64_t first, uint64_t second, uint sccNum) {
+ DOREdge edge(first, second, 0, first, second);
+ DOREdge *oldedge = edges.get(&edge);
+ if (oldedge != NULL) {
+ oldedge->orderindex = sccNum;
+ } else {
+ DOREdge *newedge = new DOREdge(first, second, sccNum, first, second);
+ edges.add(newedge);
+ }
+}
+
+void DecomposeOrderResolver::setOrder(uint sccNum, Order *neworder) {
+ orders.setExpand(sccNum, neworder);
+}
+
+Order *DecomposeOrderResolver::getOrder(uint sccNum) {
+ Order *neworder = NULL;
+ if (orders.getSize() > sccNum)
+ neworder = orders.get(sccNum);
+ return neworder;
+}
+
+void DecomposeOrderResolver::buildGraph() {
+ graph = new OrderGraph(order);
+ SetIteratorDOREdge *iterator = edges.iterator();
+ while (iterator->hasNext()) {
+ DOREdge *doredge = iterator->next();
+ if (doredge->orderindex == 0) {
+ graph->addEdge(doredge->origfirst, doredge->origsecond);
+ } else {
+ Order *suborder = orders.get(doredge->orderindex);
+ bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
+ if (isEdge)
+ graph->addEdge(doredge->origfirst, doredge->origsecond);
+ else if (order->type == SATC_TOTAL)
+ graph->addEdge(doredge->origsecond, doredge->origfirst);
+ }
+ }
+ delete iterator;
+ if (order->type == SATC_TOTAL) {
+ graph->computeStronglyConnectedComponentGraph();
+ }
}
bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
+ if (graph == NULL)
+ buildGraph();
+
OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
- ASSERT(from != NULL);
+ if (from == NULL) {
+ ASSERT(order->type != SATC_TOTAL);
+ return false;
+ }
OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
- ASSERT(to != NULL);
-
- if (from->sccNum != to->sccNum) {
- OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
- if (edge != NULL && edge->mustPos) {
- return true;
- } else if ( edge != NULL && edge->mustNeg) {
- return false;
- } else {
- switch (graph->getOrder()->type) {
- case SATC_TOTAL:
- return from->sccNum < to->sccNum;
- case SATC_PARTIAL:
- return resolvePartialOrder(from, to);
- default:
- ASSERT(0);
- }
- }
- } else {
- Order *suborder = NULL;
- // We should ask this query from the suborder ....
- suborder = orders.get(from->sccNum);
- ASSERT(suborder != NULL);
- return suborder->encoding.resolver->resolveOrder(from->id, to->id);
+ if (to == NULL) {
+ ASSERT(order->type != SATC_TOTAL);
+ return false;
+ }
+ switch (order->type) {
+ case SATC_TOTAL:
+ return from->sccNum < to->sccNum;
+ case SATC_PARTIAL:
+ return resolvePartialOrder(from, to);
+ default:
+ ASSERT(0);
}
}
-bool DecomposeOrderResolver::resolvePartialOrder(OrderNode* first, OrderNode* second){
- if(first->sccNum > second->sccNum){
+bool DecomposeOrderResolver::resolvePartialOrder(OrderNode *first, OrderNode *second) {
+ if (first->sccNum > second->sccNum) {
return false;
} else {
return graph->isTherePath(first, second);
}
-
}
#include "structs.h"
#include "orderresolver.h"
+class DOREdge {
+public:
+ DOREdge(uint64_t _origfirst, uint64_t _origsecond, uint _orderindex, uint64_t _newfirst, uint64_t _newsecond) :
+ origfirst(_origfirst),
+ origsecond(_origsecond),
+ orderindex(_orderindex),
+ newfirst(_newfirst),
+ newsecond(_newsecond) {
+ }
+ uint64_t origfirst;
+ uint64_t origsecond;
+ uint orderindex;
+ uint64_t newfirst;
+ uint64_t newsecond;
+ CMEMALLOC;
+};
+
class DecomposeOrderResolver : public OrderResolver {
public:
- DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
- bool resolveOrder(uint64_t first, uint64_t second);
- bool resolvePartialOrder(OrderNode* first, OrderNode* second);
+ DecomposeOrderResolver(Order *_order);
+ virtual bool resolveOrder(uint64_t first, uint64_t second);
virtual ~DecomposeOrderResolver();
+ void mustOrderEdge(uint64_t first, uint64_t second);
+ void remapEdge(uint64_t oldfirst, uint64_t oldsecond, uint64_t newfirst, uint64_t newsecond);
+ void setEdgeOrder(uint64_t first, uint64_t second, uint sccNum);
+ void setOrder(uint sccNum, Order *order);
+ Order *getOrder(uint sccNum);
+ CMEMALLOC;
+
private:
+ bool resolvePartialOrder(OrderNode *first, OrderNode *second);
+ void buildGraph();
OrderGraph *graph;
+ Order *order;
Vector<Order *> orders;
+ HashsetDOREdge edges;
};
#endif/* DECOMPOSEORDERRESOLVER_H */
OrderPairResolver::~OrderPairResolver() {
if (orderPairTable != NULL) {
- orderPairTable->resetanddelete();
+ orderPairTable->resetAndDeleteVals();
delete orderPairTable;
}
}
ASSERT(to != NULL);
OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-
+
if (edge != NULL && edge->mustPos) {
return true;
} else if ( edge != NULL && edge->mustNeg) {
public:
OrderPairResolver(CSolver *_solver, Order *_order);
bool resolveOrder(uint64_t first, uint64_t second);
- HashtableOrderPair* getOrderPairTable() { return orderPairTable;}
+ HashtableOrderPair *getOrderPairTable() { return orderPairTable;}
virtual ~OrderPairResolver();
private:
CSolver *solver;
Order *order;
HashtableOrderPair *orderPairTable;
-
+
bool getOrderConstraintValue(uint64_t first, uint64_t second);
};
bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
return setting1->hasVar == setting2->hasVar &&
- setting1->type1 == setting2->type1 &&
- setting1->type2 == setting2->type2 &&
- setting1->param == setting2->param;
+ setting1->type1 == setting2->type1 &&
+ setting1->type2 == setting2->type2 &&
+ setting1->param == setting2->param;
}
SearchTuner::SearchTuner() {
result = settings.get(&setting);
if ( result == NULL) {
result = new
- TunableSetting(vartype1, vartype2, param);
+ 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 OrderGraph;
class OrderNode;
class OrderEdge;
+class DOREdge;
class AutoTuner;
class SearchTuner;
#include "config.h"
#include "time.h"
+
#if 1
extern int model_out;
extern int model_err;
#endif
#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+
+
#define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1))))
#define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x))
// Deserializer deserializer("dump");
// deserializer.deserialize();
// }
-
}
Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
return set;
}
-VarType CSolver::getSetVarType(Set *set){
+VarType CSolver::getSetVarType(Set *set) {
return set->getType();
}
return element;
}
-void CSolver::finalizeMutableSet(MutableSet* set){
+void CSolver::finalizeMutableSet(MutableSet *set) {
set->finalize();
}
return element;
}
-Set* CSolver::getElementRange (Element* element){
+Set *CSolver::getElementRange (Element *element) {
return element->getRange();
}
}
bool CSolver::isTrue(BooleanEdge b) {
- return b.isNegated()?b->isFalse():b->isTrue();
+ return b.isNegated() ? b->isFalse() : b->isTrue();
}
bool CSolver::isFalse(BooleanEdge b) {
- return b.isNegated()?b->isTrue():b->isFalse();
+ return b.isNegated() ? b->isTrue() : b->isFalse();
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
static int ptrcompares(const void *p1, const void *p2) {
uintptr_t b1 = *(uintptr_t const *) p1;
- uintptr_t b2 = *(uintptr_t const *) p2;
+ uintptr_t b2 = *(uintptr_t const *) p2;
if (b1 < b2)
return -1;
else if (b1 == b2)
return 1;
}
-BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) {
- return applyLogicalOperation(op, array, asize);
- /* BooleanEdge newarray[asize];
+BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
+ BooleanEdge newarray[asize];
memcpy(newarray, array, asize * sizeof(BooleanEdge));
- for(uint i=0; i < asize; i++) {
- BooleanEdge b=newarray[i];
+ for (uint i = 0; i < asize; i++) {
+ BooleanEdge b = newarray[i];
if (b->type == LOGICOP) {
if (((BooleanLogic *) b.getBoolean())->replaced) {
newarray[i] = doRewrite(newarray[i]);
}
}
}
- return applyLogicalOperation(op, newarray, asize);*/
+ return applyLogicalOperation(op, newarray, asize);
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
case SATC_IFF: {
for (uint i = 0; i < 2; i++) {
if (array[i]->type == BOOLCONST) {
- if (isTrue(array[i])) { // It can be undefined
+ if (isTrue(array[i])) { // It can be undefined
return array[1 - i];
- } else if(isFalse(array[i])) {
+ } else if (isFalse(array[i])) {
newarray[0] = array[1 - i];
return applyLogicalOperation(SATC_NOT, newarray, 1);
}
} else if (array[i]->type == LOGICOP) {
- BooleanLogic *b =(BooleanLogic *)array[i].getBoolean();
+ BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
if (b->replaced) {
return rewriteLogicalOperation(op, array, asize);
}
break;
}
case SATC_OR: {
- for (uint i =0; i <asize; i++) {
+ for (uint i = 0; i < asize; i++) {
newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
}
return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
uint newindex = 0;
for (uint i = 0; i < asize; i++) {
BooleanEdge b = array[i];
-// model_print("And: Argument %u:", i);
-// if(b.isNegated())
-// model_print("!");
-// b->print();
if (b->type == LOGICOP) {
if (((BooleanLogic *)b.getBoolean())->replaced)
return rewriteLogicalOperation(op, array, asize);
if (b->type == BOOLCONST) {
if (isTrue(b))
continue;
- else{
+ else {
return boolFalse;
- }
+ }
} else
newarray[newindex++] = b;
}
}
case SATC_IMPLIES: {
//handle by translation
-// model_print("Implies: first:");
-// if(array[0].isNegated())
-// model_print("!");
-// array[0]->print();
-// model_print("Implies: second:");
-// if(array[1].isNegated())
-// model_print("!");
-// array[1]->print();
-// model_println("##### OK let's get the operation done");
return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
}
}
ASSERT(asize != 0);
Boolean *boolean = new BooleanLogic(this, op, array, asize);
- /* Boolean *b = boolMap.get(boolean);
+ Boolean *b = boolMap.get(boolean);
if (b == NULL) {
boolean->updateParents();
boolMap.put(boolean, boolean);
allBooleans.push(boolean);
return BooleanEdge(boolean);
} else {
- delete boolean;*/
- return BooleanEdge(boolean);
- /* }*/
+ delete boolean;
+ return BooleanEdge(b);
+ }
}
BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
-#ifdef TRACE_DEBUG
- model_println("Creating order: From:%lu => To:%lu", first, second);
-#endif
- if(first == second)
- return boolFalse;
+ ASSERT(first != second);
Boolean *constraint = new BooleanOrder(order, first, second);
allBooleans.push(constraint);
return BooleanEdge(constraint);
#endif
if (isTrue(constraint))
return;
- else if (isFalse(constraint)){
- int t=0;
-#ifdef TRACE_DEBUG
- model_println("Adding constraint which is false :|");
-#endif
- setUnSAT();
- }
+ else if (isFalse(constraint)) {
+ int t = 0;
+ setUnSAT();
+ }
else {
if (constraint->type == LOGICOP) {
- BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
+ BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
if (!constraint.isNegated()) {
- if (b->op==SATC_AND) {
- for(uint i=0;i<b->inputs.getSize();i++) {
-#ifdef TRACE_DEBUG
- model_println("In loop");
-#endif
+ if (b->op == SATC_AND) {
+ for (uint i = 0; i < b->inputs.getSize(); i++) {
addConstraint(b->inputs.get(i));
}
return;
}
}
if (b->replaced) {
-#ifdef TRACE_DEBUG
- model_println("While rewriting");
-#endif
addConstraint(doRewrite(constraint));
return;
}
}
constraints.add(constraint);
- Boolean *ptr=constraint.getBoolean();
-
- if (ptr->boolVal == BV_UNSAT){
-#ifdef TRACE_DEBUG
- model_println("BooleanValue is Set to UnSAT");
-#endif
- setUnSAT();
- }
-
+ Boolean *ptr = constraint.getBoolean();
+
+ if (ptr->boolVal == BV_UNSAT) {
+ setUnSAT();
+ }
+
replaceBooleanWithTrueNoRemove(constraint);
constraint->parents.clear();
}
long long startTime = getTimeNano();
computePolarities(this);
-// Preprocess pp(this);
-// pp.doTransform();
-
-// DecomposeOrderTransform dot(this);
-// dot.doTransform();
+ Preprocess pp(this);
+ pp.doTransform();
-// IntegerEncodingTransform iet(this);
-// iet.doTransform();
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
-// EncodingGraph eg(this);
-// eg.buildGraph();
-// eg.encode();
-
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
+
+ EncodingGraph eg(this);
+ eg.buildGraph();
+ eg.encode();
+ printConstraints();
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
- model_println("Is problem UNSAT after encoding: %d", unsat);
+ model_print("Is problem UNSAT after encoding: %d\n", unsat);
int result = unsat ? IS_UNSAT : satEncoder->solve();
- model_println("Result Computed in CSolver: %d", result);
+ model_print("Result Computed in CSolver: %d\n", result);
long long finishTime = getTimeNano();
elapsedTime = finishTime - startTime;
if (deleteTuner) {
return result;
}
+void CSolver::printConstraints() {
+ SetIteratorBooleanEdge *it = getConstraints();
+ while (it->hasNext()) {
+ BooleanEdge b = it->next();
+ if (b.isNegated())
+ model_print("!");
+ b->print();
+ model_print("\n");
+ }
+ delete it;
+
+}
+
uint64_t CSolver::getElementValue(Element *element) {
switch (element->type) {
case ELEMSET:
}
bool CSolver::getBooleanValue(BooleanEdge bedge) {
- Boolean *boolean=bedge.getBoolean();
+ Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
return getBooleanVariableValueSATTranslator(this, boolean);
Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
VarType getSetVarType(Set *set);
-
+
Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
/** This function creates a mutable set. */
items to the set. */
uint64_t createUniqueItem(MutableSet *set);
-
+
/**
* Freeze and finalize the mutableSet ...
*/
- void finalizeMutableSet(MutableSet* set);
+ void finalizeMutableSet(MutableSet *set);
/** This function creates an element variable over a set. */
/** This function creates an element constrant. */
Element *getElementConst(VarType type, uint64_t value);
-
- Set* getElementRange (Element* element);
+
+ Set *getElementRange (Element *element);
BooleanEdge getBooleanTrue();
bool isTrue(BooleanEdge b);
bool isFalse(BooleanEdge b);
- void setUnSAT() { model_println("Setting UNSAT %%%%%%"); unsat = true; }
-
+ void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
bool isUnSAT() { return unsat; }
+ void printConstraints();
+
Vector<Order *> *getOrders() { return &allOrders;}
- HashsetOrder * getActiveOrders() { return &activeOrders;}
+ HashsetOrder *getActiveOrders() { return &activeOrders;}
Tuner *getTuner() { return tuner; }
- SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
+ SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
SATEncoder *getSATEncoder() {return satEncoder;}
Vector<Order *> allOrders;
HashsetOrder activeOrders;
-
+
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;
void ourfree(void *ptr);
void * ourcalloc(size_t count, size_t size);
void * ourrealloc(void *ptr, size_t size);
-*/
+ */
-#if 1
-void * model_malloc(size_t size);
+#if 0
+void *model_malloc(size_t size);
void model_free(void *ptr);
-void * model_calloc(size_t count, size_t size);
-void * model_realloc(void *ptr, size_t size);
+void *model_calloc(size_t count, size_t size);
+void *model_realloc(void *ptr, size_t size);
#define ourmalloc model_malloc
projects / satune.git / commitdiff