feat(ldfi2): introduce skeleton for translating formulae to sat

src/ldfi2/ldfi.cabal

@@ -17,12 +17,14 @@ tested-with:         GHC ==8.10.3
 library
   hs-source-dirs:    src/
   exposed-modules:   Ldfi
-  -- GHC boot libraries
+  -- GHC boot library dependencies:
   -- (https://gitlab.haskell.org/ghc/ghc/-/blob/master/packages)
   build-depends:
       base           >=4.14 && <4.15
     , containers
-    , z3
+  -- Other dependencies:
+  build-depends:
+      z3
   default-language:  Haskell2010
 
 test-suite test

src/ldfi2/src/Ldfi.hs

@@ -1,8 +1,11 @@
+{-# LANGUAGE DeriveFoldable #-}
+
 module Ldfi where
 
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Numeric.Natural
+import Z3.Monad
 
 ------------------------------------------------------------------------
 -- * Traces
@@ -34,26 +37,32 @@ edges = foldMap (\e -> Set.singleton (from e, to e))
 infixr 3 :&&
 infixr 2 :||
 
-data Formula
+data FormulaF var
   = Formula :&& Formula
   | Formula :|| Formula
   | And [Formula]
   | Or [Formula]
   | Neg Formula
   | TT
   | FF
-  | Var String
-  deriving (Eq, Show)
-
-simplify :: Formula -> Formula
-simplify (TT :&& r)  = simplify r
-simplify (l  :&& r)  = simplify l :&& simplify r
-simplify (FF :|| r)  = simplify r
-simplify (l  :|| TT) = simplify l
-simplify (l  :|| r)  = simplify l :|| simplify r
-simplify (And [])    = TT
-simplify (And [f])   = f
-simplify (And fs)    = And (map simplify fs)
+  | Var var
+  deriving (Eq, Show, Foldable)
+
+type Formula = FormulaF String
+
+getVars :: Ord var => FormulaF var -> Set var
+getVars = foldMap Set.singleton
+
+simplify1 :: Formula -> Formula
+simplify1 (TT :&& r)  = simplify1 r
+simplify1 (l  :&& r)  = simplify1 l :&& simplify1 r
+simplify1 (FF :|| r)  = simplify1 r
+simplify1 (l  :|| TT) = simplify1 l
+simplify1 (l  :|| r)  = simplify1 l :|| simplify1 r
+simplify1 (And [])    = TT
+simplify1 (And [f])   = f
+simplify1 (And fs)    = And (map simplify1 fs)
+simplify1 f           = f
 
 -- simplify (TT :&& r)     = simplify r
 -- simplify (And xs :&& y) = And (map simplify xs ++ [simplify y])
@@ -68,11 +77,10 @@ simplify (And fs)    = And (map simplify fs)
 --     expandAnd (And xs) = xs
 --     expandAnd (l :&& r) = [l, r]
 --     expandAnd f = [f]
-simplify f          = f
 
 fixpoint :: Formula -> Formula
-fixpoint f | simplify f == f = f
-           | otherwise       = fixpoint (simplify f)
+fixpoint f | simplify1 f == f = f
+           | otherwise        = fixpoint (simplify1 f)
 
 vars :: Set String -> Formula
 vars = And . map Var . Set.toList
@@ -109,3 +117,9 @@ ldfi' ts =
 
 ldfi :: [Trace] -> Formula
 ldfi = fixpoint . ldfi'
+
+------------------------------------------------------------------------
+-- * SAT formula
+
+toSatAst :: MonadZ3 z3 => Formula -> z3 AST
+toSatAst = undefined