Как Z3 справляется с предложением forall с неинтерпретируемыми функциями в нем?

Предположим, у нас есть две неинтерпретируемые функции func1 и func2:

stuct_sort func1(struct_sort);
stuct_sort func2(struct_sort ,int).

И у них есть отношения:

func2(p,n)=func1(p)  if n==1
func2(p,n)=func1(func2(p,n-1))  if n>1

Я хочу знать, что если следующее предложение:

((forall i:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].func2(q,i)==Z)

может быть доказано в Z3? В моей программе результат проверки равен Z3_L_UNDEF.

Когда я присваиваю m такое значение, как 3, предложение становится

((forall i:[1,3].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,3-1].func2(q,i)==Z);

результат Z3_L_UNDEF. Но когда я переписываю случай отдельно (не используя forall) следующим образом, получается true.

(func2(p,1)==Z)&&(func2(p,2)==Z)&&(func2(p,3)==Z)&&(q==func1(p)) implies (func2(q,1))&&(func2(q,2)).

Не могу понять причину жду ответа


z3 forall
person user1952701    schedule 06.01.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я закодировал вашу проблему, используя интерфейс Z3 Python, и Z3 решил ее. Он нашел контрпример для гипотезы. Конечно, я мог ошибиться, когда кодировал проблему. Код Python находится в конце поста. Мы можем попробовать его в Интернете по адресу rise4fun. Кстати, какую версию Z3 вы используете? Я предполагаю, что вы используете C API. Если это так, не могли бы вы предоставить код C, который вы использовали для создания формул Z3? Другая возможность — создать журнал, который записывает взаимодействие вашего приложения и Z3. Чтобы создать файл журнала, мы должны выполнить Z3_open_log("z3.log"); до того, как вы запустите любой другой Z3 API. Мы можем использовать файл журнала, чтобы воспроизвести все взаимодействия между вашим приложением и Z3.

from z3 import *
# Declare stuct_sort 
S = DeclareSort('stuct_sort')
I = IntSort()
# Declare functions func1 and func2
func1 = Function('func1', S, S)
func2 = Function('func2', S, I, S)

# More declarations
p = Const('p', S)
n = Int('n')
m = Int('m')
i = Int('i')
q = Const('q', S)
Z = Const('Z', S)

# Encoding of the relations 
#    func2(p,n)=func1(p)  if n==1
#    func2(p,n)=func1(func2(p,n-1))  if n>1
Relations = And(func2(p, 1) == func1(p), 
                ForAll([n], Implies(n > 1, func2(p, n) == func1(func2(p, n - 1)))))

# Increase the maximum line width for the Z3 Python formula pretty printer
set_option(max_width=120)
print Relations

# Encoding of the conjecture
# ((forall i:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].func2(q,i)==Z)
Conjecture = Implies(And(q == func1(p), ForAll([i], Implies(And(1 <= i, i <= m), func2(p, i) == Z))),
                     ForAll([i], Implies(And(1 <= i, i <= m - 1), func2(q, i) == Z)))
print Conjecture

prove(Implies(Relations, Conjecture))
person Leonardo de Moura    schedule 06.01.2013
comment
Я снова протестировал последнюю версию Z3, используя C API со следующим входом и все еще не определен: (implies (and (= (func2 pp 1) (func1 pp)) (forall (ii Int) (implies (> ii 1) (= (func2 pp ii) (func1 (func2 pp (+ ii (* -1 1)))))))) (implies (and (= q (func1 p)) (forall (i Int) (implies (and (>= i 1) (<= i m)) (= (func2 p i) Z)))) (forall (i Int) (implies (and (>= i 1) (<= i (+ m (* -1 1)))) (= (func2 q i) Z))))) - person user1952701; 09.01.2013
comment
код можно найти здесь: https://gist.github.com/4491662 - person user1952701; 09.01.2013
comment
В вашем коде используются устаревшие функции, такие как Z3_check_and_get_model. Кстати, C++ API намного проще в использовании. Файл examples/c++/example.cpp содержит множество примеров с использованием C++ и нового API решателя. Вот ссылка на этот файл: z3.codeplex. com/SourceControl/changeset/view/ - person Leonardo de Moura; 09.01.2013
comment
C++ API действительно прост в использовании, и я решил проблему с его помощью. Большое спасибо за ваше терпение и советы. - person user1952701; 10.01.2013