#include <string.h>
#include <stdlib.h>
#include "inc_solver.h"
+#include "cnfexpr.h"
/** Code ported from C++ BAT implementation of NICE-SAT */
cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
cnf->enableMatching=true;
allocInlineDefVectorEdge(& cnf->constraints);
+ allocInlineDefVectorEdge(& cnf->args);
return cnf;
}
ourfree(n);
}
deleteVectorArrayEdge(& cnf->constraints);
+ deleteVectorArrayEdge(& cnf->args);
ourfree(cnf->node_array);
ourfree(cnf);
}
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);
//trivally unsat
Edge newvar=constraintNewVar(cnf);
Literal var=getEdgeVar(newvar);
- Literal clause[] = {var, -var, 0};
- addArrayClauseLiteral(cnf->solver, 3, clause);
+ 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), 0};
- addArrayClauseLiteral(cnf->solver, 2, clause);
+ Literal clause[] = { getEdgeVar(root)};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
return;
}
} else if (n->flags.type==NodeType_ITE ||
n->flags.type==NodeType_IFF) {
popVectorEdge(stack);
- pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
- pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
+ 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) ||
+ 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)) {
+ } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
+ (needNeg && !(n->flags.cnfVisitedDown & 2))) {
if (needPos)
n->flags.cnfVisitedDown|=1;
if (needNeg)
}
CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
if (isProxy(cnfExp)) {
- //solver.add(getProxy(cnfExp))
+ Literal l=getProxy(cnfExp);
+ Literal clause[] = {l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
} else if (backtrackLit) {
- //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
+ Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
+ Literal clause[] = {l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
} else {
- //solver.add(*cnfExp);
+ outputCNF(cnf, cnfExp);
}
if (!((intptr_t) cnfExp & 1)) {
- //free rootExp
+ deleteCNFExpr(cnfExp);
nroot->ptrAnnot[isNegEdge(root)] = NULL;
}
}
-//DONE
+
Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
Literal l = 0;
Node * n = getNodePtrFromEdge(e);
}
// Output the constraints on the auxiliary variable
constrainCNF(cnf, l, exp);
- //delete exp; //FIXME
+ deleteCNFExpr(exp);
n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
return l;
}
-//DONE
void produceCNF(CNF * cnf, Edge e) {
CNFExpr* expPos = NULL;
CNFExpr* expNeg = NULL;
}
}
-
-//DONE
bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
if (dest == NULL) {
} else if (isProxy(dest)) {
bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
if (alwaysTrue) {
- Literal clause[] = {getProxy(dest), 0};
- addArrayClauseLiteral(cnf->solver, 2, clause);
+ Literal clause[] = {getProxy(dest)};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
} else {
- Literal clause[] = {-getProxy(dest), 0};
- addArrayClauseLiteral(cnf->solver, 2, clause);
+ Literal clause[] = {-getProxy(dest)};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
}
dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
} else {
- clearCNF(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
}
return true;
}
void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
Node *n=getNodePtrFromEdge(e);
- n->flags.cnfVisitedUp & (1 << sign);
+ n->flags.cnfVisitedUp |= (1 << sign);
if (exp == NULL || isProxy(exp)) return;
if (exp->litSize == 1) {
- Literal l = exp->singletons()[0];
- delete exp;
+ 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 || e->isVarForced())) {
- introProxy(solver, e, exp, sign);
+ } 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 l, CNFExpr *exp) {
- if (alwaysTrueCNF(exp)) {
+void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
+ if (alwaysTrueCNF(expr)) {
return;
} else if (alwaysFalseCNF(expr)) {
- Literal clause[] = {-l, 0};
- addArrayClauseLiteral(cnf->solver, 2, clause);
+ Literal clause[] = {-lcond};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
return;
}
- //FIXME
+ 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 *exp) {
-
+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, VectorEdge * args) {
- args.clear();
+CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
+ clearVectorEdge(&cnf->args);
- *largestEdge = (void*) NULL;
- CnfExp* largest = NULL;
- int i = e->size();
+ *largestEdge = (Edge) {(Node*) NULL};
+ CNFExpr* largest = NULL;
+ Node *n=getNodePtrFromEdge(e);
+ int i = n->numEdges;
while (i != 0) {
- Edge arg = (*e)[--i]; arg.negateIf(isNeg);
+ Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
+ Node * narg = getNodePtrFromEdge(arg);
- if (arg.isVar()) {
- args.push(arg);
+ if (edgeIsVarConst(arg)) {
+ pushVectorEdge(&cnf->args, arg);
continue;
}
- if (arg->op() == NodeOp_Ite || arg->op() == NodeOp_Iff) {
- arg = arg->ptrAnnot(arg.isNeg());
+ if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
+ arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
}
- if (arg->intAnnot(arg.isNeg()) == 1) {
- CnfExp* argExp = (CnfExp*) arg->ptrAnnot(arg.isNeg());
+ if (narg->intAnnot[isNegEdge(arg)] == 1) {
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
if (!isProxy(argExp)) {
if (largest == NULL) {
largest = argExp;
- largestEdge = arg;
+ * largestEdge = arg;
continue;
} else if (argExp->litSize > largest->litSize) {
- args.push(largestEdge);
+ pushVectorEdge(&cnf->args, *largestEdge);
largest = argExp;
- largestEdge = arg;
+ * largestEdge = arg;
continue;
}
}
}
- args.push(arg);
+ pushVectorEdge(&cnf->args, arg);
}
if (largest != NULL) {
- largestEdge->ptrAnnot(largestEdge.isNeg()) = NULL;
+ Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
+ nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
}
return largest;
CNFExpr * produceConjunction(CNF * cnf, Edge e) {
Edge largestEdge;
- CnfExp* accum = fillArgs(e, false, largestEdge);
- if (accum == NULL) accum = new CnfExp(true);
- int i = _args.size();
+ CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
+ if (accum == NULL) accum = allocCNFExprBool(true);
+
+ int i = getSizeVectorEdge(&cnf->args);
while (i != 0) {
- Edge arg(_args[--i]);
- if (arg.isVar()) {
- accum->conjoin(atomLit(arg));
+ Edge arg = getVectorEdge(&cnf->args, --i);
+ if (edgeIsVarConst(arg)) {
+ conjoinCNFLit(accum, getEdgeVar(arg));
} else {
- CnfExp* argExp = (CnfExp*) arg->ptrAnnot(arg.isNeg());
+ Node *narg=getNodePtrFromEdge(arg);
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
- bool destroy = (--arg->intAnnot(arg.isNeg()) == 0);
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
if (isProxy(argExp)) { // variable has been introduced
- accum->conjoin(getProxy(argExp));
+ conjoinCNFLit(accum, getProxy(argExp));
} else {
- accum->conjoin(argExp, destroy);
- if (destroy) arg->ptrAnnot(arg.isNeg()) = NULL;
+ conjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
}
}
}
CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
Edge largestEdge;
- CNFExpr* accum = fillArgs(e, true, largestEdge);
+ CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
if (accum == NULL)
- accum = new CNFExpr(false);
+ accum = allocCNFExprBool(false);
// This is necessary to check to make sure that we don't start out
// with an accumulator that is "too large".
/// be possible to use the correct proxy. That should be fixed.
// at this point, we will either have NULL, or a destructible expression
- if (accum->clauseSize() > CLAUSE_MAX)
- accum = new CNFExpr(introProxy(solver, largestEdge, accum, largestEdge.isNeg()));
+ if (getClauseSizeCNF(accum) > CLAUSE_MAX)
+ accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
- int i = _args.size();
+ int i = getSizeVectorEdge(&cnf->args);
while (i != 0) {
- Edge arg(_args[--i]);
- if (arg.isVar()) {
- accum->disjoin(atomLit(arg));
+ Edge arg=getVectorEdge(&cnf->args, --i);
+ Node *narg=getNodePtrFromEdge(arg);
+ if (edgeIsVarConst(arg)) {
+ disjoinCNFLit(accum, getEdgeVar(arg));
} else {
- CNFExpr* argExp = (CNFExpr*) arg->ptrAnnot(arg.isNeg());
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
- bool destroy = (--arg->intAnnot(arg.isNeg()) == 0);
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
if (isProxy(argExp)) { // variable has been introduced
- accum->disjoin(getProxy(argExp));
+ disjoinCNFLit(accum, getProxy(argExp));
} else if (argExp->litSize == 0) {
- accum->disjoin(argExp, destroy);
+ disjoinCNFExpr(accum, argExp, destroy);
} else {
// check to see if we should introduce a proxy
int aL = accum->litSize; // lits in accum
int eC = getClauseSizeCNF(argExp); // clauses in argument
if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
- accum->disjoin(introProxy(solver, arg, argExp, arg.isNeg()));
+ disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
} else {
- accum->disjoin(argExp, destroy);
- if (destroy) arg->ptrAnnot(arg.isNeg()) = NULL;
+ disjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
}
}
}
projects / satune.git / blobdiff