-void countPass(CNF *cnf) {
- uint numConstraints = getSizeVectorEdge(&cnf->constraints);
- VectorEdge *ve = allocDefVectorEdge();
- for (uint i = 0; i < numConstraints; i++) {
- countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
- }
- deleteVectorEdge(ve);
-}
-
-void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
- //Skip constants and variables...
- if (edgeIsVarConst(eroot))
- return;
-
- clearVectorEdge(stack);pushVectorEdge(stack, eroot);
-
- bool isMatching = cnf->enableMatching;
-
- while (getSizeVectorEdge(stack) != 0) {
- Edge e = lastVectorEdge(stack); popVectorEdge(stack);
- bool polarity = isNegEdge(e);
- Node *n = getNodePtrFromEdge(e);
- if (getExpanded(n, polarity)) {
- if (n->flags.type == NodeType_IFF ||
- n->flags.type == NodeType_ITE) {
- Edge pExp = {(Node *)n->ptrAnnot[polarity]};
- getNodePtrFromEdge(pExp)->intAnnot[0]++;
- } else {
- n->intAnnot[polarity]++;
- }
- } else {
- setExpanded(n, polarity);
-
- if (n->flags.type == NodeType_ITE ||
- n->flags.type == NodeType_IFF) {
- n->intAnnot[polarity] = 0;
- Edge cond = n->edges[0];
- Edge thenedge = n->edges[1];
- Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
- thenedge = constraintNegateIf(thenedge, !polarity);
- elseedge = constraintNegateIf(elseedge, !polarity);
- thenedge = constraintAND2(cnf, cond, thenedge);
- cond = constraintNegate(cond);
- elseedge = constraintAND2(cnf, cond, elseedge);
- thenedge = constraintNegate(thenedge);
- elseedge = constraintNegate(elseedge);
- cnf->enableMatching = false;
- Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
- n->ptrAnnot[polarity] = succ1.node_ptr;
- cnf->enableMatching = isMatching;
- pushVectorEdge(stack, succ1);
- if (getExpanded(n, !polarity)) {
- Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
- Node *n1 = getNodePtrFromEdge(succ1);
- Node *n2 = getNodePtrFromEdge(succ2);
- n1->ptrAnnot[0] = succ2.node_ptr;
- n2->ptrAnnot[0] = succ1.node_ptr;
- n1->ptrAnnot[1] = succ2.node_ptr;
- n2->ptrAnnot[1] = succ1.node_ptr;
- }
- } else {
- n->intAnnot[polarity] = 1;
- for (uint i = 0; i < n->numEdges; i++) {
- Edge succ = n->edges[i];
- if (!edgeIsVarConst(succ)) {
- succ = constraintNegateIf(succ, polarity);
- pushVectorEdge(stack, succ);
- }
- }
- }
- }
- }
-}
-
-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)) {
- nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
- root = (Edge) { nroot };
- }
- 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)];
- ASSERT(cnfExp != NULL);
- 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, 2, 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;
-}
-