неизвестно при использовании целочисленного деления в z3 smt2

Question

Я пытаюсь найти решение для функции penta (n) = (n * (3n -1))/2 и где penta (z) = penta (a) + penta (b) для всех положительных чисел. Это работает до тех пор, пока целочисленное деление (div) не будет частью определения, но когда оно добавлено в определение, я либо получил тайм-аут, либо неизвестный. Я ожидал бы получить 8, 7, 4. Любая идея о том, что я сделал неправильно?

(declare-const a Int) 
(declare-const b Int) 
(declare-const z Int) 

(define-fun penta ((n Int)) Int (div (* (- (* 3 n) 1) n) 2)) 

(assert (= (penta z) (+ (penta a) (penta b)) )) 
(assert (> a 1)) 
(assert (> b 1)) 
(assert (> z 1)) 

(check-sat) 
(get-model) 

Я использую версию на http://rise4fun.com/Z3 сайте и версии 4.1 (x64).

Answer 1

Основная проблема заключается в том, что проблема использует целочисленное умножение между двумя нечисловыми аргументами. Нет никаких процедур принятия решений по диофантовым проблемам, поэтому Z3 делает все возможное, что не способствует перечислению модели.

Если вы не используете целочисленное деление, Z3 попытается выполнить частичную эвристику на основе , преобразуя проблему в битовые векторы конечных доменов, чтобы найти модели. Он вызывает эту эвристику, выполняя синтаксическую проверку формул. Синтаксическая проверка не работает при использовании оператора (div .. 2). Вы можете кодировать (Div х 2), так что эвристика поднимает проблему , вводя новые переменные и ограничивающие их:

(declare-const penta_z Int) 
(declare-const penta_a Int) 
(declare-const penta_b Int) 
(assert (or (= (* 2 penta_z) (penta z)) (= (+ 1 (* 2 penta_z)) (penta z)))) 
(assert (or (= (* 2 penta_a) (penta a)) (= (+ 1 (* 2 penta_a)) (penta a)))) 
(assert (or (= (* 2 penta_b) (penta b)) (= (+ 1 (* 2 penta_b)) (penta b)))) 
(assert (= penta_z (+ penta_a penta_b) )) 
(assert (> a 1)) 
(assert (> b 1)) 
(assert (> z 1)) 
(assert (>= penta_z 0)) 
(assert (<= penta_z 100)) 

Вы также можете напрямую кодировать вашу проблему с помощью битовых векторов, хотя это начинает получать к ошибкам, потому что вам нужно иметь дело с тем, как обращаться с переполнениями.