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

This reverts commit 36bd5bd888f193b70abf43a09bb4fc04cd2a2ff1.

This change is causing a test failure on several build bots:
- https://lab.llvm.org/buildbot/#/builders/139/builds/50255
- https://lab.llvm.org/buildbot/#/builders/216/builds/27735
- https://lab.llvm.org/buildbot/#/builders/247/builds/9334

1 files changed, 8 insertions, 1 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 28a8595..e81048c 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -141,6 +141,8 @@ 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());
 }
 
@@ -211,8 +213,13 @@ 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);
+    Constraint->print(OS, &Names);
     OS << "\n";
   }
 }