[WIP] Upload work on a Presburger arithmetic decision procedure

Russoul · Russoul · commit 885ab1b56e54 · 2026-04-09T00:05:36.000+04:00
diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal
@@ -79,6 +79,15 @@ library
                     , Cardano.ReCon.LTL.Satisfy
                     , Cardano.ReCon.LTL.Subst
 
+                    , Cardano.ReCon.Presburger.AffineDNF
+                    , Cardano.ReCon.Presburger.CompNF
+                    , Cardano.ReCon.Presburger.Complete
+                    , Cardano.ReCon.Presburger.DNF
+                    , Cardano.ReCon.Presburger.IntTerm.Types
+                    , Cardano.ReCon.Presburger.NegNF
+                    , Cardano.ReCon.Presburger.NormAffineDNF
+                    , Cardano.ReCon.Presburger.QuantifierFree
+
                     , Cardano.ReCon.Trace.Feed
                     , Cardano.ReCon.Trace.Ingest
 
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/AffineDNF.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/AffineDNF.hs
@@ -0,0 +1,66 @@
+module Cardano.ReCon.Presburger.AffineDNF(IntLtForm(..), IntDivForm(..), AffineDNFConjunct(..), AffineDNFDisjunct, AffineDNF, fromDNF) where
+import           Cardano.ReCon.Presburger.DNF (DNF, DNFConjunct)
+import           qualified Cardano.ReCon.Presburger.DNF as DNF
+import           Cardano.ReCon.Presburger.IntTerm.Types
+
+import qualified Data.Map.Strict as Map
+import           Data.Maybe (fromMaybe)
+import           Data.Word (Word64)
+
+data IntLtForm =
+    -- | h · x < i, where h ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
+    LtL Word64 IntTerm
+    -- | i < h · x, where h ∈ ℕ⁺, i ∈ ℤ⟦x̄\{x}⟧
+  | LtR IntTerm Word64
+    -- i < j, where i, j ∈ ℤ⟦x̄\{x}⟧
+  | LtC IntTerm IntTerm deriving (Show, Eq, Ord)
+
+data IntDivForm =
+    -- | (h | k · x + i), where h, k ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
+    DivL Word64 Word64 IntTerm
+    -- | (h | i), where h ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
+  | DivC Word64 IntTerm deriving (Show, Eq, Ord)
+
+data AffineDNFConjunct =
+     -- | h · x < i | i < h · x | i < j
+     IntLt IntLtForm
+     -- | (h | k · x + i) | (h | i)
+   | IntDiv IntDivForm
+     -- | ¬ (h | k · x + i) | ¬ (h | i)
+   | IntNegDiv IntDivForm
+   deriving (Show, Eq, Ord)
+
+type AffineDNFDisjunct = [AffineDNFConjunct]
+
+type AffineDNF = [AffineDNFDisjunct]
+
+classifyIntLt :: IntIdentifier -> IntTerm -> IntTerm -> IntLtForm
+classifyIntLt x a b =
+  let nfa = nf a in
+  let nfb = nf b in
+  let ka = fromMaybe 0 $ Map.lookup x nfa.coeff in
+  let kb = fromMaybe 0 $ Map.lookup x nfb.coeff in
+  case compare (ka - kb) 0 of
+    -- (k(a) - k(b)) · x < ...
+    GT -> LtL (fromIntegral $ ka - kb)
+              (quote (nullify x nfb `minus` nullify x nfa))
+    -- ... < ...
+    EQ -> LtC (quote $ nullify x nfa) (quote $ nullify x nfb)
+    -- ... < (k(b) - k(a)) · x
+    LT -> LtR (quote (nullify x nfa `minus` nullify x nfb))
+              (fromIntegral $ kb - ka)
+
+classifyIntDiv :: IntIdentifier -> Word64 -> IntTerm -> IntDivForm
+classifyIntDiv x k t =
+  let coef = fromMaybe 0 $ Map.lookup x (nf t).coeff in
+  if coef == 0
+    then DivC k (normalise t)
+    else DivL k (fromIntegral $ abs coef) (quote $ nullify x (nf t))
+
+fromDNFConjunct :: IntIdentifier -> DNFConjunct -> AffineDNFConjunct
+fromDNFConjunct x (DNF.IntLt i j) = IntLt $ classifyIntLt x i j
+fromDNFConjunct x (DNF.IntDiv k i) = IntDiv $ classifyIntDiv x k i
+fromDNFConjunct x (DNF.IntNegDiv k i) = IntNegDiv $ classifyIntDiv x k i
+
+fromDNF :: IntIdentifier -> DNF -> AffineDNF
+fromDNF x = map (map (fromDNFConjunct x))
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/CompNF.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/CompNF.hs
@@ -0,0 +1,51 @@
+module Cardano.ReCon.Presburger.CompNF(CompNF(..), fromNegNF) where
+import qualified Cardano.ReCon.Presburger.Complete as BinRel (IntBinRel (..))
+import           Cardano.ReCon.Presburger.IntTerm.Types
+import           Cardano.ReCon.Presburger.NegNF (NegNF)
+import qualified Cardano.ReCon.Presburger.NegNF as N
+
+import           Data.Word (Word64)
+
+data CompNF =
+     -- | φ ∨ ψ
+     Or CompNF CompNF
+     -- | φ ∧ ψ
+   | And CompNF CompNF
+     -- | T
+   | Top
+     -- | ⊥
+   | Bottom
+     -- | i < i
+   | IntLt IntTerm IntTerm
+     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
+   | IntDiv Word64 IntTerm
+     -- | ¬ (ℕ⁺ \| i)
+   | IntNegDiv Word64 IntTerm
+   deriving (Show, Eq, Ord)
+
+fromNegNF :: NegNF -> CompNF
+fromNegNF (N.Or a b) = Or (fromNegNF a) (fromNegNF b)
+fromNegNF (N.And a b) = And (fromNegNF a) (fromNegNF b)
+fromNegNF N.Bottom = Bottom
+fromNegNF N.Top = Top
+-- s = t <=> s < t + 1 ∧ t < s + 1
+fromNegNF (N.IntBinRel BinRel.IntEq s t) = And (IntLt s (IntSum t (IntConst 1))) (IntLt t (IntSum s (IntConst 1)))
+fromNegNF (N.IntBinRel BinRel.IntLt s t) = IntLt s t
+-- s ≤ t <=> s < t + 1
+fromNegNF (N.IntBinRel BinRel.IntLte s t) = IntLt s (IntSum t (IntConst 1))
+-- s > t <=> t < s
+fromNegNF (N.IntBinRel BinRel.IntGt s t) = IntLt t s
+-- s ≥ t <=> t < s + 1
+fromNegNF (N.IntBinRel BinRel.IntGte s t) = IntLt t (IntSum s (IntConst 1))
+-- ¬ (s = t) <=> s < t ∨ t < s
+fromNegNF (N.IntNegBinRel BinRel.IntEq s t) = Or (IntLt s t) (IntLt t s)
+-- ¬ (s < t) <=> t < s + 1
+fromNegNF (N.IntNegBinRel BinRel.IntLt s t) = IntLt t (IntSum s (IntConst 1))
+-- ¬ (s ≤ t) <=> s > t <=> t < s
+fromNegNF (N.IntNegBinRel BinRel.IntLte s t) = IntLt t s
+-- ¬ (s > t) <=> s ≤ t <=> s < t + 1
+fromNegNF (N.IntNegBinRel BinRel.IntGt s t) = IntLt s (IntSum t (IntConst 1))
+-- ¬ (s ≥ t) <=> s < t
+fromNegNF (N.IntNegBinRel BinRel.IntGte s t) = IntLt s t
+fromNegNF (N.IntDiv k t) = IntDiv k t
+fromNegNF (N.IntNegDiv k t) = IntNegDiv k t
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/Complete.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/Complete.hs
@@ -0,0 +1,34 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Eta reduce" #-}
+module Cardano.ReCon.Presburger.Complete(IntBinRel(..), Complete(..), unfoldImplies) where
+
+import           Cardano.ReCon.Presburger.IntTerm.Types
+
+import           Data.Word (Word64)
+
+data IntBinRel = IntEq | IntLt | IntLte | IntGt | IntGte deriving (Show, Eq, Ord)
+
+data Complete =
+     -- | φ ∨ ψ
+     Or Complete Complete
+     -- | φ ∧ ψ
+   | And Complete Complete
+     -- | ¬ φ
+   | Not Complete
+     -- | φ ⇒ ψ
+   | Implies Complete Complete
+     -- | T
+   | Top
+     -- | ⊥
+   | Bottom
+     -- | ∀x ∈ ℤ. φ
+   | IntForall IntIdentifier Complete
+     -- | ∃x ∈ ℤ. φ
+   | IntExists IntIdentifier Complete
+     -- | i = i | i < i | i ≤ i | i > i | i ≥ i
+   | IntBinRel IntBinRel IntTerm IntTerm
+     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
+   | IntDiv Word64 IntTerm deriving (Show, Eq, Ord)
+
+unfoldImplies :: Complete -> Complete -> Complete
+unfoldImplies a b = Or (Not a) b
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/DNF.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/DNF.hs
@@ -0,0 +1,28 @@
+module Cardano.ReCon.Presburger.DNF(DNFConjunct(..), DNFDisjunct, DNF, fromCompNF) where
+
+
+import           Cardano.ReCon.Presburger.CompNF (CompNF)
+import qualified Cardano.ReCon.Presburger.CompNF as C
+import           Cardano.ReCon.Presburger.IntTerm.Types
+
+import           Data.Word (Word64)
+
+data DNFConjunct =
+     -- | i < i
+     IntLt IntTerm IntTerm
+     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
+   | IntDiv Word64 IntTerm
+     -- | ¬ (ℕ⁺ \| i)
+   | IntNegDiv Word64 IntTerm deriving (Show, Eq, Ord)
+
+type DNFDisjunct = [DNFConjunct]
+type DNF = [DNFDisjunct]
+
+fromCompNF :: CompNF -> DNF
+fromCompNF (C.Or a b) = fromCompNF a ++ fromCompNF b
+fromCompNF (C.And a b) = [p ++ q | p <- fromCompNF a, q <- fromCompNF b]
+fromCompNF C.Top = [[]]
+fromCompNF C.Bottom = []
+fromCompNF (C.IntLt i j) = [[IntLt i j]]
+fromCompNF (C.IntDiv n i) = [[IntDiv n i]]
+fromCompNF (C.IntNegDiv n i) = [[IntNegDiv n i]]
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/IntTerm/Types.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/IntTerm/Types.hs
@@ -0,0 +1,84 @@
+module Cardano.ReCon.Presburger.IntTerm.Types(
+    IntIdentifier
+  , IntValue
+  , NatValue
+  , IntTerm(..)
+  , IntTermNF(..)
+  , mulTerm
+  , zero
+  , plus
+  , minus
+  , mul
+  , nullify
+  , nf
+  , quote
+  , normalise) where
+import           Data.Int (Int64)
+import qualified Data.List as List
+import           Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import           Data.Text (Text)
+import           Data.Word (Word64)
+
+type IntIdentifier = Text
+type IntValue = Int64
+type NatValue = Word64
+
+-- i, j ::= i + i | <int> · x | <int>, where <int> is an arbitrary integer
+data IntTerm = IntVar IntValue IntIdentifier | IntConst Int64 | IntSum IntTerm IntTerm deriving (Show, Eq, Ord)
+
+-- k · i
+-- k · (k' · x) = (k * k') · x
+-- k · c = k * c
+-- k · (i + j) = k · i + k · j
+mulTerm :: IntValue -> IntTerm -> IntTerm
+mulTerm k (IntVar k' x) = IntVar (k * k') x
+mulTerm k (IntConst k') = IntConst (k * k')
+mulTerm k (IntSum a b) = IntSum (mulTerm k a) (mulTerm k b)
+
+-- | c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ
+data IntTermNF = IntTermNF {
+  -- | Invariant: the coefficients must be non-zero.
+  coeff :: Map IntIdentifier IntValue,
+  constant :: IntValue
+} deriving (Show, Eq, Ord)
+
+-- 0 + 0 · x₀ + ... + 0 · xₙ
+zero :: IntTermNF
+zero = IntTermNF{coeff = Map.empty, constant = 0}
+
+-- | (c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ) + (c' + k₀' · x₀ + k₁' · x₁ + ... + kₙ' · xₙ)
+--   =
+--   ((c + c') + (k₀ + k₀') · x₀ + (k₁ + k₁') · x₁ + ... + (kₙ + kₙ') · xₙ)
+plus :: IntTermNF -> IntTermNF -> IntTermNF
+plus IntTermNF{coeff, constant} IntTermNF{coeff = coeff', constant = constant'} =
+  IntTermNF{coeff = Map.filter (/= 0) $ Map.unionWith (+) coeff coeff', constant = constant + constant'}
+
+minus :: IntTermNF -> IntTermNF -> IntTermNF
+minus IntTermNF{coeff, constant} IntTermNF{coeff = coeff', constant = constant'} =
+  IntTermNF{coeff = Map.filter (/= 0) $ Map.unionWith (-) coeff coeff', constant = constant + constant'}
+
+-- | k * (c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ)
+--   =
+--   ((k * c) + (k * k₀) · x₀ + (k * k₁) · x₁ + ... + (k * kₙ) · xₙ)
+mul :: IntValue -> IntTermNF -> IntTermNF
+mul k IntTermNF{..} = IntTermNF{constant = k * constant, coeff = Map.filter (/= 0) $ Map.map (* k) coeff}
+
+setCoeff :: IntValue -> IntIdentifier -> IntTermNF -> IntTermNF
+setCoeff k x IntTermNF{..} = IntTermNF{coeff = Map.filter (/= 0) $ Map.insert x k coeff, constant}
+
+nullify :: IntIdentifier -> IntTermNF -> IntTermNF
+nullify = setCoeff 0
+
+nf :: IntTerm -> IntTermNF
+nf (IntConst k) = IntTermNF {coeff = Map.empty, constant = k}
+nf (IntVar k x) = IntTermNF {coeff = Map.filter (/= 0) (Map.singleton x k), constant = 0}
+nf (IntSum a b) = nf a `plus` nf b
+
+quote :: IntTermNF -> IntTerm
+quote IntTermNF{..} = IntSum (IntConst constant) (List.foldl' go (IntConst 0) (Map.toList coeff)) where
+  go :: IntTerm -> (IntIdentifier, IntValue) -> IntTerm
+  go lhs (x, k) = IntSum lhs (IntVar k x)
+
+normalise :: IntTerm -> IntTerm
+normalise = quote . nf
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/NegNF.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/NegNF.hs
@@ -0,0 +1,47 @@
+module Cardano.ReCon.Presburger.NegNF(NegNF(..), fromQuantifierFree) where
+
+import           Cardano.ReCon.Presburger.Complete (IntBinRel)
+import           Cardano.ReCon.Presburger.IntTerm.Types
+import           Cardano.ReCon.Presburger.QuantifierFree (QuantifierFree, unfoldImplies)
+import qualified Cardano.ReCon.Presburger.QuantifierFree as Q
+
+import           Data.Word (Word64)
+
+data NegNF =
+     -- | φ ∨ ψ
+     Or NegNF NegNF
+     -- | φ ∧ ψ
+   | And NegNF NegNF
+     -- | T
+   | Top
+     -- | ⊥
+   | Bottom
+     -- | i = i | i < i | i ≤ i | i > i | i ≥ i
+   | IntBinRel IntBinRel IntTerm IntTerm
+     -- | ¬ (i = i) | ¬ (i < i) | ¬ (i ≤ i) | ¬ (i > i) | ¬ (i ≥ i)
+   | IntNegBinRel IntBinRel IntTerm IntTerm
+     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
+   | IntDiv Word64 IntTerm
+     -- | ¬ (ℕ⁺ \| i)
+   | IntNegDiv Word64 IntTerm
+   deriving (Show, Eq, Ord)
+
+fromQuantifierFreeNeg :: QuantifierFree -> NegNF
+fromQuantifierFreeNeg (Q.Or a b) = And (fromQuantifierFreeNeg a) (fromQuantifierFreeNeg b)
+fromQuantifierFreeNeg (Q.And a b) = Or (fromQuantifierFreeNeg a) (fromQuantifierFreeNeg b)
+fromQuantifierFreeNeg Q.Top = Bottom
+fromQuantifierFreeNeg Q.Bottom = Top
+fromQuantifierFreeNeg (Q.IntBinRel r i i') = IntNegBinRel r i i'
+fromQuantifierFreeNeg (Q.IntDiv r i) = IntNegDiv r i
+fromQuantifierFreeNeg (Q.Not t) = fromQuantifierFree t
+fromQuantifierFreeNeg (Q.Implies a b) = fromQuantifierFreeNeg (unfoldImplies a b)
+
+fromQuantifierFree :: QuantifierFree -> NegNF
+fromQuantifierFree (Q.Or a b) = Or (fromQuantifierFree a) (fromQuantifierFree b)
+fromQuantifierFree (Q.And a b) = And (fromQuantifierFree a) (fromQuantifierFree b)
+fromQuantifierFree Q.Top = Top
+fromQuantifierFree Q.Bottom = Bottom
+fromQuantifierFree (Q.IntBinRel r i i') = IntBinRel r i i'
+fromQuantifierFree (Q.IntDiv r i) = IntDiv r i
+fromQuantifierFree (Q.Not t) = fromQuantifierFreeNeg t
+fromQuantifierFree (Q.Implies a b) = fromQuantifierFree (unfoldImplies a b)
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/NormAffineDNF.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/NormAffineDNF.hs
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/QuantifierFree.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/Presburger/QuantifierFree.hs
