z3py : (check-sat ...) 구문의 가정

Question

SMT2 수식의 (check-sat ...) 문에서 솔버로 가정을 전달할 수있는 방법이 있습니까? 예상대로, unsat 범에

# cat ex.smt2 
(declare-fun p() Bool) 
(assert (not p)) 
(check-sat p) 

Z3 러닝

는 ex.smt2에 저장된 다음 예 수식을 고려한다. 지금, 나는 z3py 인터페이스를 통해 가정 (P)으로 해결하고 싶습니다 : 파서에서 (이 예에서는 즉 (P)) 가정을 얻을 수있는 API가

In [30]: ctx = z3.Context() 
In [31]: s = z3.Solver(ctx=ctx) 
In [32]: f = z3.parse_smt2_file("ex.smt2", ctx=ctx) 
In [33]: s.add(f) 
In [34]: s.check() 
Out[34]: sat 

있습니까? 또는 더 나은 점은, 해석자에게 입력 파일에서 읽은 가정을 풀라고 말하면됩니까?

Answer 1

아니요, 해당 API가 없습니다. parse_smt2_file API는 매우 간단하며 입력 파일의 어설 션에 대한 액세스 만 제공합니다. 이 API를 확장하는 것은 TODO 목록에 있지만 현재 아무도 그것에 대해 작업하지 않습니다.