在 Z3 haskell 中使用 forall

Question

我在 haskell 中使用 z3 包，但无法从文档中找出如何调用 mkForall

我正在尝试实现这个

(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
(assert (= (select a 1) 7))
(assert (forall ((x Int)) (> (select a x) 5)))
(check-sat)

到目前为止我有这个

do
  intSort <- mkIntSort
  arraySort <- mkArraySort intSort intSort
  a <- mkFreshVar "a" arraySort
  _0 <- mkInteger 0
  _1 <- mkInteger 1
  _10 <- mkInteger 10
  _7 <- mkInteger 7
  _5 <- mkInteger 5
  assert =<< mkEq _10 =<< mkSelect a _0
  assert =<< mkEq _7 =<< mkSelect a _1
  x <- mkStringSymbol "x"
  mkForall [] [x] [intSort] =<< mkLe _5 =<< mkSelect a x
  solverCheck

倒数第二行不起作用，因为我没有声明 x Int 的 AST

mkForall 的正确方法是什么？

Answer 1

你只需要 declare-const 在外面 mkForAll

do
  intSort <- mkIntSort
  arraySort <- mkArraySort intSort intSort
  a <- mkFreshVar "a" arraySort
  _0 <- mkInteger 0
  _1 <- mkInteger 1
  _10 <- mkInteger 10
  _7 <- mkInteger 7
  _5 <- mkInteger 5
  assert =<< mkEq _10 =<< mkSelect a _0
  assert =<< mkEq _7 =<< mkSelect a _1
  x <- mkStringSymbol "x"
  xv <- mkVar x intSort
  -- ^^^^^ note this line
  mkForall [] [x] [intSort] =<< mkLe _5 =<< mkSelect a xv
  solverCheck

--- 编辑

尽管做了 assert =<< mkForall ....，但我对 forall 的断言似乎并没有成立，我认为 xv 没有绑定到 mkForall 调用中的 x

---- 已解决

  arg <- mkBound 0 intSort
  assert =<< mkForall [] [x] [intSort] =<< mkLe _5 =<< mkSelect a arg

使用 mkBound 获取 deBruijn 索引参数

在 Z3 haskell 中使用 forall

Using forall in Z3 haskell

haskell

smt

z3