How to reference sorts and functions imported from an SMT2 file/string in the C++ API?

[tschuchortdev]

I have a file generated by a third-party program that contains sort definitions and function definitions but no assertions:

; SMT-LIBv2 description generated by Yosys 0.33 (git sha1 2584903a060)
; yosys-smt2-stbv
; yosys-smt2-module counter
(define-sort |counter_s| () (_ BitVec 7))
(define-fun |counter_is| ((state |counter_s|)) Bool (= ((_ extract 0 0) state) #b1))
(define-fun |counter#0| ((state |counter_s|)) Bool (= ((_ extract 1 1) state) #b1)) ; \clk
; yosys-smt2-input clk 1
; yosys-smt2-clock clk posedge
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "posedge", "width": 1}
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |counter_n clk| ((state |counter_s|)) Bool (|counter#0| state))
; yosys-smt2-witness {"offset": 0, "path": ["\\count"], "smtname": 1, "smtoffset": 0, "type": "reg", "width": 4}
(define-fun |counter#1| ((state |counter_s|)) (_ BitVec 4) ((_ extract 5 2) state)) ; \count
; yosys-smt2-output count 4
; yosys-smt2-register count 4
(define-fun |counter_n count| ((state |counter_s|)) (_ BitVec 4) (|counter#1| state))
(define-fun |counter#2| ((state |counter_s|)) Bool (= ((_ extract 6 6) state) #b1)) ; \en
; yosys-smt2-input en 1
; yosys-smt2-witness {"offset": 0, "path": ["\\en"], "smtname": "en", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |counter_n en| ((state |counter_s|)) Bool (|counter#2| state))
(define-fun |counter#3| ((state |counter_s|)) Bool (distinct (|counter#1| state) #b1111)) ; $ne$counter.v:8$1_Y
; yosys-smt2-assert 0 $assert$counter.v:6$2 counter.v:6.20-8.36
(define-fun |counter_a 0| ((state |counter_s|)) Bool (or (|counter#3| state) (not true))) ; $assert$counter.v:6$2
(define-fun |counter#4| ((state |counter_s|)) (_ BitVec 4) (bvadd (|counter#1| state) #b0001)) ; $add$counter.v:12$4_Y
(define-fun |counter#5| ((state |counter_s|)) (_ BitVec 4) (ite (|counter#2| state) (|counter#4| state) (|counter#1| state))) ; $auto$rtlil.cc:2498:Mux$11
(define-fun |counter_a| ((state |counter_s|)) Bool 
  (|counter_a 0| state)
)
(define-fun |counter_u| ((state |counter_s|)) Bool true)
(define-fun |counter_i| ((state |counter_s|)) Bool 
  (= (|counter#1| state) #b1110) ; count
)
(define-fun |counter_h| ((state |counter_s|)) Bool true)
(define-fun |counter_t| ((state |counter_s|) (next_state |counter_s|)) Bool 
  (= (|counter#5| state) (|counter#1| next_state)) ; $auto$ff.cc:266:slice$9 \count
) ; end of module counter
; yosys-smt2-topmod counter
; end of yosys output

How can I import this into the Z3 C++ API and then reference the imported definitions?

I'm importing the file as follows:

auto smt_file = std::ifstream(boost::filesystem::path{"counter.smt2"});
std::stringstream smt_file_buffer{};
smt_file_buffer << smt_file.rdbuf();
auto smt_file_str = smt_file_buffer.str();

z3::context ctx;
z3::solver solver(ctx);
solver.from_string(smt_file_str.c_str());
spdlog::info("{}", solver.to_smt2());

The call to solver.to_smt2() however, is only printing an empty file:

;
(set-info :status unknown)
(check-sat)

I assume that z3::solver is simply optimizing away all the definitions, since they are never referenced in an assertion... not great for debugging.

In z3::ctx I can not find any methods that would allow me to reference declarations without defining them myself. If I create uninterpreted definitions with the same name, they just seem to overwrite everything that was imported from the file:

solver.from_string(smt_file_str.c_str());
auto state_sort = ctx.uninterpreted_sort("|counter_s|");
auto current_state = ctx.constant("current", state_sort);
auto next_state = ctx.constant("next", state_sort);
auto do_asserts_hold = ctx.function("|counter_a|", state_sort, ctx.bool_sort());
auto is_initial_state = ctx.function("|counter_i|", state_sort, ctx.bool_sort());
auto v = z3::sort_vector(ctx);
v.push_back(state_sort);
v.push_back(state_sort);
auto transition_exists = ctx.function("|counter_t|", v, ctx.bool_sort());

solver.add(is_initial_state(current_state));
solver.add(do_asserts_hold(current_state));
solver.add(transition_exists(current_state, next_state));
solver.add(!do_asserts_hold(next_state));

spdlog::info("{}", solver.to_smt2());

prints

(set-info :status unknown)
(declare-sort |counter_s| 0)
(declare-fun |counter_i| (|counter_s|) Bool)
(declare-fun current () |counter_s|)
(declare-fun |counter_a| (|counter_s|) Bool)
(declare-fun |counter_t| (|counter_s| |counter_s|) Bool)
(declare-fun next () |counter_s|)
(assert
(|counter_i| current))
(assert
(|counter_a| current))
(assert
(|counter_t| current next))
(assert
(let (($x53 (|counter_a| next)))
(not $x53)))
(check-sat)

Before anyone asks: I can not redefine the sorts and functions in C++, since the whole point of the exercise is that I don't know in advance what they will be.