Export some additional operations from What4.Expr

what4-transition-system/test/Main.hs

@@ -28,6 +28,7 @@ import What4.Expr
   ( ExprBuilder,
     FloatModeRepr (FloatIEEERepr),
     newExprBuilder,
+    EmptyExprBuilderState(..)
   )
 import What4.Expr.Builder (SymbolBinding (..))
 import qualified What4.Interface as What4
@@ -54,17 +55,14 @@ main :: IO ()
 main =
   do
     withIONonceGenerator $ \nonceGen -> do
-      sym <- newExprBuilder FloatIEEERepr State nonceGen
+      sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen
       ts <- counterTransitionSystem sym
       displayTransitionSystem sym ts
     withIONonceGenerator $ \nonceGen -> do
-      sym <- newExprBuilder FloatIEEERepr State nonceGen
+      sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen
       ts <- realsTransitionSystem sym
       displayTransitionSystem sym ts
 
--- We don't need any information in the state
-data State t = State
-
 makeFieldNames ::
   forall stateType.
   [What4.SolverSymbol] ->

what4/README.md

@@ -57,7 +57,8 @@ import Data.Parameterized.Some (Some(..))
 import What4.Config (extendConfig)
 import What4.Expr
          ( ExprBuilder,  FloatModeRepr(..), newExprBuilder
-         , BoolExpr, GroundValue, groundEval )
+         , BoolExpr, GroundValue, groundEval
+		 , EmptyExprBuilderState(..) )
 import What4.Interface
          ( BaseTypeRepr(..), getConfiguration
          , freshConstant, safeSymbol
@@ -75,8 +76,6 @@ to our backend solver, which is Z3 in this example.
 point to your Z3.)
 
 ```
-data BuilderState st = EmptyState
-
 z3executable :: FilePath
 z3executable = "z3"
 ```
@@ -87,7 +86,7 @@ We're ready to start our `main` function:
 main :: IO ()
 main = do
   Some ng <- newIONonceGenerator
-  sym <- newExprBuilder FloatIEEERepr EmptyState ng
+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
 ```
 
 Most of the functions in `What4.Interface`, the module for building up

what4/doc/QuickStart.hs

@@ -10,7 +10,8 @@ import Data.Parameterized.Some (Some(..))
 import What4.Config (extendConfig)
 import What4.Expr
          ( ExprBuilder,  FloatModeRepr(..), newExprBuilder
-         , BoolExpr, GroundValue, groundEval )
+         , BoolExpr, GroundValue, groundEval
+         , EmptyExprBuilderState(..) )
 import What4.Interface
          ( BaseTypeRepr(..), getConfiguration
          , freshConstant, safeSymbol
@@ -21,15 +22,13 @@ import What4.Protocol.SMTLib2
          (assume, sessionWriter, runCheckSat)
 
 
-data BuilderState st = EmptyState
-
 z3executable :: FilePath
 z3executable = "z3"
 
 main :: IO ()
 main = do
   Some ng <- newIONonceGenerator
-  sym <- newExprBuilder FloatIEEERepr EmptyState ng
+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
 
   -- This line is necessary for working with z3.
   extendConfig z3Options (getConfiguration sym)

what4/src/What4/Expr.hs

@@ -13,6 +13,16 @@ module What4.Expr
   ( -- * Expression builder
     ExprBuilder
   , newExprBuilder
+  , startCaching
+  , stopCaching
+  , userState
+  , exprCounter
+  , curProgramLoc
+  , unaryThreshold
+  , cacheStartSize
+  , exprBuilderSplitConfig
+  , exprBuilderFreshConfig
+  , EmptyExprBuilderState(..)
 
     -- * Flags
   , FloatMode
@@ -97,3 +107,9 @@ import What4.Expr.Builder
 import What4.Expr.GroundEval
 import What4.Expr.WeightedSum
 import What4.Expr.UnaryBV
+
+
+-- | A \"dummy\" data type that can be used for the
+--   user state field of an 'ExprBuilder' when there
+--   is no other interesting state to track.
+data EmptyExprBuilderState t = EmptyExprBuilderState

what4/test/AdapterTest.hs

@@ -39,8 +39,6 @@ import           What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness
 import           What4.Protocol.VerilogWriter
 import           What4.Solver
 
-data State t = State
-
 allAdapters :: [SolverAdapter State]
 allAdapters =
   [ cvc4Adapter
@@ -61,13 +59,16 @@ drealAdpt = []
 #endif
 
 
-withSym :: SolverAdapter State -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a) -> IO a
+withSym ::
+  SolverAdapter EmptyBuilderState ->
+  (forall t . ExprBuilder t EmptyBuilderState (Flags FloatUninterpreted) -> IO a) ->
+  IO a
 withSym adpt pred_gen = withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
      extendConfig (solver_adapter_config_options adpt) (getConfiguration sym)
      pred_gen sym
 
-mkSmokeTest :: SolverAdapter State -> TestTree
+mkSmokeTest :: SolverAdapter EmptyBuilderState -> TestTree
 mkSmokeTest adpt = testCase (solver_adapter_name adpt) $
   withSym adpt $ \sym ->
    do res <- smokeTest sym adpt
@@ -109,13 +110,13 @@ mkConfigTests adapters =
              show e)
           _ -> assertFailure $
                "Expected OptGetFailure exception but got: " <> show err
-    withAdapters :: [SolverAdapter State]
-                 -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a)
+    withAdapters :: [SolverAdapter EmptyBuilderState]
+                 -> (forall t . ExprBuilder t EmptyBuilderState (Flags FloatUninterpreted) -> IO a)
                  -> IO a
     withAdapters adptrs op = do
         (cfgs, _getDefAdapter) <- solverAdapterOptions adptrs
         withIONonceGenerator $ \gen ->
-          do sym <- newExprBuilder FloatUninterpretedRepr State gen
+          do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
              extendConfig cfgs (getConfiguration sym)
              op sym
 
@@ -536,7 +537,7 @@ mkConfigTests adapters =
 
 ----------------------------------------------------------------------
 
-nonlinearRealTest :: SolverAdapter State -> TestTree
+nonlinearRealTest :: SolverAdapter EmptyBuilderState -> TestTree
 nonlinearRealTest adpt =
   let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]
              then expectFailBecause
@@ -579,7 +580,7 @@ nonlinearRealTest adpt =
                 ((-2) <= x2_y' && x2_y' <= (-1)) @? "correct bounds"
 
 
-mkQuickstartTest :: SolverAdapter State -> TestTree
+mkQuickstartTest :: SolverAdapter EmptyBuilderState -> TestTree
 mkQuickstartTest adpt =
   let wrap = if solver_adapter_name adpt == "stp"
              then ignoreTestBecause "STP cannot generate the model"
@@ -638,7 +639,7 @@ mkQuickstartTest adpt =
 
 verilogTest :: TestTree
 verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
      let w = knownNat @8
      x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)
      one <- bvLit sym w (mkBV w 1)

what4/test/ExprBuilderSMTLib2.hs

@@ -52,10 +52,9 @@ import qualified What4.Solver.Yices as Yices
 import           What4.Utils.StringLiteral
 import           What4.Utils.Versions (ver, SolverBounds(..), emptySolverBounds)
 
-data State t = State
 data SomePred = forall t . SomePred (BoolExpr t)
 deriving instance Show SomePred
-type SimpleExprBuilder t fs = ExprBuilder t State fs
+type SimpleExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs
 
 instance TestShow Text.Text where testShow = show
 instance TestShow (StringLiteral Unicode) where testShow = show
@@ -76,7 +75,7 @@ userSymbol' s = case userSymbol s of
 
 withSym :: FloatModeRepr fm -> (forall t . SimpleExprBuilder t (Flags fm) -> IO a) -> IO a
 withSym floatMode pred_gen = withIONonceGenerator $ \gen ->
-  pred_gen =<< newExprBuilder floatMode State gen
+  pred_gen =<< newExprBuilder floatMode EmptyExprBuilderState gen
 
 withYices :: (forall t. SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t Yices.Connection -> IO ()) -> IO ()
 withYices action = withSym FloatRealRepr $ \sym ->
@@ -90,7 +89,7 @@ withYices action = withSym FloatRealRepr $ \sym ->
 
 withZ3 :: (forall t . SimpleExprBuilder t (Flags FloatIEEE) -> Session t Z3.Z3 -> IO ()) -> IO ()
 withZ3 action = withIONonceGenerator $ \nonce_gen -> do
-  sym <- newExprBuilder FloatIEEERepr State nonce_gen
+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen
   extendConfig Z3.z3Options (getConfiguration sym)
   Z3.withZ3 sym "z3" defaultLogData { logCallbackVerbose = (\_ -> putStrLn) } (action sym)
 

what4/test/ExprsTest.hs

@@ -33,13 +33,11 @@ import           What4.Concrete
 import           What4.Expr
 import           What4.Interface
 
-
-data State t = State
-type IteExprBuilder t fs = ExprBuilder t State fs
+type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs
 
 withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a
 withTestSolver f = withIONonceGenerator $ \nonce_gen ->
-  f =<< newExprBuilder FloatIEEERepr State nonce_gen
+  f =<< newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen
 
 
 -- | Test natDiv and natMod properties described at their declaration

what4/test/IteExprs.hs

@@ -36,12 +36,11 @@ import           What4.Expr
 import           What4.Interface
 
 
-data State t = State
-type IteExprBuilder t fs = ExprBuilder t State fs
+type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs
 
 withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a
 withTestSolver f = withIONonceGenerator $ \nonce_gen ->
-  f =<< newExprBuilder FloatIEEERepr State nonce_gen
+  f =<< newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen
 
 -- | What branch (arm) is expected from the ITE evaluation?
 data ExpITEArm = Then | Else

what4/test/OnlineSolverTest.hs

@@ -50,8 +50,6 @@ import           What4.Protocol.SMTWriter
 import qualified What4.Protocol.SMTLib2 as SMT2
 import qualified What4.Solver.Yices as Yices
 
-data State t = State
-
 type SolverTestData = (SolverName, AnOnlineSolver, ProblemFeatures, [ConfigDesc], Maybe (ConfigOption BaseIntegerType))
 
 allOnlineSolvers :: [SolverTestData]
@@ -83,7 +81,7 @@ instance TCL.TestShow [PP.Doc ann] where
 mkSmokeTest :: (SolverTestData, SolverVersion) -> TestTree
 mkSmokeTest ((SolverName nm, AnOnlineSolver (_ :: Proxy s), features, opts, _), _) =
   testCase nm $ withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
      extendConfig opts (getConfiguration sym)
      proc <- startSolverProcess @s features Nothing sym
      let conn = solverConn proc
@@ -168,7 +166,7 @@ quickstartTest useFrames ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), fea
   in wrap $
   testCaseSteps nm $ \step ->
   withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      extendConfig opts (getConfiguration sym)
 
      (p,q,r,f) <- mkFormula1 sym
@@ -256,7 +254,7 @@ longTimeTest :: SolverTestData -> Maybe Time -> IO Bool
 longTimeTest (SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, mb'timeoutOpt) goal_tmo =
   TCL.withChecklist "timer tests" $
   withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      extendConfig opts (getConfiguration sym)
 
      -- Configure a solver timeout in What4 if specified for this test.

what4/test/TestTemplate.hs

@@ -38,6 +38,7 @@ import qualified What4.Protocol.Online as Online
 import           What4.Protocol.Online (SolverProcess(..), OnlineSolver(..))
 import qualified What4.Solver.CVC4 as CVC4
 
+import What4.Expr
 import What4.Expr.App (reduceApp)
 import What4.Expr.Builder
 import What4.Expr.GroundEval
@@ -53,8 +54,6 @@ import GHC.Stack
 
 --import Debug.Trace (trace)
 
-data State t = State
-
 
 
 main :: IO ()
@@ -66,7 +65,7 @@ main =
               (do r <- roundingModes
                   (Some <$> floatTemplates [r] 1 fpp))
 
-     sym <- newExprBuilder FloatIEEERepr State globalNonceGenerator
+     sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState globalNonceGenerator
 
      extendConfig CVC4.cvc4Options (getConfiguration sym)
      proc <- Online.startSolverProcess @(SMT2.Writer CVC4.CVC4) CVC4.cvc4Features Nothing sym