在 Z3 haskell 中使用 forall答案

【问题标题】：Using forall in Z3 haskell在 Z3 haskell 中使用 forall
【发布时间】：2021-03-13 02:59:30
【问题描述】：

我在 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 的正确方法是什么？

【问题讨论】：

标签： haskell z3 smt

【解决方案1】：

你只需要在mkForAll之外declare-const就可以了

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 索引参数

【讨论】：