z3py: assumptions from (check-sat ...) statement

Question

Is there a way to pass assumptions from (check-sat ...) statement of SMT2 formula into the solver ?

Consider the following example formula stored in ex.smt2:

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

Running z3 on it gives unsat, as expected. Now, I'd like to solve with assumptions (p) through z3py interface:

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

Is there an API to get assumptions (i.e. (p) in this example) from the parser ? Or even better, just tell the solver to solve with the assumptions read from the input file ?

Answer 1

No, there is no such API. The parse_smt2_file API is very simple, and only provides access to the assertions in the input file. Extending this API is in the TODO list, but nobody is currently working on that.