#include "common.h"
#include "qsort.h"
/*
- V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
- Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
-
- Permission is hereby granted, free of charge, to any person obtaining
- a copy of this software and associated documentation files (the
- "Software"), to deal in the Software without restriction, including
- without limitation the rights to use, copy, modify, merge, publish,
- distribute, sublicense, and/or sell copies of the Software, and to
- permit persons to whom the Software is furnished to do so, subject to
- the following conditions:
-
- The above copyright notice and this permission notice shall be
- included in all copies or substantial portions of the Software. If
- you download or use the software, send email to Pete Manolios
- (pete@ccs.neu.edu) with your name, contact information, and a short
- note describing what you want to use BAT for. For any reuse or
- distribution, you must make clear to others the license terms of this
- work.
-
- Contact Pete Manolios if you want any of these conditions waived.
-
- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
- MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
- LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
- OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
- WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
- */
-
-/*
- C port of CNF SAT Conversion Copyright Brian Demsky 2017.
+ CNF SAT Conversion Copyright Brian Demsky 2017.
*/
Edge E_BOGUS = {(Node *)0xffff5673};
Edge E_NULL = {(Node *)NULL};
-
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;
Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
+ n->numVars = 0;
n->type = type;
n->numEdges = numEdges;
memcpy(n->edges, edges, sizeof(Edge) * numEdges);
Node *allocBaseNode(NodeType type, uint numEdges) {
Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
+ n->numVars = 0;
n->type = type;
n->numEdges = numEdges;
return n;
Node *allocResizeNode(uint capacity) {
Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
+ n->numVars = 0;
n->numEdges = 0;
n->capacity = capacity;
return n;
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);
+ ourfree(node);
+}
+
+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->numVars = currnode->numVars;
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) {
//just swap
+ innode->numVars = currnode->numVars;
Node *tmp = innode;
innode = currnode;
*node = currnode = tmp;
} else {
Node *newnode = allocResizeNode( newsize << 1);
+ newnode->numVars = currnode->numVars;
newnode->numEdges = currnode->numEdges;
memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
ourfree(currnode);
- *node=newnode;
+ *node = newnode;
currnode = newnode;
}
} else {
if (inEdges > currEdges && newsize < innode->capacity) {
//just swap
+ innode->numVars = currnode->numVars;
Node *tmp = innode;
innode = currnode;
*node = currnode = tmp;
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;
if (newsize >= currnode->capacity) {
Node *newnode = allocResizeNode( newsize << 1);
+ newnode->numVars = currnode->numVars;
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) {
return E_True;
else if (remainSize == 1)
return edges[initindex];
- else if (equalsEdge(edges[initindex], E_False))
+ else if (equalsEdge(edges[initindex], E_False)) {
+ freeEdgesRec(numEdges, edges);
return E_False;
+ }
/** De-duplicate array */
uint lowindex = 0;
Edge e1 = edges[lowindex];
Edge e2 = edges[initindex];
if (sameNodeVarEdge(e1, e2)) {
+ ASSERT(!isNodeEdge(e1));
if (!sameSignEdge(e1, e2)) {
+ freeEdgesRec(lowindex + 1, edges);
+ 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])) {
- return 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])) {
- return 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])) {
- return 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])) {
- return 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;
}
}
Edge e;
if (equalsEdge(lpos, rpos)) {
+ freeEdgeRec(left);
+ freeEdgeRec(right);
e = E_True;
} else if (ltEdge(lpos, rpos)) {
Edge edges[] = {lpos, rpos};
Edge result;
if (equalsEdge(cond, E_True)) {
+ freeEdgeRec(elseedge);
result = thenedge;
} else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
Edge array[] = {cond, elseedge};
result = constraintOR(cnf, 2, array);
} else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
result = constraintIMPLIES(cnf, cond, thenedge);
- } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
+ } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
Edge array[] = {cond, thenedge};
result = constraintAND(cnf, 2, array);
} else if (equalsEdge(thenedge, elseedge)) {
+ freeEdgeRec(cond);
result = thenedge;
} else if (sameNodeOppSign(thenedge, elseedge)) {
if (ltEdge(cond, thenedge)) {
return result;
}
+Edge disjoinLit(Edge vec, Edge lit) {
+ Node *nvec = vec.node_ptr;
+ uint nvecedges = nvec->numEdges;
+
+ for (uint i = 0; i < nvecedges; i++) {
+ Edge ce = nvec->edges[i];
+ if (!edgeIsVarConst(ce)) {
+ Node *cne = ce.node_ptr;
+ addEdgeToResizeNode(&cne, lit);
+ nvec->edges[i] = (Edge) {cne};
+ } else {
+ Node *clause = allocResizeNode(2);
+ addEdgeToResizeNode(&clause, lit);
+ addEdgeToResizeNode(&clause, ce);
+ nvec->edges[i] = (Edge) {clause};
+ }
+ }
+ nvec->numVars += nvecedges;
+ return vec;
+}
+
+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 > cnfedges) {
+ outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
+ freeEdgeCNF(newvec);
+ return disjoinLit(cnfform, proxyVar);
+ } else {
+ outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
+ freeEdgeCNF(cnfform);
+ return disjoinLit(newvec, proxyVar);
+ }
+ }
+
+
+
+ if (newvecedges == 1 || cnfedges == 1) {
+ if (cnfedges != 1) {
+ Node *tmp = nnewvec;
+ nnewvec = ncnfform;
+ ncnfform = tmp;
+ newvecedges = cnfedges;
+ cnfedges = 1;
+ }
+ Edge e = ncnfform->edges[0];
+ if (!edgeIsVarConst(e)) {
+ Node *n = e.node_ptr;
+ for (uint i = 0; i < newvecedges; i++) {
+ Edge ce = nnewvec->edges[i];
+ if (isNodeEdge(ce)) {
+ Node *cne = ce.node_ptr;
+ mergeNodeToResizeNode(&cne, n);
+ nnewvec->edges[i] = (Edge) {cne};
+ } else {
+ Node *clause = allocResizeNode(n->numEdges + 1);
+ mergeNodeToResizeNode(&clause, n);
+ addEdgeToResizeNode(&clause, ce);
+ nnewvec->edges[i] = (Edge) {clause};
+ }
+ }
+ nnewvec->numVars += newvecedges * n->numVars;
+ } else {
+ for (uint i = 0; i < newvecedges; i++) {
+ Edge ce = nnewvec->edges[i];
+ if (!edgeIsVarConst(ce)) {
+ Node *cne = ce.node_ptr;
+ addEdgeToResizeNode(&cne, e);
+ nnewvec->edges[i] = (Edge) {cne};
+ } else {
+ Node *clause = allocResizeNode(2);
+ addEdgeToResizeNode(&clause, e);
+ addEdgeToResizeNode(&clause, ce);
+ nnewvec->edges[i] = (Edge) {clause};
+ }
+ }
+ nnewvec->numVars += newvecedges;
+ }
+ freeEdgeCNF((Edge) {ncnfform});
+ return (Edge) {nnewvec};
+ }
+
+ 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++) {
+ Edge cedge = ncnfform->edges[j];
+ uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
+ if (equalsEdge(cedge, nedge)) {
+ addEdgeToResizeNode(&result, cedge);
+ result->numVars += cSize;
+ } else if (!sameNodeOppSign(nedge, cedge)) {
+ Node *clause = allocResizeNode(cSize + nSize);
+ if (isNodeEdge(nedge)) {
+ mergeNodeToResizeNode(&clause, nedge.node_ptr);
+ } else {
+ addEdgeToResizeNode(&clause, nedge);
+ }
+ if (isNodeEdge(cedge)) {
+ mergeNodeToResizeNode(&clause, cedge.node_ptr);
+ } else {
+ addEdgeToResizeNode(&clause, cedge);
+ }
+ addEdgeToResizeNode(&result, (Edge) {clause});
+ result->numVars += clause->numEdges;
+ }
+ //otherwise skip
+ }
+ }
+ freeEdgeCNF(newvec);
+ freeEdgeCNF(cnfform);
+ return (Edge) {result};
+}
+
Edge simplifyCNF(CNF *cnf, Edge input) {
if (edgeIsVarConst(input)) {
Node *newvec = allocResizeNode(1);
addEdgeToResizeNode(&newvec, input);
+ newvec->numVars = 1;
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);
+ newvec->numVars += enumvars;
}
return (Edge) {newvec};
} else {
//free temporary nodes
ourfree(getNodePtrFromEdge(thencons));
ourfree(getNodePtrFromEdge(elsecons));
- Node * result = thencnf.node_ptr;
+ Node *result = thencnf.node_ptr;
+ uint elsenumvars = elsecnf.node_ptr->numVars;
mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
+ result->numVars += elsenumvars;
return (Edge) {result};
}
} else {
if (type == NodeType_AND) {
//OR Case
uint numEdges = node->numEdges;
-
- for(uint i = 0; i < numEdges; i++) {
+
+ Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
+ for (uint i = 1; i < numEdges; i++) {
Edge e = node->edges[i];
- bool enegate = isNegEdge(e);
- if (!edgeIsVarConst(e)) {
- Node * enode = getNodePtrFromEdge(e);
- NodeType etype = enode->type;
- if (enegate) {
- if (etype == NodeType_AND) {
- //OR of AND Case
- uint eNumEdges = enode->numEdges;
- Node * newnode = allocResizeNode(0);
- Node * clause = allocBaseNode(NodeType_AND, numEdges);
- memcpy(clause->edges, node->edges, sizeof(Edge) * i);
- if ((i + 1) < numEdges) {
- memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
- }
-
- for(uint j = 0; j < eNumEdges; j++) {
- clause->edges[i] = constraintNegate(enode->edges[j]);
- Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
- mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
- }
- ourfree(clause);
- return (Edge) {newnode};
- } else {
- //OR of IFF or ITE
- Edge cond = enode->edges[0];
- Edge thenedge = enode->edges[1];
- Edge elseedge = (enode->type == NodeType_IFF) ? constraintNegate(thenedge) : enode->edges[2];
- Edge thenedges[] = {cond, constraintNegate(thenedge)};
- Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
- Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
- Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
-
- //OR of AND Case
- Node * newnode = allocResizeNode(0);
- Node * clause = allocBaseNode(NodeType_AND, numEdges);
- memcpy(clause->edges, node->edges, sizeof(Edge) * i);
- if ((i + 1) < numEdges) {
- memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
- }
-
- clause->edges[i] = constraintNegate(thencons);
- Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
- mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
-
- clause->edges[i] = constraintNegate(elsecons);
- simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
- mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
-
- //free temporary nodes
- ourfree(getNodePtrFromEdge(thencons));
- ourfree(getNodePtrFromEdge(elsecons));
- ourfree(clause);
- return (Edge) {newnode};
- }
- } else {
- if (etype == NodeType_AND) {
- //OR of OR Case
- uint eNumEdges = enode->numEdges;
- Node * clause = allocBaseNode(NodeType_AND, eNumEdges + numEdges - 1);
- memcpy(clause->edges, node->edges, sizeof(Edge) * i);
- if ((i + 1) < numEdges) {
- memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
- }
- memcpy(&clause->edges[numEdges-1], enode->edges, sizeof(Edge) * eNumEdges);
- Edge eclause = {clause};
- Edge result = simplifyCNF(cnf, constraintNegate(eclause));
- ourfree(clause);
- return result;
- } else {
- //OR of !(IFF or ITE)
- Edge cond = node->edges[0];
- Edge thenedge = node->edges[1];
- Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
- Edge thenedges[] = {cond, constraintNegate(thenedge)};
- Edge thencons = createNode(NodeType_AND, 2, thenedges);
- Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
- Edge elsecons = createNode(NodeType_AND, 2, elseedges);
-
-
- Node * clause = allocBaseNode(NodeType_AND, numEdges + 1);
- memcpy(clause->edges, node->edges, sizeof(Edge) * i);
- if ((i + 1) < numEdges) {
- memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
- }
- clause->edges[numEdges-1] = constraintNegate(thencons);
- clause->edges[numEdges] = constraintNegate(elsecons);
- Edge result = simplifyCNF(cnf, constraintNegate((Edge) {clause}));
- //free temporary nodes
- ourfree(getNodePtrFromEdge(thencons));
- ourfree(getNodePtrFromEdge(elsecons));
- ourfree(clause);
- return result;
- }
- }
- }
- }
-
- Node *newvec = allocResizeNode(numEdges);
- for(uint i=0; i < numEdges; i++) {
- addEdgeToResizeNode(&newvec, constraintNegate(node->edges[i]));
+ Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
+ newvec = disjoinAndFree(cnf, newvec, cnfform);
}
- Node * result = allocResizeNode(1);
- addEdgeToResizeNode(&result, (Edge){newvec});
- return (Edge) {result};
+ return newvec;
} else {
Edge cond = node->edges[0];
Edge thenedge = node->edges[1];
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;
+ int orvar = getEdgeVar(eorvar);
+ ASSERT(orvar != 0);
+ uint numEdges = andNode->numEdges;
+ 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);
+ addClause(cnf, 2, array);
+ } else {
+ 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++) {
+ array[j] = getEdgeVar(clause->edges[j]);
+ ASSERT(array[j] != 0);
+ }
+ array[cnumEdges - 1] = orvar;
+ 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);
}
}
}
+void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
+ ASSERT(p != P_UNDEFINED);
+ if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
+ // proxy => expression
+ Edge cnfexpr = simplifyCNF(cnf, expression);
+ if (p == P_TRUE)
+ freeEdgeRec(expression);
+ outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
+ freeEdgeCNF(cnfexpr);
+ }
+ if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
+ // expression => proxy
+ Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
+ freeEdgeRec(expression);
+ outputCNFOR(cnf, cnfnegexpr, proxy);
+ freeEdgeCNF(cnfnegexpr);
+ }
+}
+
void addConstraintCNF(CNF *cnf, Edge constraint) {
- if (equalsEdge(constraint, E_True))
+ if (equalsEdge(constraint, E_True)) {
return;
- else if (equalsEdge(constraint, E_False)) {
+ } else if (equalsEdge(constraint, E_False)) {
cnf->unsat = true;
return;
}
+ if (cnf->unsat) {
+ freeEdgeRec(constraint);
+ return;
+ }
- Edge cnfform = simplifyCNF(cnf, constraint);
- freeEdgeRec(constraint);
- outputCNF(cnf, cnfform);
- freeEdgeCNF(cnfform);
-#ifdef CONFIG_DEBUG
+#if 0
model_print("****SATC_ADDING NEW Constraint*****\n");
printCNF(constraint);
model_print("\n******************************\n");
#endif
+
+ Edge cnfform = simplifyCNF(cnf, constraint);
+ freeEdgeRec(constraint);
+ outputCNF(cnf, cnfform);
+ freeEdgeCNF(cnfform);
}
Edge constraintNewVar(CNF *cnf) {
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;
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("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
return result;
}
}
}
+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