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};
}
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(){
+void BooleanVar::print() {
model_print("BooleanVar:%lu\n", (uintptr_t)this);
}
-void BooleanConst::print(){
- model_print("BooleanConst:%s\n", 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(){
+void BooleanOrder::print() {
model_print("{BooleanOrder: First= %lu, Second = %lu on Order:\n", first, second);
order->print();
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(){
+void BooleanPredicate::print() {
model_print("{BooleanPredicate:\n");
predicate->print();
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_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_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");
+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++){
+ for (uint i = 0; i < size; i++) {
BooleanEdge input = inputs.get(i);
- if(input.isNegated())
+ if (input.isNegated())
model_print("!");
input.getBoolean()->print();
}
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(){
+void ElementSet::print() {
model_print("{ElementSet:\n");
set->print();
model_print("}\n");
}
-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_print("{ElementConst: %lu}\n", 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(){
+void ElementFunction::print() {
model_print("{ElementFunction:\n");
function->print();
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();
}
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;
};
ElementSet(ASTNodeType type, Set *s);
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;
};
public:
ElementConst(uint64_t value, Set *_set);
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(){
+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 *));
}
}
void FunctionOperator::print() {
- model_print("{FunctionOperator: %s}\n", op == SATC_ADD? "ADD": "SUB" );
+ 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(){
+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(){
+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_print("{PredicateOperator: %s }\n", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL");
+void PredicateOperator::print() {
+ model_print("{PredicateOperator: %s }\n", op == SATC_EQUALS ? "EQUAL" : "NOT-EQUAL");
}
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;
if (constraints.contains(bexpr.negate())) {
constraints.remove(bexpr.negate());
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);
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));
serializer->mywrite(&low, sizeof(uint64_t));
serializer->mywrite(&isMutable, sizeof(bool));
uint size = members->getSize();
serializer->mywrite(&size, sizeof(uint));
- for(uint i=0; i<size; i++){
+ for (uint i = 0; i < size; i++) {
uint64_t mem = members->get(i);
serializer->mywrite(&mem, sizeof(uint64_t));
}
}
-void Set::print(){
+void Set::print() {
model_print("{Set:");
- if(isRange){
+ 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++){
+ for (uint i = 0; i < size; i++) {
uint64_t mem = members->get(i);
model_print("%lu, ", mem);
}
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(){
+void Table::print() {
model_print("{Table:\n");
- SetIteratorTableEntry* iterator = getEntries();
- while(iterator->hasNext()){
- TableEntry* entry = iterator->next();
+ SetIteratorTableEntry *iterator = getEntries();
+ while (iterator->hasNext()) {
+ TableEntry *entry = iterator->next();
model_print("<");
- for(uint i=0; i<entry->inputSize; i++){
+ for (uint i = 0; i < entry->inputSize; i++) {
model_print("%lu, ", entry->inputs[i]);
}
model_print(" == %lu>", entry->output);
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;
+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 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);
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;
}
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();
void addNode(EncodingNode *n);
- SetIteratorEncodingNode * nodeIterator();
+ SetIteratorEncodingNode *nodeIterator();
void encode();
uint getEncoding(EncodingNode *n, uint64_t val);
uint getEncodingSize(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;
};
OrderNode *sinkNode = outEdge->sink;
sinkNode->inEdges.remove(outEdge);
//Adding new edge to new sink and src nodes ...
- if(srcNode == sinkNode) {
+ if (srcNode == sinkNode) {
This->setUnSAT();
delete iterout;
delete iterin;
if (!edge->mustNeg && sources->contains(child)) {
edge->mustNeg = true;
edge->polNeg = true;
- if (edge->mustPos){
+ if (edge->mustPos) {
solver->setUnSAT();
}
}
}
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();
//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++) {
delete edges;
}
-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;
}
void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
OrderEdge *getInverseOrderEdge(OrderEdge *edge);
- Order *getOrder() {return order;}
- bool isTherePath(OrderNode* source, OrderNode* destination);
- bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
+ 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 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) {
}
}
-
+
bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
if (mustReachPrune)
removeMustBeTrueNodes(solver, graph);
-
+
//This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
decomposeOrder(order, graph);
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();
};
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;
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
* 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;
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) { \
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;
bool isMutable;
myread(&isMutable, sizeof(bool));
Set *set;
- if(isMutable){
+ if (isMutable) {
set = new MutableSet(type);
}
uint size;
myread(&size, sizeof(uint));
Vector<uint64_t> members;
- for(uint i=0; i<size; i++){
+ for (uint i = 0; i < size; i++) {
uint64_t mem;
myread(&mem, sizeof(uint64_t));
- if(isMutable) {
- ((MutableSet*) set)->addElementMSet(mem);
- }else {
+ if (isMutable) {
+ ((MutableSet *) set)->addElementMSet(mem);
+ } else {
members.push(mem);
}
}
- if(!isMutable){
- set = isRange? solver->createRangeSet(type, low, high):
- solver->createSet(type, members.expose(), size);
+ if (!isMutable) {
+ set = isRange ? solver->createRangeSet(type, low, high) :
+ solver->createSet(type, members.expose(), size);
}
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);
+ 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));
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);
+ 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) {
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));
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");
}
}
}
-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);
}
-
+
}
public:
DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
bool resolveOrder(uint64_t first, uint64_t second);
- bool resolvePartialOrder(OrderNode* first, OrderNode* second);
+ bool resolvePartialOrder(OrderNode *first, OrderNode *second);
virtual ~DecomposeOrderResolver();
private:
OrderGraph *graph;
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);
#include "time.h"
/*
- extern int model_out;
- extern int model_err;
- extern int switch_alloc;
-
- #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
- #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
- #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
-
- #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
-
- #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
+ extern int model_out;
+ extern int model_err;
+ extern int switch_alloc;
+
+ #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
+ #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
+ #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+
+ #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
+
+ #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
*/
#define model_print printf
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) {
+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]);
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));
if (b->type == BOOLCONST) {
if (isTrue(b))
continue;
- else{
+ else {
return boolFalse;
- }
+ }
} else
newarray[newindex++] = b;
}
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if(constraint.isNegated())
+ if (constraint.isNegated())
model_print("!");
constraint.getBoolean()->print();
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
- int t=0;
+ 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++) {
+ if (b->op == SATC_AND) {
+ for (uint i = 0; i < b->inputs.getSize(); i++) {
addConstraint(b->inputs.get(i));
}
return;
}
}
constraints.add(constraint);
- Boolean *ptr=constraint.getBoolean();
-
+ Boolean *ptr = constraint.getBoolean();
+
if (ptr->boolVal == BV_UNSAT) {
setUnSAT();
}
-
+
replaceBooleanWithTrueNoRemove(constraint);
constraint->parents.clear();
}
Preprocess pp(this);
pp.doTransform();
-
+
DecomposeOrderTransform dot(this);
dot.doTransform();
EncodingGraph eg(this);
eg.buildGraph();
eg.encode();
-
+
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
- model_print("Is problem UNSAT after encoding: %d\n", unsat);
+ model_print("Is problem UNSAT after encoding: %d\n", unsat);
int result = unsat ? IS_UNSAT : satEncoder->solve();
- model_print("Result Computed in CSolver: %d\n", result);
+ model_print("Result Computed in CSolver: %d\n", result);
long long finishTime = getTimeNano();
elapsedTime = finishTime - startTime;
if (deleteTuner) {
}
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 isUnSAT() { return unsat; }
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 0
-void * model_malloc(size_t size);
+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