Lines Matching defs:LHS

18 canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
19 auto Res = std::make_pair(&LHS, &RHS);
20 if (&RHS < &LHS) // FIXME: use a deterministic order instead
41 const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
42 return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
43 if (&LHS == &RHS)
44 return &LHS;
45 if (LHS.kind() == Formula::Literal)
46 return LHS.literal() ? &RHS : &LHS;
48 return RHS.literal() ? &LHS : &RHS;
50 return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
54 const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
55 return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
56 if (&LHS == &RHS)
57 return &LHS;
58 if (LHS.kind() == Formula::Literal)
59 return LHS.literal() ? &LHS : &RHS;
61 return RHS.literal() ? &RHS : &LHS;
63 return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
78 const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
79 return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
80 if (&LHS == &RHS)
82 if (LHS.kind() == Formula::Literal)
83 return LHS.literal() ? &RHS : &makeLiteral(true);
85 return RHS.literal() ? &RHS : &makeNot(LHS);
87 return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
91 const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
92 return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
93 if (&LHS == &RHS)
95 if (LHS.kind() == Formula::Literal)
96 return LHS.literal() ? &RHS : &makeNot(RHS);
98 return RHS.literal() ? &LHS : &makeNot(LHS);
100 return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});