Каковы эквивалентные клаксоны к этим пунктам? - PullRequest
Новая
       8

Каковы эквивалентные клаксоны к этим пунктам?

0 голосов
/ 14 октября 2019

Я использую Z3 и расширенный синтаксис SMT-LIB2 для решения моих клаксонов. Я знаю, что глава клаузулы рога должна быть неинтерпретируемым предикатом;но мне интересно, как мне переписать следующие пункты, чтобы они были набором клаузул рога. 

(declare-rel inv (Int Int ))
(declare-var k Int)
(declare-var k_p Int)
(declare-var a Int)
(declare-var a_p Int)

(rule (=> (and (= a 0) (= k 0)) (inv a k)))
(rule (=> (and (inv a k) (= a_p (+ a 1))(= k_p (+ k 1))) (inv  a_p k_p))) 
(rule (=> (and (inv  a k) (> k 0) ) (> a 0)))
(query inv )

Z3 жалуется, что (> a 0) не может быть главой клаузулы рога. Я могу переписать последнее предложение следующим образом: 

(rule (=> (and (inv  a k) (> k 0) ) (gtz a)))
(rule (=> (> a 0) (gtz a)))

Но тогда предложения станут настолько слабыми, что я не получу предполагаемую модель для инварианта inv. Интересно, есть ли лучший способ сделать это?

...