Description:
In the new definition of CircuitSAT, initialization includes an extra objective type parameter OBJ, controlled by the keyword argument use_constraints::Bool:
• use_constraints = false → OBJ = EXTREMA
• use_constraints = true → OBJ = SAT
However, in the current implementation of
function reduceto(::Type{<:CircuitSAT}, f::Factoring)
...
sat = CircuitSAT(Circuit(exprs))
...
end
the call to CircuitSAT does not propagate use_constraints. This means all instances created via reduceto are forced into the default EXTREMA mode, and users cannot request the SAT mode.
Position
|
sat = CircuitSAT(Circuit(exprs)) |
Expected behavior:
reduceto should accept and forward a use_constraints keyword argument, e.g.
function reduceto(::Type{<:CircuitSAT}, f::Factoring; use_constraints::Bool=false)
...
sat = CircuitSAT(Circuit(exprs); use_constraints)
...
end