{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-|
Module      : ToSBV
Description : Transform the problem into a sat problem in SBV

The main program 'toSBV' takes the list of variables,
the constraint formula (a 'FOLFormula'), and the target formula
(the translation of a 'ModalFormula' into a 'FOLFormula') 
-}

module ToSBV where

import Logics
import Data.SBV
import Data.Maybe
import Data.Map (Map, fromList, (!))

-- |'toSBV' takes a constraint \(\phi\) (in 'FOLFormula') and target formula in 'FOLFormula'.
-- The target formula is usually the translation of a 'ModalFormula' \(\tau(\ldots)\) via the "Tau" module.
-- Both formulas are converted into SBV formula. Variables are converted into SBV symbolic variables
toSBV :: [Var] -> ModalFormula -> ModalFormula -> Predicate
toSBV vars constraint formula = do freeBools <- symbolics [varname (BVar x)  | (BVar x)  <- vars] 
                                   freeVarBools <- mkForallVars (maxUBV formula) 
                                   let uvars = [uvar i | i <- [1 .. (maxUBV formula)]]
                                   let toFreeBool = fromList $ zip (vars++uvars) (freeBools++freeVarBools)
                                   constrain $ toSymb toFreeBool constraint
                                   return $ toSymb toFreeBool formula

-- | toSymb: 
-- convert a formula into SBV formula
toSymb :: Map Var SBool -> ModalFormula -> SBool
toSymb freeB (Atom b)              = toSymbBExpr freeB b
toSymb freeB (Neg alpha)           = sNot (toSymb freeB alpha)
toSymb freeB (Disj as)             = sOr [toSymb freeB a | a <- as]
toSymb freeB (Conj as)             = sAnd [toSymb freeB a | a <- as]
toSymb freeB (Imp alpha1 alpha2)   = (toSymb freeB alpha1) .=> (toSymb freeB alpha2)
toSymb freeB (Equiv alpha1 alpha2) = (toSymb freeB alpha1) .<=> (toSymb freeB alpha2)
-- toSymb freeB (ForAllB n f)         = toSymb freeB f  -- the variable for n is already made free
toSymb freeB (ForAllB n f)         = sAnd [toSymb freeB (sub (uvar n) (B v) f)  | v <- [True, False] ]
toSymb freeB (ExistsB n f)         = sOr [toSymb freeB (sub (yvar n) (B v) f)  | v <- [True, False] ]

-- | toSymbBExpr: 
-- convert a boolean expression in BExpr into SBV SBool. 
-- variables in the BExpr are replaced by SBV variables created in freeBools
toSymbBExpr :: Map Var SBool  -> BExpr -> SBool
toSymbBExpr freeB (B True)     = sTrue
toSymbBExpr freeB (B False)    = sFalse
toSymbBExpr freeB (BValue x)   = freeB!x
toSymbBExpr freeB (Xor [b])    = toSymbBExpr freeB b
toSymbBExpr freeB (Xor (b:bs)) = toSymbBExpr freeB b .<+> toSymbBExpr freeB (Xor bs)
toSymbBExpr freeB (And bs)     = sAnd [toSymbBExpr freeB b | b <- bs]
toSymbBExpr freeB (Or bs)      = sOr [toSymbBExpr freeB b | b <- bs]
toSymbBExpr freeB (BEq b b')   = toSymbBExpr freeB b .== toSymbBExpr freeB b'