如何在形式为x=y^2的Z3中添加断言

Question

我需要添加以下断言

断言（x=y^2）

是需要定义一个函数，还是可以使用任何语法直接添加它。请帮帮我。

Answer 1

Z3有一个内置的功率运算符^。如果您使用的是SMT-LIB接口，它将是(assert (= x (^ y 2)))。不过，如果功率始终为2，那么使用(assert (= x (* y y)))可能会更好。