Руководствуясь поиском доказательства Z3 - PullRequest
Новая
       6

Руководствуясь поиском доказательства Z3

0 голосов
/ 13 мая 2018

Я пытаюсь заставить z3 работать (большую часть времени) для очень простых нелинейных целочисленных арифметических задач.К сожалению, я ударил немного стены с возведением в степень.Я хочу уметь справляться с такими проблемами, как x ^ {a + b + 2} = (x * x * x ^ {a} * x {b}).Мне нужно работать только с неотрицательными показателями.

Я попытался переопределить возведение в степень как рекурсивную функцию (чтобы просто было разрешено возвращать 1 для любого неположительного показателя) и использовать шаблон, чтобы упростить z3, выводя, что x^ {a + b} = x ^ {a} * x ^ {b}, но, похоже, это не сработает - у меня все еще тайм-аут. 

(define-fun-rec pow ((x!1 Int) (x!2 Int)) Int
  (if (<= x!2 0) 1 (* x!1 (pow x!1 (- x!2 1)))))
; split +
(assert (forall ((a Int) (b Int) (c Int)) 
  (! (=> 
      (and (>= b 0) (>= c 0)) 
      (= (pow a (+ b c)) (* (pow a c) (pow a b)))) 
   :pattern ((pow a (+ b c))))))

; small cases
(assert (forall ((a Int)) (= 1 (pow a 0))))
(assert (forall ((a Int)) (= a (pow a 1))))
(assert (forall ((a Int)) (= (* a a) (pow a 2))))
(assert (forall ((a Int)) (= (* a a a) (pow a 3))))

; Our problem
(declare-const x Int)
(declare-const i Int)
(assert (>= i 0))

; This should be provably unsat, by splitting and the small case for 2
(assert (not (= (* (* x x) (pow x i)) (pow x (+ i 2)))))

(check-sat) ;times out

Неправильно ли я использую шаблоны,Есть ли способ дать более сильный намек на поиск доказательства или более простой способ добиться того, чего я хочу?

1 Ответ

0 голосов
/ 13 мая 2018

Шаблон (также называемый триггерами) может содержать только неинтерпретированные функции. Поскольку + является интерпретируемой функцией, вы, по сути, предоставляете недопустимый шаблон, и в этом случае может произойти практически все.

В качестве первого шага я отключил функцию автоконфигурации Z3, а также инстанцирование квантификатора на основе MBQI: 

(set-option :auto_config false)
(set-option :smt.mbqi false)

Затем я ввел неинтерпретированную функцию plus и заменил каждое приложение + на plus. Этого было достаточно, чтобы проверить ваше утверждение (то есть вывести unsat). Конечно, вы также можете аксиоматизировать plus в терминах +, т.е. 

(declare-fun plus (Int Int) Int)

(assert (forall ((a Int) (b Int)) 
  (! (= (plus a b) (+ a b))
   :pattern ((plus a b)))))

но ваше утверждение уже проверяется без аксиом определения для plus.

...