z3 - SMT を使用して用語を簡略化する

Question

Z3を使用して、条件が満たされるかどうかを確認しています。しかし、さらに、人間が消費する用語を単純化する必要があります。たとえば、n が Int の場合、And(n>4 , n != 5) を n > 5 に単純化します。Z3 または他のツールを使用してこれを行う方法を知っている人はいますか?

Answer 1

おそらくすでに気づいていると思いますが、Z3 には API を介して公開された単純化機能があり、SMT-LIB からも使用できます。rise4fun.com/z3 および rise4fun.com/z3py の Z3 に関するチュートリアルでは、簡略化の例がいくつか示されています。ただし、簡約器は通常の形式の変換を試みないため、希望するスタイルの結果が得られる可能性は低いです。特に、論理積 And(n > 4, n != 5) を n > 5 に単純化しません。