================
@@ -95,4 +98,94 @@ BoolValue &Arena::makeBoolValue(const Formula &F) {
return *It->second;
}
+namespace {
+const Formula *parse(Arena &A, llvm::StringRef &In) {
+ auto EatWhitespace = [&] { In = In.ltrim(' '); };
+ EatWhitespace();
+
+ if (In.consume_front("!")) {
+ if (auto *Arg = parse(A, In))
+ return &A.makeNot(*Arg);
+ return nullptr;
+ }
+
+ if (In.consume_front("(")) {
+ auto *Arg1 = parse(A, In);
+ if (!Arg1)
+ return nullptr;
+
+ EatWhitespace();
+ decltype(&Arena::makeOr) Op;
+ if (In.consume_front("|"))
+ Op = &Arena::makeOr;
+ else if (In.consume_front("&"))
+ Op = &Arena::makeAnd;
+ else if (In.consume_front("=>"))
+ Op = &Arena::makeImplies;
+ else if (In.consume_front("="))
+ Op = &Arena::makeEquals;
+ else
+ return nullptr;
+
+ auto *Arg2 = parse(A, In);
+ if (!Arg2)
+ return nullptr;
+
+ EatWhitespace();
+ if (!In.consume_front(")"))
+ return nullptr;
+
+ return &(A.*Op)(*Arg1, *Arg2);
+ }
+
+ if (In.consume_front("V")) {
+ std::underlying_type_t<Atom> At;
+ if (In.consumeInteger(10, At))
+ return nullptr;
+ return &A.makeAtomRef(static_cast<Atom>(At));
+ }
+
+ if (In.consume_front("true"))
+ return &A.makeLiteral(true);
+ if (In.consume_front("false"))
+ return &A.makeLiteral(false);
+
+ return nullptr;
+}
+
+class FormulaParseError : public llvm::ErrorInfo<FormulaParseError> {
+ unsigned Offset;
+ std::string Formula;
----------------
martinboehme wrote:
Nit: Reorder to match order of constructor parameters?
https://github.com/llvm/llvm-project/pull/66424
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
