what4 has two different representation of concrete SMT arrays (i.e., GroundArrays):
ArrayMapping: an array that is defined by a total, higher-order function.
ArrayConcrete: an array where most indices map to a constant value, with certain indices mapping to separate values instead.
It is far preferable to have ArrayConcrete instead of ArrayMapping in counterexamples, as it is much simpler to display and inspect ArrayConcrete values than it is to display ArrayMapping.
To my surprise, what4 often produces ArrayMapping values in places where an ArrayConcrete would suffice. Consider this example, for instance:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Main (main) where
import Data.Foldable (forM_)
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(..))
import System.IO (stdout)
import What4.Config
import What4.Expr
import What4.Interface
import What4.Solver
import What4.Protocol.SMTLib2
z3executable :: FilePath
z3executable = "z3"
main :: IO ()
main = do
Some ng <- newIONonceGenerator
sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
extendConfig z3Options (getConfiguration sym)
arr <-
freshConstant
sym
(safeSymbol "arr")
(BaseArrayRepr (Ctx.Empty Ctx.:> BaseIntegerRepr) BaseBoolRepr)
idx27 <- intLit sym 27
arr27 <- arrayLookup sym arr (Ctx.Empty Ctx.:> idx27)
idx42 <- intLit sym 42
arr42 <- arrayLookup sym arr (Ctx.Empty Ctx.:> idx42)
p <- andPred sym arr27 =<< notPred sym arr42
checkModel sym p arr
[ ("arr27", SomeExpr arr27)
, ("arr42", SomeExpr arr42)
]
data SomeExpr t where
SomeExpr :: Show (GroundValue tp) => Expr t tp -> SomeExpr t
printGroundArray ::
Show (GroundValue b) =>
GroundArray idx b ->
IO ()
printGroundArray gArr =
case gArr of
ArrayMapping{} ->
putStrLn "ArrayMapping"
ArrayConcrete def updates ->
putStrLn $ showString "ArrayConcrete "
. showsPrec 11 def
. showChar ' '
. showsPrec 11 updates
$ ""
checkModel ::
Show (GroundValue b) =>
ExprBuilder t st fs ->
BoolExpr t ->
Expr t (BaseArrayType idx b) ->
[(String, SomeExpr t)] ->
IO ()
checkModel sym f arr es = do
withZ3 sym z3executable defaultLogData{logHandle = Just stdout} $ \session -> do
assume (sessionWriter session) f
runCheckSat session $ \result ->
case result of
Sat (ge, _) -> do
putStrLn "Satisfiable, with model:"
gArr <- groundEval ge arr
printGroundArray gArr
forM_ es $ \(nm, SomeExpr e) -> do
v <- groundEval ge e
putStrLn $ " " ++ nm ++ " := " ++ show v
Unsat _ -> putStrLn "Unsatisfiable."
Unknown -> putStrLn "Solver failed to find a solution."
Here, the SMT array arr could be concretized as an ArrayConcrete where most indices map to True, but where the value at index 42 maps to False instead. To my surprise, however, that is not what what4 picks when concretizing arr:
Note that I am interleaving the SMT solver interactions (using defaultLogData{logHandle = Just stdout}), but the important bit is that ArrayMapping appears in the output rather than ArrayConcrete. What's more, this ArrayMapping does not come from the SMT solver, since there is no corresponding (get-value ...) call in the Z3 process for retrieving a model for arr. As such, this ArrayMapping must be coming from what4's own simplification rules.
We should investigate why this happens and see if we can make what4 produce an ArrayConcrete here instead of an ArrayMapping.
what4
has two different representation of concrete SMT arrays (i.e.,GroundArray
s):ArrayMapping
: an array that is defined by a total, higher-order function.ArrayConcrete
: an array where most indices map to a constant value, with certain indices mapping to separate values instead.It is far preferable to have
ArrayConcrete
instead ofArrayMapping
in counterexamples, as it is much simpler to display and inspectArrayConcrete
values than it is to displayArrayMapping
.To my surprise,
what4
often producesArrayMapping
values in places where anArrayConcrete
would suffice. Consider this example, for instance:Here, the SMT array
arr
could be concretized as anArrayConcrete
where most indices map toTrue
, but where the value at index 42 maps toFalse
instead. To my surprise, however, that is not whatwhat4
picks when concretizingarr
:Note that I am interleaving the SMT solver interactions (using
defaultLogData{logHandle = Just stdout}
), but the important bit is thatArrayMapping
appears in the output rather thanArrayConcrete
. What's more, thisArrayMapping
does not come from the SMT solver, since there is no corresponding(get-value ...)
call in the Z3 process for retrieving a model forarr
. As such, thisArrayMapping
must be coming fromwhat4
's own simplification rules.We should investigate why this happens and see if we can make
what4
produce anArrayConcrete
here instead of anArrayMapping
.