この単純な例では UNKNOWN が生成されます。def について理解できないことがあると思います。
from z3 import *
s = Solver()
def Min(b, r):
return If(b, r, 1)
a = Real('a')
b = Bool('b')
s.add(a==0.9)
s.add(a<=Min(b,0.9))
s.check()
print "Presenting result "
m = s.model()
print "traversing model..."
for d in m.decls():
print "%s = %s" % (d.name(), m[d])
あなたは間違いを犯していません。これは、Z3 ソルバーの 1 つの問題です。あなたの問題は、「difference-logic」と呼ばれる算術の断片にあります。算術アトムが のように書ける場合、このフラグメントの問題です。x - y <= kここkで、 は数字です。このフラグメントに問題がある場合、Z3 は専用のソルバーを使用します。unknownただし、入力問題に if-then-else 項 (If内の) も含まれている場合、このソルバーは失敗する ( を返す) 場合がありますMin。
バグは修正されており、次のリリースで利用できるようになります。それまでの間、次の回避策のいずれかを試すことができます。
ソルバーを呼び出す前に、Z3 に if-then-else 項を強制的に削除させます。s = Solver()に置き換えるだけs = Then('elim-term-ite', 'smt').solver()です。これは、rise4fun で変更されたスクリプトです。
別のロジック フラグメントにない冗長なアサーションを追加できます。例: z + w > 2. これは、rise4fun で変更されたスクリプトです。