1

以下代码介绍了使用 Z3 和 SMT-LIB 的热带算术的基本属性：

; This example illustrates basic tropical arithmetic 

(define-fun tropadd  ((a Real)(b Real)) Real (if (> a b)
                                        b
                                        a))
(define-fun tropmul ((a Real)(b Real)) Real (+ a b))
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(push)
(assert(not(= (tropadd x y) (tropadd y x))))
(check-sat)
(pop)
(push)
(assert(not(= (tropmul x y) (tropmul y x))))
(check-sat)
(pop)
(push)
(assert(not(= (tropmul x (tropmul y z)) (tropmul (tropmul x y) z))))
(check-sat)
(pop)
(push)
(assert(not(= (tropadd x (tropadd y z)) (tropadd (tropadd x y) z))))
(check-sat)
(pop)
(push)
(assert(not(= (tropmul x (tropadd y z)) (tropadd (tropmul x y) (tropmul x z)))))
(check-sat)
(pop)

(push)
(assert(not(= (tropmul x 0) x)))
(check-sat)
(pop)
(push)
(assert (= (tropmul x 2) 3))
(check-sat)
(get-model)
(pop)
(push)
(assert (= (tropadd x 2) 1))
(check-sat)
(get-model)

输出是：

unsat 
unsat 
unsat 
unsat 
unsat 
unsat 

sat 
(model (define-fun x () Real 1.0) 

sat 
(model (define-fun x () Real 1.0) )

请在此处在线运行此代码

这段代码介绍了热带加法和热带乘法。然后证明了这些操作满足：交换、关联、分配；对热带繁殖具有调节作用。

为了满足热带加法的调制，有必要引入无穷大，也就是说一个新的符号，例如：无穷大 + a = a对于所有a。

拜托，你能教我如何在热带代码中引入这种无穷大吗？非常感谢。

4

1 回答 1

3

您必须定义一种新类型，某种区分联合以包含无穷大；并扩展您的操作以涵盖这种新类型。在 SMT-Lib 中执行此操作的标准方法是引入未解释的排序，然后断言 mul/add 等的定义，作为适当的公理。底层求解器处理这些公理的能力实际上取决于它处理量词的能力以及你向它抛出的问题类型，因为这些公理无疑会涉及量词。

另一种方法是使用更高级别的方法，例如 Z3Py 或 SBV（Haskell 与 Z3 和其他 SMT 求解器的绑定）所倡导的方法，您可以在这些语言提供的高级结构中隐藏大部分机制。这是我首先要尝试的，因为当您处理许多未解释的排序、公理等时，SMT-Lib 会变得非常冗长且容易出错。

于 2013-06-05T18:14:04.030 回答