10#include "llvm/ADT/EquivalenceClasses.h"
19 const llvm::DenseMap<Atom, const Formula *> &Substitutions,
23 if (
auto iter = Substitutions.find(F.
getAtom());
24 iter != Substitutions.end())
45 llvm_unreachable(
"Unknown formula kind");
54 llvm::EquivalenceClasses<Atom> &EquivalentAtoms) {
58 Result.insert(EquivalentAtoms.getOrInsertLeaderValue(
Atom));
67 llvm::EquivalenceClasses<Atom>::iterator LeaderIt) {
69 for (
auto MemberIt = EquivalentAtoms.member_begin(LeaderIt);
70 MemberIt != EquivalentAtoms.member_end(); ++MemberIt)
71 Result.push_back(*MemberIt);
77 auto contradiction = [&]() {
82 llvm::EquivalenceClasses<Atom> EquivalentAtoms;
87 for (
const auto *Constraint : Constraints) {
88 switch (Constraint->kind()) {
90 TrueAtoms.insert(Constraint->getAtom());
94 FalseAtoms.insert(Constraint->operands()[0]->getAtom());
100 EquivalentAtoms.unionSets(operands[0]->getAtom(),
101 operands[1]->getAtom());
113 llvm::DenseMap<Atom, const Formula *> Substitutions;
114 for (
auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) {
115 Atom TheAtom = It->getData();
116 Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);
117 if (TrueAtoms.contains(Leader)) {
118 if (FalseAtoms.contains(Leader)) {
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)});
130 llvm::SetVector<const Formula *> NewConstraints;
131 for (
const auto *Constraint : Constraints) {
133 substitute(*Constraint, Substitutions, arena);
141 NewConstraints.insert(NewConstraint.
operands()[0]);
142 NewConstraints.insert(NewConstraint.
operands()[1]);
145 NewConstraints.insert(&NewConstraint);
148 if (NewConstraints == Constraints)
150 Constraints = std::move(NewConstraints);
154 for (
auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end();
158 Atom At = *EquivalentAtoms.findLeader(It);
159 if (TrueAtoms.contains(At) || FalseAtoms.contains(At))
163 if (Atoms.size() == 1)
165 std::sort(Atoms.begin(), Atoms.end());
168 for (
Atom At : TrueAtoms)
170 EquivalentAtoms, EquivalentAtoms.findValue(At)));
172 for (
Atom At : FalseAtoms)
174 EquivalentAtoms, EquivalentAtoms.findValue(At)));
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.
static llvm::SmallVector< Atom > atomsInEquivalenceClass(const llvm::EquivalenceClasses< Atom > &EquivalentAtoms, llvm::EquivalenceClasses< Atom >::iterator LeaderIt)
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...
static llvm::DenseSet< Atom > projectToLeaders(const llvm::DenseSet< Atom > &Atoms, llvm::EquivalenceClasses< Atom > &EquivalentAtoms)
static const Formula & substitute(const Formula &F, const llvm::DenseMap< Atom, const Formula * > &Substitutions, Arena &arena)
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.