Makes the FO-solver more lazy to improve performance

app/Main.hs

@@ -1,9 +1,11 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 module Main where
 
-import EquivariantSet
+import OrbitList
-import Support.Rat
+import Support (Rat)
 
-import Prelude (Show, Ord, Eq, Int, IO, print, otherwise, (.), ($))
+import Prelude (Show, Ord, Eq, Int, IO, print, otherwise, (.), ($), (!!), (+), (-), Bool, head, tail)
 import qualified Prelude as P
 
 {-
@@ -32,60 +34,70 @@ data Formula
   | Not Formula
   deriving (Show, Ord, Eq)
 
--- smart constructors to avoid unwieldy expressions
+pattern False = Not True
+
+-- Smart constructors to avoid unwieldy expressions. It is a heuristic, but
+-- good enough for us. The solver should be able to handle arbitrary formulas
+-- anyways. We also define the other connectives in terms of the constructors.
+-- I am using only the following axioms in the smart constructors:
+-- * < is irreflexive
+-- * The domain is non-empty
+-- * De Morgan laws and classical logic
+-- And nothing more, so the solver really works with the model and not the
+-- theory of the dense linear order
 infix 4 ==, /=, <, <=, >, >=
 (==), (/=), (<), (<=), (>), (>=) :: Var -> Var -> Formula
-x == y | x P.== y  = true
+x == y | x P.== y  = True
        | otherwise = Lit (Equals x y)
 x /= y = not (x == y)
-x < y  | x P.== y  = false
+x < y  | x P.== y  = False
        | otherwise = Lit (LessThan x y)
 x <= y = or (x < y) (x == y)
 x > y  = y < x
 x >= y = or (x > y) (x == y)
 
-true, false :: Formula
-true  = True
-false = Not True
-
 not :: Formula -> Formula
 not (Not x) = x
 not x = Not x
 
 infixr 3 `and`
-infixr 2 `or`, `implies`
+infixr 2 `or`
+infixr 1 `implies`
 and, or, implies :: Formula -> Formula -> Formula
-or True x = true
+or True x   = True
-or x True = true
+or x True   = True
+or False x  = x
+or x False  = x
 or x y      = Or x y
-and True x = x
-and x True = x
 and x y     = not (not x `or` not y)
 implies x y = not x `or` y
 
-forAll, exists :: Formula -> Formula
+-- Here I use that the domain is non-empty. Also not that these simplifications
-forAll p = not (exists (not p))
+-- don't work if we want to report a model to the user.
+exists, forAll :: Formula -> Formula
+exists True  = True
+exists False = False
 exists p     = Exists p
+forAll p     = not (exists (not p))
 
 
 -- Here is the solver. It keeps track of a nominal set.
 -- If that sets is empty in the end, the formula does not hold.
-type Context = EquivariantSet [Rat]
+type Context = SortedOrbitList [Rat]
 
 extend, drop :: Context -> Context
-extend ctx = map (P.uncurry (:)) (product singleVar ctx)
+extend ctx = productWith (:) rationals ctx
-  where singleVar = singleOrbit (Rat 0)
+drop ctx = projectWith (\w -> (head w, tail w)) ctx
-drop ctx = map (P.tail) ctx
 
 truth0 :: Context -> Formula -> Context
-truth0 ctx (Lit (Equals i j))   = filter (\w -> w P.!! i P.== w P.!! j) ctx
+truth0 ctx (Lit (Equals i j))   = filter (\w -> w !! i P.== w !! j) ctx
-truth0 ctx (Lit (LessThan i j)) = filter (\w -> w P.!! i P.< w P.!! j) ctx
+truth0 ctx (Lit (LessThan i j)) = filter (\w -> w !! i P.<  w !! j) ctx
 truth0 ctx True       = ctx
-truth0 ctx (Not x)    = ctx `difference` truth0 ctx x
+truth0 ctx (Not x)    = ctx `minus` truth0 ctx x
 truth0 ctx (Or x y)   = truth0 ctx x `union` truth0 ctx y
 truth0 ctx (Exists p) = drop (truth0 (extend ctx) p)
 
-truth :: Formula -> P.Bool
+truth :: Formula -> Bool
 truth f = P.not . null $ truth0 (singleOrbit []) f
 
 
@@ -98,7 +110,7 @@ test1 = forAll {-1-} (exists {-0-} (1 > 0))
 test2 = exists {-1-} (forAll {-0-} (1 <= 0))
 -- the order is dense
 test3 = forAll {-x-} (forAll {-y-} (1 {-x-} < 0 {-y-} `implies` exists {-z-} (2 < 0 `and` 0 < 1)))
--- Formulas by Niels (= true)
+-- Formulas by Niels
 test4 = forAll (forAll (forAll (2 < 1 `and` 1 < 0 `implies`
                            (forAll (forAll (4 < 1 `and` 1 < 3 `and` 3 < 0 `and` 0 < 2) `implies`
                               (exists (2 < 0 `and` 0 < 1)))))))
@@ -108,6 +120,13 @@ test5 = exists (forAll (forAll (1 < 0 `implies`
 test6 = (forAll (0 == 0)) `implies` (exists (0 /= 0))
 test7 = (forAll (forAll (0 == 1))) `implies` (exists (0 /= 0))
 
+-- Used to take a long time with EquivariantSet. It's fast with lazy lists.
+-- Still takes a long time if exists are replaced with forAlls.
+compl :: Int -> Formula
+compl n = forAll (inner n (exists (0 == (n + 1)))) where
+  inner 0 f = f
+  inner k f = exists (inner (k - 1) f)
+
 main :: IO ()
 main = do
   print test1
@@ -124,3 +143,6 @@ main = do
   print (truth test6)
   print test7
   print (truth test7)
+  let n = 37
+  print (compl n)
+  print (truth (compl n))

ons-hs.cabal

@@ -20,6 +20,7 @@ library
                      , Orbit
                      , Orbit.Class
                      , Orbit.Products
+                     , OrbitList
                      , Support
                      , Support.Rat
                      , Support.OrdList

src/OrbitList.hs

@@ -0,0 +1,64 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module OrbitList where
+
+import qualified Data.List as L
+import qualified Data.List.Ordered as LO
+import Data.Proxy
+import Prelude hiding (map, product)
+
+import Orbit
+import Support
+
+
+newtype OrbitList a = OrbitList { unOrbitList :: [Orb a] }
+
+deriving instance Eq (Orb a) => Eq (OrbitList a)
+deriving instance Ord (Orb a) => Ord (OrbitList a)
+deriving instance Show (Orb a) => Show (OrbitList a)
+
+null :: OrbitList a -> Bool
+null (OrbitList x) = L.null x
+
+empty :: OrbitList a
+empty = OrbitList []
+
+singleOrbit :: Orbit a => a -> OrbitList a
+singleOrbit a = OrbitList [toOrbit a]
+
+rationals :: OrbitList Rat
+rationals = singleOrbit (Rat 0)
+
+-- f should be equivariant
+map :: (Orbit a, Orbit b) => (a -> b) -> OrbitList a -> OrbitList b
+map f (OrbitList as) = OrbitList $ L.map (omap f) as
+
+productWith :: forall a b c. (Orbit a, Orbit b, Orbit c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c
+productWith f (OrbitList as) (OrbitList bs) = map (uncurry f) (OrbitList (concat $ product (Proxy :: Proxy a) (Proxy :: Proxy b) <$> as <*> bs))
+
+filter :: Orbit a => (a -> Bool) -> OrbitList a -> OrbitList a
+filter f = OrbitList . L.filter (f . getElementE) . unOrbitList
+
+
+type SortedOrbitList a = OrbitList a
+-- the above map and productWith preserve ordering if `f` is order preserving
+-- on orbits and filter is always order preserving
+
+union :: Ord (Orb a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a
+union (OrbitList x) (OrbitList y) = OrbitList (LO.union x y)
+
+unionAll :: Ord (Orb a) => [SortedOrbitList a] -> SortedOrbitList a
+unionAll = OrbitList . LO.unionAll . fmap unOrbitList
+
+minus :: Ord (Orb a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a
+minus (OrbitList x) (OrbitList y) = OrbitList (LO.minus x y)
+
+-- decompose a into b and c (should be order preserving), and then throw away b
+projectWith :: (Orbit a, Orbit b, Orbit c, Eq (Orb b), Ord (Orb c)) => (a -> (b, c)) -> SortedOrbitList a -> SortedOrbitList c
+projectWith f = unionAll . fmap OrbitList . groupOnFst . splitOrbs . unOrbitList . map f
+  where
+    splitOrbs = fmap (\o -> (omap fst o, omap snd o))
+    groupOnFst = fmap (fmap snd) . L.groupBy (\x y -> fst x == fst y)