gribozavr2 added inline comments.
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:40-41
// Synthetic boolean values are either atomic values or composites that
// represent conjunctions, disjunctions, and negations.
AtomicBool,
----------------
sgatev wrote:
>
Applied.
================
Comment at: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp:110
+ auto R = debugString(BV.getRightSubValue(), Depth + 1);
+ S = formatv("(=\n{0}\n{1})", L, R);
+ break;
----------------
sgatev wrote:
> I think `<=>` would be more natural.
Yeah, but `=` is what smtlib uses.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:332
+
+ if (LeftSubVar == RightSubVar) {
+ // `X <=> (A <=> A)` is equvalent to `X` which is already in
----------------
xazax.hun wrote:
> gribozavr2 wrote:
> > xazax.hun wrote:
> > > xazax.hun wrote:
> > > > I wonder why this simplification is done here only for
> > > > `BiconditionalValue`. Other operations seem to not do these sorts of
> > > > simplifications. Also, when would we take this branch? `getOrCreateIff`
> > > > has a special case when both operands are the same.
> > > Oh, looking at the other patch I see it mentioning desugaring. So can
> > > desugaring also introduce `Biconditional`s?
> > It is also necessary in the other cases due to the precondition of
> > `addClause()`, I'm adding that special handling in a separate patch:
> > https://reviews.llvm.org/D130522
> >
> > We would take this branch when someone avoids using the DataflowContext
> > API. So not extremely likely at the moment, but it is a latent bug that can
> > be exposed by some future refactoring.
> I see, thanks!
Marking done.
================
Comment at: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp:201
+
+ expectUnsatisfiable(solve({NotEquivalent}));
+}
----------------
sgatev wrote:
> Let's add a label: `!((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))`
Added!
================
Comment at: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp:303
+
+ expectUnsatisfiable(solve({NotEquivalent}));
+}
----------------
sgatev wrote:
> Let's add a label: `!((X => Y) <=> (!X v Y))`
Added!
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D130519/new/
https://reviews.llvm.org/D130519
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
