如何为偏序生成模型? [英] How to produce the model for partial orders?

问题描述

我正在尝试使用 Z3 为描述偏序理论的一组 SAT 断言生成模型.我尝试了 Z3 指南中的子类型示例，但似乎无法获得具体模型.Z3 有没有办法生成一个模型来描述元素之间的顺序并满足我所做的所有断言?

I am trying to use Z3 to produce a model for a set of SAT assertions describing a partial order theory. I tried the subtype example in Z3 guide but it seems I cannot get a concrete model. Is there a way that Z3 can produce a model that describes the orders among elements and satisfies all assertions I made?

例如，以下是子类型"的约束.Z3 是否有可能产生类似int-type *<* real-type *<* complex-type *<* obj-type *<* root-type"和string-type *<"这样的模型?;* obj-type *<* root-type"(如果我使用*<*"来表示子类型关系)?

For example, following are the constraints for "subtype". Is it possible that Z3 may produce a model like "int-type *<* real-type *<* complex-type *<* obj-type *<* root-type" and "string-type *<* obj-type *<* root-type" (if I use "*<*" to denote subtype relation)?

(set-option :produce-models true)
(declare-sort Type)
(declare-fun subtype (Type Type) Bool)

(assert (forall ((x Type)) (subtype x x)))

(assert (forall ((x Type) (y Type))
          (=> (and (subtype x y) (subtype y x)) 
              (= x y))))

(assert (forall ((x Type) (y Type) (z Type))
          (=> (and (subtype x y) (subtype y z)) 
              (subtype x z)))) 

(assert (forall ((x Type) (y Type) (z Type))
          (=> (and (subtype x y) (subtype x z)) 
              (or (subtype y z) (subtype z y)))))               

(declare-const obj-type Type)
(declare-const int-type Type)
(declare-const real-type Type)
(declare-const complex-type Type)
(declare-const string-type Type)


(assert (forall ((x Type)) (subtype x obj-type)))

(assert (subtype int-type real-type))
(assert (subtype real-type complex-type))
(assert (not (subtype string-type real-type)))
(declare-const root-type Type)
(assert (subtype obj-type root-type))


(check-sat)
(get-model)

目前，我得到了

sat
(model 
  ;; universe for Type:
  ;;   Type!val!0 Type!val!3 Type!val!2 Type!val!4 Type!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Type!val!0 () Type)
  (declare-fun Type!val!3 () Type)
  (declare-fun Type!val!2 () Type)
  (declare-fun Type!val!4 () Type)
  (declare-fun Type!val!1 () Type)
  ;; cardinality constraint:
  (forall ((x Type))
          (or (= x Type!val!0)
              (= x Type!val!3)
              (= x Type!val!2)
              (= x Type!val!4)
              (= x Type!val!1)))
  ;; -----------
  (define-fun complex-type () Type
    Type!val!2)
  (define-fun real-type () Type
    Type!val!1)
  (define-fun obj-type () Type
    Type!val!4)
  (define-fun root-type () Type
    Type!val!4)
  (define-fun string-type () Type
    Type!val!3)
  (define-fun int-type () Type
    Type!val!0)
  (define-fun subtype!73 ((x!1 Type) (x!2 Type)) Bool
    (ite (and (= x!1 Type!val!3) (= x!2 Type!val!1)) false
    (ite (and (= x!1 Type!val!2) (= x!2 Type!val!3)) false
    (ite (and (= x!1 Type!val!4) (= x!2 Type!val!1)) false
    (ite (and (= x!1 Type!val!4) (= x!2 Type!val!3)) false
    (ite (and (= x!1 Type!val!2) (= x!2 Type!val!1)) false
    (ite (and (= x!1 Type!val!1) (= x!2 Type!val!3)) false
    (ite (and (= x!1 Type!val!4) (= x!2 Type!val!0)) false
    (ite (and (= x!1 Type!val!4) (= x!2 Type!val!2)) false
    (ite (and (= x!1 Type!val!0) (= x!2 Type!val!3)) false
    (ite (and (= x!1 Type!val!2) (= x!2 Type!val!0)) false
    (ite (and (= x!1 Type!val!1) (= x!2 Type!val!0)) false
    (ite (and (= x!1 Type!val!3) (= x!2 Type!val!0)) false
      true)))))))))))))
  (define-fun k!72 ((x!1 Type)) Type
    (ite (= x!1 Type!val!1) Type!val!1
    (ite (= x!1 Type!val!4) Type!val!4
    (ite (= x!1 Type!val!3) Type!val!3
    (ite (= x!1 Type!val!0) Type!val!0
      Type!val!2)))))
  (define-fun subtype ((x!1 Type) (x!2 Type)) Bool
    (subtype!73 (k!72 x!1) (k!72 x!2)))
)

预先感谢您提供的任何帮助.

Thank you in advance for any help you could give.

推荐答案

我认为你的行

(assert (forall ((x Type)) (subtype x obj-type)))

错了.

正确的是

(assert (forall ((x Type)) (subtype x root-type)))  

可能的正确模型在这里

这篇关于如何为偏序生成模型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！