Collecting parse_smt2_string invocations (AstVectors) in Python API

[jparsert]

What I want to do is parse a SMT-LIB file and change some assertions and then use an z3 to solve this new problem with the changed assertions.
My Idea was to essentially parse every line/command in the SMT file, and if it does not need changing use parse_smt2_string (in python API) to add it to the problem. So something similar to the following:

s = Solver()     
x = parse_smt2_string("(declare-var x Int)")
s.add(x)
assertion: AstVector = parse_smt2_string('(assert (>= (* 2 x) 4))', decls={"x": x})
s.add(assertion)
print(s.check())
print(s.model())

However this leads to an error that z3 expects a declaration or constant.
On the other hand the following works:

s = Solver()

st: AstVector = parse_smt2_string("(declare-var x Int) (assert (>= (* 2 x) 4))")
s.add(st)

print(s.check())
print(s.model())

Now, obviously I could do the whole thing by string manipulation. That is, first parsing the SMT file, changing the assertions I want to change and pretty-printing everything into a string (using formatstrings and concatenation) again and using parse_smt2_string to parse the final string (like in the second code fragment, but longer). But I was wondering if there is a more elegant way of doing this.

[NikolajBjorner]

The help(parse_smt2_string) should give an idea of how to use it.

for your example, the following works:

from z3 import *
s = Solver()

# Either this
x = Function('x', IntSort())
# or this works from python
x = Int('x')

assertion: AstVector = parse_smt2_string('(assert (>= (* 2 x) 4))', decls={"x": x})
s.add(assertion)
print(s.check())
print(s.model())

Also, declare-var is really not SMTLIB2 standard. It is included to support parsing Horn clauses without having to quantify variables all the time they are use in a rule.