#include "ops.h"
class ASTNode {
- public:
- ASTNode(ASTNodeType _type) : type(_type) {}
+public:
+ ASTNode(ASTNodeType _type) : type(_type) {}
ASTNodeType type;
MEMALLOC;
};
Boolean(LOGICOP),
op(_op),
inputs(array, asize) {
- solver->allBooleans.push(this);
}
BooleanPredicate::~BooleanPredicate() {
#define GETBOOLEANVALUE(b) (b->boolVal)
class Boolean : public ASTNode {
- public:
+public:
Boolean(ASTNodeType _type);
virtual ~Boolean() {}
Polarity polarity;
};
class BooleanVar : public Boolean {
- public:
+public:
BooleanVar(VarType t);
VarType vtype;
Edge var;
};
class BooleanOrder : public Boolean {
- public:
+public:
BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
Order *order;
uint64_t first;
};
class BooleanPredicate : public Boolean {
- public:
+public:
BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus);
~BooleanPredicate();
Predicate *predicate;
FunctionEncoding encoding;
Array<Element *> inputs;
Boolean *undefStatus;
- FunctionEncoding * getFunctionEncoding() {return &encoding;}
+ FunctionEncoding *getFunctionEncoding() {return &encoding;}
MEMALLOC;
};
class BooleanLogic : public Boolean {
- public:
+public:
BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize);
LogicOp op;
Array<Boolean *> inputs;
}
ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) {
- uint64_t array[]={value};
+ uint64_t array[] = {value};
set = new Set(_type, array, 1);
}
#define GETELEMENTTYPE(o) (o->type)
#define GETELEMENTPARENTS(o) (&((Element *)o)->parents)
class Element : public ASTNode {
- public:
+public:
Element(ASTNodeType type);
virtual ~Element();
Vector<ASTNode *> parents;
};
class ElementConst : public Element {
- public:
+public:
ElementConst(uint64_t value, VarType type);
~ElementConst();
Set *set;
};
class ElementSet : public Element {
- public:
+public:
ElementSet(Set *s);
Set *set;
MEMALLOC;
};
class ElementFunction : public Element {
- public:
+public:
ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
~ElementFunction();
Function *function;
#define GETFUNCTIONTYPE(o) (((Function *)o)->type)
class Function {
- public:
- Function(FunctionType _type) : type(_type) {}
+public:
+ Function(FunctionType _type) : type(_type) {}
FunctionType type;
MEMALLOC;
virtual ~Function() {}
};
class FunctionOperator : public Function {
- public:
+public:
ArithOp op;
Array<Set *> domains;
Set *range;
};
class FunctionTable : public Function {
- public:
+public:
Table *table;
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
#include "set.h"
class MutableSet : public Set {
- public:
+public:
MutableSet(VarType t);
void addElementMSet(uint64_t element);
MEMALLOC;
delete elementTable;
}
if (graph != NULL) {
- deleteOrderGraph(graph);
+ delete graph;
}
}
#include "orderpair.h"
class Order {
- public:
+public:
Order(OrderType type, Set *set);
~Order();
OrderType type;
Set *set;
HashTableOrderPair *orderPairTable;
- HashSetOrderElement* elementTable;
+ HashSetOrderElement *elementTable;
OrderGraph *graph;
Vector<BooleanOrder *> constraints;
OrderEncoding order;
#include "set.h"
#include "table.h"
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED) , op(_op), domains(domain, numDomain) {
+PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) {
}
PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
#define GETPREDICATETYPE(o) (((Predicate *)(o))->type)
class Predicate {
- public:
- Predicate(PredicateType _type) : type(_type) {}
+public:
+ Predicate(PredicateType _type) : type(_type) {}
virtual ~Predicate() {}
PredicateType type;
MEMALLOC;
};
class PredicateOperator : public Predicate {
- public:
+public:
PredicateOperator(CompOp op, Set **domain, uint numDomain);
bool evalPredicateOperator(uint64_t *inputs);
CompOp op;
};
class PredicateTable : public Predicate {
- public:
+public:
PredicateTable(Table *table, UndefinedBehavior undefBehavior);
Table *table;
UndefinedBehavior undefinedbehavior;
#include "boolean.h"
#include "csolver.h"
-void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) {
- if (This->constraints.contains(bexpr)) {
- This->constraints.remove(bexpr);
+void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
+ if (constraints.contains(bexpr)) {
+ constraints.remove(bexpr);
}
uint size = bexpr->parents.getSize();
BooleanLogic *logicop = (BooleanLogic *) parent;
switch (logicop->op) {
case L_AND:
- handleANDTrue(This, logicop, bexpr);
+ handleANDTrue(logicop, bexpr);
break;
case L_OR:
- replaceBooleanWithTrue(This, parent);
+ replaceBooleanWithTrue(parent);
break;
case L_NOT:
- replaceBooleanWithFalse(This, parent);
+ replaceBooleanWithFalse(parent);
break;
case L_XOR:
handleXORTrue(logicop, bexpr);
break;
case L_IMPLIES:
- handleIMPLIESTrue(This, logicop, bexpr);
+ handleIMPLIESTrue(logicop, bexpr);
break;
}
}
}
-void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) {
- if (This->constraints.contains(oldb)) {
- This->constraints.remove(oldb);
- This->constraints.add(newb);
+void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
+ if (constraints.contains(oldb)) {
+ constraints.remove(oldb);
+ constraints.add(newb);
}
uint size = oldb->parents.getSize();
bexpr->op = L_NOT;
}
-void handleXORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
uint size = bexpr->inputs.getSize();
Boolean *b = bexpr->inputs.get(0);
uint otherindex = (b == child) ? 1 : 0;
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(otherindex));
+ replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
}
-void handleIMPLIESTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
uint size = bexpr->inputs.getSize();
Boolean *b = bexpr->inputs.get(0);
if (b == child) {
//Replace with other term
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(1));
+ replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
} else {
//Statement is true...
- replaceBooleanWithTrue(This, (Boolean *)bexpr);
+ replaceBooleanWithTrue(bexpr);
}
}
-void handleIMPLIESFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
uint size = bexpr->inputs.getSize();
Boolean *b = bexpr->inputs.get(0);
if (b == child) {
//Statement is true...
- replaceBooleanWithTrue(This, (Boolean *)bexpr);
+ replaceBooleanWithTrue(bexpr);
} else {
//Make into negation of first term
bexpr->inputs.get(1);
}
}
-void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
uint size = bexpr->inputs.getSize();
if (size == 1) {
- replaceBooleanWithTrue(This, (Boolean *)bexpr);
+ replaceBooleanWithTrue(bexpr);
return;
}
}
if (size == 2) {
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(0));
+ replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
}
}
-void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
uint size = bexpr->inputs.getSize();
if (size == 1) {
- replaceBooleanWithFalse(This, (Boolean *) bexpr);
+ replaceBooleanWithFalse(bexpr);
}
for (uint i = 0; i < size; i++) {
}
if (size == 2) {
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(0));
+ replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
}
}
-void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr) {
- if (This->constraints.contains(bexpr)) {
- This->unsat=true;
- This->constraints.remove(bexpr);
+void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
+ if (constraints.contains(bexpr)) {
+ setUnSAT();
+ constraints.remove(bexpr);
}
-
+
uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
Boolean *parent = bexpr->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
switch (logicop->op) {
case L_AND:
- replaceBooleanWithFalse(This, parent);
+ replaceBooleanWithFalse(parent);
break;
case L_OR:
- handleORFalse(This, logicop, bexpr);
+ handleORFalse(logicop, bexpr);
break;
case L_NOT:
- replaceBooleanWithTrue(This, parent);
+ replaceBooleanWithTrue(parent);
break;
case L_XOR:
- handleXORFalse(This, logicop, bexpr);
+ handleXORFalse(logicop, bexpr);
break;
case L_IMPLIES:
- handleIMPLIESFalse(This, logicop, bexpr);
+ handleIMPLIESFalse(logicop, bexpr);
break;
}
}
#define REWRITER_H
#include "classlist.h"
-void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr);
-void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr);
-void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb);
void handleXORTrue(BooleanLogic *bexpr, Boolean *child);
-void handleXORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleIMPLIESTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleIMPLIESFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child);
-void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child);
#endif
#include "mymemory.h"
class Set {
- public:
+public:
Set(VarType t);
Set(VarType t, uint64_t *elements, uint num);
Set(VarType t, uint64_t lowrange, uint64_t highrange);
bool exists(uint64_t element);
uint getSize();
uint64_t getElement(uint index);
-
+
VarType type;
bool isRange;
uint64_t low;//also used to count unique items
ASSERT(status);
}
-TableEntry * Table::getTableEntry(uint64_t *inputs, uint inputSize) {
+TableEntry *Table::getTableEntry(uint64_t *inputs, uint inputSize) {
TableEntry *temp = allocTableEntry(inputs, inputSize, -1);
TableEntry *result = entries->get(temp);
deleteTableEntry(temp);
#include "structs.h"
class Table {
- public:
+public:
Table(Set **domains, uint numDomain, Set *range);
void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result);
TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
#include "orderedge.h"
#include "ordergraph.h"
-OrderEdge *allocOrderEdge(OrderNode *source, OrderNode *sink) {
- OrderEdge *This = (OrderEdge *) ourmalloc(sizeof(OrderEdge));
- This->source = source;
- This->sink = sink;
- This->polPos = false;
- This->polNeg = false;
- This->mustPos = false;
- This->mustNeg = false;
- This->pseudoPos = false;
- return This;
+OrderEdge::OrderEdge(OrderNode *_source, OrderNode *_sink) {
+ source = _source;
+ sink = _sink;
+ polPos = false;
+ polNeg = false;
+ mustPos = false;
+ mustNeg = false;
+ pseudoPos = false;
}
-
-void deleteOrderEdge(OrderEdge *This) {
- ourfree(This);
-}
-
#include "classlist.h"
#include "mymemory.h"
-struct OrderEdge {
+class OrderEdge {
+public:
+ OrderEdge(OrderNode *begin, OrderNode *end);
+
OrderNode *source;
OrderNode *sink;
unsigned int polPos : 1;
unsigned int mustPos : 1;
unsigned int mustNeg : 1;
unsigned int pseudoPos : 1;
+ MEMALLOC;
};
-OrderEdge *allocOrderEdge(OrderNode *begin, OrderNode *end);
-void deleteOrderEdge(OrderEdge *This);
-void setPseudoPos(OrderGraph *graph, OrderEdge *edge);
-void setMustPos(OrderGraph *graph, OrderEdge *edge);
-void setMustNeg(OrderGraph *graph, OrderEdge *edge);
-void setPolPos(OrderGraph *graph, OrderEdge *edge);
-void setPolNeg(OrderGraph *graph, OrderEdge *edge);
-
#endif/* ORDEREDGE_H */
#include "tunable.h"
void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
- HSIteratorOrderNode *iterator = graph->nodes->iterator();
+ HSIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
if (node->status == NOTVISITED) {
}
void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
- HSIteratorOrderEdge *iterator = isReverse ? node->inEdges->iterator() : node->outEdges->iterator();
+ HSIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
if (mustvisit) {
if (!edge->mustPos)
continue;
} else
- if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
- continue;
+ if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
+ continue;
OrderNode *child = isReverse ? edge->source : edge->sink;
}
void resetNodeInfoStatusSCC(OrderGraph *graph) {
- HSIteratorOrderNode *iterator = graph->nodes->iterator();
+ HSIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
iterator->next()->status = NOTVISITED;
}
resetNodeInfoStatusSCC(graph);
}
-bool isMustBeTrueNode(OrderNode* node){
- HSIteratorOrderEdge* iterator = node->inEdges->iterator();
- while(iterator->hasNext()){
- OrderEdge* edge = iterator->next();
- if(!edge->mustPos)
+bool isMustBeTrueNode(OrderNode *node) {
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (!edge->mustPos)
return false;
}
delete iterator;
- iterator = node->outEdges->iterator();
- while(iterator->hasNext()){
- OrderEdge* edge = iterator->next();
- if(!edge->mustPos)
+ iterator = node->outEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (!edge->mustPos)
return false;
}
delete iterator;
return true;
}
-void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
- HSIteratorOrderEdge* iterin = node->inEdges->iterator();
- while(iterin->hasNext()){
- OrderEdge* inEdge = iterin->next();
- OrderNode* srcNode = inEdge->source;
- srcNode->outEdges->remove(inEdge);
- HSIteratorOrderEdge* iterout = node->outEdges->iterator();
- while(iterout->hasNext()){
- OrderEdge* outEdge = iterout->next();
- OrderNode* sinkNode = outEdge->sink;
- sinkNode->inEdges->remove(outEdge);
+void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
+ HSIteratorOrderEdge *iterin = node->inEdges.iterator();
+ while (iterin->hasNext()) {
+ OrderEdge *inEdge = iterin->next();
+ OrderNode *srcNode = inEdge->source;
+ srcNode->outEdges.remove(inEdge);
+ HSIteratorOrderEdge *iterout = node->outEdges.iterator();
+ while (iterout->hasNext()) {
+ OrderEdge *outEdge = iterout->next();
+ OrderNode *sinkNode = outEdge->sink;
+ sinkNode->inEdges.remove(outEdge);
//Adding new edge to new sink and src nodes ...
- OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
+ OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
newEdge->mustPos = true;
newEdge->polPos = true;
if (newEdge->mustNeg)
- This->unsat = true;
- srcNode->outEdges->add(newEdge);
- sinkNode->inEdges->add(newEdge);
+ This->setUnSAT();
+ srcNode->outEdges.add(newEdge);
+ sinkNode->inEdges.add(newEdge);
}
delete iterout;
}
}
void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
- HSIteratorOrderNode* iterator = graph->nodes->iterator();
- while(iterator->hasNext()) {
- OrderNode* node = iterator->next();
- if(isMustBeTrueNode(node)){
- bypassMustBeTrueNode(This,graph, node);
+ HSIteratorOrderNode *iterator = graph->getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = iterator->next();
+ if (isMustBeTrueNode(node)) {
+ bypassMustBeTrueNode(This, graph, node);
}
}
delete iterator;
}
/** This function computes a source set for every nodes, the set of
- nodes that can reach that node via pospolarity edges. It then
- looks for negative polarity edges from nodes in the the source set
- to determine whether we need to generate pseudoPos edges. */
+ nodes that can reach that node via pospolarity edges. It then
+ looks for negative polarity edges from nodes in the the source set
+ to determine whether we need to generate pseudoPos edges. */
void completePartialOrderGraph(OrderGraph *graph) {
Vector<OrderNode *> finishNodes;
HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25);
Vector<OrderNode *> sccNodes;
-
+
uint size = finishNodes.getSize();
uint sccNum = 1;
for (int i = size - 1; i >= 0; i--) {
OrderNode *node = finishNodes.get(i);
HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25);
table->put(node, sources);
-
+
if (node->status == NOTVISITED) {
//Need to do reverse traversal here...
node->status = VISITED;
for (uint j = 0; j < rSize; j++) {
OrderNode *rnode = sccNodes.get(j);
//Compute source sets
- HSIteratorOrderEdge *iterator = rnode->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = rnode->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
}
delete iterator;
}
- for (uint j=0; j < rSize; j++) {
+ for (uint j = 0; j < rSize; j++) {
//Copy in set of entire SCC
OrderNode *rnode = sccNodes.get(j);
- HashSetOrderNode * set = (j==0) ? sources : sources->copy();
+ HashSetOrderNode *set = (j == 0) ? sources : sources->copy();
table->put(rnode, set);
//Use source sets to compute pseudoPos edges
- HSIteratorOrderEdge *iterator = node->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
ASSERT(parent != rnode);
if (edge->polNeg && parent->sccNum != rnode->sccNum &&
sources->contains(parent)) {
- OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
+ OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
newedge->pseudoPos = true;
}
}
delete iterator;
}
-
+
sccNodes.clear();
}
}
}
void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
- HSIteratorOrderNode *iterator = graph->nodes->iterator();
+ HSIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
if (node->status == NOTVISITED) {
{
//Compute source sets
- HSIteratorOrderEdge *iterator = node->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
HSIteratorOrderNode *srciterator = sources->iterator();
while (srciterator->hasNext()) {
OrderNode *srcnode = srciterator->next();
- OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
+ OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
newedge->mustPos = true;
newedge->polPos = true;
if (newedge->mustNeg)
- solver->unsat = true;
- srcnode->outEdges->add(newedge);
- node->inEdges->add(newedge);
+ solver->setUnSAT();
+ srcnode->outEdges.add(newedge);
+ node->inEdges.add(newedge);
}
delete srciterator;
}
{
//Use source sets to compute mustPos edges
- HSIteratorOrderEdge *iterator =node->inEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
edge->mustPos = true;
edge->polPos = true;
if (edge->mustNeg)
- solver->unsat = true;
+ solver->setUnSAT();
}
}
delete iterator;
}
{
//Use source sets to compute mustNeg for edges that would introduce cycle if true
- HSIteratorOrderEdge *iterator = node->outEdges->iterator();
+ HSIteratorOrderEdge *iterator = node->outEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *child = edge->sink;
edge->mustNeg = true;
edge->polNeg = true;
if (edge->mustPos)
- solver->unsat = true;
+ solver->setUnSAT();
}
}
delete iterator;
must be true because of transitivity from other must be true
edges. */
-void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
+void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
Vector<OrderNode *> finishNodes;
//Topologically sort the mustPos edge graph
DFSMust(graph, &finishNodes);
had one). */
void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
- HSIteratorOrderEdge *iterator = graph->edges->iterator();
+ HSIteratorOrderEdge *iterator = graph->getEdges();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
if (edge->mustPos) {
- OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+ OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
if (invEdge != NULL) {
if (!invEdge->mustPos) {
invEdge->polPos = false;
} else {
- solver->unsat = true;
+ solver->setUnSAT();
}
invEdge->mustNeg = true;
invEdge->polNeg = true;
polarity. */
void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
- HSIteratorOrderEdge *iterator = graph->edges->iterator();
+ HSIteratorOrderEdge *iterator = graph->getEdges();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
if (edge->mustPos) {
if (!edge->mustNeg) {
edge->polNeg = false;
} else
- solver->unsat = true;
+ solver->setUnSAT();
- OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+ OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
if (invEdge != NULL) {
if (!invEdge->mustPos)
invEdge->polPos = false;
else
- solver->unsat = true;
+ solver->setUnSAT();
+
invEdge->mustNeg = true;
invEdge->polNeg = true;
}
void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void completePartialOrderGraph(OrderGraph *graph);
void resetNodeInfoStatusSCC(OrderGraph *graph);
-bool isMustBeTrueNode(OrderNode* node);
-void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node);
+bool isMustBeTrueNode(OrderNode *node);
+void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node);
void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
void completePartialOrderGraph(OrderGraph *graph);
void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
#include "ordergraph.h"
#include "order.h"
-OrderGraph *allocOrderGraph(Order *order) {
- OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
- This->nodes = new HashSetOrderNode();
- This->edges = new HashSetOrderEdge();
- This->order = order;
- return This;
+OrderGraph::OrderGraph(Order *_order) :
+ nodes(new HashSetOrderNode()),
+ edges(new HashSetOrderEdge()),
+ order(_order) {
}
OrderGraph *buildOrderGraph(Order *order) {
- OrderGraph *orderGraph = allocOrderGraph(order);
+ OrderGraph *orderGraph = new OrderGraph(order);
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
- addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
+ orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
}
return orderGraph;
}
//Builds only the subgraph for the must order graph.
OrderGraph *buildMustOrderGraph(Order *order) {
- OrderGraph *orderGraph = allocOrderGraph(order);
+ OrderGraph *orderGraph = new OrderGraph(order);
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
- addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
+ orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
}
return orderGraph;
}
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
Polarity polarity = constr->polarity;
BooleanValue mustval = constr->boolVal;
- Order *order = graph->order;
switch (polarity) {
case P_BOTHTRUEFALSE:
case P_TRUE: {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
_1to2->mustPos = true;
_1to2->polPos = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
if (constr->polarity == P_TRUE)
break;
}
case P_FALSE: {
if (order->type == TOTAL) {
- OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_2to1->mustPos = true;
_2to1->polPos = true;
- addNewOutgoingEdge(node2, _2to1);
- addNewIncomingEdge(node1, _2to1);
+ node2->addNewOutgoingEdge(_2to1);
+ node1->addNewIncomingEdge(_2to1);
} else {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_1to2->mustNeg = true;
_1to2->polNeg = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
}
break;
}
}
}
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
BooleanValue mustval = constr->boolVal;
- Order *order = graph->order;
switch (mustval) {
case BV_UNSAT:
case BV_MUSTBETRUE: {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
_1to2->mustPos = true;
_1to2->polPos = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
if (constr->boolVal == BV_MUSTBETRUE)
break;
}
case BV_MUSTBEFALSE: {
if (order->type == TOTAL) {
- OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
_2to1->mustPos = true;
_2to1->polPos = true;
- addNewOutgoingEdge(node2, _2to1);
- addNewIncomingEdge(node1, _2to1);
+ node2->addNewOutgoingEdge(_2to1);
+ node1->addNewIncomingEdge(_2to1);
} else {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
_1to2->mustNeg = true;
_1to2->polNeg = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
+ node1->addNewOutgoingEdge(_1to2);
+ node2->addNewIncomingEdge(_1to2);
}
break;
}
}
}
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
- OrderNode *node = allocOrderNode(id);
- OrderNode *tmp = graph->nodes->get(node);
+OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
+ OrderNode *node = new OrderNode(id);
+ OrderNode *tmp = nodes->get(node);
if ( tmp != NULL) {
- deleteOrderNode(node);
+ delete node;
node = tmp;
} else {
- graph->nodes->add(node);
+ nodes->add(node);
}
return node;
}
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
- OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
- OrderNode *tmp = graph->nodes->get(&node);
+OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
+ OrderNode node(id);
+ OrderNode *tmp = nodes->get(&node);
return tmp;
}
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
- OrderEdge *edge = allocOrderEdge(begin, end);
- OrderEdge *tmp = graph->edges->get(edge);
+OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
+ OrderEdge *edge = new OrderEdge(begin, end);
+ OrderEdge *tmp = edges->get(edge);
if ( tmp != NULL ) {
- deleteOrderEdge(edge);
+ delete edge;
edge = tmp;
} else {
- graph->edges->add(edge);
+ edges->add(edge);
}
return edge;
}
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
- OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
- OrderEdge *tmp = graph->edges->get(&edge);
+OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
+ OrderEdge edge(begin, end);
+ OrderEdge *tmp = edges->get(&edge);
return tmp;
}
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
- OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
- OrderEdge *tmp = graph->edges->get(&inverseedge);
+OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
+ OrderEdge inverseedge(edge->sink, edge->source);
+ OrderEdge *tmp = edges->get(&inverseedge);
return tmp;
}
-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
- OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addOrderEdge(graph, from, to, bOrder);
+void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+ addOrderEdge(from, to, bOrder);
}
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
- OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addMustOrderEdge(graph, from, to, bOrder);
+void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+ addMustOrderEdge(from, to, bOrder);
}
-void deleteOrderGraph(OrderGraph *graph) {
- HSIteratorOrderNode *iterator = graph->nodes->iterator();
+OrderGraph::~OrderGraph() {
+ HSIteratorOrderNode *iterator = nodes->iterator();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
- deleteOrderNode(node);
+ delete node;
}
delete iterator;
- HSIteratorOrderEdge *eiterator = graph->edges->iterator();
+ HSIteratorOrderEdge *eiterator = edges->iterator();
while (eiterator->hasNext()) {
OrderEdge *edge = eiterator->next();
- deleteOrderEdge(edge);
+ delete edge;
}
delete eiterator;
- delete graph->nodes;
- delete graph->edges;
- ourfree(graph);
+ delete nodes;
+ delete edges;
}
#include "structs.h"
#include "mymemory.h"
-struct OrderGraph {
+class OrderGraph {
+public:
+ OrderGraph(Order *order);
+ ~OrderGraph();
+ void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+ void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+ OrderNode *getOrderNodeFromOrderGraph(uint64_t id);
+ OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+ OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id);
+ OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+ void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+ void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+ OrderEdge *getInverseOrderEdge(OrderEdge *edge);
+ Order *getOrder() {return order;}
+ HSIteratorOrderNode *getNodes() {return nodes->iterator();}
+ HSIteratorOrderEdge *getEdges() {return edges->iterator();}
+
+ MEMALLOC;
+private:
HashSetOrderNode *nodes;
HashSetOrderEdge *edges;
Order *order;
};
-OrderGraph *allocOrderGraph(Order *order);
OrderGraph *buildOrderGraph(Order *order);
OrderGraph *buildMustOrderGraph(Order *order);
-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void deleteOrderGraph(OrderGraph *graph);
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge);
#endif/* ORDERGRAPH_H */
#include "ordernode.h"
#include "orderedge.h"
-OrderNode *allocOrderNode(uint64_t id) {
- OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode));
- This->id = id;
- This->inEdges = new HashSetOrderEdge();
- This->outEdges = new HashSetOrderEdge();
- This->status = NOTVISITED;
- This->sccNum = 0;
- return This;
+OrderNode::OrderNode(uint64_t _id) :
+ id(_id),
+ status(NOTVISITED),
+ sccNum(0),
+ inEdges(),
+ outEdges() {
}
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge) {
- node->inEdges->add(edge);
+void OrderNode::addNewIncomingEdge(OrderEdge *edge) {
+ inEdges.add(edge);
}
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge) {
- node->outEdges->add(edge);
-}
-
-void deleteOrderNode(OrderNode *node) {
- delete node->inEdges;
- delete node->outEdges;
- ourfree(node);
+void OrderNode::addNewOutgoingEdge(OrderEdge *edge) {
+ outEdges.add(edge);
}
enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
typedef enum NodeStatus NodeStatus;
-struct OrderNode {
+class OrderNode {
+public:
+ OrderNode(uint64_t id);
+ void addNewIncomingEdge(OrderEdge *edge);
+ void addNewOutgoingEdge(OrderEdge *edge);
+
uint64_t id;
- HashSetOrderEdge * inEdges;
- HashSetOrderEdge * outEdges;
NodeStatus status;
uint sccNum;
+ HashSetOrderEdge inEdges;
+ HashSetOrderEdge outEdges;
+ MEMALLOC;
};
-
-OrderNode *allocOrderNode(uint64_t id);
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge);
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge);
-void deleteOrderNode(OrderNode *node);
-
#endif/* ORDERNODE_H */
#include "csolver.h"
void computePolarities(CSolver *This) {
- HSIteratorBoolean *iterator=This->constraints.iterator();
- while(iterator->hasNext()) {
+ HSIteratorBoolean *iterator = This->getConstraints();
+ while (iterator->hasNext()) {
Boolean *boolean = iterator->next();
updatePolarity(boolean, P_TRUE);
updateMustValue(boolean, BV_MUSTBETRUE);
#include "set.h"
-void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
- Order* order = boolOrder->order;
+void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
+ Order *order = boolOrder->order;
if (order->elementTable == NULL) {
order->initializeOrderElementsHashTable();
}
//getting two elements and using LT predicate ...
- ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first);
- ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second);
- Set * sarray[]={elem1->set, elem2->set};
- Predicate *predicate =new PredicateOperator(LT, sarray, 2);
- Element * parray[]={elem1, elem2};
- BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
- {//Adding new elements and boolean/predicate to solver regarding memory management
- This->solver->allBooleans.push(boolean);
- This->solver->allPredicates.push(predicate);
- This->solver->constraints.add(boolean);
- }
- replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
+ ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->first);
+ ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->second);
+ Set *sarray[] = {elem1->set, elem2->set};
+ Predicate *predicate = This->solver->createPredicateOperator(LT, sarray, 2);
+ Element *parray[] = {elem1, elem2};
+ Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2);
+ This->solver->addConstraint(boolean);
+ This->solver->replaceBooleanWithBoolean(boolOrder, boolean);
}
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
- HashSetOrderElement* eset = order->elementTable;
- OrderElement oelement ={item, NULL};
- if( !eset->contains(&oelement)){
- Set* set = new Set(order->set->type, 1, (uint64_t) order->set->getSize());
- Element* elem = new ElementSet(set);
- eset->add(allocOrderElement(item, elem));
- This->solver->allElements.push(elem);
- This->solver->allSets.push(set);
+Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) {
+ HashSetOrderElement *eset = order->elementTable;
+ OrderElement oelement(item, NULL);
+ if ( !eset->contains(&oelement)) {
+ Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
+ Element *elem = This->solver->getElementVar(set);
+ eset->add(new OrderElement(item, elem));
return elem;
} else
return eset->get(&oelement)->elem;
* and open the template in the editor.
*/
-/*
+/*
* File: integerencoding.h
* Author: hamed
*
#include "classlist.h"
#include "structs.h"
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
+Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item);
void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
-#endif /* INTEGERENCODING_H */
+#endif/* INTEGERENCODING_H */
#include "integerencoding.h"
void orderAnalysis(CSolver *This) {
- uint size = This->allOrders.getSize();
+ Vector<Order *> *orders = This->getOrders();
+ uint size = orders->getSize();
for (uint i = 0; i < size; i++) {
- Order *order = This->allOrders.get(i);
- bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
+ Order *order = orders->get(i);
+ bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
if (!doDecompose)
continue;
-
+
OrderGraph *graph = buildOrderGraph(order);
if (order->type == PARTIAL) {
//Required to do SCC analysis for partial order graphs. It
}
- bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
+ bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
if (mustReachGlobal)
reachMustAnalysis(This, graph, false);
- bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
-
+ bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
if (mustReachLocal) {
//This pair of analysis is also optional
if (order->type == PARTIAL) {
}
}
- bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
-
+ bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
if (mustReachPrune)
removeMustBeTrueNodes(This, graph);
-
+
//This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
decomposeOrder(This, order, graph);
- deleteOrderGraph(graph);
-
- bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
- if(!doIntegerEncoding)
- continue;
- uint size = order->constraints.getSize();
- for(uint i=0; i<size; i++){
- orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
- }
+ delete graph;
+
+ /*
+ OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
+
+ bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
+ if(!doIntegerEncoding)
+ continue;
+ uint size = order->constraints.getSize();
+ for(uint i=0; i<size; i++){
+ orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+ }*/
}
}
uint size = order->constraints.getSize();
for (uint i = 0; i < size; i++) {
BooleanOrder *orderconstraint = order->constraints.get(i);
- OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+ OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
+ OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
if (from->sccNum != to->sccNum) {
- OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polPos) {
- replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
+ This->replaceBooleanWithTrue(orderconstraint);
} else if (edge->polNeg) {
- replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
+ This->replaceBooleanWithFalse(orderconstraint);
} else {
//This case should only be possible if constraint isn't in AST
ASSERT(0);
if (ordervec.getSize() > from->sccNum)
neworder = ordervec.get(from->sccNum);
if (neworder == NULL) {
- MutableSet *set = new MutableSet(order->set->type);
- This->allSets.push(set);
- neworder = new Order(order->type, set);
- This->allOrders.push(neworder);
+ MutableSet *set = This->createMutableSet(order->set->type);
+ neworder = This->createOrder(order->type, set);
ordervec.setExpand(from->sccNum, neworder);
if (order->type == PARTIAL)
partialcandidatevec.setExpand(from->sccNum, neworder);
((MutableSet *)neworder->set)->addElementMSet(to->id);
}
if (order->type == PARTIAL) {
- OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polNeg)
partialcandidatevec.setExpand(from->sccNum, NULL);
}
}
}
- uint pcvsize=partialcandidatevec.getSize();
- for(uint i=0;i<pcvsize;i++) {
- Order * neworder=partialcandidatevec.get(i);
- if (neworder != NULL){
+ uint pcvsize = partialcandidatevec.getSize();
+ for (uint i = 0; i < pcvsize; i++) {
+ Order *neworder = partialcandidatevec.get(i);
+ if (neworder != NULL) {
neworder->type = TOTAL;
model_print("i=%u\t", i);
}
* and open the template in the editor.
*/
-/*
+/*
* File: orderdecompose.h
* Author: hamed
*
void orderAnalysis(CSolver *This);
void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
-#endif /* ORDERDECOMPOSE_H */
+#endif/* ORDERDECOMPOSE_H */
return constraintAND(cnf, numvars, array);
}
-Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
- if(numvars == 0 )
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+ if (numvars == 0 )
return E_False;
- Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
+ Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
for (uint i = 1; i < numvars; i++) {
Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
- Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
- result = constraintOR2(cnf, lt, eq);
+ Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+ result = constraintOR2(cnf, lt, eq);
}
return result;
}
-Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
- if(numvars == 0 )
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+ if (numvars == 0 )
return E_True;
- Edge result =constraintIMPLIES(cnf, var1[0], var2[0]);
+ Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
for (uint i = 1; i < numvars; i++) {
Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
- Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
- result = constraintOR2(cnf, lt, eq);
+ Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+ result = constraintOR2(cnf, lt, eq);
}
return result;
}
#include "orderelement.h"
-OrderElement *allocOrderElement(uint64_t item, Element* elem) {
- OrderElement *This = (OrderElement *) ourmalloc(sizeof(OrderElement));
- This->elem = elem;
- This->item = item;
- return This;
-}
-
-void deleteOrderElement(OrderElement *pair) {
- ourfree(pair);
+OrderElement::OrderElement(uint64_t _item, Element *_elem) {
+ elem = _elem;
+ item = _item;
}
#include "mymemory.h"
#include "constraint.h"
-struct OrderElement {
+class OrderElement {
+public:
+ OrderElement(uint64_t item, Element *elem);
uint64_t item;
- Element* elem;
+ Element *elem;
+ MEMALLOC;
};
-OrderElement *allocOrderElement(uint64_t item, Element* elem);
-void deleteOrderElement(OrderElement *pair);
#endif/* ORDERELEMENT_H */
#include "constraint.h"
class OrderPair {
- public:
+public:
OrderPair(uint64_t first, uint64_t second, Edge constraint);
OrderPair();
- uint64_t first;
+ uint64_t first;
uint64_t second;
Edge constraint;
MEMALLOC;
}
void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
- HSIteratorBoolean *iterator=csolver->constraints.iterator();
- while(iterator->hasNext()) {
+ HSIteratorBoolean *iterator = csolver->getConstraints();
+ while (iterator->hasNext()) {
Boolean *constraint = iterator->next();
model_print("Encoding All ...\n\n");
Edge c = encodeConstraintSATEncoder(This, constraint);
model_print("Returned Constraint in EncodingAll:\n");
- ASSERT( ! equalsEdge(c, E_BOGUS));
+ ASSERT( !equalsEdge(c, E_BOGUS));
addConstraintCNF(This->cnf, c);
}
delete iterator;
while (notfinished) {
Edge carray[numDomains];
- if (predicate->evalPredicateOperator(vals) ^ generateNegation) {
+ if (predicate->evalPredicateOperator(vals) != generateNegation) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
Element *elem = constraint->inputs.get(i);
ASSERT(ee0->numVars == ee1->numVars);
uint numVars = ee0->numVars;
switch (predicate->op) {
- case EQUALS:
- return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
- case LT:
- return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
- case GT:
- return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
- default:
- ASSERT(0);
+ case EQUALS:
+ return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+ case LT:
+ return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+ case GT:
+ return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
+ default:
+ ASSERT(0);
}
exit(-1);
}
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
Table *table = ((PredicateTable *)constraint->predicate)->table;
FunctionEncodingType encType = constraint->encoding.type;
- Array<Element*> * inputs = &constraint->inputs;
+ Array<Element *> *inputs = &constraint->inputs;
uint inputNum = inputs->getSize();
uint size = table->entries->getSize();
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
switch ( constraint->order->type) {
- case PARTIAL:
- return encodePartialOrderSATEncoder(This, constraint);
- case TOTAL:
- return encodeTotalOrderSATEncoder(This, constraint);
- default:
- ASSERT(0);
+ case PARTIAL:
+ return encodePartialOrderSATEncoder(This, constraint);
+ case TOTAL:
+ return encodeTotalOrderSATEncoder(This, constraint);
+ default:
+ ASSERT(0);
}
return E_BOGUS;
}
-Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
+Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
if (order->graph != NULL) {
- OrderGraph *graph=order->graph;
- OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
- OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
+ OrderGraph *graph = order->graph;
+ OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
+ OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second);
if ((first != NULL) && (second != NULL)) {
- OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+ OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second);
if (edge != NULL) {
if (edge->mustPos)
return E_True;
else if (edge->mustNeg)
return E_False;
}
- OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+ OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
if (invedge != NULL) {
if (invedge->mustPos)
return E_False;
Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
- if(!edgeIsNull(gvalue))
+ if (!edgeIsNull(gvalue))
return gvalue;
-
+
HashTableOrderPair *table = order->orderPairTable;
bool negate = false;
OrderPair flipped;
table->put(paircopy, paircopy);
} else
constraint = table->get(pair)->constraint;
-
+
return negate ? constraintNegate(constraint) : constraint;
}
ASSERT(boolOrder->order->type == TOTAL);
if (boolOrder->order->orderPairTable == NULL) {
boolOrder->order->initializeOrderHashTable();
- bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+ bool doOptOrderStructure = GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
if (doOptOrderStructure) {
boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
reachMustAnalysis(This->solver, boolOrder->order->graph, true);
#define SATORDERENCODER_H
Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second);
+Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
uint index = 0;
for (int i = elemEnc->numVars - 1; i >= 0; i--) {
index = index << 1;
- if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
+ if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
index |= 1;
}
- model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, elemEnc->isinUseElement(index));
- ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
+ if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
+ model_print("WARNING: Element has undefined value!\n");
return elemEnc->encodingArray[index];
}
uint64_t value = 0;
for (int i = elemEnc->numVars - 1; i >= 0; i--) {
value = value << 1;
- if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
+ if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
value |= 1;
}
if (elemEnc->isBinaryValSigned &&
- This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
+ This->getSATEncoder()->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
//Do sign extension of negative number
uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
value += highbits;
uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
uint index = 0;
for (uint i = 0; i < elemEnc->numVars; i++) {
- if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
+ if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
index = i;
}
ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
uint i;
for (i = 0; i < elemEnc->numVars; i++) {
- if (!getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+ if (!getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
break;
}
}
bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
int index = getEdgeVar( ((BooleanVar *) boolean)->var );
- return getValueSolver(This->satEncoder->cnf->solver, index);
+ return getValueSolver(This->getSATEncoder()->cnf->solver, index);
}
HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
Edge var = getOrderConstraint(order->orderPairTable, &pair);
if (edgeIsNull(var))
return UNORDERED;
- return getValueCNF(This->satEncoder->cnf, var) ? FIRST : SECOND;
+ return getValueCNF(This->getSATEncoder()->cnf, var) ? FIRST : SECOND;
}
bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean);
HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second);
/**
- * most significant bit is represented by variable index 0
+ * most significant bit is represented by variable index 0
*/
uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc);
uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc);
template<typename type>
class Array {
- public:
- Array(uint _size) :
- array((type *)ourcalloc(1, sizeof(type) * _size)),
+public:
+ Array(uint _size) :
+ array((type *)ourcalloc(1, sizeof(type) * _size)),
size(_size)
- {
- }
-
- Array(type * _array, uint _size) :
- array((type *)ourcalloc(1, sizeof(type) * _size)),
+ {
+ }
+
+ Array(type *_array, uint _size) :
+ array((type *)ourcalloc(1, sizeof(type) * _size)),
size(_size) {
- memcpy(array, _array, _size * sizeof(type));
- }
-
- ~Array() {
- ourfree(array);
- }
-
- void remove(uint index) {
- size--;
- for (; index < size; index++) {
- array[index] = array[index + 1];
- }
- }
-
- type get(uint index) {
- return array[index];
- }
-
- void set(uint index, type item) {
- array[index] = item;
- }
-
- uint getSize() {
- return size;
- }
-
- type *expose() {
- return array;
- }
-
- private:
- type *array;
- uint size;
+ memcpy(array, _array, _size * sizeof(type));
+ }
+
+ ~Array() {
+ ourfree(array);
+ }
+
+ void remove(uint index) {
+ size--;
+ for (; index < size; index++) {
+ array[index] = array[index + 1];
+ }
+ }
+
+ type get(uint index) {
+ return array[index];
+ }
+
+ void set(uint index, type item) {
+ array[index] = item;
+ }
+
+ uint getSize() {
+ return size;
+ }
+
+ type *expose() {
+ return array;
+ }
+
+private:
+ type *array;
+ uint size;
};
template<typename type>
class Vector {
- public:
- Vector(uint _capacity = VECTOR_DEFCAP) :
- size(0),
+public:
+ Vector(uint _capacity = VECTOR_DEFCAP) :
+ size(0),
capacity(_capacity),
array((type *) ourmalloc(sizeof(type) * _capacity)) {
- }
+ }
- Vector(uint _capacity, type * _array) :
- size(_capacity),
+ Vector(uint _capacity, type *_array) :
+ size(_capacity),
capacity(_capacity),
array((type *) ourmalloc(sizeof(type) * _capacity)) {
- memcpy(array, _array, capacity * sizeof(type));
+ memcpy(array, _array, capacity * sizeof(type));
}
-
+
void pop() {
size--;
- }
+ }
type last() {
- return array[size - 1];
+ return array[size - 1];
}
-
- void setSize(uint _size) {
- if (_size <= size) {
- size = _size;
- return;
- } else if (_size > capacity) {
- array = (type *)ourrealloc(array, _size * sizeof(type));
- capacity = _size;
- }
- bzero(&array[size], (_size - size) * sizeof(type));
+
+ void setSize(uint _size) {
+ if (_size <= size) {
+ size = _size;
+ return;
+ } else if (_size > capacity) {
+ array = (type *)ourrealloc(array, _size * sizeof(type));
+ capacity = _size;
+ }
+ bzero(&array[size], (_size - size) * sizeof(type));
size = _size;
- }
+ }
- void push(type item) {
- if (size >= capacity) {
- uint newcap = capacity << 1;
- array = (type *)ourrealloc(array, newcap * sizeof(type));
- capacity = newcap;
- }
- array[size++] = item;
+ void push(type item) {
+ if (size >= capacity) {
+ uint newcap = capacity << 1;
+ array = (type *)ourrealloc(array, newcap * sizeof(type));
+ capacity = newcap;
+ }
+ array[size++] = item;
}
-
- type get(uint index) {
- return array[index];
+
+ type get(uint index) {
+ return array[index];
}
-
- void setExpand(uint index, type item) {
- if (index >= size)
- setSize(index + 1);
- set(index, item);
+
+ void setExpand(uint index, type item) {
+ if (index >= size)
+ setSize(index + 1);
+ set(index, item);
}
-
- void set(uint index, type item) {
- array[index] = item;
+
+ void set(uint index, type item) {
+ array[index] = item;
}
-
+
uint getSize() {
- return size;
+ return size;
}
-
+
~Vector() {
- ourfree(array);
+ ourfree(array);
}
-
+
void clear() {
- size = 0;
+ size = 0;
}
-
+
type *expose() {
- return array;
- }
-
- private:
+ return array;
+ }
+
+private:
uint size;
uint capacity;
type *array;
template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
class HSIterator {
public:
- HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * _set) :
+ HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> *_set) :
curr(_curr),
set(_set)
{
}
/** Override: new operator */
- void * operator new(size_t size) {
+ void *operator new(size_t size) {
return ourmalloc(size);
}
}
/** Override: new[] operator */
- void * operator new[](size_t size) {
+ void *operator new[](size_t size) {
return ourmalloc(size);
}
}
bool hasNext() {
- return curr!=NULL;
+ return curr != NULL;
}
_Key next() {
- _Key k=curr->key;
- last=curr;
- curr=curr->next;
+ _Key k = curr->key;
+ last = curr;
+ curr = curr->next;
return k;
}
}
void remove() {
- _Key k=last->key;
+ _Key k = last->key;
set->remove(k);
}
private:
LinkNode<_Key> *curr;
LinkNode<_Key> *last;
- HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * set;
+ HashSet <_Key, _KeyInt, _Shift, hash_function, equals> *set;
};
template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
/** @brief Hashset destructor */
~HashSet() {
- LinkNode<_Key> *tmp=list;
- while(tmp!=NULL) {
- LinkNode<_Key> *tmpnext=tmp->next;
+ LinkNode<_Key> *tmp = list;
+ while (tmp != NULL) {
+ LinkNode<_Key> *tmpnext = tmp->next;
ourfree(tmp);
- tmp=tmpnext;
+ tmp = tmpnext;
}
delete table;
}
- HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * copy() {
- HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
- HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator();
- while(it->hasNext())
+ HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy() {
+ HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy = new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
+ HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *it = iterator();
+ while (it->hasNext())
copy->add(it->next());
delete it;
return copy;
}
void reset() {
- LinkNode<_Key> *tmp=list;
- while(tmp!=NULL) {
- LinkNode<_Key> *tmpnext=tmp->next;
+ LinkNode<_Key> *tmp = list;
+ while (tmp != NULL) {
+ LinkNode<_Key> *tmpnext = tmp->next;
ourfree(tmp);
- tmp=tmpnext;
+ tmp = tmpnext;
}
- list=tail=NULL;
+ list = tail = NULL;
table->reset();
}
/** @brief Adds a new key to the hashset. Returns false if the key
* is already present. */
- void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) {
- HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator();
- while(it->hasNext())
+ void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *table) {
+ HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *it = iterator();
+ while (it->hasNext())
add(it->next());
delete it;
}
* is already present. */
bool add(_Key key) {
- LinkNode<_Key> * val=table->get(key);
- if (val==NULL) {
- LinkNode<_Key> * newnode=(LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>));
- newnode->prev=tail;
- newnode->next=NULL;
- newnode->key=key;
- if (tail!=NULL)
- tail->next=newnode;
+ LinkNode<_Key> *val = table->get(key);
+ if (val == NULL) {
+ LinkNode<_Key> *newnode = (LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>));
+ newnode->prev = tail;
+ newnode->next = NULL;
+ newnode->key = key;
+ if (tail != NULL)
+ tail->next = newnode;
else
- list=newnode;
- tail=newnode;
+ list = newnode;
+ tail = newnode;
table->put(key, newnode);
return true;
} else
* hashset. Returns NULL if not present. */
_Key get(_Key key) {
- LinkNode<_Key> * val=table->get(key);
- if (val!=NULL)
+ LinkNode<_Key> *val = table->get(key);
+ if (val != NULL)
return val->key;
else
return NULL;
}
bool contains(_Key key) {
- return table->get(key)!=NULL;
+ return table->get(key) != NULL;
}
bool remove(_Key key) {
- LinkNode<_Key> * oldlinknode;
- oldlinknode=table->get(key);
- if (oldlinknode==NULL) {
+ LinkNode<_Key> *oldlinknode;
+ oldlinknode = table->get(key);
+ if (oldlinknode == NULL) {
return false;
}
table->remove(key);
//remove link node from the list
- if (oldlinknode->prev==NULL)
- list=oldlinknode->next;
+ if (oldlinknode->prev == NULL)
+ list = oldlinknode->next;
else
- oldlinknode->prev->next=oldlinknode->next;
- if (oldlinknode->next!=NULL)
- oldlinknode->next->prev=oldlinknode->prev;
+ oldlinknode->prev->next = oldlinknode->next;
+ if (oldlinknode->next != NULL)
+ oldlinknode->next->prev = oldlinknode->prev;
else
- tail=oldlinknode->prev;
+ tail = oldlinknode->prev;
ourfree(oldlinknode);
return true;
}
}
bool isEmpty() {
- return getSize()==0;
+ return getSize() == 0;
}
- HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * iterator() {
+ HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *iterator() {
return new HSIterator<_Key, _KeyInt, _Shift, hash_function, equals>(list, this);
}
/** Override: new operator */
- void * operator new(size_t size) {
+ void *operator new(size_t size) {
return ourmalloc(size);
}
}
/** Override: new[] operator */
- void * operator new[](size_t size) {
+ void *operator new[](size_t size) {
return ourmalloc(size);
}
ourfree(p);
}
private:
- HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, hash_function, equals> * table;
+ HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, hash_function, equals> *table;
LinkNode<_Key> *list;
LinkNode<_Key> *tail;
};
}
/** Override: new operator */
- void * operator new(size_t size) {
+ void *operator new(size_t size) {
return ourmalloc(size);
}
}
/** Override: new[] operator */
- void * operator new[](size_t size) {
+ void *operator new[](size_t size) {
return ourmalloc(size);
}
}
void resetanddelete() {
- for(unsigned int i=0;i<capacity;i++) {
+ for (unsigned int i = 0; i < capacity; i++) {
struct hashlistnode<_Key, _Val> *bin = &table[i];
if (bin->key != NULL) {
bin->key = NULL;
}
void resetandfree() {
- for(unsigned int i=0;i<capacity;i++) {
+ for (unsigned int i = 0; i < capacity; i++) {
struct hashlistnode<_Key, _Val> *bin = &table[i];
if (bin->key != NULL) {
bin->key = NULL;
/* HashTable cannot handle 0 as a key */
if (!key) {
if (!zero) {
- zero=(struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>));
+ zero = (struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>));
size++;
}
- zero->key=key;
- zero->val=val;
+ zero->key = key;
+ zero->val = val;
return;
}
}
unsigned int oindex = hash_function(key) & capacitymask;
- unsigned int index=oindex;
+ unsigned int index = oindex;
do {
search = &table[index];
if (!search->key) {
return search->val;
index++;
index &= capacitymask;
- if (index==oindex)
+ if (index == oindex)
break;
} while (true);
return (_Val)0;
if (!zero) {
return (_Val)0;
} else {
- _Val v=zero->val;
+ _Val v = zero->val;
ourfree(zero);
- zero=NULL;
+ zero = NULL;
size--;
return v;
}
break;
} else
if (equals(search->key, key)) {
- _Val v=search->val;
+ _Val v = search->val;
//empty out this bin
- search->val=(_Val) 1;
- search->key=0;
+ search->val = (_Val) 1;
+ search->key = 0;
size--;
return v;
}
/* HashTable cannot handle 0 as a key */
if (!key) {
- return zero!=NULL;
+ return zero != NULL;
}
unsigned int index = hash_function(key);
struct hashlistnode<_Key, _Val> *bin = &oldtable[0];
struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity];
- for (;bin < lastbin;bin++) {
+ for (; bin < lastbin; bin++) {
_Key key = bin->key;
struct hashlistnode<_Key, _Val> *search;
return key1->sink == key2->sink && key1->source == key2->source;
}
-unsigned int order_element_hash_function(OrderElement* This) {
+unsigned int order_element_hash_function(OrderElement *This) {
return (uint)This->item;
}
-bool order_element_equals(OrderElement* key1, OrderElement* key2) {
+bool order_element_equals(OrderElement *key1, OrderElement *key2) {
return key1->item == key2->item;
}
bool order_node_equals(OrderNode *key1, OrderNode *key2);
unsigned int order_edge_hash_function(OrderEdge *This);
bool order_edge_equals(OrderEdge *key1, OrderEdge *key2);
-unsigned int order_element_hash_function(OrderElement* This);
-bool order_element_equals(OrderElement* key1, OrderElement* key2);
+unsigned int order_element_hash_function(OrderElement *This);
+bool order_element_equals(OrderElement *key1, OrderElement *key2);
unsigned int order_pair_hash_function(OrderPair *This);
bool order_pair_equals(OrderPair *key1, OrderPair *key2);
typedef enum ElementEncodingType ElementEncodingType;
class ElementEncoding {
- public:
+public:
ElementEncoding(Element *element);
ElementEncodingType getElementEncodingType() {return type;}
~ElementEncoding();
return -1;
}
-
+
ElementEncodingType type;
Element *element;
Edge *variables;/* List Variables Used To Encode Element */
typedef union ElementPredicate ElementPredicate;
class FunctionEncoding {
- public:
+public:
FunctionEncodingType type;
bool isFunction;//true for function, false for predicate
ElementPredicate op;
#include <strings.h>
void naiveEncodingDecision(CSolver *This) {
- HSIteratorBoolean *iterator=This->constraints.iterator();
- while(iterator->hasNext()) {
+ HSIteratorBoolean *iterator = This->getConstraints();
+ while (iterator->hasNext()) {
Boolean *boolean = iterator->next();
naiveEncodingConstraint(boolean);
}
typedef enum OrderEncodingType OrderEncodingType;
class OrderEncoding {
- public:
+public:
OrderEncoding(Order *order);
OrderEncodingType type;
Boolean *b3 = solver->getBooleanVar(0);
Boolean *b4 = solver->getBooleanVar(0);
//L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
- Boolean * barray1[]={b1,b2};
+ Boolean *barray1[] = {b1,b2};
Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2);
- Boolean * barray2[]={andb1b2, b3};
+ Boolean *barray2[] = {andb1b2, b3};
Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2);
solver->addConstraint(imply);
- Boolean * barray3[] ={b3};
+ Boolean *barray3[] = {b3};
Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1);
- Boolean * barray4[] ={notb3, b4};
+ Boolean *barray4[] = {notb3, b4};
solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2));
- Boolean * barray5[] ={b1, b4};
+ Boolean *barray5[] = {b1, b4};
solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2));
if (solver->startEncoding() == 1)
printf("b1=%d b2=%d b3=%d b4=%d\n",
CSolver *solver = new CSolver();
uint64_t set1[] = {5};
uint64_t set3[] = {1, 3, 4, 6};
- Set *s1 = solver->createSet(0, set1, 3);
+ Set *s1 = solver->createSet(0, set1, 1);
Set *s3 = solver->createSet(0, set3, 4);
Element *e1 = solver->getElementConst(4, 5);
Element *e2 = solver->getElementVar(s3);
Boolean *o81 = solver->orderConstraint(order, 8, 1);
/* Not Valid c++...Let Hamed fix...
- addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
- Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
- Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
- Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
- Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
- addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
- addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
- addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
- Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
- Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
- addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
- addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
-
- if (solver->startEncoding() == 1)
- printf("SAT\n");
- else
- printf("UNSAT\n");
- */
+ addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
+ Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
+ Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
+ Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
+ Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
+ addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
+ addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
+ addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
+ Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
+ Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
+ addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
+ addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
+
+ if (solver->startEncoding() == 1)
+ printf("SAT\n");
+ else
+ printf("UNSAT\n");
+ */
delete solver;
}
solver->addTableEntry(t1, row5, 2, 3);
solver->addTableEntry(t1, row6, 2, 5);
Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED);
- Element * tmparray[]={e1, e2};
+ Element *tmparray[] = {e1, e2};
Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
Set *deq[] = {s3,s2};
solver->addTableEntry(t1, row6, 3, true);
Predicate *p1 = solver->createPredicateTable(t1, FLAGIFFUNDEFINED);
Boolean *undef = solver->getBooleanVar(2);
- Element * tmparray[] = {e1, e2, e3};
+ Element *tmparray[] = {e1, e2, e3};
Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
solver->addConstraint(b1);
Set *d1[] = {s1, s2};
Predicate *eq = solver->createPredicateOperator(EQUALS, d1, 2);
- Element * tmparray2[] = {e1, e2};
+ Element *tmparray2[] = {e1, e2};
Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
solver->addConstraint(pred2);
#include "tunable.h"
-Tuner * allocTuner() {
- return (Tuner *) ourmalloc(sizeof(Tuner));
+Tuner::Tuner() {
}
-void deleteTuner(Tuner *This) {
- ourfree(This);
-}
-
-int getTunable(Tuner *This, TunableParam param, TunableDesc * descriptor) {
+int Tuner::getTunable(TunableParam param, TunableDesc *descriptor) {
return descriptor->defaultValue;
}
-int getVarTunable(Tuner *This, VarType vartype, TunableParam param, TunableDesc * descriptor) {
+int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
return descriptor->defaultValue;
}
#include "classlist.h"
-struct Tuner {
+class Tuner {
+public:
+ Tuner();
+ int getTunable(TunableParam param, TunableDesc *descriptor);
+ int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+ MEMALLOC;
};
-struct TunableDesc {
+class TunableDesc {
+public:
+ TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {}
int lowValue;
int highValue;
int defaultValue;
+ MEMALLOC;
};
-Tuner * allocTuner();
-void deleteTuner(Tuner *This);
-int getTunable(Tuner *This, TunableParam param, TunableDesc * descriptor);
-int getVarTunable(Tuner *This, VarType vartype, TunableParam param, TunableDesc * descriptor);
+#define GETTUNABLE(This, param, descriptor) This->getTunable(param, descriptor)
+#define GETVARTUNABLE(This, vartype, param, descriptor) This->getTunable(param, descriptor)
-#define GETTUNABLE(This, param, descriptor) getTunable(This, param, descriptor)
-#define GETVARTUNABLE(This, vartype, param, descriptor) getTunable(This, param, descriptor)
+static TunableDesc onoff(0, 1, 1);
+static TunableDesc offon(0, 1, 0);
-static TunableDesc onoff={0, 1, 1};
-static TunableDesc offon={0, 1, 0};
enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING};
typedef enum Tunables Tunables;
#endif
class Order;
class OrderPair;
-struct IncrementalSolver;
-typedef struct IncrementalSolver IncrementalSolver;
-
-
-
-struct OrderElement;
-typedef struct OrderElement OrderElement;
+class OrderElement;
class ElementEncoding;
class FunctionEncoding;
class OrderEncoding;
-struct TableEntry;
-typedef struct TableEntry TableEntry;
+class OrderGraph;
+class OrderNode;
+class OrderEdge;
-struct OrderGraph;
-typedef struct OrderGraph OrderGraph;
-struct OrderNode;
-typedef struct OrderNode OrderNode;
+struct IncrementalSolver;
+typedef struct IncrementalSolver IncrementalSolver;
-struct OrderEdge;
-typedef struct OrderEdge OrderEdge;
+struct TableEntry;
+typedef struct TableEntry TableEntry;
struct OrderEncoder;
typedef struct OrderEncoder OrderEncoder;
-struct Tuner;
-typedef struct Tuner Tuner;
-struct TunableDesc;
-typedef struct TunableDesc TunableDesc;
+class Tuner;
+class TunableDesc;
+
typedef int TunableParam;
typedef unsigned int uint;
#include "orderdecompose.h"
CSolver::CSolver() : unsat(false) {
- tuner = allocTuner();
+ tuner = new Tuner();
satEncoder = allocSATEncoder(this);
}
}
deleteSATEncoder(satEncoder);
- deleteTuner(tuner);
+ delete tuner;
}
Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
}
Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
- return new BooleanLogic(this, op, array, asize);
+ Boolean *boolean = new BooleanLogic(this, op, array, asize);
+ allBooleans.push(boolean);
+ return boolean;
}
void CSolver::addConstraint(Boolean *constraint) {
#include "structs.h"
class CSolver {
- public:
+public:
CSolver();
~CSolver();
-
- SATEncoder *satEncoder;
- bool unsat;
- Tuner *tuner;
-
- /** This is a vector of constraints that must be satisfied. */
- HashSetBoolean constraints;
-
- /** This is a vector of all boolean structs that we have allocated. */
- Vector<Boolean *> allBooleans;
-
- /** This is a vector of all set structs that we have allocated. */
- Vector<Set *> allSets;
-
- /** This is a vector of all element structs that we have allocated. */
- Vector<Element *> allElements;
-
- /** This is a vector of all predicate structs that we have allocated. */
- Vector<Predicate *> allPredicates;
-
- /** This is a vector of all table structs that we have allocated. */
- Vector<Table *> allTables;
-
- /** This is a vector of all order structs that we have allocated. */
- Vector<Order *> allOrders;
-
- /** This is a vector of all function structs that we have allocated. */
- Vector<Function *> allFunctions;
/** This function creates a set containing the elements passed in the array. */
-
Set *createSet(VarType type, uint64_t *elements, uint num);
/** This function creates a set from lowrange to highrange (inclusive). */
Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
-
+
/** This function creates a mutable set. */
-
+
MutableSet *createMutableSet(VarType type);
/** This function adds a new item to a set. */
void addItem(MutableSet *set, uint64_t element);
/** This function adds a new unique item to the set and returns it.
- This function cannot be used in conjunction with manually adding
- items to the set. */
-
+ This function cannot be used in conjunction with manually adding
+ items to the set. */
+
uint64_t createUniqueItem(MutableSet *set);
/** This function creates an element variable over a set. */
Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
/** This function adds a boolean constraint to the set of constraints
- to be satisfied */
+ to be satisfied */
void addConstraint(Boolean *constraint);
HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
+ void setUnSAT() { unsat = true; }
+
+ bool isUnSAT() { return unsat; }
+
+ Vector<Order *> *getOrders() { return &allOrders;}
+
+ Tuner *getTuner() { return tuner; }
+
+ HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+
+ SATEncoder *getSATEncoder() {return satEncoder;}
+
+ void replaceBooleanWithTrue(Boolean *bexpr);
+ void replaceBooleanWithFalse(Boolean *bexpr);
+ void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+
+
MEMALLOC;
-};
+private:
+ void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
+ void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
+ void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
+ void handleANDTrue(BooleanLogic *bexpr, Boolean *child);
+ void handleORFalse(BooleanLogic *bexpr, Boolean *child);
+
+ /** This is a vector of constraints that must be satisfied. */
+ HashSetBoolean constraints;
+
+ /** This is a vector of all boolean structs that we have allocated. */
+ Vector<Boolean *> allBooleans;
+
+ /** This is a vector of all set structs that we have allocated. */
+ Vector<Set *> allSets;
+
+ /** This is a vector of all element structs that we have allocated. */
+ Vector<Element *> allElements;
+
+ /** This is a vector of all predicate structs that we have allocated. */
+ Vector<Predicate *> allPredicates;
+
+ /** This is a vector of all table structs that we have allocated. */
+ Vector<Table *> allTables;
+
+ /** This is a vector of all order structs that we have allocated. */
+ Vector<Order *> allOrders;
+
+ /** This is a vector of all function structs that we have allocated. */
+ Vector<Function *> allFunctions;
+
+ SATEncoder *satEncoder;
+ bool unsat;
+ Tuner *tuner;
+};
#endif
static inline void *ourcalloc(size_t count, size_t size) { return calloc(count, size); }
static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
-#define MEMALLOC \
- void * operator new(size_t size) { \
- return ourmalloc(size); \
- } \
- void operator delete(void *p, size_t size) { \
- ourfree(p); \
- } \
- void * operator new[](size_t size) { \
- return ourmalloc(size); \
- } \
- void operator delete[](void *p, size_t size) { \
- ourfree(p); \
- } \
- void * operator new(size_t size, void *p) { /* placement new */ \
- return p; \
+#define MEMALLOC \
+ void *operator new(size_t size) { \
+ return ourmalloc(size); \
+ } \
+ void operator delete(void *p, size_t size) { \
+ ourfree(p); \
+ } \
+ void *operator new[](size_t size) { \
+ return ourmalloc(size); \
+ } \
+ void operator delete[](void *p, size_t size) { \
+ ourfree(p); \
+ } \
+ void *operator new(size_t size, void *p) { /* placement new */ \
+ return p; \
}
#endif/* _MY_MEMORY_H */
projects / satune.git / commitdiff