#include "boolean.h"
#include "element.h"
-bool compareArray(Array<Boolean *> * inputs1, Array<Boolean *> *inputs2) {
+bool compareArray(Array<Boolean *> *inputs1, Array<Boolean *> *inputs2) {
if (inputs1->getSize() != inputs2->getSize())
return false;
- for(uint i=0;i<inputs1->getSize();i++) {
+ for (uint i = 0; i < inputs1->getSize(); i++) {
if (inputs1->get(i) != inputs2->get(i))
return false;
}
return true;
}
-bool compareArray(Array<Element *> * inputs1, Array<Element *> *inputs2) {
+bool compareArray(Array<Element *> *inputs1, Array<Element *> *inputs2) {
if (inputs1->getSize() != inputs2->getSize())
return false;
- for(uint i=0;i<inputs1->getSize();i++) {
+ for (uint i = 0; i < inputs1->getSize(); i++) {
if (inputs1->get(i) != inputs2->get(i))
return false;
}
return true;
}
-uint hashArray(Array<Boolean *> * inputs) {
+uint hashArray(Array<Boolean *> *inputs) {
uint hash = inputs->getSize();
- for(uint i=0;i<inputs->getSize();i++) {
+ for (uint i = 0; i < inputs->getSize(); i++) {
uint newval = (uint)(uintptr_t) inputs->get(i);
hash ^= newval;
hash = (hash << 3) | (hash >> 29);
return hash;
}
-uint hashArray(Array<Element *> * inputs) {
+uint hashArray(Array<Element *> *inputs) {
uint hash = inputs->getSize();
- for(uint i=0;i<inputs->getSize();i++) {
+ for (uint i = 0; i < inputs->getSize(); i++) {
uint newval = (uint)(uintptr_t) inputs->get(i);
hash ^= newval;
hash = (hash << 3) | (hash >> 29);
return hash;
}
-uint hashBoolean(Boolean * b) {
- switch(b->type) {
+uint hashBoolean(Boolean *b) {
+ switch (b->type) {
case ORDERCONST: {
- BooleanOrder * o=(BooleanOrder *)b;
+ BooleanOrder *o = (BooleanOrder *)b;
return ((uint)(uintptr_t) o->order) ^ ((uint) o->first) ^ (((uint)(o->second)) << 2);
}
case BOOLEANVAR: {
return (uint)(uintptr_t) b;
}
case LOGICOP: {
- BooleanLogic * l=(BooleanLogic *)b;
+ BooleanLogic *l = (BooleanLogic *)b;
return ((uint)l->op) ^ hashArray(&l->inputs);
}
case PREDICATEOP: {
- BooleanPredicate * p=(BooleanPredicate *)b;
+ BooleanPredicate *p = (BooleanPredicate *)b;
return ((uint)(uintptr_t) p->predicate) ^
- (((uint)(uintptr_t) p->undefStatus) << 1) ^
- hashArray(&p->inputs);
+ (((uint)(uintptr_t) p->undefStatus) << 1) ^
+ hashArray(&p->inputs);
}
default:
ASSERT(0);
bool compareBoolean(Boolean *b1, Boolean *b2) {
if (b1->type != b2->type)
return false;
- switch(b1->type) {
+ switch (b1->type) {
case ORDERCONST: {
- BooleanOrder * o1=(BooleanOrder *)b1;
- BooleanOrder * o2=(BooleanOrder *)b2;
+ BooleanOrder *o1 = (BooleanOrder *)b1;
+ BooleanOrder *o2 = (BooleanOrder *)b2;
return (o1->order == o2->order) && (o1->first == o2->first) && (o1->second == o2->second);
}
case BOOLEANVAR: {
return b1 == b2;
}
case LOGICOP: {
- BooleanLogic * l1=(BooleanLogic *)b1;
- BooleanLogic * l2=(BooleanLogic *)b2;
+ BooleanLogic *l1 = (BooleanLogic *)b1;
+ BooleanLogic *l2 = (BooleanLogic *)b2;
return (l1->op == l2->op) && compareArray(&l1->inputs, &l2->inputs);
}
case PREDICATEOP: {
- BooleanPredicate * p1=(BooleanPredicate *)b1;
- BooleanPredicate * p2=(BooleanPredicate *)b2;
+ BooleanPredicate *p1 = (BooleanPredicate *)b1;
+ BooleanPredicate *p2 = (BooleanPredicate *)b2;
return (p1->predicate == p2->predicate) &&
- p1->undefStatus == p2->undefStatus &&
- compareArray(&p1->inputs, &p2->inputs);
+ p1->undefStatus == p2->undefStatus &&
+ compareArray(&p1->inputs, &p2->inputs);
}
default:
ASSERT(0);
}
uint hashElement(Element *e) {
- switch(e->type) {
+ switch (e->type) {
case ELEMSET: {
return (uint)(uintptr_t) e;
}
case ELEMFUNCRETURN: {
- ElementFunction * ef=(ElementFunction *) e;
+ ElementFunction *ef = (ElementFunction *) e;
return ((uint)(uintptr_t) ef->function) ^
- ((uint)(uintptr_t) ef->overflowstatus) ^
- hashArray(&ef->inputs);
+ ((uint)(uintptr_t) ef->overflowstatus) ^
+ hashArray(&ef->inputs);
}
case ELEMCONST: {
- ElementConst * ec=(ElementConst *) e;
+ ElementConst *ec = (ElementConst *) e;
return ((uint) ec->value);
}
default:
bool compareElement(Element *e1, Element *e2) {
if (e1->type != e2->type)
return false;
- switch(e1->type) {
+ switch (e1->type) {
case ELEMSET: {
return e1 == e2;
}
case ELEMFUNCRETURN: {
- ElementFunction * ef1=(ElementFunction *) e1;
- ElementFunction * ef2=(ElementFunction *) e2;
+ ElementFunction *ef1 = (ElementFunction *) e1;
+ ElementFunction *ef2 = (ElementFunction *) e2;
return (ef1->function == ef2->function) &&
- (ef1->overflowstatus == ef2->overflowstatus) &&
- compareArray(&ef1->inputs, &ef2->inputs);
+ (ef1->overflowstatus == ef2->overflowstatus) &&
+ compareArray(&ef1->inputs, &ef2->inputs);
}
case ELEMCONST: {
- ElementConst * ec1=(ElementConst *) e1;
- ElementConst * ec2=(ElementConst *) e2;
+ ElementConst *ec1 = (ElementConst *) e1;
+ ElementConst *ec2 = (ElementConst *) e2;
return (ec1->value == ec2->value);
}
default:
#include "classes.h"
#include "hashtable.h"
-uint hashBoolean(Boolean * boolean);
+uint hashBoolean(Boolean *boolean);
bool compareBoolean(Boolean *b1, Boolean *b2);
uint hashElement(Element *element);
};
class BooleanConst : public Boolean {
- public:
+public:
BooleanConst(bool isTrue);
Boolean *clone(CSolver *solver, CloneMap *map);
bool isTrue() {return istrue;}
Vector<ASTNode *> parents;
ElementEncoding encoding;
virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
-
+
CMEMALLOC;
};
orderPairTable->resetanddelete();
delete orderPairTable;
}
-
+
if (graph != NULL) {
delete graph;
}
Order *clone(CSolver *solver, CloneMap *map);
Vector<BooleanOrder *> constraints;
OrderEncoding encoding;
- void setOrderResolver(OrderResolver* _resolver) { encoding.resolver = _resolver;};
+ void setOrderResolver(OrderResolver *_resolver) { encoding.resolver = _resolver;};
void initializeOrderHashtable();
void initializeOrderElementsHashtable();
void addOrderConstraint(BooleanOrder *constraint);
}
}
-uint64_t Set::getMemberAt(uint index){
- if(isRange){
- return low+index;
- }else {
+uint64_t Set::getMemberAt(uint index) {
+ if (isRange) {
+ return low + index;
+ } else {
return members->get(index);
}
}
virtual ~Set();
bool exists(uint64_t element);
uint getSize();
- VarType getType(){return type;}
- uint64_t getNewUniqueItem(){return low++;}
+ VarType getType() {return type;}
+ uint64_t getNewUniqueItem() {return low++;}
uint64_t getMemberAt(uint index);
uint64_t getElement(uint index);
virtual Set *clone(CSolver *solver, CloneMap *map);
uint64_t low;//also used to count unique items
uint64_t high;
Vector<uint64_t> *members;
-
+
};
#endif/* SET_H */
if ( tmp != NULL) {
delete node;
node = tmp;
- } else if(create) {
+ } else if (create) {
nodes->add(node);
- } else{
+ } else {
delete node;
return NULL;
}
-/*
+/*
* File: ordertransform.cc
* Author: hamed
- *
+ *
* Created on August 28, 2017, 10:35 AM
*/
#include "ordergraph.h"
#include "csolver.h"
#include "decomposeorderresolver.h"
+#include "tunable.h"
+#include "orderanalysis.h"
-DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver)
- :Transform(_solver)
+DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
+ : Transform(_solver)
{
}
DecomposeOrderTransform::~DecomposeOrderTransform() {
}
-bool DecomposeOrderTransform::canExecuteTransform(){
- return canExecutePass(solver, currOrder->type, DECOMPOSEORDER, &onoff);
+void DecomposeOrderTransform::doTransform() {
+ Vector<Order *> *orders = solver->getOrders();
+ uint size = orders->getSize();
+ for (uint i = 0; i < size; i++) {
+ Order *order = orders->get(i);
+
+ if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
+ continue;
+ }
+
+ OrderGraph *graph = buildOrderGraph(order);
+ if (order->type == SATC_PARTIAL) {
+ //Required to do SCC analysis for partial order graphs. It
+ //makes sure we don't incorrectly optimize graphs with negative
+ //polarity edges
+ completePartialOrderGraph(graph);
+ }
+
+ bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+ if (mustReachGlobal)
+ reachMustAnalysis(solver, graph, false);
+
+ bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+ if (mustReachLocal) {
+ //This pair of analysis is also optional
+ if (order->type == SATC_PARTIAL) {
+ localMustAnalysisPartial(solver, graph);
+ } else {
+ localMustAnalysisTotal(solver, graph);
+ }
+ }
+
+ bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+ if (mustReachPrune)
+ removeMustBeTrueNodes(solver, graph);
+
+ //This is needed for splitorder
+ computeStronglyConnectedComponentGraph(graph);
+ decomposeOrder(order, graph);
+ delete graph;
+ }
}
-void DecomposeOrderTransform::doTransform(){
+void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
Vector<Order *> ordervec;
Vector<Order *> partialcandidatevec;
uint size = currOrder->constraints.getSize();
BooleanOrder *orderconstraint = currOrder->constraints.get(i);
OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
- model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
if (from->sccNum != to->sccNum) {
OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polPos) {
Order *neworder = partialcandidatevec.get(i);
if (neworder != NULL) {
neworder->type = SATC_TOTAL;
- model_print("i=%u\t", i);
}
}
}
-/*
+/*
* File: ordertransform.h
* Author: hamed
*
class DecomposeOrderTransform : public Transform {
public:
- DecomposeOrderTransform(CSolver* _solver);
- virtual ~DecomposeOrderTransform();
+ DecomposeOrderTransform(CSolver *_solver);
+ ~DecomposeOrderTransform();
void doTransform();
- void setOrderGraph(OrderGraph* _graph){
- currGraph = _graph;
- }
- void setCurrentOrder(Order* _current) { currOrder = _current;}
- bool canExecuteTransform();
+ void decomposeOrder (Order *currOrder, OrderGraph *currGraph);
+
CMEMALLOC;
- private:
- Order* currOrder;
- OrderGraph* currGraph;
+private:
+ Order *currOrder;
+ OrderGraph *currGraph;
};
-#endif /* ORDERTRANSFORM_H */
+#endif/* ORDERTRANSFORM_H */
-
#include "integerencoding.h"
#include "set.h"
#include "order.h"
#include "csolver.h"
#include "integerencodingrecord.h"
#include "integerencorderresolver.h"
+#include "tunable.h"
-
-IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver)
- :Transform(_solver)
-{
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
+ : Transform(_solver)
+{
orderIntEncoding = new HashTableOrderIntEncoding();
}
-IntegerEncodingTransform::~IntegerEncodingTransform(){
+IntegerEncodingTransform::~IntegerEncodingTransform() {
orderIntEncoding->resetanddelete();
}
-bool IntegerEncodingTransform::canExecuteTransform(){
- return canExecutePass(solver, currOrder->type, ORDERINTEGERENCODING, &offon);
+void IntegerEncodingTransform::doTransform() {
+ Vector<Order *> *orders = solver->getOrders();
+ uint size = orders->getSize();
+ for (uint i = 0; i < size; i++) {
+ Order *order = orders->get(i);
+ if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
+ integerEncode(order);
+ }
}
-void IntegerEncodingTransform::doTransform(){
- IntegerEncodingRecord* encodingRecord = NULL;
+void IntegerEncodingTransform::integerEncode(Order *currOrder) {
+ IntegerEncodingRecord *encodingRecord = NULL;
if (!orderIntEncoding->contains(currOrder)) {
encodingRecord = new IntegerEncodingRecord(
- solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize()-1));
+ solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
orderIntEncoding->put(currOrder, encodingRecord);
} else {
encodingRecord = orderIntEncoding->get(currOrder);
}
uint size = currOrder->constraints.getSize();
- for(uint i=0; i<size; i++){
+ for (uint i = 0; i < size; i++) {
orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
}
currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
- IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder);
+ IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
//getting two elements and using LT predicate ...
Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
-/*
+/*
* File: integerencoding.h
* Author: hamed
*
#include "transform.h"
#include "order.h"
-class IntegerEncodingTransform : public Transform{
+class IntegerEncodingTransform : public Transform {
public:
- IntegerEncodingTransform(CSolver* solver);
+ IntegerEncodingTransform(CSolver *solver);
void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
- void setCurrentOrder(Order* _curr) {currOrder = _curr;}
void doTransform();
- bool canExecuteTransform();
+ void integerEncode(Order *currOrder);
+
virtual ~IntegerEncodingTransform();
private:
- Order* currOrder;
+ Order *currOrder;
//FIXME:We can remove it, because we don't need it for translating anymore... -HG
- HashTableOrderIntEncoding* orderIntEncoding;
+ HashTableOrderIntEncoding *orderIntEncoding;
};
-#endif /* INTEGERENCODING_H */
+#endif/* INTEGERENCODING_H */
-/*
+/*
* File: integerencodingrecord.cpp
* Author: hamed
- *
+ *
* Created on August 26, 2017, 6:19 PM
*/
#include "csolver.h"
#include "orderelement.h"
-IntegerEncodingRecord::IntegerEncodingRecord(Set* _set):
+IntegerEncodingRecord::IntegerEncodingRecord(Set *_set) :
secondarySet(_set)
{
elementTable = new HashsetOrderElement();
}
-IntegerEncodingRecord::~IntegerEncodingRecord(){
+IntegerEncodingRecord::~IntegerEncodingRecord() {
if (elementTable != NULL) {
delete elementTable;
}
}
-Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) {
+Element *IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) {
OrderElement oelement(item, NULL);
if ( elementTable->contains(&oelement)) {
return elementTable->get(&oelement)->getElement();
-/*
+/*
* File: integerencodingrecord.h
* Author: hamed
*
class IntegerEncodingRecord {
public:
- IntegerEncodingRecord(Set* set);
+ IntegerEncodingRecord(Set *set);
~IntegerEncodingRecord();
- Element* getOrderIntegerElement(CSolver *This, uint64_t item, bool create = true);
- inline Set* getSecondarySet() { return secondarySet; }
+ Element *getOrderIntegerElement(CSolver *This, uint64_t item, bool create = true);
+ inline Set *getSecondarySet() { return secondarySet; }
CMEMALLOC;
-
+
private:
- Set* secondarySet;
+ Set *secondarySet;
HashsetOrderElement *elementTable;
};
-#endif /* INTEGERENCODINGRECORD_H */
+#endif/* INTEGERENCODINGRECORD_H */
+++ /dev/null
-/*
- * File: pass.h
- * Author: hamed
- *
- * Created on August 28, 2017, 6:23 PM
- */
-
-#ifndef PASS_H
-#define PASS_H
-#include "classlist.h"
-#include "mymemory.h"
-#include "structs.h"
-#include "tunable.h"
-#include "csolver.h"
-
-class Pass{
-public:
- Pass(){};
- virtual ~Pass(){};
- virtual inline bool canExecutePass(CSolver* This, uint type, Tunables tunable, TunableDesc* desc){
- return GETVARTUNABLE(This->getTuner(), type, tunable, desc);
- }
- CMEMALLOC;
-
-};
-
-
-#endif /* PASS_H */
-
-/*
+/*
* File: transform.cc
* Author: hamed
- *
+ *
* Created on August 26, 2017, 5:14 PM
*/
#include "transform.h"
-Transform::Transform(CSolver* _solver)
+Transform::Transform(CSolver *_solver)
{
solver = _solver;
}
-Transform::~Transform(){
+Transform::~Transform() {
}
-/*
+/*
* File: transform.h
* Author: hamed
*
#include "classlist.h"
#include "mymemory.h"
#include "structs.h"
-#include "pass.h"
-class Transform : public Pass{
+class Transform {
public:
- Transform(CSolver* _solver);
+ Transform(CSolver *_solver);
virtual ~Transform();
- virtual bool canExecuteTransform() = 0;
virtual void doTransform() = 0;
CMEMALLOC;
- protected:
+protected:
// Need solver for translating back the result ...
- CSolver* solver;
+ CSolver *solver;
};
-#endif /* TRANSFORM_H */
+#endif/* TRANSFORM_H */
+++ /dev/null
-#include "transformer.h"
-#include "common.h"
-#include "order.h"
-#include "boolean.h"
-#include "ordergraph.h"
-#include "ordernode.h"
-#include "rewriter.h"
-#include "orderedge.h"
-#include "mutableset.h"
-#include "ops.h"
-#include "csolver.h"
-#include "orderanalysis.h"
-#include "tunable.h"
-#include "transform.h"
-#include "element.h"
-#include "integerencoding.h"
-#include "decomposeordertransform.h"
-
-Transformer::Transformer(CSolver *_solver):
- integerEncoding(new IntegerEncodingTransform(_solver)),
- decomposeOrder(new DecomposeOrderTransform(_solver)),
- solver(_solver)
-{
-}
-
-Transformer::~Transformer(){
- delete integerEncoding;
- delete decomposeOrder;
-}
-
-void Transformer::orderAnalysis() {
- Vector<Order *> *orders = solver->getOrders();
- uint size = orders->getSize();
- for (uint i = 0; i < size; i++) {
- Order *order = orders->get(i);
- decomposeOrder->setCurrentOrder(order);
-
- if (true) {
- continue;
- }
-
- OrderGraph *graph = buildOrderGraph(order);
- if (order->type == SATC_PARTIAL) {
- //Required to do SCC analysis for partial order graphs. It
- //makes sure we don't incorrectly optimize graphs with negative
- //polarity edges
- completePartialOrderGraph(graph);
- }
-
-
- bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
-
- if (mustReachGlobal)
- reachMustAnalysis(solver, graph, false);
-
- bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-
- if (mustReachLocal) {
- //This pair of analysis is also optional
- if (order->type == SATC_PARTIAL) {
- localMustAnalysisPartial(solver, graph);
- } else {
- localMustAnalysisTotal(solver, graph);
- }
- }
-
- bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-
- if (mustReachPrune)
- removeMustBeTrueNodes(solver, graph);
-
- //This is needed for splitorder
- computeStronglyConnectedComponentGraph(graph);
- decomposeOrder->setOrderGraph(graph);
- decomposeOrder->doTransform();
- delete graph;
-
- integerEncoding->setCurrentOrder(order);
- if(!integerEncoding->canExecuteTransform()){
- continue;
- }
- integerEncoding->doTransform();
- }
-}
-
-
+++ /dev/null
-/*
- * File: transformer.h
- * Author: hamed
- *
- * Created on August 24, 2017, 5:33 PM
- */
-
-#ifndef ORDERDECOMPOSE_H
-#define ORDERDECOMPOSE_H
-#include "classlist.h"
-#include "structs.h"
-#include "transform.h"
-#include "integerencoding.h"
-#include "decomposeordertransform.h"
-
-class Transformer{
-public:
- Transformer(CSolver* solver);
- ~Transformer();
- IntegerEncodingTransform* getIntegerEncodingTransform(){ return integerEncoding; }
- void orderAnalysis();
- CMEMALLOC;
- private:
- //For now we can just add transforms here, but in future we may want take a smarter approach.
- IntegerEncodingTransform* integerEncoding;
- DecomposeOrderTransform* decomposeOrder;
-
- CSolver* solver;
-};
-
-
-#endif/* ORDERDECOMPOSE_H */
-
}
int solveCNF(CNF *cnf) {
- long long startTime=getTimeNano();
+ long long startTime = getTimeNano();
countPass(cnf);
convertPass(cnf, false);
finishedClauses(cnf->solver);
- long long startSolve=getTimeNano();
+ long long startSolve = getTimeNano();
int result = solve(cnf->solver);
- long long finishTime=getTimeNano();
- cnf->encodeTime=startSolve-startTime;
- cnf->solveTime=finishTime-startSolve;
+ long long finishTime = getTimeNano();
+ cnf->encodeTime = startSolve - startTime;
+ cnf->solveTime = finishTime - startSolve;
return result;
}
public:
OrderElement(uint64_t item, Element *elem);
inline uint getHash() {return (uint) item;}
- inline bool equals(OrderElement* oe){ return item == oe->item;}
- inline Element* getElement() { return elem; }
+ inline bool equals(OrderElement *oe) { return item == oe->item;}
+ inline Element *getElement() { return elem; }
CMEMALLOC;
private:
uint64_t item;
#include "predicate.h"
#include "set.h"
-SATEncoder::SATEncoder(CSolver * _solver) :
+SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
solver(_solver) {
}
Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
Edge result;
if (booledgeMap.contains(constraint)) {
- Edge e={(Node *) booledgeMap.get(constraint)};
+ Edge e = {(Node *) booledgeMap.get(constraint)};
return e;
}
-
+
switch (constraint->type) {
case ORDERCONST:
- result=encodeOrderSATEncoder((BooleanOrder *) constraint);
+ result = encodeOrderSATEncoder((BooleanOrder *) constraint);
break;
case BOOLEANVAR:
- result=encodeVarSATEncoder((BooleanVar *) constraint);
+ result = encodeVarSATEncoder((BooleanVar *) constraint);
break;
case LOGICOP:
- result=encodeLogicSATEncoder((BooleanLogic *) constraint);
+ result = encodeLogicSATEncoder((BooleanLogic *) constraint);
break;
case PREDICATEOP:
- result=encodePredicateSATEncoder((BooleanPredicate *) constraint);
+ result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
break;
default:
model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
/* Check to see if we have already encoded this element. */
if (getElementEncoding(element)->variables != NULL)
return;
-
+
/* Need to encode. */
switch ( element->type) {
case ELEMFUNCRETURN:
typedef Hashtable<Boolean *, Node *, uintptr_t, 4> BooleanToEdgeMap;
class SATEncoder {
- public:
+public:
int solve();
SATEncoder(CSolver *solver);
~SATEncoder();
void encodeAllSATEncoder(CSolver *csolver);
Edge encodeConstraintSATEncoder(Boolean *constraint);
- CNF * getCNF() { return cnf;}
+ CNF *getCNF() { return cnf;}
long long getSolveTime() { return cnf->solveTime; }
long long getEncodeTime() { return cnf->encodeTime; }
-
+
CMEMALLOC;
- private:
+private:
Edge getNewVarSATEncoder();
void getArrayNewVarsSATEncoder(uint num, Edge *carray);
Edge encodeVarSATEncoder(BooleanVar *constraint);
Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
-
+
CNF *cnf;
CSolver *solver;
BooleanToEdgeMap booledgeMap;
return false;
}
- /** @brief Return random key from set. */
+ /** @brief Return random key from set. */
- _Key getRandomElement() {
+ _Key getRandomElement() {
if (getSize() == 0)
return NULL;
else if (getSize() < 6) {
uint count = random() % getSize();
- Linknode<_Key> *ptr=list;
- while(count > 0) {
+ Linknode<_Key> *ptr = list;
+ while (count > 0) {
ptr = ptr->next;
count--;
}
size = 0;
}
- /** Doesn't work with zero value */
- _Val getRandomValue() {
- while(true) {
- unsigned int index=random() & capacitymask;
+ /** Doesn't work with zero value */
+ _Val getRandomValue() {
+ while (true) {
+ unsigned int index = random() & capacitymask;
struct Hashlistnode<_Key, _Val> *bin = &table[index];
if (bin->key != NULL && bin->val != NULL) {
return bin->val;
typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, 4> HashtableNodeToNodeSet;
typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
typedef Hashtable<void *, void *, uintptr_t, 4> CloneMap;
-typedef Hashtable<Order* , IntegerEncodingRecord*, uintptr_t, 4> HashTableOrderIntEncoding;
+typedef Hashtable<Order *, IntegerEncodingRecord *, uintptr_t, 4> HashTableOrderIntEncoding;
typedef SetIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
typedef SetIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
class OrderEncoding {
public:
OrderEncoding(Order *order);
-
- OrderResolver* resolver;
+
+ OrderResolver *resolver;
OrderEncodingType type;
Order *order;
CMEMALLOC;
Boolean *o58 = solver->orderConstraint(order, 5, 8);
Boolean *o81 = solver->orderConstraint(order, 8, 1);
- Boolean * array1[]={o12, o13, o24, o34};
+ Boolean *array1[] = {o12, o13, o24, o34};
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) );
- Boolean * array2[]={o41, o57};
-
+ Boolean *array2[] = {o41, o57};
+
Boolean *b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
- Boolean * array3[]={o34};
+ Boolean *array3[] = {o34};
Boolean *o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
- Boolean * array4[]={o24};
+ Boolean *array4[] = {o24};
Boolean *o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
- Boolean * array5[]={o34n, o24n};
+ Boolean *array5[] = {o34n, o24n};
Boolean *b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
- Boolean * array6[] = {b1, b2};
+ Boolean *array6[] = {b1, b2};
solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );
- Boolean * array7[] = {o12, o13};
+ Boolean *array7[] = {o12, o13};
solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
- Boolean * array8[] = {o76, o65};
+ Boolean *array8[] = {o76, o65};
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
- Boolean * array9[] = {o76, o65};
- Boolean* b3= solver->applyLogicalOperation(SATC_AND, array9, 2) ;
- Boolean * array10[] = {o57};
- Boolean* o57n= solver->applyLogicalOperation(SATC_NOT, array10, 1);
- Boolean * array11[] = {b3, o57n};
+ Boolean *array9[] = {o76, o65};
+ Boolean *b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
+ Boolean *array10[] = {o57};
+ Boolean *o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
+ Boolean *array11[] = {b3, o57n};
solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));
- Boolean * array12[] = {o58, o81};
+ Boolean *array12[] = {o58, o81};
solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
-
+
/* if (solver->solve() == 1)
- printf("SAT\n");
- else
- printf("UNSAT\n");*/
-
+ printf("SAT\n");
+ else
+ printf("UNSAT\n");*/
+
solver->autoTune(100);
delete solver;
}
-/*
+/*
* File: DecomposeOrderResolver.cc
* Author: hamed
- *
+ *
* Created on September 1, 2017, 10:36 AM
*/
#include "ordernode.h"
#include "ordergraph.h"
-DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*>& _orders):
+DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order *> &_orders) :
graph(_graph),
orders(_orders.getSize(), _orders.expose())
{
DecomposeOrderResolver::~DecomposeOrderResolver() {
}
-HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second){
+HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
- if(from == NULL){
+ if (from == NULL) {
return SATC_UNORDERED;
}
OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
- if(from == NULL){
+ if (from == NULL) {
return SATC_UNORDERED;
}
if (from->sccNum != to->sccNum) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
- if (edge != NULL && edge->mustPos){
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
+ if (edge != NULL && edge->mustPos) {
return SATC_FIRST;
- } else if( edge != NULL && edge->mustNeg){
+ } else if ( edge != NULL && edge->mustNeg) {
return SATC_SECOND;
- }else {
- switch(graph->getOrder()->type){
- case SATC_TOTAL:
- return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND;
- case SATC_PARTIAL:
- //Adding support for partial order ...
- default:
- ASSERT(0);
- }
+ } else {
+ switch (graph->getOrder()->type) {
+ case SATC_TOTAL:
+ return from->sccNum < to->sccNum ? SATC_FIRST : SATC_SECOND;
+ case SATC_PARTIAL:
+ //Adding support for partial order ...
+ default:
+ ASSERT(0);
+ }
}
} else {
Order *suborder = NULL;
-/*
+/*
* File: DecomposeOrderResolver.h
* Author: hamed
*
#include "structs.h"
#include "orderresolver.h"
-class DecomposeOrderResolver : public OrderResolver{
+class DecomposeOrderResolver : public OrderResolver {
public:
- DecomposeOrderResolver(OrderGraph* graph, Vector<Order *> & orders);
+ DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
HappenedBefore resolveOrder(uint64_t first, uint64_t second);
virtual ~DecomposeOrderResolver();
private:
- OrderGraph* graph;
- Vector<Order*> orders;
+ OrderGraph *graph;
+ Vector<Order *> orders;
};
-#endif /* DECOMPOSEORDERRESOLVER_H */
+#endif/* DECOMPOSEORDERRESOLVER_H */
-/*
+/*
* File: integerencorderresolver.cpp
* Author: hamed
- *
+ *
* Created on September 1, 2017, 4:58 PM
*/
#include "integerencodingrecord.h"
#include "sattranslator.h"
-IntegerEncOrderResolver::IntegerEncOrderResolver(CSolver* _solver, IntegerEncodingRecord* _ierecord):
+IntegerEncOrderResolver::IntegerEncOrderResolver(CSolver *_solver, IntegerEncodingRecord *_ierecord) :
solver(_solver),
ierecord(_ierecord)
{
}
-HappenedBefore IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second){
- Element* elem1 = ierecord->getOrderIntegerElement(solver, first, false);
- if(elem1 == NULL)
+HappenedBefore IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
+ Element *elem1 = ierecord->getOrderIntegerElement(solver, first, false);
+ if (elem1 == NULL)
return SATC_UNORDERED;
- Element* elem2 = ierecord->getOrderIntegerElement(solver, second, false);
- if(elem2 == NULL)
+ Element *elem2 = ierecord->getOrderIntegerElement(solver, second, false);
+ if (elem2 == NULL)
return SATC_UNORDERED;
-
+
uint64_t val1 = getElementValueSATTranslator(solver, elem1);
uint64_t val2 = getElementValueSATTranslator(solver, elem2);
- return val1 < val2? SATC_FIRST : val1> val2? SATC_SECOND: SATC_UNORDERED;
+ return val1 < val2 ? SATC_FIRST : val1> val2 ? SATC_SECOND : SATC_UNORDERED;
}
-/*
+/*
* File: integerencorderresolver.h
* Author: hamed
*
#define INTEGERENCORDERRESOLVER_H
#include "orderresolver.h"
-class IntegerEncOrderResolver : public OrderResolver{
+class IntegerEncOrderResolver : public OrderResolver {
public:
- IntegerEncOrderResolver(CSolver* _solver, IntegerEncodingRecord* _ierecord);
+ IntegerEncOrderResolver(CSolver *_solver, IntegerEncodingRecord *_ierecord);
HappenedBefore resolveOrder(uint64_t first, uint64_t second);
virtual ~IntegerEncOrderResolver();
private:
- CSolver* solver;
- IntegerEncodingRecord* ierecord;
+ CSolver *solver;
+ IntegerEncodingRecord *ierecord;
};
-#endif /* INTEGERENCORDERRESOLVER_H */
+#endif/* INTEGERENCORDERRESOLVER_H */
-/*
+/*
* File: orderpairresolver.cc
* Author: hamed
- *
+ *
* Created on September 1, 2017, 3:36 PM
*/
#include "satencoder.h"
#include "csolver.h"
-OrderPairResolver::OrderPairResolver(CSolver* _solver, Order* _order) :
+OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
solver(_solver),
order(_order)
{
OrderPairResolver::~OrderPairResolver() {
}
-HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second){
- if(order->graph != NULL){
+HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
+ if (order->graph != NULL) {
// For the cases that tuning framework decides no to build a graph for order ...
- OrderGraph* graph = order->graph;
+ OrderGraph *graph = order->graph;
OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
- if(from == NULL){
+ if (from == NULL) {
return SATC_UNORDERED;
}
OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
- if(from == NULL){
+ if (from == NULL) {
return SATC_UNORDERED;
}
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
- if (edge != NULL && edge->mustPos){
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
+ if (edge != NULL && edge->mustPos) {
return SATC_FIRST;
- } else if( edge != NULL && edge->mustNeg){
+ } else if ( edge != NULL && edge->mustNeg) {
return SATC_SECOND;
}
}
//Couldn't infer from graph. Should call the SAT Solver ...
- switch( order->type){
- case SATC_TOTAL:
- resolveTotalOrder(first, second);
- case SATC_PARTIAL:
- //TODO: Support for partial order ...
- default:
- ASSERT(0);
+ switch ( order->type) {
+ case SATC_TOTAL:
+ resolveTotalOrder(first, second);
+ case SATC_PARTIAL:
+ //TODO: Support for partial order ...
+ default:
+ ASSERT(0);
}
-
+
}
-/*
+/*
* File: orderpairresolver.h
* Author: hamed
*
#include "orderresolver.h"
-class OrderPairResolver : public OrderResolver{
+class OrderPairResolver : public OrderResolver {
public:
- OrderPairResolver(CSolver* _solver, Order* _order);
+ OrderPairResolver(CSolver *_solver, Order *_order);
HappenedBefore resolveOrder(uint64_t first, uint64_t second);
virtual ~OrderPairResolver();
private:
- CSolver* solver;
- Order* order;
+ CSolver *solver;
+ Order *order;
HappenedBefore resolveTotalOrder(uint64_t first, uint64_t second);
};
-#endif /* ORDERPAIRRESOLVER_H */
+#endif/* ORDERPAIRRESOLVER_H */
-/*
+/*
* File: orderresolver.h
* Author: hamed
*
class OrderResolver {
public:
- OrderResolver(){};
+ OrderResolver() {};
virtual HappenedBefore resolveOrder(uint64_t first, uint64_t second) = 0;
- virtual ~OrderResolver(){};
+ virtual ~OrderResolver() {};
CMEMALLOC;
};
-#endif /* ORDERRESOLVER_H */
+#endif/* ORDERRESOLVER_H */
solvers.push(solver);
}
-long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) {
- CSolver * copy=problem->clone();
+long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
+ CSolver *copy = problem->clone();
copy->setTuner(tuner);
int result = copy->solve();
- long long elapsedTime=copy->getElapsedTime();
- long long encodeTime=copy->getEncodeTime();
- long long solveTime=copy->getSolveTime();
- long long metric=elapsedTime;
+ long long elapsedTime = copy->getElapsedTime();
+ long long encodeTime = copy->getEncodeTime();
+ long long solveTime = copy->getSolveTime();
+ long long metric = elapsedTime;
model_print("Elapsed Time: %llu\n", elapsedTime);
model_print("Encode Time: %llu\n", encodeTime);
model_print("Solve Time: %llu\n", solveTime);
}
double AutoTuner::evaluateAll(SearchTuner *tuner) {
- double product=1;
- for(uint i=0;i<solvers.getSize();i++) {
- CSolver * problem=solvers.get(i);
- double score=evaluate(problem, tuner);
- product*=score;
+ double product = 1;
+ for (uint i = 0; i < solvers.getSize(); i++) {
+ CSolver *problem = solvers.get(i);
+ double score = evaluate(problem, tuner);
+ product *= score;
}
- return pow(product, 1/((double)solvers.getSize()));
+ return pow(product, 1 / ((double)solvers.getSize()));
}
-SearchTuner * AutoTuner::mutateTuner(SearchTuner * oldTuner, uint k) {
- SearchTuner *newTuner=oldTuner->copyUsed();
- uint numSettings=oldTuner->getSize();
- double factor=0.3;//Adjust this factor...
- uint settingsToMutate=(uint)(factor*(((double)numSettings) * (budget - k))/(budget));
+SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
+ SearchTuner *newTuner = oldTuner->copyUsed();
+ uint numSettings = oldTuner->getSize();
+ double factor = 0.3;//Adjust this factor...
+ uint settingsToMutate = (uint)(factor * (((double)numSettings) * (budget - k)) / (budget));
if (settingsToMutate < 1)
- settingsToMutate=1;
+ settingsToMutate = 1;
model_print("Mutating %u settings\n", settingsToMutate);
- while(settingsToMutate-- != 0) {
+ while (settingsToMutate-- != 0) {
newTuner->randomMutate();
}
return newTuner;
void AutoTuner::tune() {
- SearchTuner * bestTuner = NULL;
- double bestScore=DBL_MAX;
+ SearchTuner *bestTuner = NULL;
+ double bestScore = DBL_MAX;
- SearchTuner * oldTuner=new SearchTuner();
- double base_temperature=evaluateAll(oldTuner);
- double oldScore=base_temperature;
+ SearchTuner *oldTuner = new SearchTuner();
+ double base_temperature = evaluateAll(oldTuner);
+ double oldScore = base_temperature;
- for (uint i=0;i<budget;i++) {
- SearchTuner *newTuner=mutateTuner(oldTuner, i);
- double newScore=evaluateAll(newTuner);
+ for (uint i = 0; i < budget; i++) {
+ SearchTuner *newTuner = mutateTuner(oldTuner, i);
+ double newScore = evaluateAll(newTuner);
newTuner->printUsed();
model_print("Received score %f\n", newScore);
- double scoreDiff=newScore - oldScore; //smaller is better
+ double scoreDiff = newScore - oldScore; //smaller is better
if (newScore < bestScore) {
if (bestTuner != NULL)
delete bestTuner;
if (scoreDiff < 0) {
acceptanceP = 1;
} else {
- double currTemp=base_temperature * (((double)budget - i) / budget);
+ double currTemp = base_temperature * (((double)budget - i) / budget);
acceptanceP = exp(-scoreDiff / currTemp);
}
double ran = ((double)random()) / RAND_MAX;
#include "structs.h"
class AutoTuner {
- public:
+public:
AutoTuner(uint budget);
void addProblem(CSolver *solver);
void tune();
CMEMALLOC;
- private:
+private:
long long evaluate(CSolver *problem, SearchTuner *tuner);
double evaluateAll(SearchTuner *tuner);
- SearchTuner * mutateTuner(SearchTuner * oldTuner, uint k);
+ SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
- Vector<CSolver *> solvers;
+ Vector<CSolver *> solvers;
uint budget;
};
#endif
param(_param) {
}
-TunableSetting::TunableSetting(TunableSetting * ts) :
+TunableSetting::TunableSetting(TunableSetting *ts) :
hasVar(ts->hasVar),
type(ts->type),
param(ts->param),
- lowValue(ts->lowValue),
+ lowValue(ts->lowValue),
highValue(ts->highValue),
defaultValue(ts->defaultValue),
selectedValue(ts->selectedValue)
bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
return setting1->hasVar == setting2->hasVar &&
- setting1->type == setting2->type &&
- setting1->param == setting2->param;
+ setting1->type == setting2->type &&
+ setting1->param == setting2->param;
}
SearchTuner::SearchTuner() {
}
-SearchTuner * SearchTuner::copyUsed() {
- SearchTuner * tuner = new SearchTuner();
- SetIteratorTunableSetting *iterator=usedSettings.iterator();
- while(iterator->hasNext()) {
- TunableSetting *setting=iterator->next();
- TunableSetting *copy=new TunableSetting(setting);
+SearchTuner *SearchTuner::copyUsed() {
+ SearchTuner *tuner = new SearchTuner();
+ SetIteratorTunableSetting *iterator = usedSettings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
+ TunableSetting *copy = new TunableSetting(setting);
tuner->settings.add(copy);
}
delete iterator;
}
SearchTuner::~SearchTuner() {
- SetIteratorTunableSetting *iterator=settings.iterator();
- while(iterator->hasNext()) {
- TunableSetting *setting=iterator->next();
+ SetIteratorTunableSetting *iterator = settings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
delete setting;
}
delete iterator;
int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
TunableSetting setting(param);
- TunableSetting * result = usedSettings.get(&setting);
+ TunableSetting *result = usedSettings.get(&setting);
if (result == NULL) {
result = settings.get(&setting);
if ( result == NULL) {
- result=new TunableSetting(param);
- uint value = descriptor->lowValue + (random() % (1+ descriptor->highValue - descriptor->lowValue));
+ result = new TunableSetting(param);
+ uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
settings.add(result);
}
int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
TunableSetting setting(vartype, param);
- TunableSetting * result = usedSettings.get(&setting);
+ TunableSetting *result = usedSettings.get(&setting);
if (result == NULL) {
result = settings.get(&setting);
if ( result == NULL) {
- result=new TunableSetting(vartype, param);
- uint value = descriptor->lowValue + (random() % (1+ descriptor->highValue - descriptor->lowValue));
+ result = new TunableSetting(vartype, param);
+ uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
settings.add(result);
}
}
void SearchTuner::randomMutate() {
- TunableSetting * randomSetting = settings.getRandomElement();
- int range=randomSetting->highValue-randomSetting->lowValue;
- int randomchoice=(random() % range) + randomSetting->lowValue;
+ TunableSetting *randomSetting = settings.getRandomElement();
+ int range = randomSetting->highValue - randomSetting->lowValue;
+ int randomchoice = (random() % range) + randomSetting->lowValue;
if (randomchoice < randomSetting->selectedValue)
randomSetting->selectedValue = randomchoice;
else
}
void SearchTuner::print() {
- SetIteratorTunableSetting *iterator=settings.iterator();
- while(iterator->hasNext()) {
- TunableSetting *setting=iterator->next();
+ SetIteratorTunableSetting *iterator = settings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
setting->print();
}
delete iterator;
}
void SearchTuner::printUsed() {
- SetIteratorTunableSetting *iterator=usedSettings.iterator();
- while(iterator->hasNext()) {
- TunableSetting *setting=iterator->next();
+ SetIteratorTunableSetting *iterator = usedSettings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
setting->print();
}
delete iterator;
#include "structs.h"
class TunableSetting {
- public:
- TunableSetting(VarType type, TunableParam param);
+public:
+ TunableSetting(VarType type, TunableParam param);
TunableSetting(TunableParam param);
- TunableSetting(TunableSetting * ts);
+ TunableSetting(TunableSetting *ts);
void setDecision(int _low, int _high, int _default, int _selection);
void print();
CMEMALLOC;
- private:
+private:
bool hasVar;
VarType type;
TunableParam param;
typedef SetIterator<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> SetIteratorTunableSetting;
class SearchTuner : public Tuner {
- public:
+public:
SearchTuner();
~SearchTuner();
int getTunable(TunableParam param, TunableDesc *descriptor);
int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
- SearchTuner * copyUsed();
+ SearchTuner *copyUsed();
void randomMutate();
uint getSize() { return usedSettings.getSize();}
void print();
void printUsed();
CMEMALLOC;
- private:
+private:
/** Used Settings keeps track of settings that were actually used by
- the example. Mutating settings may cause the Constraint Compiler
- not to query other settings.*/
+ the example. Mutating settings may cause the Constraint Compiler
+ not to query other settings.*/
HashsetTunableSetting usedSettings;
/** Settings contains all settings. */
HashsetTunableSetting settings;
static inline long long getTimeNano() {
struct timespec time;
- clock_gettime(CLOCK_REALTIME, & time);
+ clock_gettime(CLOCK_REALTIME, &time);
return time.tv_sec * 1000000000 + time.tv_nsec;
}
#endif/* __COMMON_H__ */
#include "sattranslator.h"
#include "tunable.h"
#include "polarityassignment.h"
-#include "transformer.h"
+#include "decomposeordertransform.h"
#include "autotuner.h"
#include "astops.h"
#include "structs.h"
#include "orderresolver.h"
+#include "integerencoding.h"
CSolver::CSolver() :
boolTrue(new BooleanConst(true)),
elapsedTime(0)
{
satEncoder = new SATEncoder(this);
- transformer = new Transformer(this);
}
/** This function tears down the solver and the entire AST */
delete boolTrue;
delete boolFalse;
delete satEncoder;
- delete transformer;
}
CSolver *CSolver::clone() {
Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
- Boolean * b = boolMap.get(boolean);
+ Boolean *b = boolMap.get(boolean);
if (b == NULL) {
boolMap.put(boolean, boolean);
allBooleans.push(boolean);
return b->isFalse();
}
-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2) {
- Boolean * array[] = {arg1, arg2};
+Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) {
+ Boolean *array[] = {arg1, arg2};
return applyLogicalOperation(op, array, 2);
}
Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) {
- Boolean * array[] = {arg};
+ Boolean *array[] = {arg};
return applyLogicalOperation(op, array, 1);
}
Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
- Boolean * newarray[asize];
- switch(op) {
+ Boolean *newarray[asize];
+ switch (op) {
case SATC_NOT: {
- if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) {
+ if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) {
return ((BooleanLogic *) array[0])->inputs.get(0);
} else if (array[0]->type == BOOLCONST) {
return array[0]->isTrue() ? boolFalse : boolTrue;
break;
}
case SATC_IFF: {
- for(uint i=0;i<2;i++) {
+ for (uint i = 0; i < 2; i++) {
if (array[i]->type == BOOLCONST) {
if (array[i]->isTrue()) {
- return array[1-i];
+ return array[1 - i];
} else {
- newarray[0]=array[1-i];
+ newarray[0] = array[1 - i];
return applyLogicalOperation(SATC_NOT, newarray, 1);
}
}
break;
}
case SATC_XOR: {
- for(uint i=0;i<2;i++) {
+ for (uint i = 0; i < 2; i++) {
if (array[i]->type == BOOLCONST) {
if (array[i]->isTrue()) {
- newarray[0]=array[1-i];
+ newarray[0] = array[1 - i];
return applyLogicalOperation(SATC_NOT, newarray, 1);
} else
- return array[1-i];
+ return array[1 - i];
}
}
break;
}
case SATC_OR: {
- uint newindex=0;
- for(uint i=0;i<asize;i++) {
- Boolean *b=array[i];
+ uint newindex = 0;
+ for (uint i = 0; i < asize; i++) {
+ Boolean *b = array[i];
if (b->type == BOOLCONST) {
if (b->isTrue())
return boolTrue;
else
continue;
} else
- newarray[newindex++]=b;
+ newarray[newindex++] = b;
}
- if (newindex==0) {
+ if (newindex == 0) {
return boolFalse;
- } else if (newindex==1)
+ } else if (newindex == 1)
return newarray[0];
else if (newindex == 2) {
- bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
- bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
+ bool isNot0 = (newarray[0]->type == BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
+ bool isNot1 = (newarray[1]->type == BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
if (isNot0 != isNot1) {
if (isNot0) {
break;
}
case SATC_AND: {
- uint newindex=0;
- for(uint i=0;i<asize;i++) {
- Boolean *b=array[i];
+ uint newindex = 0;
+ for (uint i = 0; i < asize; i++) {
+ Boolean *b = array[i];
if (b->type == BOOLCONST) {
if (b->isTrue())
continue;
else
return boolFalse;
} else
- newarray[newindex++]=b;
+ newarray[newindex++] = b;
}
- if (newindex==0) {
+ if (newindex == 0) {
return boolTrue;
- } else if(newindex==1) {
+ } else if (newindex == 1) {
return newarray[0];
} else {
array = newarray;
break;
}
}
-
+
ASSERT(asize != 0);
Boolean *boolean = new BooleanLogic(this, op, array, asize);
Boolean *b = boolMap.get(boolean);
if (b == NULL) {
boolMap.put(boolean, boolean);
allBooleans.push(boolean);
- return boolean;
+ return boolean;
} else {
delete boolean;
return b;
tuner = new DefaultTuner();
deleteTuner = true;
}
-
+
long long startTime = getTimeNano();
computePolarities(this);
- transformer->orderAnalysis();
+
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
+
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
+
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
int result = unsat ? IS_UNSAT : satEncoder->solve();
}
HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
- return order->encoding.resolver->resolveOrder(first, second);
+ return order->encoding.resolver->resolveOrder(first, second);
}
long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
void CSolver::autoTune(uint budget) {
- AutoTuner * autotuner=new AutoTuner(budget);
+ AutoTuner *autotuner = new AutoTuner(budget);
autotuner->addProblem(this);
autotuner->tune();
delete autotuner;
Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
-
+
/** This function creates a mutable set. */
MutableSet *createMutableSet(VarType type);
Boolean *getBooleanTrue();
Boolean *getBooleanFalse();
-
+
/** This function creates a boolean variable. */
Boolean *getBooleanVar(VarType type);
Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
- /** This function applies a logical operation to the Booleans in its input. */
+ /** This function applies a logical operation to the Booleans in its input. */
- Boolean *applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2);
+ Boolean *applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2);
/** This function applies a logical operation to the Booleans in its input. */
bool isTrue(Boolean *b);
bool isFalse(Boolean *b);
-
+
void setUnSAT() { unsat = true; }
bool isUnSAT() { return unsat; }
Vector<Order *> *getOrders() { return &allOrders;}
Tuner *getTuner() { return tuner; }
- Transformer* getTransformer() {return transformer;}
-
+
SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
SATEncoder *getSATEncoder() {return satEncoder;}
CSolver *clone();
void autoTune(uint budget);
- void setTransformer(Transformer * _transformer) { transformer = _transformer; }
- void setTuner(Tuner * _tuner) { tuner = _tuner; }
+ void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
long long getSolveTime();
-
+
CMEMALLOC;
private:
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;
- Boolean * boolTrue;
- Boolean * boolFalse;
-
+ Boolean *boolTrue;
+ Boolean *boolFalse;
+
/** These two tables are used for deduplicating entries. */
BooleanMatchMap boolMap;
ElementMatchMap elemMap;
-
+
SATEncoder *satEncoder;
bool unsat;
Tuner *tuner;
- Transformer* transformer;
long long elapsedTime;
};
#endif
projects / satune.git / commitdiff