#include "boolean.h"
#include "element.h"
-#define HASHNEXT(hash, newval) {hash+=newval; hash += hash << 10; hash ^= hash >>6;}
-#define HASHFINAL(hash) {hash += hash <<3; hash ^= hash >> 11; hash += hash << 15;}
+#define HASHNEXT(hash, newval) {hash += newval; hash += hash << 10; hash ^= hash >> 6;}
+#define HASHFINAL(hash) {hash += hash << 3; hash ^= hash >> 11; hash += hash << 15;}
bool compareArray(Array<BooleanEdge> *inputs1, Array<BooleanEdge> *inputs2) {
if (inputs1->getSize() != inputs2->getSize())
}
case LOGICOP: {
BooleanLogic *l = (BooleanLogic *)b;
- return ((uint)l->op) + 43* hashArray(&l->inputs);
+ return ((uint)l->op) + 43 * hashArray(&l->inputs);
}
case PREDICATEOP: {
BooleanPredicate *p = (BooleanPredicate *)b;
class ElementSet : public Element {
public:
ElementSet(ASTNodeType type, Set *s);
- virtual ~ElementSet(){}
+ virtual ~ElementSet() {}
ElementSet(Set *s);
virtual Element *clone(CSolver *solver, CloneMap *map);
virtual void serialize(Serializer *serializer);
class ElementConst : public ElementSet {
public:
ElementConst(uint64_t value, Set *_set);
- virtual ~ElementConst(){}
+ virtual ~ElementConst() {}
uint64_t value;
virtual void serialize(Serializer *serializer);
virtual void print();
class ElementFunction : public Element {
public:
- virtual ~ElementFunction(){}
+ virtual ~ElementFunction() {}
ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
Array<Element *> inputs;
BooleanEdge overflowstatus;
HashtableOrderPair *Order::getOrderPairTable() {
ASSERT( encoding.resolver != NULL);
- if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
+ if (OrderPairResolver * t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
return t->getOrderPairTable();
} else {
ASSERT(0);
serializer->mywrite(&This, sizeof(Set *));
serializer->mywrite(&type, sizeof(VarType));
serializer->mywrite(&isRange, sizeof(bool));
- bool isMutable = isMutableSet();
+ bool isMutable = isMutableSet();
serializer->mywrite(&isMutable, sizeof(bool));
- if(isRange){
- serializer->mywrite(&low, sizeof(uint64_t));
- serializer->mywrite(&high, sizeof(uint64_t));
- }else {
- uint size = members->getSize();
- serializer->mywrite(&size, sizeof(uint));
- for(uint i=0; i<size; i++){
- uint64_t mem = members->get(i);
- serializer->mywrite(&mem, sizeof(uint64_t));
- }
- }
+ if (isRange) {
+ serializer->mywrite(&low, sizeof(uint64_t));
+ serializer->mywrite(&high, sizeof(uint64_t));
+ } else {
+ uint size = members->getSize();
+ serializer->mywrite(&size, sizeof(uint));
+ for (uint i = 0; i < size; i++) {
+ uint64_t mem = members->get(i);
+ serializer->mywrite(&mem, sizeof(uint64_t));
+ }
+ }
}
void Set::print() {
protected:
VarType type;
bool isRange;
- uint64_t low;//also used to count unique items
+ uint64_t low; //also used to count unique items
uint64_t high;
Vector<uint64_t> *members;
};
#include "tunable.h"
/** Returns a table that maps a node to the set of nodes that can reach the node. */
-HashtableNodeToNodeSet * getMustReachMap(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
+HashtableNodeToNodeSet *getMustReachMap(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
uint size = finishNodes->getSize();
HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-
+
for (int i = size - 1; i >= 0; i--) {
OrderNode *node = finishNodes->get(i);
HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
table->put(node, sources);
-
+
{
//Compute source sets
SetIteratorOrderEdge *iterator = node->inEdges.iterator();
return table;
}
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
uint size = finishNodes->getSize();
for (int i = size - 1; i >= 0; i--) {
OrderNode *node = finishNodes->get(i);
HashsetOrderNode *sources = table->get(node);
-
+
if (computeTransitiveClosure) {
//Compute full transitive closure for nodes
SetIteratorOrderNode *srciterator = sources->iterator();
while (srciterator->hasNext()) {
- OrderNode *srcnode = (OrderNode*)srciterator->next();
+ OrderNode *srcnode = (OrderNode *)srciterator->next();
OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
newedge->mustPos = true;
newedge->polPos = true;
//Topologically sort the mustPos edge graph
graph->DFSMust(&finishNodes);
graph->resetNodeInfoStatusSCC();
- HashtableNodeToNodeSet * table=getMustReachMap(solver, graph, & finishNodes);
+ HashtableNodeToNodeSet *table = getMustReachMap(solver, graph, &finishNodes);
//Find any backwards edges that complete cycles and force them to be mustNeg
DFSClearContradictions(solver, graph, table, &finishNodes, computeTransitiveClosure);
table->resetAndDeleteVals();
#include "structs.h"
#include "mymemory.h"
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
-HashtableNodeToNodeSet * getMustReachMap(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
+HashtableNodeToNodeSet *getMustReachMap(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
OrderNode *node = new OrderNode(id);
- OrderNode *tmp = (OrderNode*)nodes.get(node);
+ OrderNode *tmp = (OrderNode *)nodes.get(node);
if ( tmp != NULL) {
delete node;
node = tmp;
OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
OrderNodeKey node(id);
- OrderNode *tmp = (OrderNode*)nodes.get(&node);
+ OrderNode *tmp = (OrderNode *)nodes.get(&node);
return tmp;
}
void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
SetIteratorOrderNode *iterator = getNodes();
while (iterator->hasNext()) {
- OrderNode *node = (OrderNode*)iterator->next();
+ OrderNode *node = (OrderNode *)iterator->next();
if (node->status == NOTVISITED && !node->removed) {
node->status = VISITED;
DFSNodeVisit(node, finishNodes, false, false, 0);
void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
SetIteratorOrderNode *iterator = getNodes();
while (iterator->hasNext()) {
- OrderNode *node = (OrderNode*)iterator->next();
+ OrderNode *node = (OrderNode *)iterator->next();
if (node->status == NOTVISITED && !node->removed) {
node->status = VISITED;
DFSNodeVisit(node, finishNodes, false, true, 0);
void OrderGraph::resetNodeInfoStatusSCC() {
SetIteratorOrderNode *iterator = getNodes();
while (iterator->hasNext()) {
- ((OrderNode*)iterator->next())->status = NOTVISITED;
+ ((OrderNode *)iterator->next())->status = NOTVISITED;
}
delete iterator;
}
enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
typedef enum NodeStatus NodeStatus;
-class OrderNodeKey{
+class OrderNodeKey {
public:
- OrderNodeKey(uint64_t id) : id(id){}
- virtual ~OrderNodeKey(){}
- uint64_t getID() {return id;}
- uint64_t id;
+ OrderNodeKey(uint64_t id) : id(id) {}
+ virtual ~OrderNodeKey() {}
+ uint64_t getID() {return id;}
+ uint64_t id;
};
class OrderNode : public OrderNodeKey {
public:
OrderNode(uint64_t id);
- virtual ~OrderNode(){}
+ virtual ~OrderNode() {}
void addNewIncomingEdge(OrderEdge *edge);
void addNewOutgoingEdge(OrderEdge *edge);
void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
SetIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
- OrderNode *node = (OrderNode*)iterator->next();
+ OrderNode *node = (OrderNode *)iterator->next();
if (node->removed)
continue;
if (isMustBeTrueNode(node)) {
void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
SetIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
- OrderNode *node = (OrderNode*)iterator->next();
+ OrderNode *node = (OrderNode *)iterator->next();
if (node->removed)
continue;
attemptNodeMerge(graph, node, dor);
sink->inEdges.remove(outedge);
//save the remapping that we did
dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
+
//create the new edge
OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
//update the flags
#include "cnfexpr.h"
#include <stdio.h>
+#include "common.h"
/*
V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
mergeArray[mergeIndex++] = merge;
}
}
- deleteLitVector(lThis);//Done with this litVector
+ deleteLitVector(lThis); //Done with this litVector
}
/** Finally do the singleton, singleton pairs */
ourfree(cnf);
}
-void resetCNF(CNF *cnf){
- for (uint i = 0; i < cnf->capacity; i++) {
+void resetCNF(CNF *cnf) {
+ for (uint i = 0; i < cnf->capacity; i++) {
Node *n = cnf->node_array[i];
if (n != NULL)
ourfree(n);
}
- clearVectorEdge(&cnf->constraints);
- clearVectorEdge(&cnf->args);
- deleteIncrementalSolver(cnf->solver);
- memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
-
- cnf->varcount = 1;
- cnf->size = 0;
- cnf->enableMatching = true;
- cnf->solver = allocIncrementalSolver();
- cnf->solveTime = 0;
+ clearVectorEdge(&cnf->constraints);
+ clearVectorEdge(&cnf->args);
+ resetSolver(cnf->solver);
+ memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
+
+ cnf->varcount = 1;
+ cnf->size = 0;
+ cnf->enableMatching = true;
+ cnf->solveTime = 0;
cnf->encodeTime = 0;
}
}
int comparefunction(const Edge *e1, const Edge *e2) {
- return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
+ if (e1->node_ptr == e2->node_ptr)
+ return 0;
+ if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
+ return -1;
+ else
+ return 1;
}
Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
int result = solve(cnf->solver);
long long finishTime = getTimeNano();
cnf->encodeTime = startSolve - startTime;
- model_print("CNF Encode time: %f\n", cnf->encodeTime/1000000000.0);
+ model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
cnf->solveTime = finishTime - startSolve;
- model_print("Solve time: %f\n", cnf->solveTime/ 1000000000.0);
+ model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
return result;
}
}
void finishedClauses(IncrementalSolver *This) {
- addClauseLiteral(This, 0);
+ This->buffer[This->offset++] = 0;
+ if (This->offset == IS_BUFFERSIZE) {
+ flushBufferSolver(This);
+ }
}
void freeze(IncrementalSolver *This, int variable) {
deleteCNF(cnf);
}
-void SATEncoder::resetSATEncoder(){
- resetCNF(cnf);
- booledgeMap.reset();
+void SATEncoder::resetSATEncoder() {
+ resetCNF(cnf);
+ booledgeMap.reset();
}
int SATEncoder::solve() {
int solve();
SATEncoder(CSolver *solver);
~SATEncoder();
- void resetSATEncoder();
+ void resetSATEncoder();
void encodeAllSATEncoder(CSolver *csolver);
Edge encodeConstraintSATEncoder(BooleanEdge constraint);
CNF *getCNF() { return cnf;}
class Array {
public:
Array(uint _size) :
- array((type *)ourcalloc(1, sizeof(type) * _size)),
+ array((type *) ourcalloc(1, sizeof(type) * _size)),
size(_size)
{
}
Array(type *_array, uint _size) :
- array((type *)ourcalloc(1, sizeof(type) * _size)),
+ array((type *) ourcalloc(1, sizeof(type) * _size)),
size(_size) {
memcpy(array, _array, _size * sizeof(type));
}
Linknode<_Key> *next;
};
-template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key), bool (*equals)(_Key, _Key)>
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function) (_Key), bool (*equals) (_Key, _Key)>
class Hashset;
-template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
class SetIterator {
public:
SetIterator(Linknode<_Key> *_curr, 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) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
class Hashset {
public:
Hashset(unsigned int initialcapacity = 16, double factor = 0.5) :
* manipulation and storage.
* @tparam _Shift Logical shift to apply to all keys. Default 0.
*/
-template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
class Hashtable {
public:
/**
if (!search->val)
break;
} else
- if (hashcode == search->hashcode)
- if (equals(search->key, key))
- return search->val;
+ if (hashcode == search->hashcode)
+ if (equals(search->key, key))
+ return search->val;
index++;
index &= capacitymask;
if (index == oindex)
if (!search->val)
break;
} else
- if (hashcode == search->hashcode)
- if (equals(search->key, key)) {
- _Val v = search->val;
- //empty out this bin
- search->val = (_Val) 1;
- search->key = 0;
- size--;
- return v;
- }
+ if (hashcode == search->hashcode)
+ if (equals(search->key, key)) {
+ _Val v = search->val;
+ //empty out this bin
+ search->val = (_Val) 1;
+ search->key = 0;
+ size--;
+ return v;
+ }
index++;
} while (true);
return (_Val)0;
if (!search->val)
break;
} else
- if (hashcode == search->hashcode)
- if (equals(search->key, key))
- return true;
+ if (hashcode == search->hashcode)
+ if (equals(search->key, key))
+ return true;
index++;
} while (true);
return false;
* arithmetic gets lost in the time required for comparison function calls.
*/
#define SWAP(a, b, count, size, tmp) { \
- count = size; \
+ count = size; \
do { \
- tmp = *a; \
+ tmp = *a; \
*a++ = *b; \
- *b++ = tmp; \
+ *b++ = tmp; \
} while (--count); \
}
/* Copy one block of size size to another. */
-#define COPY(a, b, count, size, tmp1, tmp2) { \
- count = size; \
- tmp1 = a; \
- tmp2 = b; \
+#define COPY(a, b, count, size, tmp1, tmp2) { \
+ count = size; \
+ tmp1 = a; \
+ tmp2 = b; \
do { \
*tmp1++ = *tmp2++; \
} while (--count); \
* j < nmemb, select largest of Ki, Kj and Kj+1.
*/
#define CREATE(initval, nmemb, par_i, child_i, par, child, size, count, tmp) { \
- for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
- par_i = child_i) { \
+ for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
+ par_i = child_i) { \
child = base + child_i * size; \
- if (child_i < nmemb && compar(child, child + size) < 0) { \
+ if (child_i < nmemb && compar(child, child + size) < 0) { \
child += size; \
++child_i; \
- } \
+ } \
par = base + par_i * size; \
if (compar(child, par) <= 0) \
break; \
- SWAP(par, child, count, size, tmp); \
- } \
+ SWAP(par, child, count, size, tmp); \
+ } \
}
/*
*
* XXX Don't break the #define SELECT line, below. Reiser cpp gets upset.
*/
-#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \
+#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \
for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
child = base + child_i * size; \
- if (child_i < nmemb && compar(child, child + size) < 0) { \
+ if (child_i < nmemb && compar(child, child + size) < 0) { \
child += size; \
++child_i; \
- } \
+ } \
par = base + par_i * size; \
COPY(par, child, count, size, tmp1, tmp2); \
- } \
- for (;; ) { \
+ } \
+ for (;; ) { \
child_i = par_i; \
par_i = child_i / 2; \
child = base + child_i * size; \
par = base + par_i * size; \
- if (child_i == 1 || compar(k, par) < 0) { \
+ if (child_i == 1 || compar(k, par) < 0) { \
COPY(child, k, count, size, tmp1, tmp2); \
break; \
- } \
+ } \
COPY(child, par, count, size, tmp1, tmp2); \
- } \
+ } \
}
/*
#define SWAPTYPE_INT 4
#define SWAPTYPE_LONG 5
-#define TYPE_ALIGNED(TYPE, a, es) \
+#define TYPE_ALIGNED(TYPE, a, es) \
(((char *)a - (char *)0) % sizeof(TYPE) == 0 && es % sizeof(TYPE) == 0)
-#define swapcode(TYPE, parmi, parmj, n) { \
- size_t i = (n) / sizeof (TYPE); \
- TYPE *pi = (TYPE *) (parmi); \
- TYPE *pj = (TYPE *) (parmj); \
- do { \
- TYPE t = *pi; \
- *pi++ = *pj; \
- *pj++ = t; \
- } while (--i > 0); \
+#define swapcode(TYPE, parmi, parmj, n) { \
+ size_t i = (n) / sizeof (TYPE); \
+ TYPE *pi = (TYPE *) (parmi); \
+ TYPE *pj = (TYPE *) (parmj); \
+ do { \
+ TYPE t = *pi; \
+ *pi++ = *pj; \
+ *pj++ = t; \
+ } while (--i > 0); \
}
static __inline void
}
}
-#define swap(a, b) do { \
- switch (swaptype) { \
- case SWAPTYPE_INT: { \
- int t = *(int *)(a); \
- *(int *)(a) = *(int *)(b); \
- *(int *)(b) = t; \
- break; \
- } \
- case SWAPTYPE_LONG: { \
- long t = *(long *)(a); \
- *(long *)(a) = *(long *)(b); \
- *(long *)(b) = t; \
- break; \
- } \
- default: \
- swapfunc(a, b, es, swaptype); \
- } \
+#define swap(a, b) do { \
+ switch (swaptype) { \
+ case SWAPTYPE_INT: { \
+ int t = *(int *)(a); \
+ *(int *)(a) = *(int *)(b); \
+ *(int *)(b) = t; \
+ break; \
+ } \
+ case SWAPTYPE_LONG: { \
+ long t = *(long *)(a); \
+ *(long *)(a) = *(long *)(b); \
+ *(long *)(b) = t; \
+ break; \
+ } \
+ default: \
+ swapfunc(a, b, es, swaptype); \
+ } \
} while (0)
#define vecswap(a, b, n) if ((n) > 0) swapfunc(a, b, n, swaptype)
#include "structs.h"
#include "decomposeorderresolver.h"
-#define HASHNEXT(hash, newval) {hash+=newval; hash += hash << 10; hash ^= hash >>6;}
-#define HASHFINAL(hash) {hash += hash <<3; hash ^= hash >> 11; hash += hash << 15;}
+#define HASHNEXT(hash, newval) {hash += newval; hash += hash << 10; hash ^= hash >> 6;}
+#define HASHFINAL(hash) {hash += hash << 3; hash ^= hash >> 11; hash += hash << 15;}
unsigned int table_entry_hash_function(TableEntry *This) {
unsigned int h = 0;
}
unsigned int order_edge_hash_function(OrderEdge *This) {
- uint hash=0;
+ uint hash = 0;
HASHNEXT(hash, (uint)(uintptr_t) This->sink);
HASHNEXT(hash, (uint)(uintptr_t) This->source);
HASHFINAL(hash);
}
unsigned int order_pair_hash_function(OrderPair *This) {
- uint hash=0;
+ uint hash = 0;
HASHNEXT(hash, This->first);
HASHNEXT(hash, This->second);
HASHFINAL(hash);
}
unsigned int doredge_hash_function(DOREdge *key) {
- uint hash=0;
+ uint hash = 0;
HASHNEXT(hash, (uint) key->newfirst);
HASHNEXT(hash, (uint) key->newsecond);
HASHFINAL(hash);
#define VECTOR_H
#include <string.h>
-#define VectorDef(name, type) \
- struct Vector ## name { \
- uint size; \
- uint capacity; \
- type *array; \
- }; \
- typedef struct Vector ## name Vector ## name; \
- Vector ## name * allocVector ## name(uint capacity); \
- Vector ## name * allocDefVector ## name(); \
- Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
- void pushVector ## name(Vector ## name * vector, type item); \
- type lastVector ## name(Vector ## name * vector); \
- void popVector ## name(Vector ## name * vector); \
- type getVector ## name(Vector ## name * vector, uint index); \
- void setExpandVector ## name(Vector ## name * vector, uint index, type item); \
- void setVector ## name(Vector ## name * vector, uint index, type item); \
- uint getSizeVector ## name(const Vector ## name * vector); \
- void setSizeVector ## name(Vector ## name * vector, uint size); \
- void deleteVector ## name(Vector ## name * vector); \
- void clearVector ## name(Vector ## name * vector); \
- void deleteVectorArray ## name(Vector ## name * vector); \
- type *exposeArray ## name(Vector ## name * vector); \
+#define VectorDef(name, type) \
+ struct Vector ## name { \
+ uint size; \
+ uint capacity; \
+ type *array; \
+ }; \
+ typedef struct Vector ## name Vector ## name; \
+ Vector ## name * allocVector ## name(uint capacity); \
+ Vector ## name * allocDefVector ## name(); \
+ Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
+ void pushVector ## name(Vector ## name * vector, type item); \
+ type lastVector ## name(Vector ## name * vector); \
+ void popVector ## name(Vector ## name * vector); \
+ type getVector ## name(Vector ## name * vector, uint index); \
+ void setExpandVector ## name(Vector ## name * vector, uint index, type item); \
+ void setVector ## name(Vector ## name * vector, uint index, type item); \
+ uint getSizeVector ## name(const Vector ## name * vector); \
+ void setSizeVector ## name(Vector ## name * vector, uint size); \
+ void deleteVector ## name(Vector ## name * vector); \
+ void clearVector ## name(Vector ## name * vector); \
+ void deleteVectorArray ## name(Vector ## name * vector); \
+ type *exposeArray ## name(Vector ## name * vector); \
void initVector ## name(Vector ## name * vector, uint capacity); \
- void initDefVector ## name(Vector ## name * vector); \
+ void initDefVector ## name(Vector ## name * vector); \
void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
-#define VectorImpl(name, type, defcap) \
- Vector ## name * allocDefVector ## name() { \
- return allocVector ## name(defcap); \
- } \
- Vector ## name * allocVector ## name(uint capacity) { \
- Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \
- tmp->size = 0; \
- tmp->capacity = capacity; \
- tmp->array = (type *) ourmalloc(sizeof(type) * capacity); \
- return tmp; \
- } \
- Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \
- Vector ## name * tmp = allocVector ## name(capacity); \
- tmp->size = capacity; \
- memcpy(tmp->array, array, capacity * sizeof(type)); \
- return tmp; \
- } \
- void popVector ## name(Vector ## name * vector) { \
- vector->size--; \
- } \
- type lastVector ## name(Vector ## name * vector) { \
- return vector->array[vector->size - 1]; \
- } \
- void setSizeVector ## name(Vector ## name * vector, uint size) { \
- if (size <= vector->size) { \
- vector->size = size; \
- return; \
- } else if (size > vector->capacity) { \
- vector->array = (type *)ourrealloc(vector->array, size * sizeof(type)); \
- vector->capacity = size; \
- } \
+#define VectorImpl(name, type, defcap) \
+ Vector ## name * allocDefVector ## name() { \
+ return allocVector ## name(defcap); \
+ } \
+ Vector ## name * allocVector ## name(uint capacity) { \
+ Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \
+ tmp->size = 0; \
+ tmp->capacity = capacity; \
+ tmp->array = (type *) ourmalloc(sizeof(type) * capacity); \
+ return tmp; \
+ } \
+ Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \
+ Vector ## name * tmp = allocVector ## name(capacity); \
+ tmp->size = capacity; \
+ memcpy(tmp->array, array, capacity * sizeof(type)); \
+ return tmp; \
+ } \
+ void popVector ## name(Vector ## name * vector) { \
+ vector->size--; \
+ } \
+ type lastVector ## name(Vector ## name * vector) { \
+ return vector->array[vector->size - 1]; \
+ } \
+ void setSizeVector ## name(Vector ## name * vector, uint size) { \
+ if (size <= vector->size) { \
+ vector->size = size; \
+ return; \
+ } else if (size > vector->capacity) { \
+ vector->array = (type *)ourrealloc(vector->array, size * sizeof(type)); \
+ vector->capacity = size; \
+ } \
bzero(&vector->array[vector->size], (size - vector->size) * sizeof(type)); \
- vector->size = size; \
- } \
- void pushVector ## name(Vector ## name * vector, type item) { \
- if (vector->size >= vector->capacity) { \
- uint newcap = vector->capacity << 1; \
- vector->array = (type *)ourrealloc(vector->array, newcap * sizeof(type)); \
- vector->capacity = newcap; \
- } \
- vector->array[vector->size++] = item; \
- } \
- type getVector ## name(Vector ## name * vector, uint index) { \
- return vector->array[index]; \
- } \
+ vector->size = size; \
+ } \
+ void pushVector ## name(Vector ## name * vector, type item) { \
+ if (vector->size >= vector->capacity) { \
+ uint newcap = vector->capacity << 1; \
+ vector->array = (type *)ourrealloc(vector->array, newcap * sizeof(type)); \
+ vector->capacity = newcap; \
+ } \
+ vector->array[vector->size++] = item; \
+ } \
+ type getVector ## name(Vector ## name * vector, uint index) { \
+ return vector->array[index]; \
+ } \
void setExpandVector ## name(Vector ## name * vector, uint index, type item) { \
- if (index >= vector->size) \
- setSizeVector ## name(vector, index + 1); \
- setVector ## name(vector, index, item); \
- } \
+ if (index >= vector->size) \
+ setSizeVector ## name(vector, index + 1); \
+ setVector ## name(vector, index, item); \
+ } \
void setVector ## name(Vector ## name * vector, uint index, type item) { \
- vector->array[index] = item; \
- } \
- uint getSizeVector ## name(const Vector ## name * vector) { \
- return vector->size; \
- } \
- void deleteVector ## name(Vector ## name * vector) { \
- ourfree(vector->array); \
- ourfree(vector); \
- } \
- void clearVector ## name(Vector ## name * vector) { \
- vector->size = 0; \
- } \
- type *exposeArray ## name(Vector ## name * vector) { \
- return vector->array; \
- } \
- void deleteVectorArray ## name(Vector ## name * vector) { \
- ourfree(vector->array); \
- } \
- void initVector ## name(Vector ## name * vector, uint capacity) { \
- vector->size = 0; \
- vector->capacity = capacity; \
- vector->array = (type *) ourmalloc(sizeof(type) * capacity); \
- } \
- void initDefVector ## name(Vector ## name * vector) { \
- initVector ## name(vector, defcap); \
- } \
- void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) { \
- initVector ## name(vector, capacity); \
- vector->size = capacity; \
- memcpy(vector->array, array, capacity * sizeof(type)); \
+ vector->array[index] = item; \
+ } \
+ uint getSizeVector ## name(const Vector ## name * vector) { \
+ return vector->size; \
+ } \
+ void deleteVector ## name(Vector ## name * vector) { \
+ ourfree(vector->array); \
+ ourfree(vector); \
+ } \
+ void clearVector ## name(Vector ## name * vector) { \
+ vector->size = 0; \
+ } \
+ type *exposeArray ## name(Vector ## name * vector) { \
+ return vector->array; \
+ } \
+ void deleteVectorArray ## name(Vector ## name * vector) { \
+ ourfree(vector->array); \
+ } \
+ void initVector ## name(Vector ## name * vector, uint capacity) { \
+ vector->size = 0; \
+ vector->capacity = capacity; \
+ vector->array = (type *) ourmalloc(sizeof(type) * capacity); \
+ } \
+ void initDefVector ## name(Vector ## name * vector) { \
+ initVector ## name(vector, defcap); \
+ } \
+ void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) { \
+ initVector ## name(vector, capacity); \
+ vector->size = capacity; \
+ memcpy(vector->array, array, capacity * sizeof(type)); \
}
#endif
}
void ElementEncoding::allocInUseArrayElement(uint size) {
- uint bytes = ((size + ((1 << 9) - 1)) >> 6) & ~7;//Depends on size of inUseArray
+ uint bytes = ((size + 63) >> 3) & ~7; //Depends on size of inUseArray
inUseArray = (uint64_t *) ourcalloc(1, bytes);
}
};
struct {
uint64_t offset;/* Value = offset + encoded number (interpretted according to isBinaryValSigned) */
- uint64_t low;/* Lowest value to encode */
+ uint64_t low; /* Lowest value to encode */
uint64_t high;/* High value to encode. If low > high, we assume wrap around to include 0. */
uint numBits;
bool isBinaryValSigned;
#define READBUFFERSIZE 16384
Deserializer::Deserializer(const char *file) :
- buffer((char *)ourmalloc(READBUFFERSIZE)),
+ buffer((char *) ourmalloc(READBUFFERSIZE)),
bufferindex(0),
bufferbytes(0),
buffercap(READBUFFERSIZE),
solver(new CSolver())
{
filedesc = open(file, O_RDONLY);
-
+
if (filedesc < 0) {
exit(-1);
}
}
ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
- char * out = (char * ) __buf;
+ char *out = (char * ) __buf;
size_t totalbytesread = 0;
while (bytestoread) {
if (bufferbytes != 0) {
out += bytestocopy;
bytestoread -= bytestocopy;
} else {
- size_t bytesread=read (filedesc, buffer, buffercap);
+ size_t bytesread = read (filedesc, buffer, buffercap);
bufferindex = 0;
bufferbytes = bytesread;
if (bytesread == 0) {
ASSERT(map.contains(tmp.getBoolean()));
b_ptr = (Boolean *) map.get(tmp.getBoolean());
BooleanEdge res(b_ptr);
- bool isTopLevel;
- myread(&isTopLevel, sizeof(bool));
- if(isTopLevel){
- solver->addConstraint(isNegated ? res.negate() : res);
- }
+ bool isTopLevel;
+ myread(&isTopLevel, sizeof(bool));
+ if (isTopLevel) {
+ solver->addConstraint(isNegated ? res.negate() : res);
+ }
}
void Deserializer::deserializeBooleanVar() {
myread(&isRange, sizeof(bool));
bool isMutable;
myread(&isMutable, sizeof(bool));
- if(isRange){
+ if (isRange) {
uint64_t low;
myread(&low, sizeof(uint64_t));
uint64_t high;
map.put(s_ptr, new Set(type, low, high));
} else {
Set *set = NULL;
- if(isMutable) {
+ if (isMutable) {
set = new MutableSet(type);
}
uint size;
myread(&size, sizeof(uint));
Vector<uint64_t> members;
- for(uint i=0; i<size; i++) {
+ for (uint i = 0; i < size; i++) {
uint64_t mem;
myread(&mem, sizeof(uint64_t));
- if(isMutable) {
- ((MutableSet*) set)->addElementMSet(mem);
+ if (isMutable) {
+ ((MutableSet *) set)->addElementMSet(mem);
} else {
members.push(mem);
}
}
- if(!isMutable) {
+ if (!isMutable) {
set = solver->createSet(type, members.expose(), size);
}
map.put(s_ptr, set);
void Serializer::flushBuffer() {
ssize_t datatowrite = bufferoffset;
ssize_t index = 0;
- while(datatowrite) {
+ while (datatowrite) {
ssize_t byteswritten = write(filedesc, &buffer[index], datatowrite);
if (byteswritten == -1)
exit(-1);
datatowrite -= byteswritten;
index += byteswritten;
}
- bufferoffset=0;
+ bufferoffset = 0;
}
Serializer::~Serializer() {
}
void Serializer::mywrite(const void *__buf, size_t __n) {
- char *towrite=(char *) __buf;
- if (__n > SERIALBUFFERLENGTH *2) {
+ char *towrite = (char *) __buf;
+ if (__n > SERIALBUFFERLENGTH * 2) {
if (bufferoffset != 0)
flushBuffer();
while (__n > 0) {
- ssize_t result=write(filedesc, &towrite, __n);
+ ssize_t result = write(filedesc, &towrite, __n);
if (result != (ssize_t) __n)
exit(-1);
towrite += result;
}
} else {
do {
- uint spacefree = bufferlength-bufferoffset;
+ uint spacefree = bufferlength - bufferoffset;
uint datatowrite = spacefree > __n ? __n : spacefree;
memcpy(&buffer[bufferoffset], towrite, datatowrite);
bufferoffset += datatowrite;
} else {
return;
}
- } while(true);
+ } while (true);
}
}
CMEMALLOC;
private:
void flushBuffer();
- char * buffer;
+ char *buffer;
uint bufferoffset;
uint bufferlength;
int filedesc;
-void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel=false);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel = false);
#endif/* SERIALIZER_H */
#include "csolver.h"
#include "autotuner.h"
-int main(int argc, char ** argv){
- if(argc < 2){
+int main(int argc, char **argv) {
+ if (argc < 2) {
printf("You should specify file names ...");
- exit(-1);
+ exit(-1);
}
- CSolver * solvers[argc-1];
+ CSolver *solvers[argc - 1];
AutoTuner *autotuner = new AutoTuner(100);
- for(int i = 1; i < argc; i++) {
- solvers[i-1] = CSolver::deserialize(argv[i]);
- autotuner->addProblem(solvers[i-1]);
+ for (int i = 1; i < argc; i++) {
+ solvers[i - 1] = CSolver::deserialize(argv[i]);
+ autotuner->addProblem(solvers[i - 1]);
}
autotuner->tune();
delete autotuner;
-
- for(int i = 1; i < argc; i++) {
- delete solvers[i-1];
+
+ for (int i = 1; i < argc; i++) {
+ delete solvers[i - 1];
}
return 1;
#include "csolver.h"
-int main(int argc, char ** argv){
- if(argc < 2){
+int main(int argc, char **argv) {
+ if (argc < 2) {
printf("You should specify file names ...");
- exit(-1);
+ exit(-1);
}
- for(int i = 1; i < argc; i++) {
- CSolver* solver = CSolver::deserialize(argv[i]);
+ for (int i = 1; i < argc; i++) {
+ CSolver *solver = CSolver::deserialize(argv[i]);
solver->printConstraints();
- int value=solver->solve();
- if (value ==1) {
+ int value = solver->solve();
+ if (value == 1) {
printf("%s is SAT\n", argv[i]);
} else {
printf("%s is UNSAT\n", argv[i]);
#include "csolver.h"
-int main(int argc, char ** argv){
- if(argc < 2){
+int main(int argc, char **argv) {
+ if (argc < 2) {
printf("You should specify file names ...");
- exit(-1);
+ exit(-1);
}
- for(int i = 1; i < argc; i++) {
- CSolver* solver = CSolver::deserialize(argv[i]);
- int value=solver->solve();
- if (value ==1) {
+ for (int i = 1; i < argc; i++) {
+ CSolver *solver = CSolver::deserialize(argv[i]);
+ int value = solver->solve();
+ if (value == 1) {
printf("%s is SAT\n", argv[i]);
} else {
printf("%s is UNSAT\n", argv[i]);
#include "csolver.h"
-int main(int argc, char ** argv){
- if(argc < 2){
+int main(int argc, char **argv) {
+ if (argc < 2) {
printf("You should specify file names ...");
- exit(-1);
+ exit(-1);
}
- for(int i = 1; i < argc; i++) {
- CSolver* solver = CSolver::deserialize(argv[i]);
- int value=solver->solve();
- if (value ==1) {
+ for (int i = 1; i < argc; i++) {
+ CSolver *solver = CSolver::deserialize(argv[i]);
+ int value = solver->solve();
+ if (value == 1) {
printf("%s is SAT\n", argv[i]);
} else {
printf("%s is UNSAT\n", argv[i]);
#include "csolver.h"
-int main(int argc, char ** argv){
- if(argc != 2){
+int main(int argc, char **argv) {
+ if (argc != 2) {
printf("You only specify the name of the file ...");
- exit(-1);
+ exit(-1);
}
- CSolver* solver = CSolver::deserialize(argv[1]);
+ CSolver *solver = CSolver::deserialize(argv[1]);
solver->printConstraints();
- delete solver;
+ delete solver;
return 1;
-
+
}
if (!(expr)) { \
fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
/* print_trace(); // Trace printing may cause dynamic memory allocation */ \
- assert_hook(); \
- exit(EXIT_FAILURE); \
- } \
+ assert_hook(); \
+ exit(EXIT_FAILURE); \
+ } \
} while (0)
#else
#define ASSERT(expr) \
size = allElements.getSize();
for (uint i = 0; i < size; i++) {
- Element* el = allElements.get(i);
+ Element *el = allElements.get(i);
delete el;
}
delete satEncoder;
}
-void CSolver::resetSolver(){
- //serialize();
- uint size = allBooleans.getSize();
+void CSolver::resetSolver() {
+ //serialize();
+ uint size = allBooleans.getSize();
for (uint i = 0; i < size; i++) {
delete allBooleans.get(i);
}
size = allElements.getSize();
for (uint i = 0; i < size; i++) {
- Element* el = allElements.get(i);
+ Element *el = allElements.get(i);
delete el;
}
delete allFunctions.get(i);
}
delete boolTrue.getBoolean();
- allBooleans.clear();
- allSets.clear();
- allElements.clear();
- allTables.clear();
- allPredicates.clear();
- allOrders.clear();
- allFunctions.clear();
- constraints.reset();
- activeOrders.reset();
- boolMap.reset();
+ allBooleans.clear();
+ allSets.clear();
+ allElements.clear();
+ allTables.clear();
+ allPredicates.clear();
+ allOrders.clear();
+ allFunctions.clear();
+ constraints.reset();
+ activeOrders.reset();
+ boolMap.reset();
elemMap.reset();
-
- boolTrue = BooleanEdge(new BooleanConst(true));
+
+ boolTrue = BooleanEdge(new BooleanConst(true));
boolFalse = boolTrue.negate();
- unsat = false;
- elapsedTime = 0;
- tuner = NULL;
- satEncoder->resetSATEncoder();
-
+ unsat = false;
+ elapsedTime = 0;
+ tuner = NULL;
+ satEncoder->resetSATEncoder();
+
}
CSolver *CSolver::clone() {
return copy;
}
-CSolver* CSolver::deserialize(const char * file){
+CSolver *CSolver::deserialize(const char *file) {
model_print("deserializing ...\n");
Deserializer deserializer(file);
return deserializer.deserialize();
void CSolver::serialize() {
model_print("serializing ...\n");
char buffer[255];
- long long nanotime=getTimeNano();
- int numchars=sprintf(buffer, "DUMP%llu", nanotime);
+ long long nanotime = getTimeNano();
+ int numchars = sprintf(buffer, "DUMP%llu", nanotime);
Serializer serializer(buffer);
SetIteratorBooleanEdge *it = getConstraints();
while (it->hasNext()) {
boolMap.put(constraint, constraint);
constraint->updateParents();
if (order->graph != NULL) {
- OrderGraph *graph=order->graph;
- OrderNode *from=graph->lookupOrderNodeFromOrderGraph(first);
+ OrderGraph *graph = order->graph;
+ OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
if (from != NULL) {
- OrderNode *to=graph->lookupOrderNodeFromOrderGraph(second);
+ OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
if (to != NULL) {
- OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(from, to);
+ OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
OrderEdge *invedge;
if (edge != NULL && edge->mustPos) {
replaceBooleanWithTrueNoRemove(constraint);
} else if (edge != NULL && edge->mustNeg) {
replaceBooleanWithFalseNoRemove(constraint);
- } else if ((invedge=graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+ } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
&& invedge->mustPos) {
replaceBooleanWithFalseNoRemove(constraint);
}
}
/** Computes static ordering information to allow isTrue/isFalse
- queries on newly created orders to work. */
+ queries on newly created orders to work. */
void CSolver::inferFixedOrder(Order *order) {
if (order->graph != NULL) {
order->graph = buildMustOrderGraph(order);
reachMustAnalysis(this, order->graph, true);
}
-
+
void CSolver::inferFixedOrders() {
SetIteratorOrder *orderit = activeOrders.iterator();
while (orderit->hasNext()) {
#define NANOSEC 1000000000.0
int CSolver::solve() {
- long long starttime = getTimeNano();
+ long long starttime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
tuner = new DefaultTuner();
computePolarities(this);
long long time2 = getTimeNano();
- model_print("Polarity time: %f\n", (time2-starttime)/NANOSEC);
+ model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
Preprocess pp(this);
pp.doTransform();
long long time3 = getTimeNano();
- model_print("Preprocess time: %f\n", (time3-time2)/NANOSEC);
-
+ model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+
DecomposeOrderTransform dot(this);
dot.doTransform();
long long time4 = getTimeNano();
- model_print("Decompose Order: %f\n", (time4-time3)/NANOSEC);
+ model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
IntegerEncodingTransform iet(this);
iet.doTransform();
naiveEncodingDecision(this);
long long time5 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time5-time4)/NANOSEC);
-
+ model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
+
long long startTime = getTimeNano();
satEncoder->encodeAllSATEncoder(this);
long long endTime = getTimeNano();
elapsedTime = endTime - startTime;
- model_print("Elapse Encode time: %f\n", elapsedTime/NANOSEC);
-
+ model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
+
model_print("Is problem UNSAT after encoding: %d\n", unsat);
int result = unsat ? IS_UNSAT : satEncoder->solve();
model_print("Result Computed in CSolver: %d\n", result);
-
+
if (deleteTuner) {
delete tuner;
tuner = NULL;
public:
CSolver();
~CSolver();
- void resetSolver();
+ void resetSolver();
/** This function creates a set containing the elements passed in the array. */
Set *createSet(VarType type, uint64_t *elements, uint num);
void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
CSolver *clone();
void serialize();
- static CSolver* deserialize(const char * file);
+ static CSolver *deserialize(const char *file);
void autoTune(uint budget);
void inferFixedOrders();
void inferFixedOrder(Order *order);
-
+
void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
#endif
-#define CMEMALLOC \
- 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 CMEMALLOC \
+ 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