Give a bit order a type, make the SMT interface usable, and let the call policy reach a property

[julianspeith]

Four commits, in the order they were made, because each one made the next possible.

The plugin had no tests

bc395af447d adds five that describe what the bit-order propagation does today, before anything changed, so that an interface rewrite touching every entry point and the 1677 lines behind them could be shown not to alter the behaviour.

Three of the five assert something other than what was expected, which is the reason for writing them first:

• enforce_continuous_bitorders=false does not preserve gaps. Given {0,1,2,4} the destination comes out {0,1,2,3}. The flag decides what may be given, not what is produced.
• With enforce_continuous_bitorders=true and the same input, the destination is simply absent from the result, and no error is reported.
• A module pin group created with the C++ defaults is indexed 0, -1, -2, -3, because the default is to descend from the start index, and move_pin then refuses every positive index, so reordering such a group fails. The Python binding defaults differ and produce 3, 2, 1, 0 for the same call.

The SMT interface was unusable from Python

52e2d32c592, four defects that belong together:

• SymbolicExecution::evaluate raised a TypeError on every call: both overloads were bound directly, so they returned a Result, which is not a registered type. Every other binding in that file unwraps it.
• SymbolicState::set used emplace, which leaves an existing binding alone, so setting a variable a second time did nothing and a loop stepping a state forward silently kept the value it started with.
• SolverCall was never bound, so QueryConfig::with_call and Solver::has_local_solver_for could not be called although both were bound; SolverType was missing Bitwuzla; Solver::to_smt2 was not exposed at all.
• Solver::has_local_solver_for tested SolverCall::Binary in both of its branches, so the one for Library was unreachable and library availability always reported false. Note this last one cannot be observed in a build that links no solver library, as CI does not — the corrected branch returns false there just as falling through did.

The call policy was inert on every property

9c98546fc20. Fifty-five properties were given the hal::borrowed() policy introduced in #639 and none of them had it: def_property_readonly builds the cpp_function from the getter there and then, and only afterwards forwards the attributes passed alongside, so an attribute meant for the call never reaches the function that makes it. It compiles and reads as though it works.

The effect was that reading gate.module, gate.fan_out_nets or netlist.gates handed over an object without keeping its netlist alive, while calling gate.get_module() did — the very defect the policy was introduced to fix, still present wherever a binding is a property rather than a method. Measured on a netlist of 3458 gates:

	before	after
gate.module	3 → 3	3 → 4
gate.fan_out_nets	3 → 3	3 → 4
netlist.gates	3 → 3	3 → 3461
gate.get_module()	3 → 4	3 → 4

A bit order now has a type

28865d54979. The interface spoke in std::map<std::pair<Module*, PinGroup<ModulePin>*>, std::map<Net*, u32>>, which says four things at once and none of them by name, and appeared twenty-one times across the plugin.

It is now a BitOrder — one pin group and the index of each of its nets — and a BitOrderResult, which is what a propagation reports. The index is kept with each net rather than implied by position, so an order with gaps can be expressed: propagation produces a continuous order today, but that is a property of the algorithm rather than of the interface.

Two things follow from a result being an object rather than a container. Python can be handed one and keep the netlist it refers to alive, which a list cannot do. And a result holds its bit orders by module and pin group ID, so walking one no longer depends on where the modules and pin groups were allocated.

The algorithm is untouched. The new types are translated to the map at the entry points and back at the exits rather than the sixteen hundred lines behind them being rewritten, and the tests written beforehand pass unchanged, which is what says the behaviour is the same.

export_bitorder_propagation_information keeps returning one number per pin group, but that number is the index of the word it became in the exported file and not the index of a bit, so it is a WordIndex now.

Verified

ctest 38/38, the ten-hazard lifetime suite holds, and the 500-gate/500-net use-after-free test reports 0 wrong names and 0 wrong IDs. The wiki page for the plugin is updated in the same pass, including two descriptions that were already wrong: enforce_continuous_bitorders was documented backwards, and export_bitorder_propagation_information was described as a debugging dump rather than as an export for an external solver.