Z3 (API) 中求解器的设置逻辑 [英] Setting logic for solver in Z3 (API)

问题描述

我注意到 Z3 C++(和 C)API 允许您提供逻辑用过.

I notice that the Z3 C++ (and C) API allows you to supply the logic to be used.

我有两个关于此的问题，我无法通过在线查找来回答:

I have two questions about this that I couldn't answer by looking online:

1. 这些是否应该是标准的SMT-LIB 逻辑，即QF_LRA
2. 这些信息什么时候值得提供，即 Z3 什么时候会真正使用这些信息

我的背景主要是 QF 无 BV，但其他一切皆有可能，我正在逐步使用 SMT 求解器，并且我总是可以计算出我将在开始时采用的逻辑.

My context is mainly QF no BV but everything else possible, I am using the SMT solver incrementally and I can always work out what logic I will be in at the start.

推荐答案

Z3 也将尝试找出逻辑是什么(当使用默认选项运行时)，但它没有针对所有理论组合的自定义策略(请参阅 default_tactic.cpp 和 smt_strategic_solver.cpp).当您不确定 Z3 将决定做什么时，最好预先设置策略，这样如果您尝试使用不在该逻辑中的内容，就会出错.它还将使用该信息来设置 smt 内核，例如启用各种预处理器、各种求解器功能和选择启发式算法(参见例如 smt_setup.cpp).

Z3 will also try to figure out what the logic is (when run with default options), but it doesn't have custom tactics for all combinations of theories (see default_tactic.cpp and smt_strategic_solver.cpp). When you are not sure what Z3 will decide to do, then it's best to set the tactic right up front, so that you will get errors if you try to use things that are not in that logic. It will also use that information to set up the smt kernel, e.g., enabling various preprocessors, various solver features, and chosing heuristics (see e.g., smt_setup.cpp).

这篇关于Z3 (API) 中求解器的设置逻辑的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！