2

My program, bounded synthesizer of reactive finite state systems, produces SMT queries to annotate a product automaton of the (uninterpreted) system and a specification. Essentially it is a model checking with uninterpreted functions. If the annotation exists => the model found by Z3 satisfies the spec. The queries contain:

  • datatype (to encode states of a system and of a specification automaton)
  • >= (greater), > (strictly) (to specify ranking function of states of automaton system*spec, which is used to search lassos with bad states)or in other words, ordering of states of that automaton, which
  • uninterpreted functions with boolean domain and range
  • all clauses are horn clauses

An example is https://dl.dropboxusercontent.com/u/444947/posts/full_arbiter2.smt2 ('forall' are used to encode "don't care" inputs to functions)

Currently queries take strictly greater > operator from integers arithmetic (that is a ranking function has Int range).

Question: is it worth developing a custom theory solver in Z3 for such queries? It could exploit DFS based search of lassos which might be faster than integers theory solver (or diff-neg tactic).

Or Z3 already efficiently handles this? (efficiently means "comparable to graph-based search of lassos").

4

1 回答 1

1

算术不是基准测试的瓶颈。我们可以通过使用

valgrind --tool=callgrind z3 full_arbiter2.smt2 
kcachegrind

Valgrind 和 kcachegrind 在大多数 Linux 发行版中都可用。所以，我认为如果你为顺序理论实施求解器，你不会获得显着的性能提升。一个瓶颈是数据类型理论。如果您使用位向量对类型 Q 和 T 进行编码，您可能会获得性能提升。另一个瓶颈是量词推理。在调用 Z3 之前，您是否尝试过扩展它们？在 Z3 中，qe（量词消除）策略本质上将扩展布尔量词。我通过更换得到了一点加速

(check-sat)

和

(check-sat-using (then qe smt))
于 2013-07-23T00:08:30.327 回答