Как правильно сделать аксиому в Z3Py?

Question

Я работаю в этой аксиоме ForAll X (f (x)> 0 -> b == True).

Как я мог сделать это в Z3Py? Я пытаюсь сделать это:

from z3 import *

Z = IntSort()
f = Function('f', Z, Z)
g = Function('g', Z, Z)
a, n, x = Ints('a n x')
b = BoolSort()
solve(ForAll(x,Implies(f(x) > 0,b ==True)))

но Python вернуть мне AttributeError: 'bool' object has no attribute 'ast'

Answer 1

Что ваша аксиома пытается сформулировать? Обратите внимание, что в формуле ForAll X. (f(x) > 0 -> b == True), b является свободной переменной. Так что, похоже, это не соответствует чему-то логическому. Но, если это то, что вы действительно хотите сказать, вот как вы могли бы написать это:

from z3 import *

Z = IntSort()
f = Function('f', Z, Z)
g = Function('g', Z, Z)
a, n, x = Ints('a n x')
b = Bool('b')
solve(ForAll(x,Implies(f(x) > 0, b)))

И мы получим:

$ python a.py
[b = False, f = [else -> 0]]

Что говорит нам z3? Там написано, хорошо, я выберу f как функцию, которая отображает все на 0. Таким образом, у вашего подтекста будет антецедент 0 > 0, который всегда равен false, и, следовательно, импликация всегда верна. (Ложь подразумевает что-либо.) Выбор False для b в модели действительно не имеет значения.

Итак, z3 действительно нашел модель для f и b, которая удовлетворяла вашему количественному утверждению , Как ты и просил. Но я подозреваю, что это была не та формула, которую вы пытались отстаивать. Аксиомы обычно закрыты: то есть у них нет свободных переменных, кроме символов неинтерпретируемых функций, которые они включают. Конечно, все зависит от того, что именно вы пытаетесь сделать.

Answer 2

Вы можете объявить b как b = Bool('b'). Тогда это работает.

Кстати, вы можете заменить b == True просто b, как в

solve(ForAll(x,Implies(f(x) > 0, b ))).

BoolSort et c , предназначены для параметров функций Z3Py, а не для переменных.