인쇄 불가능 Solver.model()

다음 프로그램 (89c1785b 커밋) 마스터 자식 지점에서 Z3의 최신 버전을 사용하여 인쇄 할 수없는 Z3 모델 (즉이 print solver.model() 예외를 throw) 생성인쇄 불가능 Solver.model()

x = Int('x') 
a = Array('a', IntSort(), BoolSort()) 
b = Array('b', IntSort(), BoolSort()) 
c = Array('c', BoolSort(), BoolSort()) 

e = ForAll(x, Or(Not(a[x]), c[b[x]])) 
print e 

solver = Solver() 
solver.add(e) 
c = solver.check() 
print c 
if c == sat: 
    print solver.model()

는 생산 : 나는 또한 http://rise4fun.com/Z3Py/lfQG에서 온라인 z3py 인터페이스에 동일한 동작을 재현 할 수

ForAll(x, Or(Not(a[x]), c[b[x]])) 
sat 
Traceback (most recent call last): 
    File "z3bug.py", line 16, in <module> 
    print solver.model() 
    File "src/api/python/z3.py", line 5177, in __repr__ 
    File "src/api/python/z3printer.py", line 939, in obj_to_string 
    File "src/api/python/z3printer.py", line 841, in __call__ 
    File "src/api/python/z3printer.py", line 831, in main 
    File "src/api/python/z3printer.py", line 760, in pp_model 
    File "src/api/python/z3printer.py", line 794, in pp_func_interp 
    File "src/api/python/z3.py", line 5088, in else_value 
    File "src/api/python/z3.py", line 818, in _to_expr_ref 
    File "src/api/python/z3core.py", line 2307, in Z3_get_ast_kind 
z3types.Z3Exception: 'invalid argument'

. 약간 더 많은 디버깅을하면 else_value()을 호출 할 때 c에 대한 모델의 할당이 z3.FuncInterp이고 '잘못된 인수'예외가 발생합니다.

Z3의 버그입니까? 내 기대치가 맞지 않습니까? 내 기대는 else_value()이 FuncInterp 인 경우 항상 가능해야한다는 것이 었습니다. 그렇지 않으면 완전한 기능이 아니기 때문에 항상 올바른 것은 아닙니다.

출처

2012-12-17 user1861926

이것은 Z3 Python 프린터의 버그입니다. 나는 버그를 고쳤으며, 수정은 이미 codeplex에서 가능하다.

http://z3.codeplex.com/SourceControl/changeset/f8014f54c18a

수정 프로그램을 (지금) 얻으려면, 우리는 "작업 진행"( unstable) 지점을 검색 할 수 있습니다. 이 수정본은 다음 공식 릴리스의 master 지점에서 사용할 수 있습니다. unstable 지점을 검색하려면, 우리는 사용한다 :

git clone https://git01.codeplex.com/z3 -b unstable

또 다른 옵션은 print solver.model().sexpr()을 사용하는 것입니다. 파이썬 기반 프린터 대신 Z3 내부 프린터를 사용할 것입니다.

else_value()에 대해서는 그 값을 Z3으로 지정할 수 없습니다. 의미 : 그것은 "상관 없어"입니다. 즉, 수식을 만족시키기 위해 모든 해석을 사용할 수 있습니다. 또한 else_value을 지정하지 않은 경우 Z3 Python API를 None으로 반환하도록 수정했습니다.

출처

2012-12-17 23:23:27

인쇄 불가능 Solver.model()

답변

관련 문제