過於簡單，題目懶得放了。
不過，藉此機會我終於搞明白怎麼把使用z3的輸出了（過菜，勿噴）
先看一看這個：
我們可以看出，z3宣告的變數是arithref型別；
它好像沒有什麼好用的型別轉化方法，python也很難將其作為變數繼續呼叫。
solve的結果是直接輸出的，其沒有返回值，使用solve獲得的結果也不能繼續在程式裡直接使用。
所以，我們需要使用solver以及modelref類。
solver是乙個求解器；建立它以後，可以用.add方法逐步新增約束；
.check方法驗證是否有解；如果有解，解就可以使用.model獲得，其形式和solve直接輸出的東西是一樣的。
.model是modelref類，其擁有許多方法（as_***）將其中的解提取出來，轉化為其他型別。
回到本題：
信安數基學習筆記（1）
密碼學中經常需要使用到數論知識 再加上不少學長說信安數基這門課很難 因此我決定在假期先學學信安數基 我使用的是清華大學出版社的版本 第一章 整數的可除性 整除 a,b為任意整數，若存在整數q使得a qb，則稱b整除a，稱a為b的倍數，b為a的因數 素數 對除0與 1以外的整數，若它除了 1與 n以外...