From c71fb23e6fa0805d7f30661a1c23adb33e4d28b1 Mon Sep 17 00:00:00 2001
From: Xuan <tanqazx@gmail.com>
Date: Sat, 27 Apr 2024 01:06:47 +0800
Subject: [PATCH] Fix abstraction of Boolean functions.

---
 src/abstractions/boolean.jl  |  5 +++--
 src/abstractions/interval.jl | 38 +++++++++++++++++++++------------
 src/abstractions/set.jl      | 41 ++++++++++++++++++++++++------------
 test/runtests.jl             |  5 ++++-
 4 files changed, 58 insertions(+), 31 deletions(-)

diff --git a/src/abstractions/boolean.jl b/src/abstractions/boolean.jl
index 7574525..f1bf75e 100644
--- a/src/abstractions/boolean.jl
+++ b/src/abstractions/boolean.jl
@@ -61,8 +61,9 @@ end
 
 widen(a::BooleanAbs, b::BooleanAbs) = lub(a, b)
 
-equiv(a::Both, b::Bool) = true
-equiv(a::Bool, b::Both) = true
+equiv(a::Both, b::Both) = both
+equiv(a::Both, b::Bool) = both
+equiv(a::Bool, b::Both) = both
 
 Base.:(!)(::Both) = both
 
diff --git a/src/abstractions/interval.jl b/src/abstractions/interval.jl
index 019f5ee..ce1a5e7 100644
--- a/src/abstractions/interval.jl
+++ b/src/abstractions/interval.jl
@@ -133,17 +133,27 @@ Base.issubset(a::IntervalAbs, b::IntervalAbs) =
 Base.in(a::Real, b::IntervalAbs) =
     a >= b.lo && a <= b.hi
 
-equiv(a::IntervalAbs, b::IntervalAbs) = !(a.lo > b.hi || a.hi < b.lo)
-nequiv(a::IntervalAbs, b::IntervalAbs) = a.lo > b.hi || a.hi < b.lo
-Base.:<(a::IntervalAbs, b::IntervalAbs) = a.lo < b.hi
-Base.:<=(a::IntervalAbs, b::IntervalAbs) = a.lo <= b.hi
-
-equiv(a::IntervalAbs, b::Real) = b in a
-nequiv(a::IntervalAbs, b::Real) = !(a.lo == a.hi == b)
-Base.:<(a::IntervalAbs, b::Real) = a.lo < b
-Base.:<=(a::IntervalAbs, b::Real) = a.lo <= b
-
-equiv(a::Real, b::IntervalAbs) = a in b
-nequiv(a::Real, b::IntervalAbs) = !(a == b.lo == b.hi)
-Base.:<(a::Real, b::IntervalAbs) = a < b.hi
-Base.:<=(a::Real, b::IntervalAbs) = a <= b.hi
+equiv(a::IntervalAbs, b::IntervalAbs) = (a.lo > b.hi || a.hi < b.lo) ?
+    false : ((a.lo == a.hi == b.lo == b.hi) ? true : both)
+nequiv(a::IntervalAbs, b::IntervalAbs) = (a.lo > b.hi || a.hi < b.lo) ?
+    true : ((a.lo == a.hi == b.lo == b.hi) ? false : both)
+Base.:<(a::IntervalAbs, b::IntervalAbs) =
+    a.hi < b.lo ? true : ((a.lo < b.hi) ? both : false)
+Base.:<=(a::IntervalAbs, b::IntervalAbs) = 
+    a.hi <= b.lo ? true : ((a.lo <= b.hi) ? both : false)
+
+equiv(a::IntervalAbs, b::Real) =
+    (b in a) ? ((a.lo == a.hi) ? true : both) : false
+nequiv(a::IntervalAbs, b::Real) =
+    (b in a) ? ((a.lo == a.hi) ? false : both) : true
+Base.:<(a::IntervalAbs, b::Real) =
+    (a.hi < b) ? true : ((a.lo < b) ? both : false)
+Base.:<=(a::IntervalAbs, b::Real) =
+    (a.hi <= b) ? true : ((a.lo <= b) ? both : false)
+
+equiv(a::Real, b::IntervalAbs) = equiv(b, a)
+nequiv(a::Real, b::IntervalAbs) = nequiv(b, a)
+Base.:<(a::Real, b::IntervalAbs) =
+    (a < b.lo) ? true : ((a < b.hi) ? both : false)
+Base.:<=(a::Real, b::IntervalAbs) =
+    (a <= b.lo) ? true : ((a <= b.hi) ? both : false)
diff --git a/src/abstractions/set.jl b/src/abstractions/set.jl
index 546ce77..ca9fbe1 100644
--- a/src/abstractions/set.jl
+++ b/src/abstractions/set.jl
@@ -76,20 +76,33 @@ for f in (:+, :-, :*, :/)
         SetAbs(set=Set(($f(a, y) for y in b.set)))
 end
 
-equiv(a::SetAbs, b::SetAbs) = !isdisjoint(a.set, b.set)
-nequiv(a::SetAbs, b::SetAbs) = isdisjoint(a.set, b.set)
+uniquely_equal(a::SetAbs, b::SetAbs) =
+    (length(a.set) == length(b.set) == 1) && first(a.set) == first(b.set)
+
+equiv(a::SetAbs, b::SetAbs) = 
+    isdisjoint(a.set, b.set) ? false : (uniquely_equal(a, b) ? true : both)
+nequiv(a::SetAbs, b::SetAbs) =
+    isdisjoint(a.set, b.set) ? true : (uniquely_equal(a, b) ? false : both)
 
 Base.:<(a::SetAbs, b::SetAbs) =
-    any(x < y for x in a.set, y in b.set)
+    lub(BooleanAbs, (x < y for x in a.set, y in b.set))
 Base.:<=(a::SetAbs, b::SetAbs) =
-    any(x <= y for x in a.set, y in b.set)
-
-equiv(a::SetAbs{T}, b::T) where {T} = b in a.set
-nequiv(a::SetAbs{T}, b::T) where {T} = !(b in a.set)
-Base.:<(a::SetAbs, b::Real) = any(x < b for x in a.set)
-Base.:<=(a::SetAbs, b::Real) = any(x <= b for x in a.set)
-
-equiv(a::T, b::SetAbs{T}) where {T} = a in b.set
-nequiv(a::T, b::SetAbs{T}) where {T} = !(a in b.set)
-Base.:<(a::Real, b::SetAbs) = any(a < x for x in b.set)
-Base.:<=(a::Real, b::SetAbs) = any(a <= b for x in b.set)
+    lub(BooleanAbs, (x <= y for x in a.set, y in b.set))
+
+equiv(a::SetAbs{T}, b::T) where {T} =
+    b in a.set ? (length(a.set) == 1 ? true : both) : false
+nequiv(a::SetAbs{T}, b::T) where {T} =
+    b in a.set ? (length(a.set) == 1 ? false : both) : true
+Base.:<(a::SetAbs, b::Real) =
+    lub(BooleanAbs, (x < b for x in a.set))
+Base.:<=(a::SetAbs, b::Real) =
+    lub(BooleanAbs, (x <= b for x in a.set))
+
+equiv(a::T, b::SetAbs{T}) where {T} =
+    a in b.set ? (length(b.set) == 1 ? true : both) : false
+nequiv(a::T, b::SetAbs{T}) where {T} =
+    a in b.set ? (length(b.set) == 1 ? false : both) : true
+Base.:<(a::Real, b::SetAbs) =
+    lub(BooleanAbs, (a < y for y in b.set))
+Base.:<=(a::Real, b::SetAbs) =
+    lub(BooleanAbs, (a <= y for y in b.set))
diff --git a/test/runtests.jl b/test/runtests.jl
index fcacd5c..58c779e 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -1,7 +1,10 @@
 using PDDL, PDDL.Parser, Test
 
 # Define equivalence shorthand for abstract interpreter testing
-≃(a, b) = PDDL.equiv(a, b)
+function ≃(a, b)
+    val = PDDL.equiv(a, b)
+    return (val == true) || (val == PDDL.both)
+end
 
 include("parser/test.jl")
 include("strips/test.jl")