CODEWITHSUNDEEP
z3
mmpourhashem
mmpourhashem

Reputation: 91

Variable selection in Z3

Is there any way to find the mapping between variable names (or the name of intermediate variables after transformations) and their representative numbers in sat_solver.cpp (solver::next_var) or smt_case_split_queue.cpp (next_case_split(bool_var & next, lbool & phase))? I know that it is not straightforward, but can someone give me some hints please? Thank you in advance.

Upvotes: 0

Views: 76

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

Yes, that is possible, but potentially a lot of work. The formula undergoes numerous transformations before it reaches the SAT solver. Each of them has their own mapping (if they introduce/remove variables), so getting the mapping that is done last may not get you to where you want to get.

The mapping that you are looking for is most likely atom2bool_var, but those Boolean variables are (most likely) introduced in the bit-blaster, which has its own model converter that translates those back to bit-vector variables as demonstrated in bit_blaster_model_converter.cpp.

Upvotes: 1

Related Questions