@@ -22,63 +22,83 @@ canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
2222 return Res;
2323}
2424
25- const Formula &Arena::makeAtomRef (Atom A) {
26- auto [It, Inserted] = AtomRefs.try_emplace (A);
25+ template <class Key , class ComputeFunc >
26+ const Formula &cached (llvm::DenseMap<Key, const Formula *> &Cache, Key K,
27+ ComputeFunc &&Compute) {
28+ auto [It, Inserted] = Cache.try_emplace (std::forward<Key>(K));
2729 if (Inserted)
28- It->second =
29- &Formula::create (Alloc, Formula::AtomRef, {}, static_cast <unsigned >(A));
30+ It->second = Compute ();
3031 return *It->second ;
3132}
3233
33- const Formula &Arena::makeAnd (const Formula &LHS, const Formula &RHS) {
34- if (&LHS == &RHS)
35- return LHS;
34+ const Formula &Arena::makeAtomRef (Atom A) {
35+ return cached (AtomRefs, A, [&] {
36+ return &Formula::create (Alloc, Formula::AtomRef, {},
37+ static_cast <unsigned >(A));
38+ });
39+ }
3640
37- auto [It, Inserted] =
38- Ands.try_emplace (canonicalFormulaPair (LHS, RHS), nullptr );
39- if (Inserted)
40- It->second = &Formula::create (Alloc, Formula::And, {&LHS, &RHS});
41- return *It->second ;
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;
47+ if (RHS.kind () == Formula::Literal)
48+ return RHS.literal () ? &LHS : &RHS;
49+
50+ return &Formula::create (Alloc, Formula::And, {&LHS, &RHS});
51+ });
4252}
4353
4454const Formula &Arena::makeOr (const Formula &LHS, const Formula &RHS) {
45- if (&LHS == &RHS)
46- return LHS;
47-
48- auto [It, Inserted] =
49- Ors.try_emplace (canonicalFormulaPair (LHS, RHS), nullptr );
50- if (Inserted)
51- It->second = &Formula::create (Alloc, Formula::Or, {&LHS, &RHS});
52- return *It->second ;
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;
60+ if (RHS.kind () == Formula::Literal)
61+ return RHS.literal () ? &RHS : &LHS;
62+
63+ return &Formula::create (Alloc, Formula::Or, {&LHS, &RHS});
64+ });
5365}
5466
5567const Formula &Arena::makeNot (const Formula &Val) {
56- auto [It, Inserted] = Nots.try_emplace (&Val, nullptr );
57- if (Inserted)
58- It->second = &Formula::create (Alloc, Formula::Not, {&Val});
59- return *It->second ;
68+ return cached (Nots, &Val, [&] {
69+ if (Val.kind () == Formula::Not)
70+ return Val.operands ()[0 ];
71+ if (Val.kind () == Formula::Literal)
72+ return &makeLiteral (!Val.literal ());
73+
74+ return &Formula::create (Alloc, Formula::Not, {&Val});
75+ });
6076}
6177
6278const Formula &Arena::makeImplies (const Formula &LHS, const Formula &RHS) {
63- if (&LHS == &RHS)
64- return makeLiteral (true );
65-
66- auto [It, Inserted] =
67- Implies.try_emplace (std::make_pair (&LHS, &RHS), nullptr );
68- if (Inserted)
69- It->second = &Formula::create (Alloc, Formula::Implies, {&LHS, &RHS});
70- return *It->second ;
79+ return cached (Implies, std::make_pair (&LHS, &RHS), [&] {
80+ if (&LHS == &RHS)
81+ return &makeLiteral (true );
82+ if (LHS.kind () == Formula::Literal)
83+ return LHS.literal () ? &RHS : &makeLiteral (true );
84+ if (RHS.kind () == Formula::Literal)
85+ return RHS.literal () ? &RHS : &makeNot (LHS);
86+
87+ return &Formula::create (Alloc, Formula::Implies, {&LHS, &RHS});
88+ });
7189}
7290
7391const Formula &Arena::makeEquals (const Formula &LHS, const Formula &RHS) {
74- if (&LHS == &RHS)
75- return makeLiteral (true );
76-
77- auto [It, Inserted] =
78- Equals.try_emplace (canonicalFormulaPair (LHS, RHS), nullptr );
79- if (Inserted)
80- It->second = &Formula::create (Alloc, Formula::Equal, {&LHS, &RHS});
81- return *It->second ;
92+ return cached (Equals, canonicalFormulaPair (LHS, RHS), [&] {
93+ if (&LHS == &RHS)
94+ return &makeLiteral (true );
95+ if (LHS.kind () == Formula::Literal)
96+ return LHS.literal () ? &RHS : &makeNot (RHS);
97+ if (RHS.kind () == Formula::Literal)
98+ return RHS.literal () ? &LHS : &makeNot (LHS);
99+
100+ return &Formula::create (Alloc, Formula::Equal, {&LHS, &RHS});
101+ });
82102}
83103
84104IntegerValue &Arena::makeIntLiteral (llvm::APInt Value) {
0 commit comments