{-
Generate the Z3 code checking if the given statement matches the given post-condition
We do this by negating the proposition, then checkign if it is satisfiable.
First we search for all free-variables in the program, so that we can
declare them in our Z3 string.
-}
z3wlpMulti :: ([Program], (PostConds, ProgParams)) -> [(String, [String])]
z3wlpMulti (progs, postConds) =
  let

    varDecs vars = foldr (\v decs -> decs ++ "\n" ++ varDec v) "" vars
    wlpsAndConds  = map (programWLP postConds) progs
    progWlpConds = zip progs wlpsAndConds
    formatPred prog pred = (varDecs (progFreeVars prog) ++ "\n") ++ (formatZ3 $ pred )
    formattedPreds = map (\(prog, (theWLP, conds)) ->
                           (formatPred prog theWLP,  (map (formatPred prog) conds) ) ) progWlpConds
  in formattedPreds
z3wlpMulti :: ([Program], (PostConds, ProgParams)) -> [(String, [String])]
z3wlpMulti (progs, postConds) =
  let

    varDecs vars = foldr (\v decs -> decs ++ "\n" ++ varDec v) "" vars
    wlpsAndConds  = map (programWLP postConds) progs
    progWlpConds = zip progs wlpsAndConds
    formatPred prog pred = (varDecs (progFreeVars prog) ++ "\n") ++ (formatZ3 $ pred )
    formattedPreds = map (\(prog, (theWLP, conds)) ->
                           (formatPred prog theWLP,  (map (formatPred prog) conds) ) ) progWlpConds
  in formattedPreds
z3wlpMulti (progs, postConds) =
  let

    varDecs vars = foldr (\v decs -> decs ++ "\n" ++ varDec v) "" vars
    wlpsAndConds  = map (programWLP postConds) progs
    progWlpConds = zip progs wlpsAndConds
    formatPred prog pred = (varDecs (progFreeVars prog) ++ "\n") ++ (formatZ3 $ pred )
    formattedPreds = map (\(prog, (theWLP, conds)) ->
                           (formatPred prog theWLP,  (map (formatPred prog) conds) ) ) progWlpConds
  in formattedPreds