write_smt2: Check for constant bool after fully resolving signal

[georgerennie]

Fixes #3769.

The issue occured when exporting a bit that is driven through some connections by the output of a cell, but is known to be a constant. This happens with e.g. the following

module top(input wire a, output wire b);
wire [1:0] inner = |a;
assign b = inner[1];
endmodule

where b is always 0, but is driven by the $reduce_or cell.

The previous code would export the $reduce_or just for inner[0]. When exporting b, the sigmap would be unable to map b through to the constant value driving it, so would create a fresh declare-fun for it.

With this change, when exporting b we first ensure that if there is a cell driving b it has been mapped and apply the sigmap. This allows the subsequent code to see that b is constant, and thus emit true/false directly, instead of doing declare-fun.