Lines Matching defs:Formula

10 #include "clang/Analysis/FlowSensitive/Formula.h"
17 static std::pair<const Formula *, const Formula *>
18 canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
26 static const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
34 const Formula &Arena::makeAtomRef(Atom A) {
36     return &Formula::create(Alloc, Formula::AtomRef, {},
41 const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
45     if (LHS.kind() == Formula::Literal)
47     if (RHS.kind() == Formula::Literal)
50     return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
54 const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
58     if (LHS.kind() == Formula::Literal)
60     if (RHS.kind() == Formula::Literal)
63     return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
67 const Formula &Arena::makeNot(const Formula &Val) {
69     if (Val.kind() == Formula::Not)
71     if (Val.kind() == Formula::Literal)
74     return &Formula::create(Alloc, Formula::Not, {&Val});
78 const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
82     if (LHS.kind() == Formula::Literal)
84     if (RHS.kind() == Formula::Literal)
87     return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
91 const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
95     if (LHS.kind() == Formula::Literal)
97     if (RHS.kind() == Formula::Literal)
100     return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
112 BoolValue &Arena::makeBoolValue(const Formula &F) {
115     It->second = (F.kind() == Formula::AtomRef)
122 const Formula *parse(Arena &A, llvm::StringRef &In) {
179   std::string Formula;
184   FormulaParseError(llvm::StringRef Formula, unsigned Offset)
185       : Formula(Formula), Offset(Offset) {}
189     OS << Formula << "\n";
202 llvm::Expected<const Formula &> Arena::parseFormula(llvm::StringRef In) {