CODEWITHSUNDEEP
z3smt
Artem Yu
Artem Yu

Reputation: 4552

Can I use z3 just to "simplify" an smt2-file

I'd like to use some of z3 tactics to modify an expression in an ".smt2" file. I'm doing it so that other SMT-solvers (cvc, mathsat etc) can benefit from z3 tactics, even though they don't support them.

Here's an example of how it can be done through z3's Python API:

def simplify_smt2_file(file_path: str) -> str:
    tactics = ("simplify", "solve-eqs", "propagate-values", "simplify")
    query = z3.parse_smt2_file(file_path)
    goal = z3.Goal()
    goal.add(query)
    simplified = z3.Then(*tactics)(goal).as_expr()
    solver = z3.SolverFor("NIA")
    solver.add(simplified)
    return solver.sexpr()

However, I need to not use Python. Is there a way to do it through z3's SMT2 interface?

Upvotes: 0

Views: 355

Answers (1)

alias
alias

Reputation: 30525

So far as I know, there's no easy way to do this using the SMTLib interface. If you're bound to using SMTLib, then you'll have to literally run z3, parse the output, and feed it back to the other solvers.

Feel free to also ask at https://groups.google.com/g/smt-lib, which is subscribed to by folks in the SMTLib community.

Upvotes: 1

Related Questions