有人可以给我提供一些示例，这些示例可以使用SMT求解器（如microsoft z3）解决，但不能由约束求解器（如Gecode）解决？约束求解器和SMT求解器之间的基本区别是什么？
一般来说，SMT求解器可以处理许多有趣的理论：整数，实数，字符串，序列，集合，未解释的函数，数据类型，递归定义，线性和非线性算术...
您可以查看http://smtlib.cs.uiowa.edu/logics.shtml，以查看受支持的常见逻辑。 SMT求解器的亮点在于如何在一个通用框架中自由混合和匹配来自这些域的约束。
我对Gecode并不十分熟悉，但是我认为它更加集中，只关注一类约束。当然，这将使其对于打算使用的域非常强大，但也意味着它们不具备SMT求解器提供的通用性。
[如果您尝试“挑选”一个，我建议视情况而定：对于每个问题，您可能会发现获胜者可能是SMT求解器或其他不基于SMT的约束求解器-技术。我怀疑您是否可以“唯一”选择一个可能会遇到的问题。如果您发布您感兴趣的特定问题，则可以获得更好的建议。