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});