LPPaver-0.0.3.1: app/LPPaver.hs

module Main where

import MixedTypesNumPrelude
import AERN2.MP.Ball
import LPPaver.Decide.Algorithm
import PropaFP.Expression
import PropaFP.Eliminator
import PropaFP.VarMap
import PropaFP.Parsers.Smt (parseSMT2, parseVCToF, ParsingMode (Why3, CNF))
import PropaFP.Parsers.DRealSmt
import Options.Applicative
import System.Directory
import Data.Ratio

data ProverOptions = ProverOptions
  {
    provingProcessDone :: Bool,
    ceMode :: Bool,
    depthCutoff :: Integer,
    bestFirstSearchCutoff :: Integer,
    precision :: Integer,
    -- relativeImprovementCutoff :: Rational, make this a flag, as a double is probably easier
    fileName :: String
  }

-- data DRealOptions = DRealOptions
--   {
--     dRealFileName :: String,
--     dRealTargetName :: String
--   }

proverOptions :: Parser ProverOptions
proverOptions = ProverOptions
  <$> switch
    (
      long "propafp-done"
      <> short 'a'
      <> help "Add this option if the target file was generated by PropaFP"
    )
  <*> switch
    (
      long "ce-mode"
      <> short 'c'
      <> help "Tell LPPaver to focus on finding a counterexample"
    )
  <*> option auto
    (
      long "depth-cutoff"
      <> short 'd'
      <> help "How hard LPPaver 'works' until giving up. This option is ignored when ce-mode is on"
      <> showDefault
      <> value 100
      <> metavar "INT"
    )
  <*> option auto
    (
      long "best-first-search-cutoff"
      <> short 'b'
      <> help "How hard LPPaver 'works' until giving up when searching for a counterexample. This option is ignored when ce-mode is off"
      <> showDefault
      <> value 1000
      <> metavar "INT"
    )
  <*> option auto
    (
      long "precision"
      <> short 'p'
      <> help "Precision of floating-point numbers used within the prover. Higher precision slows down the prover but may be needed for more difficult problems"
      <> showDefault
      <> value 100
      <> metavar "INT"
    )
  <*> strOption
    (
      long "file-path"
      <> short 'f'
      <> help "SMT2 file to be checked"
      <> metavar "filePath"
    )
main :: IO ()
main = 
  do 
    runProver =<< execParser opts
    where
      opts = info (proverOptions <**> helper)
        ( fullDesc
        <> progDesc "todo"
        <> header "LPPaver - prover" )

runProver :: ProverOptions -> IO ()
runProver proverOptions@(ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath) =
  do 
    if provingProcessDone
      then do
        parsedFile <- parseSMT2 filePath
        case parseDRealSmtToF parsedFile of
          (Just vc, typedVarMap) ->
            let 
              -- If there are variable free comparisons here, we could not deal with them earlier in the proving process.
              -- LPPaver cannot perform any better with these so we safely remove them.
              ednf = fDNFToEDNF . simplifyFDNF . fToFDNF . simplifyF . minMaxAbsEliminatorF . simplifyF . removeVariableFreeComparisons $ vc
            in do
              decideEDNFWithVarMap ednf typedVarMap proverOptions
          (_, _) -> error "Error - Issue parsing given SMT file"
      else do
        -- PATH needs to include folder containing FPTaylor binary after make
        -- symlink to the binary in somewhere like ~/.local/bin will NOT work reliably
        mFptaylorPath <- findExecutable "fptaylor"
        case mFptaylorPath of
          Nothing -> putStrLn "Error - fptaylor executable not in path"
          Just fptaylorPath -> do
            mParsedVC <- parseVCToF filePath fptaylorPath
            case mParsedVC of
              Just (vc, typedVarMap) ->
                let 
                  -- If there are variable free comparisons here, we could not deal with them earlier in the proving process.
                  -- LPPaver cannot perform any better with these so we safely remove them.
                  ednf = fDNFToEDNF . simplifyFDNF . fToFDNF . simplifyF . minMaxAbsEliminatorF . simplifyF . removeVariableFreeComparisons $ vc
                in do
                  decideEDNFWithVarMap ednf typedVarMap proverOptions
              Nothing -> do
                putStrLn "unknown"
                putStrLn "Issue parsing file"

decideEDNFWithVarMap :: [[ESafe]] -> TypedVarMap -> ProverOptions -> IO ()
decideEDNFWithVarMap ednf typedVarMap (ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath) = do
  let result =
        if ceMode
          then checkEDNFBestFirstWithSimplexCE ednf typedVarMap bestFirstSearchCutoff 1.2 (prec p)
          else checkEDNFDepthFirstWithSimplex  ednf typedVarMap depthCutoff           1.2 (prec p)
  case result of
    (Just True, Just model) -> do
      putStrLn "sat"
      printSMTModel model
      prettyPrintCounterExample model
    (Just False, _) -> do
      putStrLn "unsat"
    r@(_, Just indeterminateExample) -> do
      putStrLn "unknown"
      printSMTModel indeterminateExample
      prettyPrintCounterExample indeterminateExample
    r@(_, _) -> do
      putStrLn "unknown"

prettyPrintCounterExample :: TypedVarMap -> IO ()
prettyPrintCounterExample [] = return ()
prettyPrintCounterExample ((TypedVar (v, (l, r)) t) : vs) = 
  if l == r
    then do 
      putStrLn (v ++ " = " ++ show (double l))
      prettyPrintCounterExample vs
    else do
      putStrLn (v ++ " = [" ++ show (double l) ++ ", " ++ show (double r) ++ "]")
      prettyPrintCounterExample vs

printSMTModel :: TypedVarMap -> IO ()
printSMTModel typedVarMap =
  do
    putStrLn "(model"
    printModels typedVarMap
    putStrLn ")"
  where
    printModels [] = return ()
    printModels ((TypedVar (v, (l, r)) t) : vs) = do
      putStrLn $ "(define-fun " ++ v ++ " () " ++ show t ++ " " ++ showNum (l) ++ ")"
      putStrLn $ "(define-fun " ++ v ++ "_vc_constant" ++ " () " ++ show t ++ " " ++ showNum (l) ++ ")" --FIXME: Only do this with a Why3 or similar flag?
      printModels vs

    showNum :: Rational -> String
    showNum num =
      if num < 0
        then "(/ " ++ "(" ++ show (numerator num) ++ ") " ++ show (denominator num) ++ ")"
        else "(/ " ++ show (numerator num) ++ " " ++ show (denominator num) ++ ")"