gribozavr updated this revision to Diff 447609.
gribozavr added a comment.
Actually visit a subexpression
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D130522/new/
https://reviews.llvm.org/D130522
Files:
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -120,7 +120,7 @@
expectUnsatisfiable(solve({NotXAndY, XAndY}));
}
-TEST(SolverTest, DisjunctionSameVars) {
+TEST(SolverTest, DisjunctionSameVarWithNegation) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
@@ -130,6 +130,15 @@
expectSatisfiable(solve({XOrNotX}), _);
}
+TEST(SolverTest, DisjunctionSameVar) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto XOrX = Ctx.disj(X, X);
+
+ // X v X
+ expectSatisfiable(solve({XOrX}), _);
+}
+
TEST(SolverTest, ConjunctionSameVarsConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
@@ -140,6 +149,15 @@
expectUnsatisfiable(solve({XAndNotX}));
}
+TEST(SolverTest, ConjunctionSameVar) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto XAndX = Ctx.conj(X, X);
+
+ // X ^ X
+ expectSatisfiable(solve({XAndX}), _);
+}
+
TEST(SolverTest, PureVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -263,30 +263,52 @@
const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
const Variable RightSubVar = GetVar(&C->getRightSubValue());
- // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
- // which is already in conjunctive normal form. Below we add each of the
- // conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(negLit(Var), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
+ if (LeftSubVar == RightSubVar) {
+ // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
+ // already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Formula.addClause(negLit(Var), posLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar));
+
+ // Visit a sub-value of `Val` (pick any, they are identical).
+ UnprocessedSubVals.push(&C->getLeftSubValue());
+ } else {
+ // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
+ // which is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Formula.addClause(negLit(Var), posLit(LeftSubVar));
+ Formula.addClause(negLit(Var), posLit(RightSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&C->getLeftSubValue());
+ UnprocessedSubVals.push(&C->getRightSubValue());
+ }
} else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
const Variable RightSubVar = GetVar(&D->getRightSubValue());
- // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
- // which is already in conjunctive normal form. Below we add each of the
- // conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
+ if (LeftSubVar == RightSubVar) {
+ // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
+ // already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Formula.addClause(negLit(Var), posLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar));
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
+ // Visit a sub-value of `Val` (pick any, they are identical).
+ UnprocessedSubVals.push(&D->getLeftSubValue());
+ } else {
+ // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
+ // which is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(RightSubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&D->getLeftSubValue());
+ UnprocessedSubVals.push(&D->getRightSubValue());
+ }
} else if (auto *N = dyn_cast<NegationValue>(Val)) {
const Variable SubVar = GetVar(&N->getSubVal());
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
