what4 struct nat bug

StructNatBug.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Main where

import Data.Foldable (forM_)
import System.IO (FilePath, openFile, IOMode(..))

import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(..))
import Data.Parameterized.Context

import What4.Config (extendConfig)
import What4.Expr
         ( ExprBuilder,  FloatModeRepr(..), newExprBuilder
         , BoolExpr, GroundValue, groundEval, Expr, GroundValueWrapper(..) )
import What4.Interface
         ( BaseTypeRepr(..), BaseStructType, BaseNatType, getConfiguration, knownRepr
         , freshConstant, safeSymbol
         , notPred, orPred, andPred, truePred
         , natLit, natLt, structField)
import What4.Solver
         (defaultLogData, logCallbackVerbose, z3Options, withZ3, SatResult(..))
import What4.Solver.Z3 (Z3(..))
import What4.Protocol.SMTLib2
         (assume, sessionWriter, runCheckSat, defaultFeatures, Writer(..))
import What4.Protocol.Online (startSolverProcess, checkSatisfiableWithModel, SolverProcess(..))


data BuilderState st = EmptyState

z3executable :: FilePath
z3executable = "z3"

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

  -- This line is necessary for working with z3.
  extendConfig z3Options (getConfiguration sym)

  x <- freshConstant sym (safeSymbol "x") (BaseStructRepr (Empty :> BaseNatRepr))
  a <- structField sym x baseIndex

  m <- natLit sym 4294967295
  p <- natLt sym a m

  checkModel sym p [("x", x)]

-- | Determine whether a predicate is satisfiable, and print out the values of a
-- set of expressions if a satisfying instance is found.
checkModel ::
  ExprBuilder t st fs ->
  BoolExpr t ->
  [(String, Expr t (BaseStructType (EmptyCtx ::> BaseNatType)))] ->
  IO ()
checkModel sym f es = do
  -- We will use z3 to determine if f is satisfiable.
  h <- openFile "z3.out" WriteMode
  s :: SolverProcess t (Writer Z3) <- startSolverProcess (defaultFeatures Z3) (Just h) sym
  checkSatisfiableWithModel s "check" f $ \result ->
    case result of
      Sat ge -> do
        putStrLn "Satisfiable, with model:"
        forM_ es $ \(nm, e) -> do
          (Empty :> GVW n) <- groundEval ge e
          putStrLn $ "  " ++ nm ++ " := " ++ show n
      Unsat _ -> putStrLn "Unsatisfiable."
      Unknown -> putStrLn "Solver failed to find a solution."

z3.out

(set-option :print-success true)
; success
(set-option :produce-models true)
; success
(set-option :pp.decimal true)
; success
(set-option :global-declarations true)
; success
(get-info :error-behavior)
; (:error-behavior continued-execution)
(push 1)
; success
; :1:0
(declare-datatypes (T0) ((Struct1 (mk-struct1 (struct1-proj0 T0)))))
; success
(declare-fun x () (Struct1 Int))
; success
(define-fun x!0 () Int (struct1-proj0 x))
; success
(define-fun x!1 () Bool (<= 4294967295 x!0))
; success
(define-fun x!2 () Bool (not x!1))
; success
(assert x!2)
; success
(check-sat)
; sat
(get-value ((struct1-proj0 x)))
; (((struct1-proj0 x) 0))
(pop 1)
; success