Z3py : 144 개의 변수가있는 큰 수식을 인쇄하십시오.

Question

저는 Z3 정리 프로 버를 사용하며 큰 수식 (114 개 변수)이 있습니다. 모든 절과 함께 큰 수식을 인쇄 할 수 있습니까? 보통 print str(f)은 출력을 절단하고 모든 절이 아닌 "..."만 끝에 인쇄됩니다.

나는 print f.sexpr()을 테스트했으며 항상 모든 절을 인쇄합니다. 그러나 sexpr 구문에서만.

수식의 모든 절을 인쇄 할 수 있지만 s- 표현식 구문은 사용하지 않아도됩니까?

참고 : 코드 예제는 문제를 보여주기에는 너무 작지만 큰 수식을 게시하면 너무 많은 공간이 필요합니다.

from z3 import * 


C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B') 
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True)))) 



f = simplify(C) 

# 
# PRINTING 
# 

# for large a formula with 114 variables, the output of str(f) gets truncated 
# only "..." is displayed at the end, not all the clauses are shown 
# this is printed in the format I need: 
print str(f) 

# this always prints all the clauses, even for very large formulae 
# here all clauses are printed, but not the format I need: 
print f.sexpr() 

# if you try the above two commands with a very large formula you see the difference! 

Answer 1

Z3Py는 자체 프린터를 표현식으로 사용합니다. 파일 src/api/python/z3printer.py에 정의되어 있습니다. 이 예쁜 프린터에는 몇 가지 구성 매개 변수가 있습니다. 다음과 같은 명령을 사용하여 설정할 수 있습니다 :

set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000) 

이 출력을 방지 할 큰 표현식 절약 할 수 있습니다. 참고 : Z3Py 예쁜 프린터는 Z3 라이브러리에서 사용할 수있는 것보다 비효율적입니다. 성능이 문제가되면 Nuno Lopes에서 제안한대로 SMT2 형식 프린터를 사용해야합니다.