无量词的方式来指定Z3和类型的构造函数

Question

假设我在Z3中有一个简单的和类型，有几个不同的构造函数：

(declare-datatypes ()
  ((Foo bar
        (baz (unbaz String))
        (quux (unquux1 String) (unquux2 Int)))))

我怎么断言我知道Foo类型的价值是quux？我可以介绍一个关于quux1和quux2的存在主义，但我很谨慎地引入看似不必要的量词。是否有更好的方法来断言？

Answer 1

当假设时，存在是相当无害的，因为存在量化的变量是直接实例化的，因此只需要额外的符号。也就是说，片段的后半部分

(declare-datatypes ()
  ((Foo bar
        (baz (unbaz String))
        (quux (unquux1 String) (unquux2 Int)))))

(declare-const f Foo)

(assert (exists ((s String) (i Int)) ;; Let f be a quux
  (= f (quux s i))
))

(assert (= f (baz "test"))) ;; Also let f be a baz
(check-sat) ;; UNSAT - as expected

相当于

...
(declare-const _s String)
(declare-const _i Int)
(assert (= f (quux _s _i))) ;; Let f be a quux

(assert (= f (baz "test"))) ;; Also let f be a baz
(check-sat) ;; UNSAT - as expected

如果你对存在感而不是foralls警惕，那么你可以通过公理化从Foo构造函数到不同标记的映射来标记Foo值：

(set-option :smt.mbqi false)

(declare-datatypes ()
  ((Foo bar
        (baz (unbaz String))
        (quux (unquux1 String) (unquux2 Int)))))

;; Declare a finite sort Foo_tag with three distinct elements
(declare-datatypes () ((Foo_tag Foo_tag.bar Foo_tag.baz Foo_tag.quux)))

;; Alternatively, three distinct elements from an infinite sort such 
;; as Int can be used. Either by choosing distinct but unspecified 
;; values, as done below, or by directly choosing concrete values,
;; e.g. 1, 2, 3.
; (define-sort Foo_tag () Int)
; (declare-const Foo_tag.bar Foo_tag)
; (declare-const Foo_tag.baz Foo_tag)
; (declare-const Foo_tag.quux Foo_tag)
; (assert (distinct Foo_tag.bar Foo_tag.baz Foo_tag.quux))

;; Tagging function
(declare-fun tag_of (Foo) Foo_tag)

;; Tagging axiom for bar ...
(assert (= (tag_of bar) Foo_tag.bar))

;; ... baz ...
(assert (forall ((s String)) (! 
  (= (tag_of (baz s)) Foo_tag.baz)
  :pattern ((baz s))
)))

;; ... and quux
(assert (forall ((s String) (i Int)) (! 
  (= (tag_of (quux s i)) Foo_tag.quux)
  :pattern ((quux s i))
)))

;; Let's do some testing

(declare-const f Foo)

(assert (= (tag_of f) Foo_tag.quux)) ;; Tag f as a quux

(push)
  (assert (= f bar))
  (check-sat) ;; UNSAT - as expected
(pop)

(push)
  (assert (= f (baz "test")))
  (check-sat) ;; UNSAT - as expected
(pop)