Наличие утверждений внутри определений в SMT - PullRequest
Новая
       21

Наличие утверждений внутри определений в SMT

1 голос
/ 02 ноября 2019

Я хочу захватить утверждение внутри фак. 

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))

Я не хочу этого. Есть ли другой способ сделать это без повторения?

РЕДАКТИРОВАТЬ Моя цель - найти значения, нарушающие утверждения.

1 Ответ

1 голос
/ 02 ноября 2019

Насколько я знаю , невозможно встроить утверждения в определения функций.

Я бы попытался отделить ожидаемое поведение, исходные предположения игарантии вывода (если есть).

Пример: 

(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. Вывод с использованием онлайн-инструмента Z3 выглядит следующим образом: 

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

Я бы сказал, что такой подход может стать хитрым, как только f и g используются как в положительном, так и в отрицательном контекстах. В этом случае следует обратить особое внимание на правильность полярности утверждений. ожидаемый результат.

...