I need help with extracting sort details from an SMT2 file using Z3’s C++ interface. My goal is to collect all sorts that appear in the formula but don’t have constructor definitions.
I discovered that m.get_func_decl() works well for getting sorts from argument functions when there are no constructors involved. For example, with declarations like (declare-fun MyFunction (Int Bool Int) Int), I can successfully extract the sort information.
However, I’m running into issues with define-fun statements. When I have something like (define-fun Process@execute ((value Int)) (Int) ...), the m.get_func_decl() method doesn’t seem to work. I think some internal optimization might be removing these declarations.
Is there another approach I can use to get a complete list of all sorts that are used in the SMT file when they don’t have constructors defined? Any suggestions would be really helpful.
Hit the same issue with smt2 parsers. Use z3::expr::get_sort() on each expr node when walking the AST - define-fun sorts still appear there even when the decl gets optimized out. Also try z3::context::num_sorts() and loop through with z3::context::get_sort() to catch things AST traversal misses.
Yeah, that’s exactly what’s happening with define-fun statements. Z3 treats them as macro expansions rather than regular function declarations, so they don’t show up where you’d expect.
I’d suggest traversing the AST directly with z3::expr::for_each_expr() or similar methods. You can visit every subexpression in your formula and grab sort info from bound variables, function calls, and constants that the top-level declarations miss.
You could also parse the SMT2 file yourself before passing it to Z3 - pull sort info from both declare-sort statements and actual usage. I’ve had good luck combining AST traversal with this preprocessing approach. It gives you the full picture of all sorts, especially in complex files with quantifiers and defined functions that Z3 optimizes away.
Hit this exact problem six months ago on a similar SMT analysis tool. Z3’s internal representation doesn’t always keep the original structure from your SMT2 file - especially with define-fun constructs.
I used z3::model::get_sorts() after calling check_sat() and getting a model, but that only gives you sorts that actually show up in the satisfying assignment. For something more complete, I walked through all assertions in the solver using z3::solver::assertions() and recursively examined each expression’s sort with z3::expr::get_sort().
Here’s the key: even when function declarations get optimized away, the sorts are still embedded in expressions that use them. Also try z3::context::get_sorts() - sometimes catches additional sorts the AST traversal misses, though it’s hit or miss depending on your Z3 version.