在使用z3处理我的硕士论文时,我发现了一些我无法理解的奇怪的东西.我希望你能帮助我.:)
我写的smt文件看起来像这样:
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
;Declare sort Node and its objects.
(declare-sort Node 0)
(declare-fun n0 () Node)
(declare-fun n1 () Node)
;Predicate
(declare-fun dead_0 (Node) Bool)
;Abbreviation
(declare-fun I () Bool)
;initial configuration
(assert(= I (and
(not(= n0 n1))
(not(dead_0 n0))
(dead_0 n1))))
;Predicate
(declare-fun dead_1 (Node) Bool)
;variable
(declare-fun m0_1 () Node)
;Abbreviation for Transformation
(declare-fun TL1_1 () Bool)
;Transformation1neuerKnoten1
(assert(or (= m0_1 n0)(= m0_1 n1)))
;Is the whole formula satisfiable?
(assert(= (and I TL1_1) true)) …z3 ×1