z3 - 减少具有相同数量参数排序和返回排序的函数声明

Question

我有一个 smt 程序，需要声明具有相同数量的参数(和排序)和相同的返回排序的多个函数。 例如:

(declare-fun main0 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun main1 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun main2 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun main3 (Bool Bool Bool Bool Bool Bool Bool) Bool)
...

有什么方法可以减少声明，以便我可以对这些函数的参数(例如主体)进行排序)，而我需要定义的所有内容是:

(declare-fun main0 (body) Bool)
(declare-fun main1 (body) Bool)
(declare-fun main2 (body) Bool)
(declare-fun main3 (body) Bool)
...

Answer 1

这对你有用吗？

(declare-sort MySort 7)
(define-sort Body (Bool) (MySort Bool Bool Bool Bool Bool Bool Bool))

(declare-fun main0 (Body (Bool)) Bool)
(declare-fun main1 (Body (Bool)) Bool)
(declare-fun main2 (Body (Bool)) Bool)
(declare-fun main3 (Body (Bool)) Bool)

如果你的所有参数都是 Bool，你可以考虑使用位向量:

(declare-fun main0 (_ BitVec 7) Bool)
(declare-fun main1 (_ BitVec 7) Bool)
(declare-fun main2 (_ BitVec 7) Bool)
(declare-fun main3 (_ BitVec 7) Bool)