私はZ3 C++ APIを使用して、いくつかのブール型変数（b0、...、bnを真と呼ぶ）に関して最小限の充足可能な式を見つけました。 私はブール変数b0、...、bnを含む数式を持っています。そして、私はb0、...、bnの最小数が真であるいくつかの充足可能な数式を探したいと思います。 これは、真に割り当てられ、私の式を満たすことができるb0、...、bnのサブセットを最初に見つけることによって
この質問それはZ3ソルバーツールで使用するためのもの、それはC++ APIですされていることをご検討くださいを読む前に（それは通常のC++構文ではありませんので、すべてが再定義される） は は、誰かが説明することができますブール論理を整数とどのように混在させるのですか？ 例： y = (x > 10 and x < 100) //y hsould be true or false (boolean