From f8e02e472ac87299c100dce8dcde91a96ca060b1 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 28 Aug 2026 12:53:33 -0700 Subject: [PATCH 1/4] code --- src/ir/constraint.cpp | 86 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index c38c97162b6..6d903d633e0 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -255,6 +255,88 @@ Result provesConstantPair(Abstract::Op aOp, return Unknown; } +// Evaluate whether a => b, where a and b are operations on identical terms. +Result provesEqualTermPair(Abstract::Op aOp, Abstract::Op bOp) { + using namespace Abstract; + + // Trivial cases where aOp == bOp or aOp == !bOp are taken care of elsewhere. + assert(aOp != bOp && aOp != Abstract::negateRelational(bOp)); + + switch (aOp) { + case Eq: + // == proves >= etc. true, and > (without =) false + if (bOp == LeU || bOp == LeS || bOp == GeU || bOp == GeS) { + return True; + } + if (bOp == LtU || bOp == LtS || bOp == GtU || bOp == GtS) { + return False; + } + break; + case LtS: + // < proves <= true and >, >= false + if (bOp == LeS) { + return True; + } + if (bOp == GtS || bOp == GeS) { + return False; + } + break; + case LeS: + // <= proves > false + if (bOp == GtS) { + return False; + } + break; + case GtS: + // Ditto, with G instead of L. + if (bOp == GeS) { + return True; + } + if (bOp == LtS || bOp == LeS) { + return False; + } + break; + case GeS: + if (bOp == LtS) { + return False; + } + break; + case LtU: + // Ditto, with unsigned. + if (bOp == LeU) { + return True; + } + if (bOp == GtU || bOp == GeU) { + return False; + } + break; + case LeU: + // <= proves > false + if (bOp == GtU) { + return False; + } + break; + case GtU: + // Ditto, with G instead of L. + if (bOp == GeU) { + return True; + } + if (bOp == LtU || bOp == LeU) { + return False; + } + break; + case GeU: + if (bOp == LtU) { + return False; + } + break; + default: { + } + } + + return Unknown; +} + // Core comparison of two constraints: whether a => b Result provesPair(const Constraint& a, const Constraint& b) { // A thing always implies itself. @@ -309,6 +391,10 @@ Result provesPair(const Constraint& a, const Constraint& b) { } } + if (a.term == b.term) { + return provesEqualTermPair(a.op, b.op); + } + return Unknown; } From ae7b8a6c13e7fe6f8705a0283c90c708c97217f4 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 28 Aug 2026 13:11:36 -0700 Subject: [PATCH 2/4] tests --- test/gtest/constraint.cpp | 200 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 200 insertions(+) diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index 5c00d18f047..38efdfc1bb8 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -1408,3 +1408,203 @@ TEST(ConstraintTest, FloatNegativeZero) { EXPECT_EQ(s32.proves(Constraint{Eq, {Literal(float(-0.0f))}}), True); EXPECT_EQ(s32.proves(Constraint{Ne, {Literal(float(-0.0f))}}), False); } + +TEST(ConstraintTest, EqualTermPairs) { + // Constraints with the term equal to local $1. + Constraint eq1{Eq, {Index(1)}}; + Constraint ne1{Ne, {Index(1)}}; + Constraint ltS1{LtS, {Index(1)}}; + Constraint leS1{LeS, {Index(1)}}; + Constraint gtS1{GtS, {Index(1)}}; + Constraint geS1{GeS, {Index(1)}}; + Constraint ltU1{LtU, {Index(1)}}; + Constraint leU1{LeU, {Index(1)}}; + Constraint gtU1{GtU, {Index(1)}}; + Constraint geU1{GeU, {Index(1)}}; + + // Constraints with a different term, local $2. + Constraint eq2{Eq, {Index(2)}}; + Constraint ne2{Ne, {Index(2)}}; + Constraint ltS2{LtS, {Index(2)}}; + Constraint leS2{LeS, {Index(2)}}; + Constraint gtS2{GtS, {Index(2)}}; + Constraint geS2{GeS, {Index(2)}}; + Constraint ltU2{LtU, {Index(2)}}; + Constraint leU2{LeU, {Index(2)}}; + Constraint gtU2{GtU, {Index(2)}}; + Constraint geU2{GeU, {Index(2)}}; + + // 1. Eq (x == $1): + // == proves <= and >= (both signed and unsigned) are True. + EXPECT_EQ(AndedConstraintSet{eq1}.proves(leS1), True); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(leU1), True); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(geS1), True); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(geU1), True); + + // == proves < and > (both signed and unsigned) are False. + EXPECT_EQ(AndedConstraintSet{eq1}.proves(ltS1), False); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(ltU1), False); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(gtS1), False); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(gtU1), False); + + // == proves == is True, and != is False. + EXPECT_EQ(AndedConstraintSet{eq1}.proves(eq1), True); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(ne1), False); + + // 2. LtS (x <_s $1): + // < proves <= is True. + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(leS1), True); + // < proves > and >= are False. + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(gtS1), False); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(geS1), False); + // Self + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ltS1), True); + // Cross-signedness and equality are Unknown. + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ltU1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(leU1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(gtU1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(geU1), Unknown); + + // 3. LeS (x <=_s $1): + // <= proves > is False. + EXPECT_EQ(AndedConstraintSet{leS1}.proves(gtS1), False); + // Self + EXPECT_EQ(AndedConstraintSet{leS1}.proves(leS1), True); + // Others are Unknown. + EXPECT_EQ(AndedConstraintSet{leS1}.proves(ltS1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(geS1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(ltU1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(leU1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(gtU1), Unknown); + EXPECT_EQ(AndedConstraintSet{leS1}.proves(geU1), Unknown); + + // 4. GtS (x >_s $1): + // > proves >= is True. + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(geS1), True); + // > proves < and <= are False. + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ltS1), False); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(leS1), False); + // Self + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(gtS1), True); + // Cross-signedness and equality are Unknown. + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ltU1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(leU1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(gtU1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(geU1), Unknown); + + // 5. GeS (x >=_s $1): + // >= proves < is False. + EXPECT_EQ(AndedConstraintSet{geS1}.proves(ltS1), False); + // Self + EXPECT_EQ(AndedConstraintSet{geS1}.proves(geS1), True); + // Others are Unknown. + EXPECT_EQ(AndedConstraintSet{geS1}.proves(gtS1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(leS1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(ltU1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(leU1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(gtU1), Unknown); + EXPECT_EQ(AndedConstraintSet{geS1}.proves(geU1), Unknown); + + // 6. LtU (x <_u $1): + // < proves <= is True. + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(leU1), True); + // < proves > and >= are False. + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(gtU1), False); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(geU1), False); + // Self + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ltU1), True); + // Cross-signedness and equality are Unknown. + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ltS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(leS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(gtS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(geS1), Unknown); + + // 7. LeU (x <=_u $1): + // <= proves > is False. + EXPECT_EQ(AndedConstraintSet{leU1}.proves(gtU1), False); + // Self + EXPECT_EQ(AndedConstraintSet{leU1}.proves(leU1), True); + // Others are Unknown. + EXPECT_EQ(AndedConstraintSet{leU1}.proves(ltU1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(geU1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(ltS1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(leS1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(gtS1), Unknown); + EXPECT_EQ(AndedConstraintSet{leU1}.proves(geS1), Unknown); + + // 8. GtU (x >_u $1): + // > proves >= is True. + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(geU1), True); + // > proves < and <= are False. + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ltU1), False); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(leU1), False); + // Self + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(gtU1), True); + // Cross-signedness and equality are Unknown. + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ltS1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(leS1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(gtS1), Unknown); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(geS1), Unknown); + + // 9. GeU (x >=_u $1): + // >= proves < is False. + EXPECT_EQ(AndedConstraintSet{geU1}.proves(ltU1), False); + // Self + EXPECT_EQ(AndedConstraintSet{geU1}.proves(geU1), True); + // Others are Unknown. + EXPECT_EQ(AndedConstraintSet{geU1}.proves(gtU1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(leU1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(eq1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(ne1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(ltS1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(leS1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(gtS1), Unknown); + EXPECT_EQ(AndedConstraintSet{geU1}.proves(geS1), Unknown); + + // 10. Ne (x != $1): + EXPECT_EQ(AndedConstraintSet{ne1}.proves(ne1), True); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(eq1), False); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(ltS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(leS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(gtS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(geS1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(ltU1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(leU1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(gtU1), Unknown); + EXPECT_EQ(AndedConstraintSet{ne1}.proves(geU1), Unknown); + + // 11. Different terms ($1 != $2) cannot prove one another. + EXPECT_EQ(AndedConstraintSet{eq1}.proves(eq2), Unknown); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(leS2), Unknown); + EXPECT_EQ(AndedConstraintSet{eq1}.proves(ltS2), Unknown); + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(leS2), Unknown); + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(geS2), Unknown); + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(leU2), Unknown); + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(geU2), Unknown); + + // 12. ANDing equal-term constraints: + // Redundant constraints are ignored. + AndedConstraintSet sEq{eq1}; + sEq.approximateAnd(leS1); + EXPECT_EQ(sEq.size(), 1); + EXPECT_EQ(sEq[0], eq1); + + // Contradicting constraints turn the set into a contradiction. + AndedConstraintSet sEqContra{eq1}; + sEqContra.approximateAnd(ltS1); + EXPECT_TRUE(sEqContra.provesEverything()); +} From 798f3478aacc7b2b3cd477aa7203a3194062ce03 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 28 Aug 2026 16:17:05 -0700 Subject: [PATCH 3/4] add more --- src/ir/constraint.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 6d903d633e0..3f9d023ef28 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -256,7 +256,7 @@ Result provesConstantPair(Abstract::Op aOp, } // Evaluate whether a => b, where a and b are operations on identical terms. -Result provesEqualTermPair(Abstract::Op aOp, Abstract::Op bOp) { +Result provesTermEqualPair(Abstract::Op aOp, Abstract::Op bOp) { using namespace Abstract; // Trivial cases where aOp == bOp or aOp == !bOp are taken care of elsewhere. @@ -273,11 +273,11 @@ Result provesEqualTermPair(Abstract::Op aOp, Abstract::Op bOp) { } break; case LtS: - // < proves <= true and >, >= false + // < proves <= true and ==, >, >= false if (bOp == LeS) { return True; } - if (bOp == GtS || bOp == GeS) { + if (bOp == Eq || bOp == GtS || bOp == GeS) { return False; } break; @@ -292,7 +292,7 @@ Result provesEqualTermPair(Abstract::Op aOp, Abstract::Op bOp) { if (bOp == GeS) { return True; } - if (bOp == LtS || bOp == LeS) { + if (bOp == Eq || bOp == LtS || bOp == LeS) { return False; } break; @@ -306,7 +306,7 @@ Result provesEqualTermPair(Abstract::Op aOp, Abstract::Op bOp) { if (bOp == LeU) { return True; } - if (bOp == GtU || bOp == GeU) { + if (bOp == Eq || bOp == GtU || bOp == GeU) { return False; } break; @@ -321,7 +321,7 @@ Result provesEqualTermPair(Abstract::Op aOp, Abstract::Op bOp) { if (bOp == GeU) { return True; } - if (bOp == LtU || bOp == LeU) { + if (bOp == Eq || bOp == LtU || bOp == LeU) { return False; } break; @@ -392,7 +392,7 @@ Result provesPair(const Constraint& a, const Constraint& b) { } if (a.term == b.term) { - return provesEqualTermPair(a.op, b.op); + return provesTermEqualPair(a.op, b.op); } return Unknown; From 05b17b17d3cd09b48a5e9d57f8cc2194cb670f7d Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 28 Aug 2026 16:34:44 -0700 Subject: [PATCH 4/4] tests --- src/ir/constraint.cpp | 40 +++++---------------- test/gtest/constraint.cpp | 76 ++++++++++++++++++++++++++++----------- 2 files changed, 65 insertions(+), 51 deletions(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 3f9d023ef28..868618bd9f2 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -273,60 +273,38 @@ Result provesTermEqualPair(Abstract::Op aOp, Abstract::Op bOp) { } break; case LtS: - // < proves <= true and ==, >, >= false - if (bOp == LeS) { + // < proves <=, != true and ==, > false + if (bOp == LeS || bOp == Ne) { return True; } - if (bOp == Eq || bOp == GtS || bOp == GeS) { - return False; - } - break; - case LeS: - // <= proves > false - if (bOp == GtS) { + if (bOp == Eq || bOp == GtS) { return False; } break; case GtS: // Ditto, with G instead of L. - if (bOp == GeS) { + if (bOp == GeS || bOp == Ne) { return True; } - if (bOp == Eq || bOp == LtS || bOp == LeS) { - return False; - } - break; - case GeS: - if (bOp == LtS) { + if (bOp == Eq || bOp == LtS) { return False; } break; case LtU: // Ditto, with unsigned. - if (bOp == LeU) { + if (bOp == LeU || bOp == Ne) { return True; } - if (bOp == Eq || bOp == GtU || bOp == GeU) { - return False; - } - break; - case LeU: - // <= proves > false - if (bOp == GtU) { + if (bOp == Eq || bOp == GtU) { return False; } break; case GtU: // Ditto, with G instead of L. - if (bOp == GeU) { + if (bOp == GeU || bOp == Ne) { return True; } - if (bOp == Eq || bOp == LtU || bOp == LeU) { - return False; - } - break; - case GeU: - if (bOp == LtU) { + if (bOp == Eq || bOp == LtU) { return False; } break; diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index 38efdfc1bb8..ae0a77d61a3 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -1452,16 +1452,16 @@ TEST(ConstraintTest, EqualTermPairs) { EXPECT_EQ(AndedConstraintSet{eq1}.proves(ne1), False); // 2. LtS (x <_s $1): - // < proves <= is True. + // < proves <= and != are True. EXPECT_EQ(AndedConstraintSet{ltS1}.proves(leS1), True); - // < proves > and >= are False. + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ne1), True); + // < proves ==, >, and >= are False. + EXPECT_EQ(AndedConstraintSet{ltS1}.proves(eq1), False); EXPECT_EQ(AndedConstraintSet{ltS1}.proves(gtS1), False); EXPECT_EQ(AndedConstraintSet{ltS1}.proves(geS1), False); // Self EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ltS1), True); - // Cross-signedness and equality are Unknown. - EXPECT_EQ(AndedConstraintSet{ltS1}.proves(eq1), Unknown); - EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ne1), Unknown); + // Cross-signedness are Unknown. EXPECT_EQ(AndedConstraintSet{ltS1}.proves(ltU1), Unknown); EXPECT_EQ(AndedConstraintSet{ltS1}.proves(leU1), Unknown); EXPECT_EQ(AndedConstraintSet{ltS1}.proves(gtU1), Unknown); @@ -1483,16 +1483,16 @@ TEST(ConstraintTest, EqualTermPairs) { EXPECT_EQ(AndedConstraintSet{leS1}.proves(geU1), Unknown); // 4. GtS (x >_s $1): - // > proves >= is True. + // > proves >= and != are True. EXPECT_EQ(AndedConstraintSet{gtS1}.proves(geS1), True); - // > proves < and <= are False. + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ne1), True); + // > proves ==, <, and <= are False. + EXPECT_EQ(AndedConstraintSet{gtS1}.proves(eq1), False); EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ltS1), False); EXPECT_EQ(AndedConstraintSet{gtS1}.proves(leS1), False); // Self EXPECT_EQ(AndedConstraintSet{gtS1}.proves(gtS1), True); - // Cross-signedness and equality are Unknown. - EXPECT_EQ(AndedConstraintSet{gtS1}.proves(eq1), Unknown); - EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ne1), Unknown); + // Cross-signedness are Unknown. EXPECT_EQ(AndedConstraintSet{gtS1}.proves(ltU1), Unknown); EXPECT_EQ(AndedConstraintSet{gtS1}.proves(leU1), Unknown); EXPECT_EQ(AndedConstraintSet{gtS1}.proves(gtU1), Unknown); @@ -1514,16 +1514,16 @@ TEST(ConstraintTest, EqualTermPairs) { EXPECT_EQ(AndedConstraintSet{geS1}.proves(geU1), Unknown); // 6. LtU (x <_u $1): - // < proves <= is True. + // < proves <= and != are True. EXPECT_EQ(AndedConstraintSet{ltU1}.proves(leU1), True); - // < proves > and >= are False. + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ne1), True); + // < proves ==, >, and >= are False. + EXPECT_EQ(AndedConstraintSet{ltU1}.proves(eq1), False); EXPECT_EQ(AndedConstraintSet{ltU1}.proves(gtU1), False); EXPECT_EQ(AndedConstraintSet{ltU1}.proves(geU1), False); // Self EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ltU1), True); - // Cross-signedness and equality are Unknown. - EXPECT_EQ(AndedConstraintSet{ltU1}.proves(eq1), Unknown); - EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ne1), Unknown); + // Cross-signedness are Unknown. EXPECT_EQ(AndedConstraintSet{ltU1}.proves(ltS1), Unknown); EXPECT_EQ(AndedConstraintSet{ltU1}.proves(leS1), Unknown); EXPECT_EQ(AndedConstraintSet{ltU1}.proves(gtS1), Unknown); @@ -1545,16 +1545,16 @@ TEST(ConstraintTest, EqualTermPairs) { EXPECT_EQ(AndedConstraintSet{leU1}.proves(geS1), Unknown); // 8. GtU (x >_u $1): - // > proves >= is True. + // > proves >= and != are True. EXPECT_EQ(AndedConstraintSet{gtU1}.proves(geU1), True); - // > proves < and <= are False. + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ne1), True); + // > proves ==, <, and <= are False. + EXPECT_EQ(AndedConstraintSet{gtU1}.proves(eq1), False); EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ltU1), False); EXPECT_EQ(AndedConstraintSet{gtU1}.proves(leU1), False); // Self EXPECT_EQ(AndedConstraintSet{gtU1}.proves(gtU1), True); - // Cross-signedness and equality are Unknown. - EXPECT_EQ(AndedConstraintSet{gtU1}.proves(eq1), Unknown); - EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ne1), Unknown); + // Cross-signedness are Unknown. EXPECT_EQ(AndedConstraintSet{gtU1}.proves(ltS1), Unknown); EXPECT_EQ(AndedConstraintSet{gtU1}.proves(leS1), Unknown); EXPECT_EQ(AndedConstraintSet{gtU1}.proves(gtS1), Unknown); @@ -1603,8 +1603,44 @@ TEST(ConstraintTest, EqualTermPairs) { EXPECT_EQ(sEq.size(), 1); EXPECT_EQ(sEq[0], eq1); + AndedConstraintSet sLtS{ltS1}; + sLtS.approximateAnd(ne1); + EXPECT_EQ(sLtS.size(), 1); + EXPECT_EQ(sLtS[0], ltS1); + + AndedConstraintSet sGtS{gtS1}; + sGtS.approximateAnd(ne1); + EXPECT_EQ(sGtS.size(), 1); + EXPECT_EQ(sGtS[0], gtS1); + + AndedConstraintSet sLtU{ltU1}; + sLtU.approximateAnd(ne1); + EXPECT_EQ(sLtU.size(), 1); + EXPECT_EQ(sLtU[0], ltU1); + + AndedConstraintSet sGtU{gtU1}; + sGtU.approximateAnd(ne1); + EXPECT_EQ(sGtU.size(), 1); + EXPECT_EQ(sGtU[0], gtU1); + // Contradicting constraints turn the set into a contradiction. AndedConstraintSet sEqContra{eq1}; sEqContra.approximateAnd(ltS1); EXPECT_TRUE(sEqContra.provesEverything()); + + AndedConstraintSet sLtSContra{ltS1}; + sLtSContra.approximateAnd(eq1); + EXPECT_TRUE(sLtSContra.provesEverything()); + + AndedConstraintSet sGtSContra{gtS1}; + sGtSContra.approximateAnd(eq1); + EXPECT_TRUE(sGtSContra.provesEverything()); + + AndedConstraintSet sLtUContra{ltU1}; + sLtUContra.approximateAnd(eq1); + EXPECT_TRUE(sLtUContra.provesEverything()); + + AndedConstraintSet sGtUContra{gtU1}; + sGtUContra.approximateAnd(eq1); + EXPECT_TRUE(sGtUContra.provesEverything()); }