#include "element.h"
#include "order.h"
-Boolean::Boolean(ASTNodeType _type) : ASTNode(_type), polarity(P_UNDEFINED), boolVal(BV_UNDEFINED) {
- initDefVectorBoolean(GETBOOLEANPARENTS(this));
+Boolean::Boolean(ASTNodeType _type) :
+ ASTNode(_type),
+ polarity(P_UNDEFINED),
+ boolVal(BV_UNDEFINED),
+ parents() {
}
-BooleanVar::BooleanVar(VarType t) : Boolean(BOOLEANVAR), vtype(t), var(E_NULL) {
+BooleanVar::BooleanVar(VarType t) :
+ Boolean(BOOLEANVAR),
+ vtype(t),
+ var(E_NULL) {
}
-BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : Boolean(ORDERCONST), order(_order), first(_first), second(_second) {
- pushVectorBooleanOrder(&order->constraints, this);
+BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
+ Boolean(ORDERCONST),
+ order(_order),
+ first(_first),
+ second(_second) {
+ order->constraints.push(this);
}
BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) :
inputs(_inputs, _numInputs),
undefStatus(_undefinedStatus) {
for (uint i = 0; i < _numInputs; i++) {
- pushVectorASTNode(GETELEMENTPARENTS(_inputs[i]), this);
+ GETELEMENTPARENTS(_inputs[i])->push(this);
}
initPredicateEncoding(&encoding, this);
}
Boolean(LOGICOP),
op(_op),
inputs(array, asize) {
- pushVectorBoolean(solver->allBooleans, (Boolean *) this);
-}
-
-Boolean::~Boolean() {
- deleteVectorArrayBoolean(GETBOOLEANPARENTS(this));
+ solver->allBooleans.push(this);
}
BooleanPredicate::~BooleanPredicate() {
Boolean(ASTNodeType _type);
Polarity polarity;
BooleanValue boolVal;
- VectorBoolean parents;
- ~Boolean();
+ Vector<Boolean *> parents;
MEMALLOC;
};
#include "table.h"
Element::Element(ASTNodeType _type) : ASTNode(_type) {
- initDefVectorASTNode(GETELEMENTPARENTS(this));
initElementEncoding(&encoding, (Element *) this);
}
ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) : Element(ELEMFUNCRETURN), function(_function), inputs(array, numArrays), overflowstatus(_overflowstatus) {
for (uint i = 0; i < numArrays; i++)
- pushVectorASTNode(GETELEMENTPARENTS(array[i]), this);
+ GETELEMENTPARENTS(array[i])->push(this);
initFunctionEncoding(&functionencoding, this);
}
Element::~Element() {
deleteElementEncoding(&encoding);
- deleteVectorArrayASTNode(GETELEMENTPARENTS(this));
}
public:
Element(ASTNodeType type);
~Element();
- VectorASTNode parents;
+ Vector<ASTNode *> parents;
ElementEncoding encoding;
MEMALLOC;
};
#include "mutableset.h"
-MutableSet *allocMutableSet(VarType t) {
- MutableSet *This = (MutableSet *)ourmalloc(sizeof(MutableSet));
- This->type = t;
- This->isRange = false;
- This->low = 0;
- This->high = 0;
- This->members = allocDefVectorInt();
- return This;
+MutableSet::MutableSet(VarType t) : Set(t) {
}
-void addElementMSet(MutableSet *set, uint64_t element) {
- pushVectorInt(set->members, element);
+void MutableSet::addElementMSet(uint64_t element) {
+ members->push(element);
}
#define MUTABLESET_H
#include "set.h"
-MutableSet *allocMutableSet(VarType t);
-void addElementMSet(MutableSet *set, uint64_t element);
+class MutableSet : public Set {
+ public:
+ MutableSet(VarType t);
+ void addElementMSet(uint64_t element);
+ MEMALLOC;
+};
#endif
#include "ordergraph.h"
Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTable(NULL), elementTable(NULL), graph(NULL) {
- initDefVectorBooleanOrder(&constraints);
initOrderEncoding(&order, this);
}
}
void Order::addOrderConstraint(BooleanOrder *constraint) {
- pushVectorBooleanOrder(&constraints, constraint);
+ constraints.push(constraint);
}
void Order::setOrderEncodingType(OrderEncodingType type) {
}
Order::~Order() {
- deleteVectorArrayBooleanOrder(&constraints);
deleteOrderEncoding(&order);
if (orderPairTable != NULL) {
resetAndDeleteHashTableOrderPair(orderPairTable);
HashTableOrderPair *orderPairTable;
HashSetOrderElement* elementTable;
OrderGraph *graph;
- VectorBooleanOrder constraints;
+ Vector<BooleanOrder *> constraints;
OrderEncoding order;
void initializeOrderHashTable();
void initializeOrderElementsHashTable();
removeHashSetBoolean(This->constraints, bexpr);
}
- uint size = getSizeVectorBoolean(&bexpr->parents);
+ uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
- Boolean *parent = getVectorBoolean(&bexpr->parents, i);
+ Boolean *parent = bexpr->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
switch (logicop->op) {
case L_AND:
addHashSetBoolean(This->constraints, newb);
}
- uint size = getSizeVectorBoolean(&oldb->parents);
+ uint size = oldb->parents.getSize();
for (uint i = 0; i < size; i++) {
- Boolean *parent = getVectorBoolean(&oldb->parents, i);
+ Boolean *parent = oldb->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
uint parentsize = logicop->inputs.getSize();
Boolean *b = logicop->inputs.get(i);
if (b == oldb) {
logicop->inputs.set(i, newb);
- pushVectorBoolean(&newb->parents, parent);
+ newb->parents.push(parent);
}
}
}
removeHashSetBoolean(This->constraints, bexpr);
}
- uint size = getSizeVectorBoolean(&bexpr->parents);
+ uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
- Boolean *parent = getVectorBoolean(&bexpr->parents, i);
+ Boolean *parent = bexpr->parents.get(i);
BooleanLogic *logicop = (BooleanLogic *) parent;
switch (logicop->op) {
case L_AND:
#include "set.h"
#include <stddef.h>
+Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
+ members = new Vector<uint64_t>();
+}
+
Set::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) {
- members = allocVectorArrayInt(num, elements);
+ members = new Vector<uint64_t>(num, elements);
}
Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) : type(t), isRange(true), low(lowrange), high(highrange), members(NULL) {
if (isRange) {
return element >= low && element <= high;
} else {
- uint size = getSizeVectorInt(members);
+ uint size = members->getSize();
for (uint i = 0; i < size; i++) {
- if (element == getVectorInt(members, i))
+ if (element == members->get(i))
return true;
}
return false;
if (isRange)
return low + index;
else
- return getVectorInt(members, index);
+ return members->get(index);
}
uint Set::getSize() {
if (isRange) {
return high - low + 1;
} else {
- return getSizeVectorInt(members);
+ return members->getSize();
}
}
Set::~Set() {
if (!isRange)
- deleteVectorInt(members);
+ delete members;
}
class Set {
public:
+ Set(VarType t);
Set(VarType t, uint64_t *elements, uint num);
Set(VarType t, uint64_t lowrange, uint64_t highrange);
~Set();
bool isRange;
uint64_t low;//also used to count unique items
uint64_t high;
- VectorInt *members;
+ Vector<uint64_t> *members;
MEMALLOC;
};
-
#endif/* SET_H */
#include "mutableset.h"
#include "tunable.h"
-void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
+void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
while (hasNextOrderNode(iterator)) {
OrderNode *node = nextOrderNode(iterator);
node->status = VISITED;
DFSNodeVisit(node, finishNodes, false, false, 0);
node->status = FINISHED;
- pushVectorOrderNode(finishNodes, node);
+ finishNodes->push(node);
}
}
deleteIterOrderNode(iterator);
}
-void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
- uint size = getSizeVectorOrderNode(finishNodes);
+void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
+ uint size = finishNodes->getSize();
uint sccNum = 1;
for (int i = size - 1; i >= 0; i--) {
- OrderNode *node = getVectorOrderNode(finishNodes, i);
+ OrderNode *node = finishNodes->get(i);
if (node->status == NOTVISITED) {
node->status = VISITED;
DFSNodeVisit(node, NULL, true, false, sccNum);
}
}
-void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
+void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
while (hasNextOrderEdge(iterator)) {
OrderEdge *edge = nextOrderEdge(iterator);
DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
child->status = FINISHED;
if (finishNodes != NULL)
- pushVectorOrderNode(finishNodes, child);
+ finishNodes->push(child);
if (isReverse)
child->sccNum = sccNum;
}
}
void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
- VectorOrderNode finishNodes;
- initDefVectorOrderNode(&finishNodes);
+ Vector<OrderNode *> finishNodes;
DFS(graph, &finishNodes);
resetNodeInfoStatusSCC(graph);
DFSReverse(graph, &finishNodes);
resetNodeInfoStatusSCC(graph);
- deleteVectorArrayOrderNode(&finishNodes);
}
bool isMustBeTrueNode(OrderNode* node){
to determine whether we need to generate pseudoPos edges. */
void completePartialOrderGraph(OrderGraph *graph) {
- VectorOrderNode finishNodes;
- initDefVectorOrderNode(&finishNodes);
+ Vector<OrderNode *> finishNodes;
DFS(graph, &finishNodes);
resetNodeInfoStatusSCC(graph);
HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
- VectorOrderNode sccNodes;
- initDefVectorOrderNode(&sccNodes);
+ Vector<OrderNode *> sccNodes;
- uint size = getSizeVectorOrderNode(&finishNodes);
+ uint size = finishNodes.getSize();
uint sccNum = 1;
for (int i = size - 1; i >= 0; i--) {
- OrderNode *node = getVectorOrderNode(&finishNodes, i);
+ OrderNode *node = finishNodes.get(i);
HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
putNodeToNodeSet(table, node, sources);
node->status = FINISHED;
node->sccNum = sccNum;
sccNum++;
- pushVectorOrderNode(&sccNodes, node);
+ sccNodes.push(node);
//Compute in set for entire SCC
- uint rSize = getSizeVectorOrderNode(&sccNodes);
+ uint rSize = sccNodes.getSize();
for (uint j = 0; j < rSize; j++) {
- OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
+ OrderNode *rnode = sccNodes.get(j);
//Compute source sets
HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
while (hasNextOrderEdge(iterator)) {
}
for (uint j=0; j < rSize; j++) {
//Copy in set of entire SCC
- OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
+ OrderNode *rnode = sccNodes.get(j);
HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
putNodeToNodeSet(table, rnode, set);
deleteIterOrderEdge(iterator);
}
- clearVectorOrderNode(&sccNodes);
+ sccNodes.clear();
}
}
resetAndDeleteHashTableNodeToNodeSet(table);
deleteHashTableNodeToNodeSet(table);
resetNodeInfoStatusSCC(graph);
- deleteVectorArrayOrderNode(&sccNodes);
- deleteVectorArrayOrderNode(&finishNodes);
}
-void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
+void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
while (hasNextOrderNode(iterator)) {
OrderNode *node = nextOrderNode(iterator);
node->status = VISITED;
DFSNodeVisit(node, finishNodes, false, true, 0);
node->status = FINISHED;
- pushVectorOrderNode(finishNodes, node);
+ finishNodes->push(node);
}
}
deleteIterOrderNode(iterator);
}
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
- uint size = getSizeVectorOrderNode(finishNodes);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
+ uint size = finishNodes->getSize();
HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
for (int i = size - 1; i >= 0; i--) {
- OrderNode *node = getVectorOrderNode(finishNodes, i);
+ OrderNode *node = finishNodes->get(i);
HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
putNodeToNodeSet(table, node, sources);
edges. */
void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
- VectorOrderNode finishNodes;
- initDefVectorOrderNode(&finishNodes);
+ Vector<OrderNode *> finishNodes;
//Topologically sort the mustPos edge graph
DFSMust(graph, &finishNodes);
resetNodeInfoStatusSCC(graph);
//Find any backwards edges that complete cycles and force them to be mustNeg
DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
- deleteVectorArrayOrderNode(&finishNodes);
}
/* This function finds edges that must be positive and forces the
}
void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
- VectorOrder ordervec;
- VectorOrder partialcandidatevec;
- initDefVectorOrder(&ordervec);
- initDefVectorOrder(&partialcandidatevec);
- uint size = getSizeVectorBooleanOrder(&order->constraints);
+ Vector<Order *> ordervec;
+ Vector<Order *> partialcandidatevec;
+ uint size = order->constraints.getSize();
for (uint i = 0; i < size; i++) {
- BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
+ BooleanOrder *orderconstraint = order->constraints.get(i);
OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
} else {
//Build new order and change constraint's order
Order *neworder = NULL;
- if (getSizeVectorOrder(&ordervec) > from->sccNum)
- neworder = getVectorOrder(&ordervec, from->sccNum);
+ if (ordervec.getSize() > from->sccNum)
+ neworder = ordervec.get(from->sccNum);
if (neworder == NULL) {
- Set *set = (Set *) allocMutableSet(order->set->type);
+ MutableSet *set = new MutableSet(order->set->type);
neworder = new Order(order->type, set);
- pushVectorOrder(This->allOrders, neworder);
- setExpandVectorOrder(&ordervec, from->sccNum, neworder);
+ This->allOrders.push(neworder);
+ ordervec.setExpand(from->sccNum, neworder);
if (order->type == PARTIAL)
- setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder);
+ partialcandidatevec.setExpand(from->sccNum, neworder);
else
- setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
+ partialcandidatevec.setExpand(from->sccNum, NULL);
}
if (from->status != ADDEDTOSET) {
from->status = ADDEDTOSET;
- addElementMSet((MutableSet *)neworder->set, from->id);
+ ((MutableSet *)neworder->set)->addElementMSet(from->id);
}
if (to->status != ADDEDTOSET) {
to->status = ADDEDTOSET;
- addElementMSet((MutableSet *)neworder->set, to->id);
+ ((MutableSet *)neworder->set)->addElementMSet(to->id);
}
if (order->type == PARTIAL) {
OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
if (edge->polNeg)
- setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
+ partialcandidatevec.setExpand(from->sccNum, NULL);
}
orderconstraint->order = neworder;
neworder->addOrderConstraint(orderconstraint);
}
}
- uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
+ uint pcvsize=partialcandidatevec.getSize();
for(uint i=0;i<pcvsize;i++) {
- Order * neworder=getVectorOrder(&partialcandidatevec, i);
+ Order * neworder=partialcandidatevec.get(i);
if (neworder != NULL){
neworder->type = TOTAL;
model_print("i=%u\t", i);
}
}
-
- deleteVectorArrayOrder(&ordervec);
- deleteVectorArrayOrder(&partialcandidatevec);
}
void orderAnalysis(CSolver *This) {
- uint size = getSizeVectorOrder(This->allOrders);
+ uint size = This->allOrders.getSize();
for (uint i = 0; i < size; i++) {
- Order *order = getVectorOrder(This->allOrders, i);
+ Order *order = This->allOrders.get(i);
bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
if (!doDecompose)
continue;
void computeStronglyConnectedComponentGraph(OrderGraph *graph);
void orderAnalysis(CSolver *solver);
void initializeNodeInfoSCC(OrderGraph *graph);
-void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
-void DFS(OrderGraph *graph, VectorOrderNode *finishNodes);
-void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes);
+void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
+void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void completePartialOrderGraph(OrderGraph *graph);
void resetNodeInfoStatusSCC(OrderGraph *graph);
bool isMustBeTrueNode(OrderNode* node);
void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node);
void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
void completePartialOrderGraph(OrderGraph *graph);
-void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes);
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure);
+void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
OrderGraph *buildOrderGraph(Order *order) {
OrderGraph *orderGraph = allocOrderGraph(order);
- uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+ uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
- addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+ addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
}
return orderGraph;
}
//Builds only the subgraph for the must order graph.
OrderGraph *buildMustOrderGraph(Order *order) {
OrderGraph *orderGraph = allocOrderGraph(order);
- uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+ uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
- addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+ addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
}
return orderGraph;
}
Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
addConstraintCNF(This->cnf, cor);
deleteVectorEdge(clauses);
-
}
BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
setFunctionEncodingType(boolean->getFunctionEncoding(), CIRCUIT);
{//Adding new elements and boolean/predicate to solver regarding memory management
- pushVectorBoolean(This->solver->allBooleans, boolean);
- pushVectorPredicate(This->solver->allPredicates, predicate);
- pushVectorElement(This->solver->allElements, elem1);
- pushVectorElement(This->solver->allElements, elem2);
+ This->solver->allBooleans.push(boolean);
+ This->solver->allPredicates.push(predicate);
+ This->solver->allElements.push(elem1);
+ This->solver->allElements.push(elem2);
}
return encodeConstraintSATEncoder(This, boolean);
}
model_print("in total order ...\n");
#endif
ASSERT(order->type == TOTAL);
- VectorInt *mems = order->set->members;
- uint size = getSizeVectorInt(mems);
+ Vector<uint64_t> *mems = order->set->members;
+ uint size = mems->getSize();
for (uint i = 0; i < size; i++) {
- uint64_t valueI = getVectorInt(mems, i);
+ uint64_t valueI = mems->get(i);
for (uint j = i + 1; j < size; j++) {
- uint64_t valueJ = getVectorInt(mems, j);
+ uint64_t valueJ = mems->get(j);
OrderPair pairIJ = {valueI, valueJ};
Edge constIJ = getPairConstraint(This, order, &pairIJ);
for (uint k = j + 1; k < size; k++) {
- uint64_t valueK = getVectorInt(mems, k);
+ uint64_t valueK = mems->get(k);
OrderPair pairJK = {valueJ, valueK};
OrderPair pairIK = {valueI, valueK};
Edge constIK = getPairConstraint(This, order, &pairIK);
--- /dev/null
+#ifndef CPPVECTOR_H
+#define CPPVECTOR_H
+#include <string.h>
+
+#define VECTOR_DEFCAP 8
+
+template<typename type>
+class Vector {
+ public:
+ Vector(uint _capacity = VECTOR_DEFCAP) :
+ size(0),
+ capacity(_capacity),
+ array((type *) ourmalloc(sizeof(type) * _capacity)) {
+ }
+
+ Vector(uint _capacity, type * _array) :
+ size(_capacity),
+ capacity(_capacity),
+ array((type *) ourmalloc(sizeof(type) * _capacity)) {
+ memcpy(array, _array, capacity * sizeof(type));
+ }
+
+ void pop() {
+ size--;
+ }
+
+ type last() {
+ 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));
+ 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;
+ }
+
+ type get(uint index) {
+ return array[index];
+ }
+
+ void setExpand(uint index, type item) {
+ if (index >= size)
+ setSize(index + 1);
+ set(index, item);
+ }
+
+ void set(uint index, type item) {
+ array[index] = item;
+ }
+
+ uint getSize() {
+ return size;
+ }
+
+ ~Vector() {
+ ourfree(array);
+ }
+
+ void clear() {
+ size = 0;
+ }
+
+ type *expose() {
+ return array;
+ }
+
+ private:
+ uint size;
+ uint capacity;
+ type *array;
+};
+#endif
-#include "structs.h"
#include "mymemory.h"
+#include "structs.h"
#include "orderpair.h"
#include "tableentry.h"
#include "ordernode.h"
#include "ordergraph.h"
#include "orderelement.h"
-VectorImpl(Table, Table *, 4);
-VectorImpl(Set, Set *, 4);
-VectorImpl(Boolean, Boolean *, 4);
-VectorImpl(BooleanOrder, BooleanOrder *, 4);
-VectorImpl(Function, Function *, 4);
-VectorImpl(Predicate, Predicate *, 4);
-VectorImpl(Element, Element *, 4);
-VectorImpl(Order, Order *, 4);
-VectorImpl(TableEntry, TableEntry *, 4);
-VectorImpl(ASTNode, ASTNode *, 4);
-VectorImpl(Int, uint64_t, 4);
-VectorImpl(OrderNode, OrderNode *, 4);
-VectorImpl(OrderGraph, OrderGraph *, 4);
-
static inline unsigned int Ptr_hash_function(void *hash) {
return (unsigned int)((int64)hash >> 4);
}
#ifndef STRUCTS_H
#define STRUCTS_H
-#include "vector.h"
+#include "cppvector.h"
#include "hashtable.h"
#include "hashset.h"
#include "classlist.h"
#include "array.h"
-VectorDef(Table, Table *);
-VectorDef(Set, Set *);
-VectorDef(Boolean, Boolean *);
-VectorDef(BooleanOrder, BooleanOrder *);
-VectorDef(Function, Function *);
-VectorDef(Predicate, Predicate *);
-VectorDef(Element, Element *);
-VectorDef(Order, Order *);
-VectorDef(TableEntry, TableEntry *);
-VectorDef(ASTNode, ASTNode *);
-VectorDef(Int, uint64_t);
-VectorDef(OrderNode, OrderNode *);
-VectorDef(OrderGraph, OrderGraph *);
-
HashTableDef(Void, void *, void *);
HashTableDef(OrderPair, OrderPair *, OrderPair *);
Element *element = This->element;
Set *set = getElementSet(element);
ASSERT(set->isRange == false);
- uint size = getSizeVectorInt(set->members);
+ uint size = set->members->getSize();
uint encSize = getSizeEncodingArray(This, size);
allocEncodingArrayElement(This, encSize);
allocInUseArrayElement(This, encSize);
for (uint i = 0; i < size; i++) {
- This->encodingArray[i] = getVectorInt(set->members, i);
+ This->encodingArray[i] = set->members->get(i);
setInUseElement(This, i);
}
}
class BooleanPredicate;
class ASTNode;
class Set;
-typedef class Set MutableSet;
+class MutableSet;
class ElementFunction;
class ElementSet;
CSolver::CSolver() : unsat(false) {
constraints = allocDefHashSetBoolean();
- allBooleans = allocDefVectorBoolean();
- allSets = allocDefVectorSet();
- allElements = allocDefVectorElement();
- allPredicates = allocDefVectorPredicate();
- allTables = allocDefVectorTable();
- allOrders = allocDefVectorOrder();
- allFunctions = allocDefVectorFunction();
tuner = allocTuner();
satEncoder = allocSATEncoder(this);
}
CSolver::~CSolver() {
deleteHashSetBoolean(constraints);
- uint size = getSizeVectorBoolean(allBooleans);
+ uint size = allBooleans.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorBoolean(allBooleans, i);
+ delete allBooleans.get(i);
}
- deleteVectorBoolean(allBooleans);
- size = getSizeVectorSet(allSets);
+ size = allSets.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorSet(allSets, i);
+ delete allSets.get(i);
}
- deleteVectorSet(allSets);
- size = getSizeVectorElement(allElements);
+ size = allElements.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorElement(allElements, i);
+ delete allElements.get(i);
}
- deleteVectorElement(allElements);
- size = getSizeVectorTable(allTables);
+ size = allTables.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorTable(allTables, i);
+ delete allTables.get(i);
}
- deleteVectorTable(allTables);
- size = getSizeVectorPredicate(allPredicates);
+ size = allPredicates.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorPredicate(allPredicates, i);
+ delete allPredicates.get(i);
}
- deleteVectorPredicate(allPredicates);
- size = getSizeVectorOrder(allOrders);
+ size = allOrders.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorOrder(allOrders, i);
+ delete allOrders.get(i);
}
- deleteVectorOrder(allOrders);
- size = getSizeVectorFunction(allFunctions);
+ size = allFunctions.getSize();
for (uint i = 0; i < size; i++) {
- delete getVectorFunction(allFunctions, i);
+ delete allFunctions.get(i);
}
- deleteVectorFunction(allFunctions);
+
deleteSATEncoder(satEncoder);
deleteTuner(tuner);
}
Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
Set *set = new Set(type, elements, numelements);
- pushVectorSet(allSets, set);
+ allSets.push(set);
return set;
}
Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
Set *set = new Set(type, lowrange, highrange);
- pushVectorSet(allSets, set);
+ allSets.push(set);
return set;
}
MutableSet *CSolver::createMutableSet(VarType type) {
- MutableSet *set = allocMutableSet(type);
- pushVectorSet(allSets, set);
+ MutableSet *set = new MutableSet(type);
+ allSets.push(set);
return set;
}
void CSolver::addItem(MutableSet *set, uint64_t element) {
- addElementMSet(set, element);
+ set->addElementMSet(element);
}
uint64_t CSolver::createUniqueItem(MutableSet *set) {
uint64_t element = set->low++;
- addElementMSet(set, element);
+ set->addElementMSet(element);
return element;
}
Element *CSolver::getElementVar(Set *set) {
Element *element = new ElementSet(set);
- pushVectorElement(allElements, element);
+ allElements.push(element);
return element;
}
Element *CSolver::getElementConst(VarType type, uint64_t value) {
Element *element = new ElementConst(value, type);
- pushVectorElement(allElements, element);
+ allElements.push(element);
return element;
}
Boolean *CSolver::getBooleanVar(VarType type) {
Boolean *boolean = new BooleanVar(type);
- pushVectorBoolean(allBooleans, boolean);
+ allBooleans.push(boolean);
return boolean;
}
Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
- pushVectorFunction(allFunctions, function);
+ allFunctions.push(function);
return function;
}
Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
Predicate *predicate = new PredicateOperator(op, domain,numDomain);
- pushVectorPredicate(allPredicates, predicate);
+ allPredicates.push(predicate);
return predicate;
}
Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
Predicate *predicate = new PredicateTable(table, behavior);
- pushVectorPredicate(allPredicates, predicate);
+ allPredicates.push(predicate);
return predicate;
}
Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
Table *table = new Table(domains,numDomain,range);
- pushVectorTable(allTables, table);
+ allTables.push(table);
return table;
}
Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
Function *function = new FunctionTable(table, behavior);
- pushVectorFunction(allFunctions,function);
+ allFunctions.push(function);
return function;
}
Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
- pushVectorElement(allElements, element);
+ allElements.push(element);
return element;
}
Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
Boolean *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
- pushVectorBoolean(allBooleans, boolean);
+ allBooleans.push(boolean);
return boolean;
}
Order *CSolver::createOrder(OrderType type, Set *set) {
Order *order = new Order(type, set);
- pushVectorOrder(allOrders, order);
+ allOrders.push(order);
return order;
}
Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
Boolean *constraint = new BooleanOrder(order, first, second);
- pushVectorBoolean(allBooleans,constraint);
+ allBooleans.push(constraint);
return constraint;
}
HashSetBoolean *constraints;
/** This is a vector of all boolean structs that we have allocated. */
- VectorBoolean *allBooleans;
+ Vector<Boolean *> allBooleans;
/** This is a vector of all set structs that we have allocated. */
- VectorSet *allSets;
+ Vector<Set *> allSets;
/** This is a vector of all element structs that we have allocated. */
- VectorElement *allElements;
+ Vector<Element *> allElements;
/** This is a vector of all predicate structs that we have allocated. */
- VectorPredicate *allPredicates;
+ Vector<Predicate *> allPredicates;
/** This is a vector of all table structs that we have allocated. */
- VectorTable *allTables;
+ Vector<Table *> allTables;
/** This is a vector of all order structs that we have allocated. */
- VectorOrder *allOrders;
+ Vector<Order *> allOrders;
/** This is a vector of all function structs that we have allocated. */
- VectorFunction *allFunctions;
+ Vector<Function *> allFunctions;
/** This function creates a set containing the elements passed in the array. */