#include "nodeedge.h"
#include <string.h>
#include <stdlib.h>
+#include "inc_solver.h"
+#include "cnfexpr.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.
+*/
+
VectorImpl(Edge, Edge, 16)
cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
cnf->enableMatching=true;
allocInlineDefVectorEdge(& cnf->constraints);
- return cnf;
+ allocInlineDefVectorEdge(& cnf->args);
+ cnf->solver=allocIncrementalSolver();
+ return cnf;
}
void deleteCNF(CNF * cnf) {
ourfree(n);
}
deleteVectorArrayEdge(& cnf->constraints);
+ deleteVectorArrayEdge(& cnf->args);
+ deleteIncrementalSolver(cnf->solver);
ourfree(cnf->node_array);
ourfree(cnf);
}
memcpy(n->edges, edges, sizeof(Edge)*numEdges);
n->flags.type=type;
n->flags.wasExpanded=0;
+ n->flags.cnfVisitedDown=0;
+ n->flags.cnfVisitedUp=0;
+ n->flags.varForced=0;
n->numEdges=numEdges;
n->hashCode=hashcode;
n->intAnnot[0]=0;n->intAnnot[1]=0;
uint hashNode(NodeType type, uint numEdges, Edge * edges) {
uint hashvalue=type ^ numEdges;
for(uint i=0;i<numEdges;i++) {
- hashvalue ^= (uint) edges[i].node_ptr;
+ hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
}
return (uint) hashvalue;
/** De-duplicate array */
uint lowindex=0;
- edges[lowindex++]=edges[initindex++];
+ edges[lowindex]=edges[initindex++];
for(;initindex<numEdges;initindex++) {
Edge e1=edges[lowindex];
return E_False;
}
} else
- edges[lowindex++]=edges[initindex];
+ edges[++lowindex]=edges[initindex];
}
+ lowindex++; //Make lowindex look like size
+
if (lowindex==1)
return edges[0];
}
}
- return createNode(cnf, NodeType_AND, numEdges, edges);
+ return createNode(cnf, NodeType_AND, lowindex, edges);
}
Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
return e;
}
+void solveCNF(CNF *cnf) {
+ countPass(cnf);
+ convertPass(cnf, false);
+ finishedClauses(cnf->solver);
+ solve(cnf->solver);
+}
+
+
void countPass(CNF *cnf) {
uint numConstraints=getSizeVectorEdge(&cnf->constraints);
VectorEdge *ve=allocDefVectorEdge();
deleteVectorEdge(ve);
}
-void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
+void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
//Skip constants and variables...
- if (edgeIsVarConst(e))
+ if (edgeIsVarConst(eroot))
return;
- clearVectorEdge(stack);pushVectorEdge(stack, e);
+ clearVectorEdge(stack);pushVectorEdge(stack, eroot);
bool isMatching=cnf->enableMatching;
n->intAnnot[polarity]++;
}
} else {
- setExpanded(n, polarity); n->intAnnot[polarity]=1;
-
+ setExpanded(n, polarity);
+
if (n->flags.type == NodeType_ITE||
n->flags.type == NodeType_IFF) {
n->intAnnot[polarity]=0;
n2->ptrAnnot[1]=succ1.node_ptr;
}
} else {
+ n->intAnnot[polarity]=1;
for (uint i=0;i<n->numEdges;i++) {
Edge succ=n->edges[i];
succ=constraintNegateIf(succ, polarity);
}
}
}
+
+void convertPass(CNF *cnf, bool backtrackLit) {
+ uint numConstraints=getSizeVectorEdge(&cnf->constraints);
+ VectorEdge *ve=allocDefVectorEdge();
+ for(uint i=0; i<numConstraints;i++) {
+ convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
+ }
+ deleteVectorEdge(ve);
+}
+
+void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
+ Node *nroot=getNodePtrFromEdge(root);
+
+ if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
+ root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
+ }
+
+ if (edgeIsConst(root)) {
+ if (isNegEdge(root)) {
+ //trivally unsat
+ Edge newvar=constraintNewVar(cnf);
+ Literal var=getEdgeVar(newvar);
+ Literal clause[] = {var};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ clause[0]=-var;
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ return;
+ } else {
+ //trivially true
+ return;
+ }
+ } else if (edgeIsVarConst(root)) {
+ Literal clause[] = { getEdgeVar(root)};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ return;
+ }
+
+ clearVectorEdge(stack);pushVectorEdge(stack, root);
+ while(getSizeVectorEdge(stack)!=0) {
+ Edge e=lastVectorEdge(stack);
+ Node *n=getNodePtrFromEdge(e);
+
+ if (edgeIsVarConst(e)) {
+ popVectorEdge(stack);
+ continue;
+ } else if (n->flags.type==NodeType_ITE ||
+ n->flags.type==NodeType_IFF) {
+ popVectorEdge(stack);
+ if (n->ptrAnnot[0]!=NULL)
+ pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
+ if (n->ptrAnnot[1]!=NULL)
+ pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
+ continue;
+ }
+
+ bool needPos = (n->intAnnot[0] > 0);
+ bool needNeg = (n->intAnnot[1] > 0);
+ if ((!needPos || n->flags.cnfVisitedUp & 1) &&
+ (!needNeg || n->flags.cnfVisitedUp & 2)) {
+ popVectorEdge(stack);
+ } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
+ (needNeg && !(n->flags.cnfVisitedDown & 2))) {
+ if (needPos)
+ n->flags.cnfVisitedDown|=1;
+ if (needNeg)
+ n->flags.cnfVisitedDown|=2;
+ for(uint i=0; i<n->numEdges; i++) {
+ Edge arg=n->edges[i];
+ arg=constraintNegateIf(arg, isNegEdge(e));
+ pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
+ }
+ } else {
+ popVectorEdge(stack);
+ produceCNF(cnf, e);
+ }
+ }
+ CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
+ if (isProxy(cnfExp)) {
+ Literal l=getProxy(cnfExp);
+ Literal clause[] = {l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ } else if (backtrackLit) {
+ Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
+ Literal clause[] = {l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ } else {
+ outputCNF(cnf, cnfExp);
+ }
+
+ if (!((intptr_t) cnfExp & 1)) {
+ deleteCNFExpr(cnfExp);
+ nroot->ptrAnnot[isNegEdge(root)] = NULL;
+ }
+}
+
+
+Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
+ Literal l = 0;
+ Node * n = getNodePtrFromEdge(e);
+
+ if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
+ if (isProxy(otherExp))
+ l = -getProxy(otherExp);
+ } else {
+ Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
+ Node * nsemNeg=getNodePtrFromEdge(semNeg);
+ if (nsemNeg != NULL) {
+ if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
+ if (isProxy(otherExp))
+ l = -getProxy(otherExp);
+ } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
+ if (isProxy(otherExp))
+ l = getProxy(otherExp);
+ }
+ }
+ }
+
+ if (l == 0) {
+ Edge newvar = constraintNewVar(cnf);
+ l = getEdgeVar(newvar);
+ }
+ // Output the constraints on the auxiliary variable
+ constrainCNF(cnf, l, exp);
+ deleteCNFExpr(exp);
+
+ n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
+
+ return l;
+}
+
+void produceCNF(CNF * cnf, Edge e) {
+ CNFExpr* expPos = NULL;
+ CNFExpr* expNeg = NULL;
+ Node *n = getNodePtrFromEdge(e);
+
+ if (n->intAnnot[0] > 0) {
+ expPos = produceConjunction(cnf, e);
+ }
+
+ if (n->intAnnot[1] > 0) {
+ expNeg = produceDisjunction(cnf, e);
+ }
+
+ /// @todo Propagate constants across semantic negations (this can
+ /// be done similarly to the calls to propagate shown below). The
+ /// trick here is that we need to figure out how to get the
+ /// semantic negation pointers, and ensure that they can have CNF
+ /// produced for them at the right point
+ ///
+ /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
+
+ // propagate from positive to negative, negative to positive
+ if (!propagate(cnf, & expPos, expNeg, true))
+ propagate(cnf, & expNeg, expPos, true);
+
+ // The polarity heuristic entails visiting the discovery polarity first
+ if (isPosEdge(e)) {
+ saveCNF(cnf, expPos, e, false);
+ saveCNF(cnf, expNeg, e, true);
+ } else {
+ saveCNF(cnf, expNeg, e, true);
+ saveCNF(cnf, expPos, e, false);
+ }
+}
+
+bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
+ if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
+ if (*dest == NULL) {
+ *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ } else if (isProxy(*dest)) {
+ bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ if (alwaysTrue) {
+ Literal clause[] = {getProxy(*dest)};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ } else {
+ Literal clause[] = {-getProxy(*dest)};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ }
+
+ *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ } else {
+ clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ }
+ return true;
+ }
+ return false;
+}
+
+void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
+ Node *n=getNodePtrFromEdge(e);
+ n->flags.cnfVisitedUp |= (1 << sign);
+ if (exp == NULL || isProxy(exp)) return;
+
+ if (exp->litSize == 1) {
+ Literal l = getLiteralLitVector(&exp->singletons, 0);
+ deleteCNFExpr(exp);
+ n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
+ } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
+ introProxy(cnf, e, exp, sign);
+ } else {
+ n->ptrAnnot[sign] = exp;
+ }
+}
+
+void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
+ if (alwaysTrueCNF(expr)) {
+ return;
+ } else if (alwaysFalseCNF(expr)) {
+ Literal clause[] = {-lcond};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ return;
+ }
+
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ Literal clause[] = {-lcond, l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ addClauseLiteral(cnf->solver, -lcond); //Add first literal
+ addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
+ }
+}
+
+void outputCNF(CNF *cnf, CNFExpr *expr) {
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ Literal clause[] = {l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
+ }
+}
+
+CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
+ clearVectorEdge(&cnf->args);
+
+ *largestEdge = (Edge) {(Node*) NULL};
+ CNFExpr* largest = NULL;
+ Node *n=getNodePtrFromEdge(e);
+ int i = n->numEdges;
+ while (i != 0) {
+ Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
+ Node * narg = getNodePtrFromEdge(arg);
+
+ if (edgeIsVarConst(arg)) {
+ pushVectorEdge(&cnf->args, arg);
+ continue;
+ }
+
+ if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
+ arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
+ }
+
+ if (narg->intAnnot[isNegEdge(arg)] == 1) {
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
+ if (!isProxy(argExp)) {
+ if (largest == NULL) {
+ largest = argExp;
+ * largestEdge = arg;
+ continue;
+ } else if (argExp->litSize > largest->litSize) {
+ pushVectorEdge(&cnf->args, *largestEdge);
+ largest = argExp;
+ * largestEdge = arg;
+ continue;
+ }
+ }
+ }
+ pushVectorEdge(&cnf->args, arg);
+ }
+
+ if (largest != NULL) {
+ Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
+ nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
+ }
+
+ return largest;
+}
+
+
+CNFExpr * produceConjunction(CNF * cnf, Edge e) {
+ Edge largestEdge;
+
+ CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
+ if (accum == NULL) accum = allocCNFExprBool(true);
+
+ int i = getSizeVectorEdge(&cnf->args);
+ while (i != 0) {
+ Edge arg = getVectorEdge(&cnf->args, --i);
+ if (edgeIsVarConst(arg)) {
+ conjoinCNFLit(accum, getEdgeVar(arg));
+ } else {
+ Node *narg=getNodePtrFromEdge(arg);
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
+
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
+ if (isProxy(argExp)) { // variable has been introduced
+ conjoinCNFLit(accum, getProxy(argExp));
+ } else {
+ conjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+ }
+ }
+ }
+
+ return accum;
+}
+
+#define CLAUSE_MAX 3
+
+CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
+ Edge largestEdge;
+ CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
+ if (accum == NULL)
+ accum = allocCNFExprBool(false);
+
+ // This is necessary to check to make sure that we don't start out
+ // with an accumulator that is "too large".
+
+ /// @todo Strictly speaking, introProxy doesn't *need* to free
+ /// memory, then this wouldn't have to reallocate CNFExpr
+
+ /// @todo When this call to introProxy is made, the semantic
+ /// negation pointer will have been destroyed. Thus, it will not
+ /// be possible to use the correct proxy. That should be fixed.
+
+ // at this point, we will either have NULL, or a destructible expression
+ if (getClauseSizeCNF(accum) > CLAUSE_MAX)
+ accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
+
+ int i = getSizeVectorEdge(&cnf->args);
+ while (i != 0) {
+ Edge arg=getVectorEdge(&cnf->args, --i);
+ Node *narg=getNodePtrFromEdge(arg);
+ if (edgeIsVarConst(arg)) {
+ disjoinCNFLit(accum, getEdgeVar(arg));
+ } else {
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
+
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
+ if (isProxy(argExp)) { // variable has been introduced
+ disjoinCNFLit(accum, getProxy(argExp));
+ } else if (argExp->litSize == 0) {
+ disjoinCNFExpr(accum, argExp, destroy);
+ } else {
+ // check to see if we should introduce a proxy
+ int aL = accum->litSize; // lits in accum
+ int eL = argExp->litSize; // lits in argument
+ int aC = getClauseSizeCNF(accum); // clauses in accum
+ int eC = getClauseSizeCNF(argExp); // clauses in argument
+
+ if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
+ disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
+ } else {
+ disjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+ }
+ }
+ }
+ }
+
+ return accum;
+}
projects / satune.git / blobdiff