class Boolean : public ASTNode {
private:
- static uint64_t counter;
+ static uint64_t counter;
public:
Boolean(ASTNodeType _type);
virtual ~Boolean() {}
BooleanValue boolVal;
Vector<ASTNode *> parents;
virtual void updateParents() {}
- uint64_t id;
+ uint64_t id;
CMEMALLOC;
};
HashtableOrderPair *Order::getOrderPairTable() {
ASSERT( encoding.resolver != NULL);
- if (OrderPairResolver * t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
+ if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
return t->getOrderPairTable();
} else {
ASSERT(0);
}
}
-void CSolver::handleFunction(ElementFunction * ef, BooleanEdge child) {
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
BooleanEdge childNegate = child.negate();
elemMap.remove(ef);
if (ef->overflowstatus == child) {
} else {
BooleanLogic *logicop = (BooleanLogic *) parent;
boolMap.remove(logicop); //could change parent's hash
-
+
uint parentsize = logicop->inputs.getSize();
for (uint j = 0; j < parentsize; j++) {
BooleanEdge b = logicop->inputs.get(j);
EncodingSubGraph *subgraph = graphMap.get(n);
DEBUG("graphMap.get(subgraph=%p, n=%p)\n", subgraph, n);
if (subgraph == NULL) {
- encoding->encodingArrayInitialization();
- continue;
+ encoding->encodingArrayInitialization();
+ continue;
}
uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
return;
EncodingSubGraph *leftGraph = graphMap.get(left);
- DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
+ DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
EncodingSubGraph *rightGraph = graphMap.get(right);
- DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
+ DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
if (leftGraph == NULL && rightGraph != NULL) {
EncodingNode *tmp = left; left = right; right = tmp;
EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
Boolean *bdst = dst.getBoolean();
bool isNegated = dst.isNegated();
if (isNegated)
- p=negatePolarity(p);
+ p = negatePolarity(p);
updatePolarity(bdst, p);
}
if (This->undefStatus) {
computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
}
- for(uint i=0; i < This->inputs.getSize(); i++) {
- Element * e = This->inputs.get(i);
+ for (uint i = 0; i < This->inputs.getSize(); i++) {
+ Element *e = This->inputs.get(i);
computeElement(e);
}
}
computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
}
- for(uint i=0; i < ef->inputs.getSize(); i++) {
- Element * echild = ef->inputs.get(i);
+ for (uint i = 0; i < ef->inputs.getSize(); i++) {
+ Element *echild = ef->inputs.get(i);
computeElement(echild);
- }
+ }
}
}
ElementOpt::ElementOpt(CSolver *_solver)
: Transform(_solver),
- updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+ updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
{
}
void ElementOpt::doTransform() {
if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
return;
-
+
SetIteratorBooleanEdge *iterator = solver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
workList.push((BooleanPredicate *)constraint.getBoolean());
}
while (workList.getSize() != 0) {
- BooleanPredicate * pred = workList.last(); workList.pop();
+ BooleanPredicate *pred = workList.last(); workList.pop();
processPredicate(pred);
}
delete iterator;
}
-void ElementOpt::processPredicate(BooleanPredicate * pred) {
+void ElementOpt::processPredicate(BooleanPredicate *pred) {
uint numInputs = pred->inputs.getSize();
if (numInputs != 2)
return;
- Predicate * p = pred->getPredicate();
+ Predicate *p = pred->getPredicate();
if (p->type == TABLEPRED)
- return;
+ return;
- PredicateOperator * pop = (PredicateOperator *) p;
+ PredicateOperator *pop = (PredicateOperator *) p;
CompOp op = pop->getOp();
- Element * left = pred->inputs.get(0);
- Element * right = pred->inputs.get(1);
+ Element *left = pred->inputs.get(0);
+ Element *right = pred->inputs.get(1);
if (left->type == ELEMCONST) {
- Element * tmp = left;
+ Element *tmp = left;
left = right;
right = tmp;
op = flipOp(op);
} else if (right->type != ELEMCONST)
return;
- if (left->type !=ELEMSET)
+ if (left->type != ELEMSET)
return;
-
+
if (op == SATC_EQUALS) {
handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
} else if (updateSets) {
}
void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
- Predicate * p = pred->getPredicate();
- PredicateOperator * pop = (PredicateOperator *) p;
+ Predicate *p = pred->getPredicate();
+ PredicateOperator *pop = (PredicateOperator *) p;
CompOp op = pop->getOp();
if (pred->isFalse()) {
ASSERT(0);
}
- Set * s = var->getRange();
+ Set *s = var->getRange();
if (s->isRange)
return;
-
+
uint size = s->getSize();
uint64_t elemArray[size];
uint count = 0;
uint64_t cvalue = value->value;
- switch(op) {
+ switch (op) {
case SATC_LT: {
- for(uint i=0; i<size; i++) {
+ for (uint i = 0; i < size; i++) {
uint64_t val = s->getElement(i);
if (val < cvalue)
elemArray[count++] = val;
break;
}
case SATC_GT: {
- for(uint i=0; i<size; i++) {
+ for (uint i = 0; i < size; i++) {
uint64_t val = s->getElement(i);
if (val > cvalue)
elemArray[count++] = val;
break;
}
case SATC_LTE: {
- for(uint i=0; i<size; i++) {
+ for (uint i = 0; i < size; i++) {
uint64_t val = s->getElement(i);
if (val <= cvalue)
elemArray[count++] = val;
break;
}
case SATC_GTE: {
- for(uint i=0; i<size; i++) {
+ for (uint i = 0; i < size; i++) {
uint64_t val = s->getElement(i);
if (val >= cvalue)
elemArray[count++] = val;
}
break;
}
-
+
default:
ASSERT(0);
}
if (size == count)
return;
-
+
Set *newset = solver->createSet(s->type, elemArray, count);
solver->elemMap.remove(var);
var->set = newset;
solver->elemMap.put(var, var);
if (count == 1) {
- ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+ ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
replaceVarWithConst(pred, var, elemconst);
}
}
void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
- Set * s = var->getRange();
+ Set *s = var->getRange();
if (s->isRange)
return;
uint size = s->getSize();
uint64_t elemArray[size];
uint count = 0;
uint64_t cvalue = value->value;
- for(uint i=0; i<size; i++) {
+ for (uint i = 0; i < size; i++) {
uint64_t val = s->getElement(i);
if (val != cvalue)
elemArray[count++] = val;
solver->elemMap.put(var, var);
if (count == 1) {
- ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+ ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
replaceVarWithConst(pred, var, elemconst);
}
}
-void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {
+void ElementOpt::replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
uint size = var->parents.getSize();
- for(uint i=0; i < size; i++) {
- ASTNode * parent = var->parents.get(i);
+ for (uint i = 0; i < size; i++) {
+ ASTNode *parent = var->parents.get(i);
if (parent->type == PREDICATEOP && pred != parent) {
- BooleanPredicate * newpred = (BooleanPredicate *) parent;
- for(uint j=0; j < newpred->inputs.getSize(); j++) {
- Element * e = newpred->inputs.get(j);
+ BooleanPredicate *newpred = (BooleanPredicate *) parent;
+ for (uint j = 0; j < newpred->inputs.getSize(); j++) {
+ Element *e = newpred->inputs.get(j);
if (e == var) {
solver->boolMap.remove(newpred);
newpred->inputs.set(j, value);
void processPredicate(BooleanPredicate *);
void handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
void handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
- void replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value);
+ void replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
void constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
Vector<BooleanPredicate *> workList;
Edge cloneEdge(Edge e) {
if (edgeIsVarConst(e))
return e;
- Node * node = getNodePtrFromEdge(e);
+ Node *node = getNodePtrFromEdge(e);
bool isneg = isNegEdge(e);
uint numEdges = node->numEdges;
- Node * clone = allocBaseNode(node->type, numEdges);
- for(uint i=0; i < numEdges; i++) {
+ Node *clone = allocBaseNode(node->type, numEdges);
+ for (uint i = 0; i < numEdges; i++) {
clone->edges[i] = cloneEdge(node->edges[i]);
}
return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
void freeEdgeRec(Edge e) {
if (edgeIsVarConst(e))
return;
- Node * node = getNodePtrFromEdge(e);
+ Node *node = getNodePtrFromEdge(e);
uint numEdges = node->numEdges;
- for(uint i=0; i < numEdges; i++) {
+ for (uint i = 0; i < numEdges; i++) {
freeEdgeRec(node->edges[i]);
}
ourfree(node);
void freeEdge(Edge e) {
if (edgeIsVarConst(e))
return;
- Node * node = getNodePtrFromEdge(e);
+ Node *node = getNodePtrFromEdge(e);
ourfree(node);
}
-void freeEdgesRec(uint numEdges, Edge * earray) {
- for(uint i=0; i < numEdges; i++) {
+void freeEdgesRec(uint numEdges, Edge *earray) {
+ for (uint i = 0; i < numEdges; i++) {
Edge e = earray[i];
freeEdgeRec(e);
}
}
void freeEdgeCNF(Edge e) {
- Node * node = getNodePtrFromEdge(e);
+ Node *node = getNodePtrFromEdge(e);
uint numEdges = node->numEdges;
- for(uint i=0; i < numEdges; i++) {
+ for (uint i = 0; i < numEdges; i++) {
Edge ec = node->edges[i];
if (!edgeIsVarConst(ec)) {
ourfree(ec.node_ptr);
ourfree(node);
}
-void addEdgeToResizeNode(Node ** node, Edge e) {
+void addEdgeToResizeNode(Node **node, Edge e) {
Node *currnode = *node;
if (currnode->capacity == currnode->numEdges) {
Node *newnode = allocResizeNode( currnode->capacity << 1);
newnode->numEdges = currnode->numEdges;
memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
ourfree(currnode);
- *node=newnode;
+ *node = newnode;
currnode = newnode;
}
currnode->edges[currnode->numEdges++] = e;
}
-void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
- Node * currnode = *node;
+void mergeFreeNodeToResizeNode(Node **node, Node *innode) {
+ Node *currnode = *node;
uint currEdges = currnode->numEdges;
uint inEdges = innode->numEdges;
-
+
uint newsize = currEdges + inEdges;
if (newsize >= currnode->capacity) {
if (newsize < innode->capacity) {
newnode->numEdges = currnode->numEdges;
memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
ourfree(currnode);
- *node=newnode;
+ *node = newnode;
currnode = newnode;
}
} else {
ourfree(innode);
}
-void mergeNodeToResizeNode(Node **node, Node * innode) {
- Node * currnode = *node;
+void mergeNodeToResizeNode(Node **node, Node *innode) {
+ Node *currnode = *node;
uint currEdges = currnode->numEdges;
uint inEdges = innode->numEdges;
uint newsize = currEdges + inEdges;
newnode->numEdges = currnode->numEdges;
memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
ourfree(currnode);
- *node=newnode;
+ *node = newnode;
currnode = newnode;
}
memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
ASSERT(!isNodeEdge(e1));
if (!sameSignEdge(e1, e2)) {
freeEdgesRec(lowindex + 1, edges);
- freeEdgesRec(numEdges-initindex, &edges[initindex]);
+ freeEdgesRec(numEdges - initindex, &edges[initindex]);
return E_False;
}
} else
Edge *e0edges = getEdgeArray(edges[0]);
Edge *e1edges = getEdgeArray(edges[1]);
if (sameNodeOppSign(e0edges[0], e1edges[0])) {
- Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+ Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
freeEdge(edges[0]);
freeEdge(edges[1]);
return result;
} else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
- Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+ Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
freeEdge(edges[0]);
freeEdge(edges[1]);
return result;
} else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
- Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+ Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
freeEdge(edges[0]);
freeEdge(edges[1]);
return result;
} else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
- Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+ Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
freeEdge(edges[0]);
freeEdge(edges[1]);
return result;
Node *nvec = vec.node_ptr;
uint nvecedges = nvec->numEdges;
- for(uint i=0; i < nvecedges; i++) {
+ for (uint i = 0; i < nvecedges; i++) {
Edge ce = nvec->edges[i];
if (!edgeIsVarConst(ce)) {
Node *cne = ce.node_ptr;
nvec->edges[i] = (Edge) {clause};
}
}
- nvec->numVars+=nvecedges;
+ nvec->numVars += nvecedges;
return vec;
}
-Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
+Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
Node *nnewvec = newvec.node_ptr;
Node *ncnfform = cnfform.node_ptr;
uint newvecedges = nnewvec->numEdges;
uint cnfedges = ncnfform->numEdges;
uint newvecvars = nnewvec->numVars;
uint cnfvars = ncnfform->numVars;
-
+
if (cnfedges > 3 ||
((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
Edge proxyVar = constraintNewVar(cnf);
- if (newvecedges == 1 || cnfedges ==1) {
+ if (newvecedges == 1 || cnfedges == 1) {
if (cnfedges != 1) {
Node *tmp = nnewvec;
nnewvec = ncnfform;
Edge e = ncnfform->edges[0];
if (!edgeIsVarConst(e)) {
Node *n = e.node_ptr;
- for(uint i=0; i < newvecedges; i++) {
+ for (uint i = 0; i < newvecedges; i++) {
Edge ce = nnewvec->edges[i];
if (isNodeEdge(ce)) {
Node *cne = ce.node_ptr;
}
nnewvec->numVars += newvecedges * n->numVars;
} else {
- for(uint i=0; i < newvecedges; i++) {
+ for (uint i = 0; i < newvecedges; i++) {
Edge ce = nnewvec->edges[i];
if (!edgeIsVarConst(ce)) {
Node *cne = ce.node_ptr;
}
nnewvec->numVars += newvecedges;
}
- freeEdgeCNF((Edge){ncnfform});
+ freeEdgeCNF((Edge) {ncnfform});
return (Edge) {nnewvec};
}
-
- Node * result = allocResizeNode(1);
- for(uint i=0; i <newvecedges; i++) {
+ Node *result = allocResizeNode(1);
+
+ for (uint i = 0; i < newvecedges; i++) {
Edge nedge = nnewvec->edges[i];
uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
- for(uint j=0; j < cnfedges; j++) {
+ for (uint j = 0; j < cnfedges; j++) {
Edge cedge = ncnfform->edges[j];
uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
if (equalsEdge(cedge, nedge)) {
} else {
addEdgeToResizeNode(&clause, cedge);
}
- addEdgeToResizeNode(&result, (Edge){clause});
+ addEdgeToResizeNode(&result, (Edge) {clause});
result->numVars += clause->numEdges;
}
//otherwise skip
return (Edge) {newvec};
}
bool negated = isNegEdge(input);
- Node * node = getNodePtrFromEdge(input);
+ Node *node = getNodePtrFromEdge(input);
NodeType type = node->type;
if (!negated) {
if (type == NodeType_AND) {
//AND case
Node *newvec = allocResizeNode(node->numEdges);
uint numEdges = node->numEdges;
- for(uint i = 0; i < numEdges; i++) {
+ for (uint i = 0; i < numEdges; i++) {
Edge e = simplifyCNF(cnf, node->edges[i]);
uint enumvars = e.node_ptr->numVars;
mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
//free temporary nodes
ourfree(getNodePtrFromEdge(thencons));
ourfree(getNodePtrFromEdge(elsecons));
- Node * result = thencnf.node_ptr;
- uint elsenumvars=elsecnf.node_ptr->numVars;
+ Node *result = thencnf.node_ptr;
+ uint elsenumvars = elsecnf.node_ptr->numVars;
mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
- result->numVars+=elsenumvars;
+ result->numVars += elsenumvars;
return (Edge) {result};
}
} else {
uint numEdges = node->numEdges;
Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
- for(uint i = 1; i < numEdges; i++) {
+ for (uint i = 1; i < numEdges; i++) {
Edge e = node->edges[i];
Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
newvec = disjoinAndFree(cnf, newvec, cnfform);
Edge thencons = createNode(NodeType_AND, 2, thenedges);
Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
Edge elsecons = createNode(NodeType_AND, 2, elseedges);
-
+
Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
Edge result = simplifyCNF(cnf, combined);
}
void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
- Node * andNode = cnfform.node_ptr;
+ Node *andNode = cnfform.node_ptr;
int orvar = getEdgeVar(eorvar);
ASSERT(orvar != 0);
uint numEdges = andNode->numEdges;
- for(uint i=0; i < numEdges; i++) {
+ for (uint i = 0; i < numEdges; i++) {
Edge e = andNode->edges[i];
if (edgeIsVarConst(e)) {
int array[2] = {getEdgeVar(e), orvar};
ASSERT(array[0] != 0);
addArrayClauseLiteral(cnf->solver, 2, array);
} else {
- Node * clause = e.node_ptr;
+ Node *clause = e.node_ptr;
uint cnumEdges = clause->numEdges + 1;
if (cnumEdges > cnf->asize) {
cnf->asize = cnumEdges << 1;
ourfree(cnf->array);
cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
}
- int * array = cnf->array;
- for(uint j=0; j < (cnumEdges - 1); j++) {
+ int *array = cnf->array;
+ for (uint j = 0; j < (cnumEdges - 1); j++) {
array[j] = getEdgeVar(clause->edges[j]);
ASSERT(array[j] != 0);
}
}
void outputCNF(CNF *cnf, Edge cnfform) {
- Node * andNode = cnfform.node_ptr;
+ Node *andNode = cnfform.node_ptr;
uint numEdges = andNode->numEdges;
- for(uint i=0; i < numEdges; i++) {
+ for (uint i = 0; i < numEdges; i++) {
Edge e = andNode->edges[i];
if (edgeIsVarConst(e)) {
int array[1] = {getEdgeVar(e)};
ASSERT(array[0] != 0);
addArrayClauseLiteral(cnf->solver, 1, array);
} else {
- Node * clause = e.node_ptr;
+ Node *clause = e.node_ptr;
uint cnumEdges = clause->numEdges;
if (cnumEdges > cnf->asize) {
cnf->asize = cnumEdges << 1;
ourfree(cnf->array);
cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
}
- int * array = cnf->array;
- for(uint j=0; j < cnumEdges; j++) {
+ int *array = cnf->array;
+ for (uint j = 0; j < cnumEdges; j++) {
array[j] = getEdgeVar(clause->edges[j]);
ASSERT(array[j] != 0);
}
printCNF(constraint);
model_print("\n******************************\n");
#endif
-
+
Edge cnfform = simplifyCNF(cnf, constraint);
freeEdgeRec(constraint);
outputCNF(cnf, cnfform);
}
void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
- //TO WRITE....
+ //TO WRITE....
}
Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
uint varcount;
uint asize;
IncrementalSolver *solver;
- int * array;
+ int *array;
long long solveTime;
long long encodeTime;
bool unsat;
Node *allocBaseNode(NodeType type, uint numEdges);
Node *allocResizeNode(uint capacity);
Edge cloneEdge(Edge e);
-void addEdgeToResizeNode(Node ** node, Edge e);
-void mergeFreeNodeToResizeNode(Node **node, Node * innode);
-void mergeNodeToResizeNode(Node **node, Node * innode);
+void addEdgeToResizeNode(Node **node, Edge e);
+void mergeFreeNodeToResizeNode(Node **node, Node *innode);
+void mergeNodeToResizeNode(Node **node, Node *innode);
void freeEdgeRec(Edge e);
void outputCNF(CNF *cnf, Edge cnfform);
void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
#include "predicate.h"
-void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
+void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
uint numParents = elem->parents.getSize();
uint posPolarity = 0;
uint negPolarity = 0;
if (elem->type == ELEMFUNCRETURN) {
memo = true;
}
- for(uint i = 0; i < numParents; i++) {
- ASTNode * node = elem->parents.get(i);
+ for (uint i = 0; i < numParents; i++) {
+ ASTNode *node = elem->parents.get(i);
if (node->type == PREDICATEOP) {
- BooleanPredicate * pred = (BooleanPredicate *) node;
+ BooleanPredicate *pred = (BooleanPredicate *) node;
Polarity polarity = pred->polarity;
FunctionEncodingType encType = pred->encoding.type;
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior;
- Polarity tpolarity=polarity;
+ Polarity tpolarity = polarity;
if (generateNegation)
tpolarity = negatePolarity(tpolarity);
- if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+ if (undefStatus == SATC_FLAGFORCEUNDEFINED)
tpolarity = P_BOTHTRUEFALSE;
if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
memo = true;
if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
memo = true;
} else if (pred->predicate->type == OPERATORPRED) {
- if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
- Polarity tpolarity = polarity;
- if (generateNegation)
- tpolarity = negatePolarity(tpolarity);
- PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
- uint numDomains = pred->inputs.getSize();
- bool isConstant = true;
- for (uint i = 0; i < numDomains; i++) {
- Element *e = pred->inputs.get(i);
- if (elem != e && e->type != ELEMCONST) {
- isConstant = false;
- }
+ if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
+ Polarity tpolarity = polarity;
+ if (generateNegation)
+ tpolarity = negatePolarity(tpolarity);
+ PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
+ uint numDomains = pred->inputs.getSize();
+ bool isConstant = true;
+ for (uint i = 0; i < numDomains; i++) {
+ Element *e = pred->inputs.get(i);
+ if (elem != e && e->type != ELEMCONST) {
+ isConstant = false;
}
- if (predicate->getOp() == SATC_EQUALS) {
+ }
+ if (predicate->getOp() == SATC_EQUALS) {
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+ posPolarity++;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+ negPolarity++;
+ } else {
+ if (isConstant) {
if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
posPolarity++;
if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
negPolarity++;
} else {
- if (isConstant) {
- if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
- posPolarity++;
- if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
- negPolarity++;
- } else {
- if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
- memo = true;
- if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
- memo = true;
- }
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+ memo = true;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+ memo = true;
}
}
- } else {
+ }
+ } else {
ASSERT(0);
}
} else if (node->type == ELEMFUNCRETURN) {
if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
if (elemEnc->numVars == 0)
return E_True;
-
+
if (elemEnc->encoding != EENC_NONE && elemEnc->numVars > 1) {
if (impliesPolarity(elemEnc->polarityArray[i], p)) {
return elemEnc->edgeArray[i];
generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_BOTHTRUEFALSE);
elemEnc->polarityArray[i] = p;
} else if (!impliesPolarity(elemEnc->polarityArray[i], P_TRUE) && impliesPolarity(p, P_TRUE)) {
- generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);
- elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_TRUE));
- } else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE) && impliesPolarity(p, P_FALSE)) {
- generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);
- elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_FALSE));
+ generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);
+ elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_TRUE));
+ } else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE) && impliesPolarity(p, P_FALSE)) {
+ generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);
+ elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_FALSE));
}
return elemEnc->edgeArray[i];
}
ASSERT(encoding->type == BINARYVAL);
allocElementConstraintVariables(encoding, encoding->numBits);
getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
- if(encoding->anyValue)
+ if (encoding->anyValue)
generateAnyValueBinaryValueEncoding(encoding);
}
ASSERT(encoding->type == BINARYINDEX);
allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
- if(encoding->anyValue)
+ if (encoding->anyValue)
generateAnyValueBinaryIndexEncoding(encoding);
}
addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
}
}
- if(encoding->anyValue)
+ if (encoding->anyValue)
addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
}
}
}
-void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
- if(encoding->numVars == 0)
+void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
+ if (encoding->numVars == 0)
return;
int index = -1;
- for(uint i= encoding->encArraySize-1; i>=0; i--){
- if(encoding->isinUseElement(i)){
- if(i+1 < encoding->encArraySize){
- index = i+1;
+ for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
+ if (encoding->isinUseElement(i)) {
+ if (i + 1 < encoding->encArraySize) {
+ index = i + 1;
}
break;
}
}
- if( index != -1 ){
+ if ( index != -1 ) {
addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
}
- index = index == -1? encoding->encArraySize-1 : index-1;
- for(int i= index; i>=0; i--) {
- if (!encoding->isinUseElement(i)){
+ index = index == -1 ? encoding->encArraySize - 1 : index - 1;
+ for (int i = index; i >= 0; i--) {
+ if (!encoding->isinUseElement(i)) {
addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
}
}
}
-void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
+void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
uint64_t minvalueminusoffset = encoding->low - encoding->offset;
uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
solver(_solver),
- vector(allocDefVectorEdge()) {
+ vector(allocDefVectorEdge()) {
}
SATEncoder::~SATEncoder() {
CMEMALLOC;
private:
- void shouldMemoize(Element *elem, uint64_t val, bool & memo);
+ void shouldMemoize(Element *elem, uint64_t val, bool &memo);
Edge getNewVarSATEncoder();
void getArrayNewVarsSATEncoder(uint num, Edge *carray);
Edge encodeVarSATEncoder(BooleanVar *constraint);
}
bool notfinished = true;
- Edge carray[numDomains];
+ Edge carray[numDomains];
while (notfinished) {
if (predicate->evalPredicateOperator(vals) != generateNegation) {
//Include this in the set of terms
}
bool notfinished = true;
- Edge carray[numDomains + 1];
+ Edge carray[numDomains + 1];
while (notfinished) {
uint64_t result = function->applyFunctionOperator(numDomains, vals);
bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
if (generateNegation)
polarity = negatePolarity(polarity);
- if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+ if (undefStatus == SATC_FLAGFORCEUNDEFINED)
polarity = P_BOTHTRUEFALSE;
Edge constraints[size];
case SATC_FLAGFORCEUNDEFINED: {
row = constraintAND(cnf, inputNum, carray);
uint pSize = constraint->parents.getSize();
- if(!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)){
+ if (!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)) {
Edge proxy = constraintNewVar(cnf);
generateProxy(cnf, row, proxy, P_BOTHTRUEFALSE);
Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
if (generateNegation)
polarity = negatePolarity(polarity);
-
- ASSERT(numDomains != 0);
+
+ ASSERT(numDomains != 0);
VectorEdge *clauses = allocDefVectorEdge();
uint indices[numDomains]; //setup indices
Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
switch (undefStatus ) {
case SATC_IGNOREBEHAVIOR: {
- if(inputNum == 0){
- addConstraintCNF(cnf, output);
- }else{
- addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
- }
+ if (inputNum == 0) {
+ addConstraintCNF(cnf, output);
+ } else {
+ addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
+ }
break;
}
case SATC_FLAGFORCEUNDEFINED: {
Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
- if(inputNum ==0){
- addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
- }else{
- addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
- }
+ if (inputNum == 0) {
+ addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
+ } else {
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
+ }
break;
}
default:
model_print("Enumeration Table functions ...\n");
#endif
ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
-
+
//First encode children
Array<Element *> *elements = &elemFunc->inputs;
for (uint i = 0; i < elements->getSize(); i++) {
switch (function->undefBehavior) {
case SATC_UNDEFINEDSETSFLAG: {
if (isInRange) {
- if(numDomains == 0){
- addConstraintCNF(cnf,carray[numDomains]);
- }else{
- addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
- }
+ if (numDomains == 0) {
+ addConstraintCNF(cnf,carray[numDomains]);
+ } else {
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
+ }
} else {
Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
case SATC_FLAGIFFUNDEFINED: {
Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
if (isInRange) {
- if(numDomains == 0){
- addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
- }else{
- Edge freshvar = constraintNewVar(cnf);
- addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
- addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
- addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
- }
-
+ if (numDomains == 0) {
+ addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
+ } else {
+ Edge freshvar = constraintNewVar(cnf);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
+ }
+
} else {
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
#include "corestructs.h"
#include "boolean.h"
-void BooleanEdge::print(){
+void BooleanEdge::print() {
if (isNegated())
model_print("!");
getBoolean()->print();
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:
/**
* 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)
#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 print();
- bool anyValue;
+ bool anyValue;
ElementEncodingType type;
Element *element;
Edge *variables;/* List Variables Used To Encode Element */
struct {
uint64_t *encodingArray; /* List the Variables in the appropriate order */
uint64_t *inUseArray; /* Bitmap to track variables in use */
- Edge * edgeArray;
- Polarity * polarityArray;
+ Edge *edgeArray;
+ Polarity *polarityArray;
uint encArraySize;
ElemEnc encoding;
};
Element *e2 = solver->getElementVar(s2);
solver->mustHaveValue(e1);
solver->mustHaveValue(e2);
-
+
Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
Element *inputs[] = {e1, e2};
BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
b = solver->applyLogicalOperation(SATC_NOT, b);
solver->addConstraint(b);
-
+
if (solver->solve() == 1)
printf("e1=%" PRIu64 "e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
else
#include "csolver.h"
/**
- * !b1 AND
+ * !b1 AND
* !b2 OR b1 or (!b3 and b4) AND
* b7 OR (!b1 AND (b5 or !b6))
- *
+ *
*/
int main(int numargs, char **argv) {
CSolver *solver = new CSolver();
solver->printConstraints();
if (solver->solve() == 1)
printf("b1=%d\nb2=%d\nb3=%d\nb4=%d\nb5=%d\nb6=%d\nb7=%d\n",
- solver->getBooleanValue(b1), solver->getBooleanValue(b2),
- solver->getBooleanValue(b3), solver->getBooleanValue(b4),
- solver->getBooleanValue(b5), solver->getBooleanValue(b6),
- solver->getBooleanValue(b7));
+ solver->getBooleanValue(b1), solver->getBooleanValue(b2),
+ solver->getBooleanValue(b3), solver->getBooleanValue(b4),
+ solver->getBooleanValue(b5), solver->getBooleanValue(b6),
+ solver->getBooleanValue(b7));
else
printf("UNSAT\n");
delete solver;
printf("You should specify file names ...");
exit(-1);
}
- //usleep(20000000);
+ //usleep(20000000);
for (int i = 1; i < argc; i++) {
CSolver *solver = CSolver::deserialize(argv[i]);
CSolver *copy = solver->clone();
- CSolver *copy2 = solver->clone();
- CSolver *copy3 = solver->clone();
- CSolver *copy4 = solver->clone();
- int value = copy->solve();
- if (value == 1) {
+ CSolver *copy2 = solver->clone();
+ CSolver *copy3 = solver->clone();
+ CSolver *copy4 = solver->clone();
+ int value = copy->solve();
+ if (value == 1) {
printf("Copy %s is SAT\n", argv[i]);
} else {
printf("Copy %s is UNSAT\n", argv[i]);
}
- value = copy2->solve();
- if (value == 1) {
+ value = copy2->solve();
+ if (value == 1) {
printf("Copy2 %s is SAT\n", argv[i]);
} else {
printf("Copy2 %s is UNSAT\n", argv[i]);
}
- value = copy3->solve();
- if (value == 1) {
+ value = copy3->solve();
+ if (value == 1) {
printf("Copy3 %s is SAT\n", argv[i]);
} else {
printf("Copy3 %s is UNSAT\n", argv[i]);
}
- value = copy4->solve();
- if (value == 1) {
+ value = copy4->solve();
+ if (value == 1) {
printf("Copy4 %s is SAT\n", argv[i]);
} else {
printf("Copy4 %s is UNSAT\n", argv[i]);
}
- value = solver->solve();
+ value = solver->solve();
if (value == 1) {
printf("Original %s is SAT\n", argv[i]);
} else {
printf("Original %s is UNSAT\n", argv[i]);
}
-
+
delete solver;
}
return 1;
printf("You should specify file names ...");
exit(-1);
}
- //usleep(20000000);
+ //usleep(20000000);
for (int i = 1; i < argc; i++) {
CSolver *solver = CSolver::deserialize(argv[i]);
int value = solver->solve();
void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
DOREdge edge(first, second, 0, first, second);
- DOREdge *oldedge=edges.get(&edge);
+ DOREdge *oldedge = edges.get(&edge);
if (oldedge != NULL) {
- oldedge->mustbetrue=true;
+ oldedge->mustbetrue = true;
} else {
DOREdge *newedge = new DOREdge(first, second, 0, first, second);
- newedge->mustbetrue=true;
+ newedge->mustbetrue = true;
edges.add(newedge);
}
}
DOREdge *doredge = iterator->next();
if (doredge->mustbetrue) {
graph->addEdge(doredge->origfirst, doredge->origsecond);
- if (doredge->newfirst != doredge->origfirst || doredge->newsecond!=doredge->origsecond) {
+ if (doredge->newfirst != doredge->origfirst || doredge->newsecond != doredge->origsecond) {
graph->addEdge(doredge->newfirst, doredge->newsecond);
}
} else if (doredge->orderindex != 0) {
uint index = 0;
bool overflow = true;
for (uint i = 0; i < elemEnc->numVars; i++) {
- if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))){
+ if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) {
index = i;
overflow = false;
}
}
- if(overflow)
+ if (overflow)
model_print("WARNING: Element has undefined value!\n");
ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
return elemEnc->encodingArray[index];
long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
CSolver *copy = problem->clone();
copy->setTuner(tuner);
- model_print("**********************\n");
+ model_print("**********************\n");
int sat = copy->solve();
- if(result == UNSETVALUE)
- result = sat;
- else if(result != sat){
- model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
- copy->printConstraints();
- }
+ if (result == UNSETVALUE)
+ result = sat;
+ else if (result != sat) {
+ model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+ copy->printConstraints();
+ }
//model_print("SAT %d\n", result);
long long elapsedTime = copy->getElapsedTime();
// long long encodeTime = copy->getEncodeTime();
Vector<CSolver *> solvers;
uint budget;
- int result;
+ int result;
};
#endif
return descriptor->defaultValue;
}
-const char* tunableParameterToString(Tunables tunable){
- switch(tunable){
- case DECOMPOSEORDER:
- return "DECOMPOSEORDER";
- case MUSTREACHGLOBAL:
- return "MUSTREACHGLOBAL";
- case MUSTREACHLOCAL:
- return "MUSTREACHLOCAL";
- case MUSTREACHPRUNE:
- return "MUSTREACHPRUNE";
- case OPTIMIZEORDERSTRUCTURE:
- return "OPTIMIZEORDERSTRUCTURE";
- case ORDERINTEGERENCODING:
- return "ORDERINTEGERENCODING";
- case PREPROCESS:
- return "PREPROCESS";
- case NODEENCODING:
- return "NODEENCODING";
- case EDGEENCODING:
- return "EDGEENCODING";
- case MUSTEDGEPRUNE:
- return "MUSTEDGEPRUNE";
- default:
- ASSERT(0);
- }
+const char *tunableParameterToString(Tunables tunable) {
+ switch (tunable) {
+ case DECOMPOSEORDER:
+ return "DECOMPOSEORDER";
+ case MUSTREACHGLOBAL:
+ return "MUSTREACHGLOBAL";
+ case MUSTREACHLOCAL:
+ return "MUSTREACHLOCAL";
+ case MUSTREACHPRUNE:
+ return "MUSTREACHPRUNE";
+ case OPTIMIZEORDERSTRUCTURE:
+ return "OPTIMIZEORDERSTRUCTURE";
+ case ORDERINTEGERENCODING:
+ return "ORDERINTEGERENCODING";
+ case PREPROCESS:
+ return "PREPROCESS";
+ case NODEENCODING:
+ return "NODEENCODING";
+ case EDGEENCODING:
+ return "EDGEENCODING";
+ case MUSTEDGEPRUNE:
+ return "MUSTEDGEPRUNE";
+ default:
+ ASSERT(0);
+ }
}
\ No newline at end of file
enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
typedef enum Tunables Tunables;
-const char* tunableParameterToString(Tunables tunable);
+const char *tunableParameterToString(Tunables tunable);
#endif
#include "csolver.h"
#include "ccsolver.h"
-#define CCSOLVER(solver) ((CSolver*)solver)
+#define CCSOLVER(solver) ((CSolver *)solver)
-void* createCCSolver(){
- return (void*) new CSolver();
+void *createCCSolver() {
+ return (void *) new CSolver();
}
-void deleteCCSolver(void* solver){
+void deleteCCSolver(void *solver) {
delete CCSOLVER(solver);
}
-void *createSet(void* solver,unsigned int type, long *elements, unsigned int num){
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num) {
return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num);
}
-void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange){
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange) {
return CCSOLVER(solver)->createRangeSet((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
}
-void *createRangeVar(void* solver,unsigned int type, long lowrange, long highrange){
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange) {
return CCSOLVER(solver)->createRangeVar((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
}
-void *createMutableSet(void* solver,unsigned int type){
+void *createMutableSet(void *solver,unsigned int type) {
return CCSOLVER(solver)->createMutableSet((VarType) type);
}
-void addItem(void* solver,void *set, long element){
- CCSOLVER(solver)->addItem((MutableSet*) set, (uint64_t) element);
+void addItem(void *solver,void *set, long element) {
+ CCSOLVER(solver)->addItem((MutableSet *) set, (uint64_t) element);
}
-void finalizeMutableSet(void* solver,void *set){
- CCSOLVER(solver)->finalizeMutableSet((MutableSet*) set);
+void finalizeMutableSet(void *solver,void *set) {
+ CCSOLVER(solver)->finalizeMutableSet((MutableSet *) set);
}
-void *getElementVar(void* solver,void *set){
- return CCSOLVER(solver)->getElementVar((Set*) set);
+void *getElementVar(void *solver,void *set) {
+ return CCSOLVER(solver)->getElementVar((Set *) set);
}
-void *getElementConst(void* solver,unsigned int type, long value){
+void *getElementConst(void *solver,unsigned int type, long value) {
return CCSOLVER(solver)->getElementConst((VarType) type, (uint64_t) value);
}
-void *getElementRange (void* solver,void *element){
- return CCSOLVER(solver)->getElementRange ((Element*) element);
+void *getElementRange (void *solver,void *element) {
+ return CCSOLVER(solver)->getElementRange ((Element *) element);
}
-void* getBooleanVar(void* solver,unsigned int type){
+void *getBooleanVar(void *solver,unsigned int type) {
return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
}
-void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior){
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior) {
return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set *)range, (OverFlowBehavior) overflowbehavior);
}
-void *createPredicateOperator(void* solver,unsigned int op) {
+void *createPredicateOperator(void *solver,unsigned int op) {
return CCSOLVER(solver)->createPredicateOperator((CompOp) op);
}
-void *createPredicateTable(void* solver,void *table, unsigned int behavior){
+void *createPredicateTable(void *solver,void *table, unsigned int behavior) {
return CCSOLVER(solver)->createPredicateTable((Table *)table, (UndefinedBehavior) behavior);
}
-void *createTable(void* solver, void *range){
+void *createTable(void *solver, void *range) {
return CCSOLVER(solver)->createTable((Set *)range);
}
-void *createTableForPredicate(void* solver) {
+void *createTableForPredicate(void *solver) {
return CCSOLVER(solver)->createTableForPredicate();
}
-void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result){
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result) {
CCSOLVER(solver)->addTableEntry((Table *)table, (uint64_t *)inputs, (uint) inputSize, (uint64_t) result);
}
-void *completeTable(void* solver,void *table, unsigned int behavior){
+void *completeTable(void *solver,void *table, unsigned int behavior) {
return CCSOLVER(solver)->completeTable((Table *) table, (UndefinedBehavior) behavior);
}
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus){
- return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean*)overflowstatus));
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus) {
+ return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean *)overflowstatus));
}
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus){
- return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean*) undefinedStatus)).getRaw();
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus) {
+ return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean *) undefinedStatus)).getRaw();
}
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs){
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs) {
return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw();
}
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize){
+void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize) {
return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw();
}
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2){
- return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg1), BooleanEdge((Boolean*) arg2)).getRaw();
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2) {
+ return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg1), BooleanEdge((Boolean *) arg2)).getRaw();
}
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg){
- return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg)).getRaw();
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg) {
+ return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg)).getRaw();
}
-void addConstraint(void* solver,void* constraint){
- CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean*) constraint));
+void addConstraint(void *solver,void *constraint) {
+ CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean *) constraint));
}
-void *createOrder(void* solver,unsigned int type, void *set){
+void *createOrder(void *solver,unsigned int type, void *set) {
return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set);
}
-void* orderConstraint(void* solver,void *order, long first, long second){
+void *orderConstraint(void *solver,void *order, long first, long second) {
return CCSOLVER(solver)->orderConstraint((Order *)order, (uint64_t) first, (uint64_t) second).getRaw();
}
-int solve(void* solver){
+int solve(void *solver) {
return CCSOLVER(solver)->solve();
}
-long getElementValue(void* solver,void *element){
+long getElementValue(void *solver,void *element) {
return (long) CCSOLVER(solver)->getElementValue((Element *)element);
}
-int getBooleanValue(void* solver, void* boolean){
- return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean*) boolean));
+int getBooleanValue(void *solver, void *boolean) {
+ return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean *) boolean));
}
-int getOrderConstraintValue(void* solver,void *order, long first, long second){
+int getOrderConstraintValue(void *solver,void *order, long first, long second) {
return CCSOLVER(solver)->getOrderConstraintValue((Order *)order, (uint64_t) first, (uint64_t) second);
}
-void printConstraints(void* solver){
+void printConstraints(void *solver) {
CCSOLVER(solver)->printConstraints();
}
-void serialize(void* solver){
+void serialize(void *solver) {
CCSOLVER(solver)->serialize();
}
-void mustHaveValue(void *solver, void *element){
- CCSOLVER(solver)->mustHaveValue( (Element*) element);
+void mustHaveValue(void *solver, void *element) {
+ CCSOLVER(solver)->mustHaveValue( (Element *) element);
}
-void* clone(void * solver){
+void *clone(void *solver) {
return CCSOLVER(solver)->clone();
}
\ No newline at end of file
#define __CCSOLVER_H
-typedef void* CCSolver;
+typedef void *CCSolver;
#ifdef __cplusplus
extern "C" {
#endif
-void* createCCSolver();
-void deleteCCSolver(void* solver);
-void *createSet(void* solver,unsigned int type, long *elements, unsigned int num);
-void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange);
-void *createRangeVar(void* solver,unsigned int type, long lowrange, long highrange);
-void *createMutableSet(void* solver,unsigned int type);
-void addItem(void* solver,void *set, long element);
-void finalizeMutableSet(void* solver,void *set);
-void *getElementVar(void* solver,void *set);
-void *getElementConst(void* solver,unsigned int type, long value);
-void *getElementRange (void* solver,void *element);
-void* getBooleanVar(void* solver,unsigned int type);
-void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior);
-void *createPredicateOperator(void* solver,unsigned int op);
-void *createPredicateTable(void* solver,void *table, unsigned int behavior);
-void *createTable(void* solver, void *range);
-void *createTableForPredicate(void* solver);
-void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result);
-void *completeTable(void* solver,void *table, unsigned int behavior);
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus);
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus);
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs);
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize);
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2);
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg);
-void addConstraint(void* solver,void* constraint);
-void *createOrder(void* solver,unsigned int type, void *set);
-void* orderConstraint(void* solver,void *order, long first, long second);
-int solve(void* solver);
-long getElementValue(void* solver,void *element);
-int getBooleanValue(void* solver,void* boolean);
-int getOrderConstraintValue(void* solver,void *order, long first, long second);
-void printConstraints(void* solver);
-void serialize(void* solver);
+void *createCCSolver();
+void deleteCCSolver(void *solver);
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num);
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange);
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange);
+void *createMutableSet(void *solver,unsigned int type);
+void addItem(void *solver,void *set, long element);
+void finalizeMutableSet(void *solver,void *set);
+void *getElementVar(void *solver,void *set);
+void *getElementConst(void *solver,unsigned int type, long value);
+void *getElementRange (void *solver,void *element);
+void *getBooleanVar(void *solver,unsigned int type);
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior);
+void *createPredicateOperator(void *solver,unsigned int op);
+void *createPredicateTable(void *solver,void *table, unsigned int behavior);
+void *createTable(void *solver, void *range);
+void *createTableForPredicate(void *solver);
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result);
+void *completeTable(void *solver,void *table, unsigned int behavior);
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus);
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus);
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs);
+void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize);
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2);
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg);
+void addConstraint(void *solver,void *constraint);
+void *createOrder(void *solver,unsigned int type, void *set);
+void *orderConstraint(void *solver,void *order, long first, long second);
+int solve(void *solver);
+long getElementValue(void *solver,void *element);
+int getBooleanValue(void *solver,void *boolean);
+int getOrderConstraintValue(void *solver,void *order, long first, long second);
+void printConstraints(void *solver);
+void serialize(void *solver);
void mustHaveValue(void *solver, void *element);
-void* clone(void * solver);
+void *clone(void *solver);
#ifdef __cplusplus
}
#endif
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) \
return set;
}
-bool CSolver::itemExistInSet(Set *set, uint64_t item){
- return set->exists(item);
+bool CSolver::itemExistInSet(Set *set, uint64_t item) {
+ return set->exists(item);
}
VarType CSolver::getSetVarType(Set *set) {
return element;
}
-void CSolver::mustHaveValue(Element *element){
+void CSolver::mustHaveValue(Element *element) {
element->getElementEncoding()->anyValue = true;
}
/** This function creates a set from lowrange to highrange (inclusive). */
Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
-
- bool itemExistInSet(Set *set, uint64_t item);
+
+ bool itemExistInSet(Set *set, uint64_t item);
VarType getSetVarType(Set *set);
Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
/** This function creates a mutable set.
- * Note: You should use addItem for adding new item to Mutable sets, and
- * at the end, you should call finalizeMutableSet!
- */
+ * Note: You should use addItem for adding new item to Mutable sets, and
+ * at the end, you should call finalizeMutableSet!
+ */
MutableSet *createMutableSet(VarType type);
Set *getElementRange (Element *element);
void mustHaveValue(Element *element);
-
+
BooleanEdge getBooleanTrue();
BooleanEdge getBooleanFalse();
private:
void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
- void handleFunction(ElementFunction * ef, BooleanEdge child);
-
+ void handleFunction(ElementFunction *ef, BooleanEdge child);
+
//These two functions are helpers if the client has a pointer to a
//Boolean object that we have since replaced
BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
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