对于Z3,我没有在文档中看到这样的列表,但是如果你真的想知道的话,你可以在源代码中找到它.该列表从check_logic.cpp的第65行开始.我使用一个可怕的awk单行解析了你的清单,并在2016年5月20日(Z3 4.4.1和4.4.2之间)发现了这个:
"AUFLIA", "AUFLIRA", "AUFNIRA", "LRA", "QF_ABV", "QF_AUFBV", "QF_UFBV", "QF_AUFLIA", "QF_AX", "QF_BV", "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", "QF_NIA", "QF_NRA", "QF_UF", "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", "QF_UFNRA", "UFLRA", "UFNIA", "UFBV", "QF_S"
您可以将其与SMT-LIB 2逻辑的官方列表进行比较.
对您来说可能更重要的是您的应用程序的"最佳逻辑".听起来你有一大堆不同的问题,你希望Z3能够应用任何策略.在这种情况下,目前,最好不要指定逻辑.问题是在SMT-LIB v2.0中没有包罗万象的逻辑 - 某些标准的最大逻辑是AUFNIRA,但这不包括例如位向量.因此,CVC4引入了非标准的ALL_SUPPORTED逻辑,当没有指定逻辑时,Z3对某些类问题表现最佳.SMT-LIB 2.0标准的这一缺点在SMT-LIB 2.5中得到解决,其新的逻辑称为"ALL".但是,Z3或CVC4尚不支持此功能.