what4-1.7: test/BoolNormalization.hs

-- See what percentage of randomly-generated boolean expressions can be
-- completely simplified away. Higher is better. This is one mechanism for
-- evaluating rewrite rules.

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

module Main (main) where

import Control.Monad (foldM)
import qualified Control.Monad.State.Strict as State
import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(Some))
import Data.Parameterized.TraversableFC (traverseFC_)
import qualified Hedgehog.Internal.Gen as HG
import qualified Hedgehog.Internal.Tree as HG
import qualified Hedgehog as HG
import What4.Expr.Builder
import What4.Expr (EmptyExprBuilderState(EmptyExprBuilderState))
import What4.Interface

import Bool

-- | Get the size of an expression. Lower is better.
sz :: Expr t tp -> Int
sz =
  \case
    SemiRingLiteral {} -> 1
    BoolExpr {} -> 1
    FloatExpr {} -> 1
    StringExpr {} -> 1
    AppExpr ae ->
      State.execState (traverseFC_ (\e -> State.modify (+ sz e)) (appExprApp ae)) 1
    NonceAppExpr nae ->
      State.execState (traverseFC_ (\e -> State.modify (+ sz e)) (nonceExprApp nae)) 1
    BoundVarExpr {} -> 1

main :: IO ()
main = do
  Some ng <- newIONonceGenerator
  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
  let eliminated i = do
        x <- HG.runTreeT (HG.evalGenT (HG.Size 100) (HG.Seed i 1) (doGenExpr sym))
        case HG.nodeValue x of
          Nothing -> error "whoops"
          Just (bExpr, _vars) -> do
            e <- toSymExpr sym (pure . uninterpVar) bExpr
            -- Audit the quality of the generated expressions:
            -- putStrLn "--------------------------------------"
            -- putStrLn (show bExpr)
            -- putStrLn "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"
            -- putStrLn (show (printSymExpr e))
            -- putStrLn "______________________________________"
            -- putStrLn (show (sz e))
            case asConstantPred e of
              Just {} -> pure (1, sz e)
              Nothing -> pure (0, sz e)
  let total = 20000
  let count (accFull, accSize) (full, size) = (accFull + full, accSize + size)
  (full, size) <- foldM (\acc seed -> count acc <$> eliminated seed) (0 :: Int, 0 :: Int) [0..total]
  putStrLn ("Fully eliminated " ++ show full ++ "/" ++ show total)
  putStrLn ("Total size: " ++ show size)