-------------------------------------------------------------------------------
-- | This module defines a function to solve NNF constraints,
--   by reducing them to the standard FInfo.
-------------------------------------------------------------------------------

module Language.Fixpoint.Horn.Solve (solveHorn, solve) where

import           System.Exit
import           Control.DeepSeq
import qualified Language.Fixpoint.Solver       as Solver
import qualified Language.Fixpoint.Parse        as Parse
import qualified Language.Fixpoint.Types        as F
import qualified Language.Fixpoint.Types.Config as F
import qualified Language.Fixpoint.Horn.Types   as H
import qualified Language.Fixpoint.Horn.Parse   as H
import qualified Language.Fixpoint.Horn.Transformations as Tx
import           Language.Fixpoint.Horn.Info

import           System.Console.CmdArgs.Verbosity

-- import Debug.Trace (traceM)

----------------------------------------------------------------------------------
solveHorn :: F.Config -> IO ExitCode
----------------------------------------------------------------------------------
solveHorn :: Config -> IO ExitCode
solveHorn Config
cfg = do
  (Query ()
q, [String]
opts) <- Parser (Query (), [String]) -> String -> IO (Query (), [String])
forall b. Parser b -> String -> IO b
Parse.parseFromFile Parser (Query (), [String])
H.hornP (Config -> String
F.srcFile Config
cfg)

  -- If you want to set --eliminate=none, you better make it a pragma
  Config
cfg <- if Config -> Eliminate
F.eliminate Config
cfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
F.None
           then Config -> IO Config
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Config
cfg { eliminate :: Eliminate
F.eliminate =  Eliminate
F.Some })
           else Config -> IO Config
forall (f :: * -> *) a. Applicative f => a -> f a
pure Config
cfg
  Config
cfg <- Config -> [String] -> IO Config
F.withPragmas Config
cfg [String]
opts

  Result (Integer, ())
r <- Config -> Query () -> IO (Result (Integer, ()))
forall a.
(PPrint a, NFData a, Loc a, Show a, Fixpoint a) =>
Config -> Query a -> IO (Result (Integer, a))
solve Config
cfg Query ()
q
  Result Integer -> IO ExitCode
Solver.resultExitCode ((Integer, ()) -> Integer
forall a b. (a, b) -> a
fst ((Integer, ()) -> Integer)
-> Result (Integer, ()) -> Result Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Result (Integer, ())
r)

----------------------------------------------------------------------------------
eliminate :: (F.PPrint a) => F.Config -> H.Query a -> IO (H.Query a)
----------------------------------------------------------------------------------
eliminate :: Config -> Query a -> IO (Query a)
eliminate Config
cfg Query a
q
  | Config -> Eliminate
F.eliminate Config
cfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
F.Existentials = do
    Query a
q <- Config -> Query a -> IO (Query a)
forall a. PPrint a => Config -> Query a -> IO (Query a)
Tx.solveEbs Config
cfg Query a
q
    -- b <- SI.checkValid cfg "/tmp/asdf.smt2" [] F.PTrue $ Tx.cstrToExpr side
    -- if b then print "checked side condition" else error "side failed"
    Query a -> IO (Query a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Query a
q
  | Config -> Eliminate
F.eliminate Config
cfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
F.Horn = do
    let c :: Cstr a
c = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
Tx.elim (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Query a -> Cstr a
forall a. Query a -> Cstr a
H.qCstr Query a
q
    IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Horn Elim:"
    IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
c
    Query a -> IO (Query a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Query a -> IO (Query a)) -> Query a -> IO (Query a)
forall a b. (a -> b) -> a -> b
$ Query a
q { qCstr :: Cstr a
H.qCstr = Cstr a
c }
  | Bool
otherwise = Query a -> IO (Query a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Query a
q

----------------------------------------------------------------------------------
solve :: (F.PPrint a, NFData a, F.Loc a, Show a, F.Fixpoint a) => F.Config -> H.Query a
       -> IO (F.Result (Integer, a))
----------------------------------------------------------------------------------
solve :: Config -> Query a -> IO (Result (Integer, a))
solve Config
cfg Query a
q = do
  let c :: Cstr a
c = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
Tx.uniq (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a -> Cstr a
forall a. Flatten a => a -> a
Tx.flatten (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Query a -> Cstr a
forall a. Query a -> Cstr a
H.qCstr Query a
q
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Horn Uniq:"
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
c
  Query a
q <- Config -> Query a -> IO (Query a)
forall a. PPrint a => Config -> Query a -> IO (Query a)
eliminate Config
cfg ({- void $ -} Query a
q { qCstr :: Cstr a
H.qCstr = Cstr a
c })
  Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
Solver.solve Config
cfg (Query a -> FInfo a
forall a. Query a -> FInfo a
hornFInfo Query a
q)