'dann' vs 'und-dann' Z3 Kombinator

Question

In Z3 and-then und then und beide gültigen Kombinatoren. Was ist der Unterschied, wenn überhaupt? and-then gibt die folgende Meldung aus (help-tactic):

- (and-then <tactic>+) executes the given tactics sequencially. 

jedoch then nicht überall definiert zu sein scheint.

Answer 1

Es gibt keinen Unterschied. Wenn wir für "then" oder "and-then" in der Z3 Quellbaum grep, dann finden wir, dass diese Strings nur einmal vorkommen, und sie sind Synonyme:

grep -rE '"and-then"|"then"' 
src/cmd_context/tactic_cmds.cpp:  if (cmd_name == "and-then" || cmd_name == "then")