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