在SMT的定义中包含断言

Question

我想捕获事实事实断言。

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，此方法可能会变得棘手。在这种情况下，应该特别注意断言的极性正确。预期的结果。