/// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
// propagate from positive to negative, negative to positive
- propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
+ propagate(cnf, & expPos, expNeg, true) || propagate(cnf, & expNeg, expPos, true);
// The polarity heuristic entails visiting the discovery polarity first
if (isPosEdge(e)) {
}
}
-bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
+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));
+ *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
} else if (isProxy(dest)) {
bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
if (alwaysTrue) {
addArrayClauseLiteral(cnf->solver, 1, clause);
}
- dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
} else {
clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
}
void produceCNF(CNF * cnf, Edge e);
CNFExpr * produceConjunction(CNF * cnf, Edge e);
CNFExpr* produceDisjunction(CNF *cnf, Edge e);
-bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
+bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate);
void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);