diff options
author | Dmitri Gribenko <gribozavr@gmail.com> | 2022-07-07 21:37:26 +0200 |
---|---|---|
committer | Dmitri Gribenko <gribozavr@gmail.com> | 2022-07-07 21:50:52 +0200 |
commit | 63fac424e674bbd77f63e2c76cda9ae28552916a (patch) | |
tree | c6ea55e7c445cdc5644eaacba08f4d44a373c100 /clang/unittests | |
parent | 65cac0ed9266e3551663358de677161ce25a25bf (diff) | |
download | llvm-63fac424e674bbd77f63e2c76cda9ae28552916a.zip llvm-63fac424e674bbd77f63e2c76cda9ae28552916a.tar.gz llvm-63fac424e674bbd77f63e2c76cda9ae28552916a.tar.bz2 |
Revert "[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`."
This reverts commit 19e21887eb18aa019000c2384ea7f2c91d937489. I
accidentally landed the non-final version of the patch that used
decomposition declarations (not yet usable in LLVM/Clang source).
Diffstat (limited to 'clang/unittests')
-rw-r--r-- | clang/unittests/Analysis/FlowSensitive/SolverTest.cpp | 81 |
1 files changed, 21 insertions, 60 deletions
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index cfce7a0..c5116b9 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -20,12 +20,6 @@ namespace { using namespace clang; using namespace dataflow; -using testing::_; -using testing::AnyOf; -using testing::Optional; -using testing::Pair; -using testing::UnorderedElementsAre; - class SolverTest : public ::testing::Test { protected: // Checks if the conjunction of `Vals` is satisfiable and returns the @@ -70,17 +64,6 @@ protected: return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal)); } - void expectUnsatisfiable(Solver::Result Result) { - EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable); - EXPECT_FALSE(Result.getSolution().has_value()); - } - - template <typename Matcher> - void expectSatisfiable(Solver::Result Result, Matcher Solution) { - EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable); - EXPECT_THAT(Result.getSolution(), Optional(Solution)); - } - private: std::vector<std::unique_ptr<BoolValue>> Vals; }; @@ -89,9 +72,7 @@ TEST_F(SolverTest, Var) { auto X = atom(); // X - expectSatisfiable( - solve({X}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue))); + EXPECT_EQ(solve({X}), Solver::Result::Satisfiable); } TEST_F(SolverTest, NegatedVar) { @@ -99,9 +80,7 @@ TEST_F(SolverTest, NegatedVar) { auto NotX = neg(X); // !X - expectSatisfiable( - solve({NotX}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse))); + EXPECT_EQ(solve({NotX}), Solver::Result::Satisfiable); } TEST_F(SolverTest, UnitConflict) { @@ -109,7 +88,7 @@ TEST_F(SolverTest, UnitConflict) { auto NotX = neg(X); // X ^ !X - expectUnsatisfiable(solve({X, NotX})); + EXPECT_EQ(solve({X, NotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, DistinctVars) { @@ -118,10 +97,7 @@ TEST_F(SolverTest, DistinctVars) { auto NotY = neg(Y); // X ^ !Y - expectSatisfiable( - solve({X, NotY}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), - Pair(Y, Solver::Result::Assignment::AssignedFalse))); + EXPECT_EQ(solve({X, NotY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, DoubleNegation) { @@ -130,7 +106,7 @@ TEST_F(SolverTest, DoubleNegation) { auto NotNotX = neg(NotX); // !!X ^ !X - expectUnsatisfiable(solve({NotNotX, NotX})); + EXPECT_EQ(solve({NotNotX, NotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, NegatedDisjunction) { @@ -140,7 +116,7 @@ TEST_F(SolverTest, NegatedDisjunction) { auto NotXOrY = neg(XOrY); // !(X v Y) ^ (X v Y) - expectUnsatisfiable(solve({NotXOrY, XOrY})); + EXPECT_EQ(solve({NotXOrY, XOrY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, NegatedConjunction) { @@ -150,7 +126,7 @@ TEST_F(SolverTest, NegatedConjunction) { auto NotXAndY = neg(XAndY); // !(X ^ Y) ^ (X ^ Y) - expectUnsatisfiable(solve({NotXAndY, XAndY})); + EXPECT_EQ(solve({NotXAndY, XAndY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, DisjunctionSameVars) { @@ -159,7 +135,7 @@ TEST_F(SolverTest, DisjunctionSameVars) { auto XOrNotX = disj(X, NotX); // X v !X - expectSatisfiable(solve({XOrNotX}), _); + EXPECT_EQ(solve({XOrNotX}), Solver::Result::Satisfiable); } TEST_F(SolverTest, ConjunctionSameVarsConflict) { @@ -168,7 +144,7 @@ TEST_F(SolverTest, ConjunctionSameVarsConflict) { auto XAndNotX = conj(X, NotX); // X ^ !X - expectUnsatisfiable(solve({XAndNotX})); + EXPECT_EQ(solve({XAndNotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, PureVar) { @@ -180,10 +156,7 @@ TEST_F(SolverTest, PureVar) { auto NotXOrNotY = disj(NotX, NotY); // (!X v Y) ^ (!X v !Y) - expectSatisfiable( - solve({NotXOrY, NotXOrNotY}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), - Pair(Y, _))); + EXPECT_EQ(solve({NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, MustAssumeVarIsFalse) { @@ -196,10 +169,7 @@ TEST_F(SolverTest, MustAssumeVarIsFalse) { auto NotXOrNotY = disj(NotX, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) - expectSatisfiable( - solve({XOrY, NotXOrY, NotXOrNotY}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), - Pair(Y, Solver::Result::Assignment::AssignedTrue))); + EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, DeepConflict) { @@ -213,7 +183,8 @@ TEST_F(SolverTest, DeepConflict) { auto XOrNotY = disj(X, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y) - expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY})); + EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), + Solver::Result::Unsatisfiable); } TEST_F(SolverTest, IffSameVars) { @@ -221,7 +192,7 @@ TEST_F(SolverTest, IffSameVars) { auto XEqX = iff(X, X); // X <=> X - expectSatisfiable(solve({XEqX}), _); + EXPECT_EQ(solve({XEqX}), Solver::Result::Satisfiable); } TEST_F(SolverTest, IffDistinctVars) { @@ -230,14 +201,7 @@ TEST_F(SolverTest, IffDistinctVars) { auto XEqY = iff(X, Y); // X <=> Y - expectSatisfiable( - solve({XEqY}), - AnyOf(UnorderedElementsAre( - Pair(X, Solver::Result::Assignment::AssignedTrue), - Pair(Y, Solver::Result::Assignment::AssignedTrue)), - UnorderedElementsAre( - Pair(X, Solver::Result::Assignment::AssignedFalse), - Pair(Y, Solver::Result::Assignment::AssignedFalse)))); + EXPECT_EQ(solve({XEqY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, IffWithUnits) { @@ -246,10 +210,7 @@ TEST_F(SolverTest, IffWithUnits) { auto XEqY = iff(X, Y); // (X <=> Y) ^ X ^ Y - expectSatisfiable( - solve({XEqY, X, Y}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), - Pair(Y, Solver::Result::Assignment::AssignedTrue))); + EXPECT_EQ(solve({XEqY, X, Y}), Solver::Result::Satisfiable); } TEST_F(SolverTest, IffWithUnitsConflict) { @@ -259,7 +220,7 @@ TEST_F(SolverTest, IffWithUnitsConflict) { auto NotY = neg(Y); // (X <=> Y) ^ X !Y - expectUnsatisfiable(solve({XEqY, X, NotY})); + EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, IffTransitiveConflict) { @@ -271,7 +232,7 @@ TEST_F(SolverTest, IffTransitiveConflict) { auto NotX = neg(X); // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X - expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX})); + EXPECT_EQ(solve({XEqY, YEqZ, Z, NotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, DeMorgan) { @@ -287,7 +248,7 @@ TEST_F(SolverTest, DeMorgan) { auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W))); // A ^ B - expectSatisfiable(solve({A, B}), _); + EXPECT_EQ(solve({A, B}), Solver::Result::Satisfiable); } TEST_F(SolverTest, RespectsAdditionalConstraints) { @@ -297,7 +258,7 @@ TEST_F(SolverTest, RespectsAdditionalConstraints) { auto NotY = neg(Y); // (X <=> Y) ^ X ^ !Y - expectUnsatisfiable(solve({XEqY, X, NotY})); + EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, ImplicationConflict) { @@ -307,7 +268,7 @@ TEST_F(SolverTest, ImplicationConflict) { auto *XAndNotY = conj(X, neg(Y)); // X => Y ^ X ^ !Y - expectUnsatisfiable(solve({XImplY, XAndNotY})); + EXPECT_EQ(solve({XImplY, XAndNotY}), Solver::Result::Unsatisfiable); } } // namespace |