what4-1.4: test/Abduct.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}

module Main where

import           Test.Tasty
import           Test.Tasty.HUnit

import           Data.Foldable (forM_)
import qualified Data.Text as Text
import           Data.Parameterized.Nonce (newIONonceGenerator)
import           Data.Parameterized.Some (Some(..))

import           System.IO (FilePath, IOMode(..), openFile, hClose)
import           System.IO.Temp (withSystemTempFile)
import           What4.Config (extendConfig)
import           What4.Expr
                   ( ExprBuilder,  FloatModeRepr(..), newExprBuilder
                   , BoolExpr, IntegerExpr, GroundValue, groundEval
                   , EmptyExprBuilderState(..))
import           What4.Interface
                   ( BaseTypeRepr(..), getConfiguration
                   , freshConstant, safeSymbol, notPred
                   , impliesPred, intLit, intAdd, intLe )
import           What4.Solver
import           What4.Symbol (SolverSymbol(..))
import           What4.Protocol.SMTLib2 as SMT2
                   (assume, sessionWriter, runCheckSat, runGetAbducts, Writer)
import           What4.Protocol.SMTWriter
                   (mkSMTTerm)
import           What4.Protocol.Online

cvc5executable :: FilePath
cvc5executable = "cvc5"

-- Call the online getAbduct tactic
testGetAbductOnline ::
  ExprBuilder t st fs ->
  [BoolExpr t] ->
  BoolExpr t ->
  Int ->
  IO [String]
testGetAbductOnline sym hs g n = do
  -- Print SMT file in /tmp/
  withSystemTempFile "what4abdonline" $ \fname mirroredOutput -> do
    proc <- startSolverProcess @(SMT2.Writer CVC5) cvc5Features (Just mirroredOutput) sym
    let conn = solverConn proc
    inNewFrame proc $ do
      mapM_ (\x -> assume conn x) hs
      getAbducts proc n (Text.pack "abd") g

-- Call the offline getAbduct tactic
testGetAbductOffline ::
  ExprBuilder t st fs ->
  BoolExpr t ->
  Int ->
  IO [String]
testGetAbductOffline sym f n = do
  -- Print SMT file in /tmp/
  withSystemTempFile "what4abdoffline" $ \fname mirroredOutput -> do
    let logData = LogData { logCallbackVerbose = \_ _ -> return ()
                          , logVerbosity = 2
                          , logReason = "defaultReason"
                          , logHandle = Just mirroredOutput }
    withCVC5 sym cvc5executable logData $ \session -> do
      f_term <- mkSMTTerm (sessionWriter session) f
      runGetAbducts session n (Text.pack "abd") f_term

-- Prove f using an SMT solver, by checking if ~f is unsatisfiable
prove ::
  ExprBuilder t st fs ->
  BoolExpr t ->
  [(String, IntegerExpr t)] ->
  IO (SatResult () ())
prove sym f es = do
  -- Print SMT file in /tmp/
  withSystemTempFile "what4prove" $ \fname mirroredOutput -> do
    proc <- startSolverProcess @(SMT2.Writer CVC5) cvc5Features (Just mirroredOutput) sym
    let logData = LogData { logCallbackVerbose = \_ _ -> return ()
                           , logVerbosity = 2
                           , logReason = "defaultReason"
                           , logHandle = Just mirroredOutput }
    
    -- To prove f, we check whether not f is unsat
    notf <- notPred sym f
    withCVC5 sym cvc5executable logData $ \session -> do
      checkSatisfiable proc "test" notf

-- Tests

testAbdOnline :: ExprBuilder t st fs -> 
  [BoolExpr t] -> 
  BoolExpr t -> 
  TestTree
testAbdOnline sym hs g = testCase "getting 3 abducts using cvc5 online" $ do
  -- Ask for 3 abducts for f
  res <- testGetAbductOnline sym hs g 3
  (length res == 3) @? "3 online abducts"

testAbdOffline :: ExprBuilder t st fs -> 
  BoolExpr t -> 
  [(String, IntegerExpr t)] -> 
  TestTree
testAbdOffline sym f es = testCase "getting 3 abducts using cvc5 offline" $ do
  -- Ask for 3 abducts for f
  res <- testGetAbductOffline sym f 3
  (length res == 3) @? "3 offline abducts"

testSatAbd :: ExprBuilder t st fs -> 
  BoolExpr t -> 
  [(String, IntegerExpr t)] -> 
  TestTree
testSatAbd sym f es = testCase "testing SAT query for abduction" $ do
  -- Prove f (is ~f unsatisfiable?). We expect ~f to be satisfiable
  res <- prove sym f es
  isSat res @? "sat"


main :: IO ()
main = do
  Some ng <- newIONonceGenerator
  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng

  -- This line is necessary for working with cvc5.
  extendConfig cvc5Options (getConfiguration sym)

  -- Build this formula: ~(y >= 0 => (x + y + z) >= 0)
  
  -- First, declare fresh constants for each of the three variables x, y, z.
  x <- freshConstant sym (safeSymbol "x") BaseIntegerRepr
  y <- freshConstant sym (safeSymbol "y") BaseIntegerRepr
  z <- freshConstant sym (safeSymbol "z") BaseIntegerRepr

  -- Next, build up the clause
  zero <- intLit sym 0                    -- 0
  pxyz <- intAdd sym x =<< intAdd sym y z -- x + y + z
  ygte0 <- intLe sym zero y               -- 0 <= y
  xyzgte0 <- intLe sym zero pxyz          -- 0 <= (x + y + z) 
  f <- impliesPred sym ygte0 xyzgte0      -- (0 <= y) -> (0 <= (x + y + z))

  defaultMain $ testGroup "Tests" $
    [ -- test passes if f is disproved (~f is sat)
      testSatAbd sym f [ ("x", x)
                       , ("y", y)
                       , ("z", z)
                       ],
      -- test passes if cvc5 returns 3 abducts (offline)
      testAbdOffline sym f [ ("x", x)
                           , ("y", y)
                           , ("z", z)
                           ],
      -- test passes if cvc5 returns 3 abducts (online)
      testAbdOnline sym [ygte0] xyzgte0
    ]