在 SMT 中的定义中包含断言

Question

我想捕获 fac 中的断言。

int f( x )
{
     if( x == 1) return 1;
     else{
         assert( x > 0 );
         return 2;         
         }
}

int g (x)
{  assert( x > 5 );
   return f(x-1) + f(x-2);
}

我想要一个 smt2 代码。 我可以通过剥离参数并使用唯一名称使其全局化（也在 f 内重命名）来做到这一点，然后每次使用不同的函数名称执行 3 次。如下所示：

( declare-const x1 Int )
(define-fun f1 () Int 
            ( ite ( x1 > 0) 1 2 )
) 
(assert (> x1 0))

( declare-const x2 Int )
(define-fun f2 () Int 
            ( ite ( x2 > 0) 1 2 )
) 
(assert (> x2 0))

( declare-const x3 Int )
(define-fun g1 () Int 
            ( + f1 f2 )
) 
(assert (> x3 5))

我不想这样。有没有其他方法可以做到这一点而不重复？

编辑 我的目的是找到违反断言的值。

Answer 1

据我所知，不可能在函数定义中嵌入断言。

我会尝试做的是将预期行为、输入假设和输出保证（如果有的话）分开。

示例：

(define-fun f ((x Int)) Int
      (ite (= x 1) 1 2)
)

(define-fun f-helper ((x Int)) Bool
      (< 0 x)
)

(define-fun g ((x Int)) Int
    (+ (f (- x 1)) (f (- x 2)))
)

(define-fun g-helper ((x Int)) Bool
    (and (< 5 x)
         (f-helper (- x 1))
         (f-helper (- x 2))
    )
)

(declare-const x Int)
(declare-const y Int)

(assert (and (= y (g x))
             (g-helper x)
))

(check-sat)
(get-model)

在这个例子中，我们使用f 来模拟原始函数f 的行为，并使用f-helper 来模拟f 的假设。使用online Z3 tool的输出如下：

sat
(model 
  (define-fun x () Int
    6)
  (define-fun y () Int
    4)
)

---

我的结论是，一旦在正面和负面的上下文中使用f 和g，这种方法可能会变得棘手。在这种情况下，应该特别注意断言的极性是正确的.预期的结果。