Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add := operator for Boolean satisfiability problems #3530

Merged
merged 8 commits into from
Oct 15, 2023
Merged

Add := operator for Boolean satisfiability problems #3530

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
06b0d60
Add := operator for Boolean satisfiability problems
odow Sep 28, 2023
892bc1f
Update
odow Sep 28, 2023
ad43e49
Apply suggestions from code review
odow Sep 28, 2023
0bc09cf
Replace with dispatch
odow Oct 11, 2023
4199024
Refactor
odow Oct 12, 2023
9a93f0e
Restrict rhs to Bool
odow Oct 12, 2023
0f48516
Add docs
odow Oct 12, 2023
fa07a0f
Apply suggestions from code review
odow Oct 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions docs/src/developers/extensions.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,20 +200,20 @@ julia> model = Model(); @variable(model, x);

julia> function JuMP.parse_constraint_head(
_error::Function,
::Val{:(:=)},
::Val{:≝},
odow marked this conversation as resolved.
Show resolved Hide resolved
lhs,
rhs,
)
println("Rewriting := as ==")
println("Rewriting ≝ as ==")
odow marked this conversation as resolved.
Show resolved Hide resolved
new_lhs, parse_code = MutableArithmetics.rewrite(lhs)
build_code = :(
build_constraint($(_error), $(new_lhs), MOI.EqualTo($(rhs)))
)
return false, parse_code, build_code
end

julia> @constraint(model, x + x := 1.0)
Rewriting := as ==
julia> @constraint(model, x + x ≝ 1.0)
odow marked this conversation as resolved.
Show resolved Hide resolved
Rewriting ≝ as ==
odow marked this conversation as resolved.
Show resolved Hide resolved
2 x = 1
```

Expand Down
19 changes: 19 additions & 0 deletions src/constraints.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1542,3 +1542,22 @@ function relax_with_penalty!(
) where {T}
return relax_with_penalty!(model, Dict(); default = default)
end

function parse_constraint_head(error_fn::Function, ::Val{:(:=)}, lhs, rhs)
new_lhs, parse_code_lhs = _rewrite_expression(lhs)
new_rhs, parse_code_rhs = _rewrite_expression(rhs)
parse_code = quote
$parse_code_lhs
$parse_code_rhs
end
build_code = quote
if $new_rhs isa Bool
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since we do it at the parsing level, it won't work if rhs is a Julia variable (not a JuMP decision variable) for which the value is a Bool right ?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This part is at runtime. See the tests.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah indeed. I guess it's best to add code inside the build_constraint that add code that is generated by the macro if possible

Copy link
Member

@blegat blegat Sep 29, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But in this case, it might be difficult

Copy link
Member

@blegat blegat Sep 29, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We would need a new JuMP set Equal with and do build_constraint(error, (a, b), JuMP.Equal())

ScalarConstraint($new_lhs, MOI.EqualTo($new_rhs))
elseif $new_lhs isa Bool
ScalarConstraint($new_rhs, MOI.EqualTo($new_lhs))
else
ScalarConstraint(op_equal_to($new_lhs, $new_rhs), MOI.EqualTo(true))
end
end
return false, parse_code, build_code
end
4 changes: 4 additions & 0 deletions src/macros.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1160,6 +1160,10 @@ function model_convert(model::AbstractModel, set::MOI.AbstractScalarSet)
return set
end

function model_convert(model::GenericModel{Bool}, set::MOI.EqualTo{Bool})
return set
end

function model_convert(model::AbstractModel, α::Number)
T = value_type(typeof(model))
V = variable_ref_type(model)
Expand Down
76 changes: 76 additions & 0 deletions test/test_constraint.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1721,4 +1721,80 @@ function test_triangle_vec()
return
end

function test_def_equal_to_operator()
model = GenericModel{Bool}()
@variable(model, x[1:3])
# x[1] := x[2]
c = @constraint(model, x[1] := x[2])
o = constraint_object(c)
@test isequal_canonical(o.func, op_equal_to(x[1], x[2]))
@test o.set == MOI.EqualTo(true)
# x[1] == x[2] := false
c = @constraint(model, x[1] == x[2] := false)
o = constraint_object(c)
@test isequal_canonical(o.func, op_equal_to(x[1], x[2]))
@test o.set == MOI.EqualTo(false)
# x[1] && x[2] := false
c = @constraint(model, x[1] && x[2] := false)
o = constraint_object(c)
@test isequal_canonical(o.func, op_and(x[1], x[2]))
@test o.set == MOI.EqualTo(false)
# x[1] && x[2] := true
c = @constraint(model, x[1] && x[2] := true)
o = constraint_object(c)
@test isequal_canonical(o.func, op_and(x[1], x[2]))
@test o.set == MOI.EqualTo(true)
# x[1] || x[2] := y
y = true
c = @constraint(model, x[1] || x[2] := y)
odow marked this conversation as resolved.
Show resolved Hide resolved
o = constraint_object(c)
@test isequal_canonical(o.func, op_or(x[1], x[2]))
@test o.set == MOI.EqualTo(y)
# y := x[1] || x[2]
y = true
c = @constraint(model, y := x[1] || x[2])
o = constraint_object(c)
@test isequal_canonical(o.func, op_or(x[1], x[2]))
@test o.set == MOI.EqualTo(y)
return
end

function test_def_equal_to_operator_float()
model = Model()
@variable(model, x[1:3])
# x[1] := x[2]
c = @constraint(model, x[1] := x[2])
o = constraint_object(c)
@test isequal_canonical(o.func, op_equal_to(x[1], x[2]))
@test o.set == MOI.EqualTo(1.0)
# x[1] == x[2] := false
c = @constraint(model, x[1] == x[2] := false)
o = constraint_object(c)
@test isequal_canonical(o.func, op_equal_to(x[1], x[2]))
@test o.set == MOI.EqualTo(0.0)
# x[1] && x[2] := false
c = @constraint(model, x[1] && x[2] := false)
o = constraint_object(c)
@test isequal_canonical(o.func, op_and(x[1], x[2]))
@test o.set == MOI.EqualTo(0.0)
# x[1] && x[2] := true
c = @constraint(model, x[1] && x[2] := true)
o = constraint_object(c)
@test isequal_canonical(o.func, op_and(x[1], x[2]))
@test o.set == MOI.EqualTo(1.0)
# x[1] || x[2] := y
y = true
c = @constraint(model, x[1] || x[2] := y)
o = constraint_object(c)
@test isequal_canonical(o.func, op_or(x[1], x[2]))
@test o.set == MOI.EqualTo(1.0)
# y := x[1] || x[2]
y = true
c = @constraint(model, y := x[1] || x[2])
o = constraint_object(c)
@test isequal_canonical(o.func, op_or(x[1], x[2]))
@test o.set == MOI.EqualTo(1.0)
return
end

end
4 changes: 2 additions & 2 deletions test/test_macros.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ end

struct CustomType end

function JuMP.parse_constraint_head(_error::Function, ::Val{:(:=)}, lhs, rhs)
function JuMP.parse_constraint_head(_error::Function, ::Val{:≝}, lhs, rhs)
odow marked this conversation as resolved.
Show resolved Hide resolved
return false, :(), :(build_constraint($_error, $(esc(lhs)), $(esc(rhs))))
end

Expand Down Expand Up @@ -326,7 +326,7 @@ function test_extension_custom_expression_test(
)
model = ModelType()
@variable(model, x)
@constraint(model, con_ref, x := CustomType())
@constraint(model, con_ref, x ≝ CustomType())
odow marked this conversation as resolved.
Show resolved Hide resolved
con = constraint_object(con_ref)
@test jump_function(con) == x
@test moi_set(con) isa CustomSet
Expand Down
Loading