Z3 최대화 API : 가능한 버그?

Question

현재 최대화 API 인 Z3 (선택 지점)을 사용하고 있는데 다음과 같은 버그가 발생했습니다 :

무제한적인 문제가 생길 때마다 OPT를 반환하고 결과 모델 (예 : 모델에 제약없이 Real ('x') 최대화).

파이썬 예 :

from z3 import * 

context = main_ctx() 
x = Real('x') 
optimize_context = Z3_mk_optimize(context.ctx) 
Z3_optimize_assert(context.ctx, optimize_context, (x >= 0).ast) 

Z3_optimize_maximize(context.ctx, optimize_context, x.ast) 
out = Z3_optimize_check(context.ctx, optimize_context) 
print out 

그리고 그것은 -1을해야처럼 보이는 동안 나는 out의 값이 1 (OPT)를 할 수.

Answer 1

이 실험군을 사용해 주셔서 감사합니다. 요즘에는 개발이 여전히 상당히 어려워지고 있지만 대부분의 기능은 비교적 안정적이며 사용자가 직접 사용해 볼 수 있습니다.

질문에 답변하십시오. Z3의 최적화 기능을 사용하는 고유 한 방법이 있습니다. 이 예를 의역, 여기에 관련된 것입니다 :

sat 
oo 
[x = 0] 

첫 번째 줄은 주장이 만족할 수 있다고 말한다 :

from z3 import * 

x = Real('x') 
opt = Optimize() 
opt.add(x >= 0) 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

를 실행하면 다음과 같은 출력을 볼 수 있습니다. 두 번째 줄은 satisfiabilty 호출에서 핸들 "h"의 값을 인쇄합니다.

핸들 값에는 opt.maximize/opt.minimize를 호출하여 선언 된 최대화/최소화 기준을 충족하는 표현식이 들어 있습니다. 이 경우 표현식은 "oo"입니다. 그것은 다소 "해킹"입니다. 왜냐하면 "oo"는 무한대를 의미한다고 생각하기에 당신에게 달려 있기 때문입니다. 이 값을 Z3으로 해석하면 무한대가되지 않습니다. (비표준 숫자를 노출시키지 않는 Z3의 사용을 제한합니다. 비표준 숫자를 포함하는 Z3의 또 다른 부분이 있지만 그것은 다른 이야기입니다.)

opt.maximize 호출은 나중에 "최적의 값"을 쿼리하는 데 사용되는 핸들 "h"를 반환합니다. 마지막 줄은 제약 조건을 충족시키는 일부 모델입니다. 목적이 바운드 될 때, 모델은 당신이 기대하는 것일 것이지만,이 경우 목적은 제한되지 않습니다. 한정된 최상의 가치가 없습니다. 대신 예를 들어

시도 :

x = Real('x') 
opt = Optimize() 
opt.add(x >= 0) 
opt.add(x <= 10) 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

당신은 X = 10을 설정하는 모델을 얻고,이 또한 최대 값이 시간.

또한 시도 할 수 :

x = Real('x') 
opt = Optimize() 
opt.add(x >= 0) 
opt.add(x < 10) 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

출력은 지금 :

sat 
10 + -1*epsilon 
[x = 9] 

엡실론은 비표준 번호 (미소)을 의미합니다. 임의로 작게 설정할 수 있습니다. 다시 표준 모델 만 사용하므로 모델 번호가 선택됩니다.