[dataflow] use true/false literals in formulas, rather than variables

And simplify formulas containing true/false
It's unclear to me how useful this is, it does make formulas more
conveniently self-contained now (we can usefully print them without
carrying around the "true/false" labels)

(while here, simplify !!X to X, too)

Differential Revision: https://reviews.llvm.org/D153485

1 files changed, 1 insertions, 8 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index e81048c..28a8595 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -141,8 +141,6 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
 
 Solver::Result DataflowAnalysisContext::querySolver(
     llvm::SetVector<const Formula *> Constraints) {
-  Constraints.insert(&arena().makeLiteral(true));
-  Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
   return S->solve(Constraints.getArrayRef());
 }
 
@@ -213,13 +211,8 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
   Constraints.insert(&arena().makeAtomRef(Token));
   addTransitiveFlowConditionConstraints(Token, Constraints);
 
-  // TODO: have formulas know about true/false directly instead
-  Atom True = arena().makeLiteral(true).getAtom();
-  Atom False = arena().makeLiteral(false).getAtom();
-  Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
-
   for (const auto *Constraint : Constraints) {
-    Constraint->print(OS, &Names);
+    Constraint->print(OS);
     OS << "\n";
   }
 }