-----------------------------------------------------------------
-- General Description

type Factory
type Object

newFactory :: IO Factory

newObject  :: Factory -> IO Object

useObjects :: Factory -> [Object] -> IO Answer











-----------------------------------------------------------------
-- The Original Challenge (C++) (by Niklas Sörensson)

{-

  factory     object      users

  "Circuit"   "Signal"    "SignalMap"  \
                                        }  "Clausifier"
  "Solver"    "Lit"                    /

* We can create several Circuits / Solvers

* Signals are created from a Circuit factory

* Signals should not be used in other Circuits

* SignalMaps are created from a Circuit factory

* Signals can be stored in a SignalMap (again, do not mix)

* Lits are created from a Solver factory

* Clausifiers are created from a Circuit and a Solver factory together

* A Clausifier maps Signals to Lits; do not mix!

-}





-----------------------------------------------------------------
-- Low-level API to MiniSat

type Solver
type Lit

newSolver  :: IO Solver
newLit     :: Solver -> IO Lit
neg        :: Lit -> Lit
addClause  :: Solver -> [Lit] -> IO ()

solve      :: Solver -> [Lit] -> IO Bool
modelValue :: Solver -> Lit -> IO Bool








-----------------------------------------------------------------
-- What I want

{-

* Use several SAT solvers simultaneously

* Do not mix up Lits from different solvers

* Have the ability to turn these into pure functions

-}










-----------------------------------------------------------------
-- A special SAT monad

-- Why not:

type S a -- monad
type Lit

newLit     :: S Lit
neg        :: Lit -> Lit
addClause  :: [Lit] -> S ()

solve      :: [Lit] -> S Bool
modelValue :: Lit -> S Bool

run        :: S a -> a

{-

* Cannot mix literals created in different instances of S!

-}


-----------------------------------------------------------------
-- Idea: ST monad

type ST s a -- monad
type Ref s a 

newRef   :: a -> ST s (Ref s a)
writeRef :: Ref s a -> a -> ST s ()
readRef  :: Ref s a -> ST s a

runST    :: (forall s . ST s a) -> a

{-

* Enforces all s to be the same.

* Creates a "new" s when running an ST computation.

* Turns everything into a pure computation!

-}








-----------------------------------------------------------------
-- The embeddable SAT monad

type S s a -- monad
type Lit s

newLit     :: S s (Lit s)
neg        :: Lit s -> Lit s
addClause  :: [Lit s] -> S s ()

solve      :: [Lit s] -> S s Bool
modelValue :: Lit s -> S s Bool

run        :: (forall s . S s a) -> a










-----------------------------------------------------------------
-- Pure functions using SAT

{-

This allows pure functions to use a SAT solver!

  * clique finding (in Paradox/Equinox)
  
  * solving constraints (type analysis) (in Paradox/Equinox)

But only in particular control structure:

  * sub-routine-like

-}












-----------------------------------------------------------------
-- Multiple SAT instances

{-

How to deal with multiple SAT instances that cooperate?

E.g. algorithms that use several SAT solvers simultaneously.

Example: Temporal Induction

  * Base case (for n)
  
  * Step case (for n)

==> Two approaches.

-}










-----------------------------------------------------------------
-- Approach #1: Lazy SAT monad

{-

In a lazy monad, we can have large (infinite) computations,
but can start looking at parts of the answer as soon as they
become available.

(cf. lazy ST monad)

-}











-----------------------------------------------------------------
-- Systems

type State s =
  [Lit s]

data System =
  MkSystem
  { initial    :: forall s . S s (State s)
  , transition :: forall s . State s -> State s -> S s ()
  , property   :: forall s . State s -> S s (Lit s)
  }











-----------------------------------------------------------------
-- Example: BMC / base cases

-- output: [True,True,True,False,False,True,False,..]
--          yes, yes, yes, CEX,  CEX,  yes, CEX, ...

bases :: System -> [Bool]
bases sys =
  run (do s0 <- initial sys
          iter s0)
 where
  iter s =
    do p  <- property s
       b  <- solve [neg p]
       s' <- sequence [ newLit | x <- s ]
       transition s s'
       bs <- iter s'
       return (not b:bs)

{-

In a lazy S monad, results become available lazily.

-}











-----------------------------------------------------------------
-- Temporal Induction

steps :: System -> [Bool]
steps = ...

induction :: System -> Bool
induction sys = match (steps sys) (bases sys)
 where
  match (True : _) _           = True
  match _          (False : _) = False
  match (_ : sts)  (_ : bas)   = match sts bas
  










-----------------------------------------------------------------
-- Approach #2: Direct mixing

{-

Idea:

  * Decouple the "trick with the s" from the monad.

-}











-----------------------------------------------------------------
-- Creating several solvers API

type Solver s
type Lit s

newLit     :: Solver s -> IO (Lit s)
neg        :: Lit s -> Lit s
addClause  :: Solver s -> [Lit s] -> IO ()

solve      :: Solver s -> [Lit s] -> IO Bool
modelValue :: Solver s -> Lit s -> IO Bool









-----------------------------------------------------------------
-- Creating solvers

{-

Each time a solver is created, a new s should be created.

-}

newSolver :: exists s . IO (Solver s)

{-

Not valid Haskell. This is:

-}

withNewSolver :: (forall s . Solver s -> IO a) -> IO a











-----------------------------------------------------------------
-- Temporal Induction

induction :: System -> IO Bool
induction sys =
  withNewSolver (\solBase ->
    withNewSolver (\solStep ->
      iter solBase solStep
  ))
 where
  iter solBase solStep =
    do ...
       {- base and step cases combined -}
       ...

{-

Different style:

  * more direct cooperation between results
  
  * passing around of Solver objects
  
    - implicit parameters?
  
  * less modular?

 (* C++ challenge solved here
    
    - generalizes to Circuits, Clausifiers, GateMaps, ...)

-}

{-
  * in IO
-}











-----------------------------------------------------------------
-- Creating several solvers, purely, try #1

type S a
type Solver s
type Lit s

withNewSolver :: (forall s . Solver s -> S a) -> S a
newLit        :: Solver s -> S (Lit s)
neg           :: Lit s -> Lit s
addClause     :: Solver s -> [Lit s] -> S ()

solve         :: Solver s -> [Lit s] -> S Bool
modelValue    :: Solver s -> Lit s -> S Bool

run           :: S a -> a












-----------------------------------------------------------------
-- Example showing unsoundness

example :: Bool
example =
  withNewSolver (\s ->
    let x = run (do x <- newLit s
                    return x)
        
        y = run (do x <- newLit s
                    return x)
     
     in return (x == y)
  )
  
  
  
  
  








-----------------------------------------------------------------
-- Creating several solvers, purely, fixed

type S t a
type Solver t s
type Lit s

withNewSolver :: (forall s . Solver t s -> S t a) -> S t a
newLit        :: Solver t s -> S t (Lit s)
neg           :: Lit s -> Lit s
addClause     :: Solver t s -> [Lit s] -> S t ()

solve         :: Solver t s -> [Lit s] -> S t Bool
modelValue    :: Solver t s -> Lit s -> S t Bool

run           :: (forall t . S t a) -> a














-----------------------------------------------------------------
-- Summary

{-

* The ST monad "trick with the s" can be used for other monads

* Laziness helps in increasing the expressiveness

* The "trick with the s" can be generalized, allowing multiple s's

-}











-----------------------------------------------------------------
-- Issues

{-

* What is the best style?
  
  - IO monad vs. Dialogue IO

* exists vs. forall

* Implicit parameters?

* Lists of solvers?

* How to prove this correct?

-}











-----------------------------------------------------------------
-- Regions?

type ST t a -- monad
type Region t s
type Ref s a 

withNewRegion :: (forall s . Region s -> ST t a) -> ST t a
newRef        :: Region t s -> a -> ST t (Ref s a)
writeRef      :: Region t s -> Ref s a -> a -> ST t ()
readRef       :: Region t s -> Ref s a -> ST t a

runST         :: (forall t . ST t a) -> a