混合整数演算 - Z3の証明

Question

この質問それはZ3ソルバーツールで使用するためのもの、それはC++ APIですされていることをご検討くださいを読む前に（それは通常のC++構文ではありませんので、すべてが再定義される）

は

は、誰かが説明することができますブール論理を整数とどのように混在させるのですか？ 例：

y = (x > 10 and x < 100) //y hsould be true or false (boolean) 
z = (y == true and k > 20 and k < 200) 
m = (z or w) //suppose w takes true of false (boolean) 

Iは、C++ファイルで与えられた例で試みたが、Iは、整数演算およびブールを混合する際にそれがどのように動作するかを把握することができません。

Answer 1

C++の初心者であると回答しています。

あなたはこれを探しているかもしれません。

bool y,z,m,w; 
int x, k; 
y = (x>10 && x<100); 
z = (y == true && k > 20 && k < 200); 
m = (z || w); 

この行の意味を見てみましょう： Y =（X> 10 & & X < 100）。

ここで、xが1x>10より大きい場合、結果はtrueです。同じ方法でxが100未満の場合x<100結果true。両方がtrueの場合、右側が真となり、yに割り当てられます。 ||を意味します。