-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;
-}
-