CNF *createCNF() {
CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
cnf->varcount = 1;
+ cnf->clausecount = 0;
cnf->solver = allocIncrementalSolver();
cnf->solveTime = 0;
cnf->encodeTime = 0;
void resetCNF(CNF *cnf) {
resetSolver(cnf->solver);
cnf->varcount = 1;
+ cnf->clausecount = 0;
cnf->solveTime = 0;
cnf->encodeTime = 0;
cnf->unsat = false;
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));
}
Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
- Edge edgearray[numEdges];
+ if (numEdges < 200000) {
+ Edge edgearray[numEdges];
- for (uint i = 0; i < numEdges; i++) {
- edgearray[i] = constraintNegate(edges[i]);
+ for (uint i = 0; i < numEdges; i++) {
+ edgearray[i] = constraintNegate(edges[i]);
+ }
+ Edge eand = constraintAND(cnf, numEdges, edgearray);
+ return constraintNegate(eand);
+ } else {
+ Edge * edgearray=(Edge *)ourmalloc(numEdges*sizeof(Edge));
+
+ for (uint i = 0; i < numEdges; i++) {
+ edgearray[i] = constraintNegate(edges[i]);
+ }
+ Edge eand = constraintAND(cnf, numEdges, edgearray);
+ ourfree(edgearray);
+ return constraintNegate(eand);
}
- Edge eand = constraintAND(cnf, numEdges, edgearray);
- return constraintNegate(eand);
}
Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
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 addClause(CNF *cnf, uint numliterals, int *literals) {
+ cnf->clausecount++;
+ addArrayClauseLiteral(cnf->solver, numliterals, literals);
+}
+
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);
+ addClause(cnf, 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);
}
array[cnumEdges - 1] = orvar;
- addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+ addClause(cnf, cnumEdges, array);
}
}
}
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);
+ addClause(cnf, 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);
}
- addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+ addClause(cnf, cnumEdges, array);
}
}
}
printCNF(constraint);
model_print("\n******************************\n");
#endif
-
+
Edge cnfform = simplifyCNF(cnf, constraint);
freeEdgeRec(constraint);
outputCNF(cnf, cnfform);
long long startTime = getTimeNano();
finishedClauses(cnf->solver);
long long startSolve = getTimeNano();
+ model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
long long finishTime = getTimeNano();
cnf->encodeTime = startSolve - startTime;
}
}
+void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
+ //TO WRITE....
+}
+
Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
if (numvars == 0)
return E_True;
projects / satune.git / blobdiff