SimplifyConstraints.cpp Source File (original) (raw)

10#include "llvm/ADT/EquivalenceClasses.h"

19 const llvm::DenseMap<Atom, const Formula *> &Substitutions,

21 switch (F.kind()) {

23 if (auto iter = Substitutions.find(F.getAtom());

24 iter != Substitutions.end())

25 return *iter->second;

26 return F;

28 return F;

44 }

45 llvm_unreachable("Unknown formula kind");

46}

52static llvm::DenseSet

54 llvm::EquivalenceClasses &EquivalentAtoms) {

55 llvm::DenseSet Result;

58 Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom));

61}

67 const Atom &At) {

69 for (auto MemberIt = EquivalentAtoms.findLeader(At);

70 MemberIt != EquivalentAtoms.member_end(); ++MemberIt)

71 Result.push_back(*MemberIt);

73}

77 auto contradiction = [&]() {

78 Constraints.clear();

79 Constraints.insert(&arena.makeLiteral(false));

80 };

82 llvm::EquivalenceClasses EquivalentAtoms;

83 llvm::DenseSet TrueAtoms;

84 llvm::DenseSet FalseAtoms;

86 while (true) {

87 for (const auto *Constraint : Constraints) {

88 switch (Constraint->kind()) {

90 TrueAtoms.insert(Constraint->getAtom());

91 break;

94 FalseAtoms.insert(Constraint->operands()[0]->getAtom());

95 break;

100 EquivalentAtoms.unionSets(operands[0]->getAtom(),

101 operands[1]->getAtom());

102 }

103 break;

104 }

105 default:

106 break;

107 }

108 }

109

112

113 llvm::DenseMap<Atom, const Formula *> Substitutions;

114 for (const auto &E : EquivalentAtoms) {

115 Atom TheAtom = E->getData();

116 Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);

117 if (TrueAtoms.contains(Leader)) {

118 if (FalseAtoms.contains(Leader)) {

119 contradiction();

120 return;

121 }

122 Substitutions.insert({TheAtom, &arena.makeLiteral(true)});

123 } else if (FalseAtoms.contains(Leader)) {

124 Substitutions.insert({TheAtom, &arena.makeLiteral(false)});

125 } else if (TheAtom != Leader) {

126 Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});

127 }

128 }

129

130 llvm::SetVector<const Formula *> NewConstraints;

131 for (const auto *Constraint : Constraints) {

132 const Formula &NewConstraint =

133 substitute(*Constraint, Substitutions, arena);

134 if (NewConstraint.isLiteral(true))

135 continue;

136 if (NewConstraint.isLiteral(false)) {

137 contradiction();

138 return;

139 }

141 NewConstraints.insert(NewConstraint.operands()[0]);

142 NewConstraints.insert(NewConstraint.operands()[1]);

143 continue;

144 }

145 NewConstraints.insert(&NewConstraint);

146 }

147

148 if (NewConstraints == Constraints)

149 break;

150 Constraints = std::move(NewConstraints);

151 }

152

153 if (Info) {

154 for (const auto &E : EquivalentAtoms) {

155 if (!E->isLeader())

156 continue;

157 Atom At = *EquivalentAtoms.findLeader(*E);

158 if (TrueAtoms.contains(At) || FalseAtoms.contains(At))

159 continue;

162 if (Atoms.size() == 1)

163 continue;

164 std::sort(Atoms.begin(), Atoms.end());

166 }

167 for (Atom At : TrueAtoms)

170 for (Atom At : FalseAtoms)

173 }

174}

175

176}

177}

The Arena owns the objects that model data within an analysis.

const Formula & makeEquals(const Formula &LHS, const Formula &RHS)

Returns a formula for LHS <=> RHS.

const Formula & makeAtomRef(Atom A)

Returns a formula for the variable A.

const Formula & makeNot(const Formula &Val)

Returns a formula for the negation of Val.

const Formula & makeOr(const Formula &LHS, const Formula &RHS)

Returns a formula for the disjunction of LHS and RHS.

const Formula & makeAnd(const Formula &LHS, const Formula &RHS)

Returns a formula for the conjunction of LHS and RHS.

const Formula & makeImplies(const Formula &LHS, const Formula &RHS)

Returns a formula for LHS => RHS.

const Formula & makeLiteral(bool Value)

Returns a formula for a literal true/false.

ArrayRef< const Formula * > operands() const

bool isLiteral(bool b) const

@ Equal

True if LHS is false or RHS is true.

@ Implies

True if either LHS or RHS is true.

@ AtomRef

A reference to an atomic boolean variable.

@ Literal

Constant true or false.

@ Or

True if LHS and RHS are both true.

@ And

True if its only operand is false.

Dataflow Directional Tag Classes.

static llvm::SmallVector< Atom > atomsInEquivalenceClass(const llvm::EquivalenceClasses< Atom > &EquivalentAtoms, const Atom &At)

Definition SimplifyConstraints.cpp:66

Atom

Identifies an atomic boolean variable such as "V1".

void simplifyConstraints(llvm::SetVector< const Formula * > &Constraints, Arena &arena, SimplifyConstraintsInfo *Info=nullptr)

Simplifies a set of constraints (implicitly connected by "and") in a way that does not change satisfi...

Definition SimplifyConstraints.cpp:75

static llvm::DenseSet< Atom > projectToLeaders(const llvm::DenseSet< Atom > &Atoms, llvm::EquivalenceClasses< Atom > &EquivalentAtoms)

Definition SimplifyConstraints.cpp:53

static const Formula & substitute(const Formula &F, const llvm::DenseMap< Atom, const Formula * > &Substitutions, Arena &arena)

Definition SimplifyConstraints.cpp:18

The JSON file list parser is used to communicate input to InstallAPI.

@ Result

The result type of a method or function.

Information on the way a set of constraints was simplified.

llvm::SmallVector< Atom > TrueAtoms

Atoms that the original constraints imply must be true.

llvm::SmallVector< llvm::SmallVector< Atom > > EquivalentAtoms

List of equivalence classes of atoms.

llvm::SmallVector< Atom > FalseAtoms

Atoms that the original constraints imply must be false.