Merge pull request #92 from hdavid16/proposition_single_variable

Disallow logical propositions with only 1 logical variable

Author: hdavid16

src/constraints.jl

@@ -493,14 +493,23 @@ end
 
 # Check that logical expression is valid
 function _check_logical_expression(ex)
+    _check_logical_expression_literal(ex)
+    _check_logical_expression_operator(ex)
+end
+function _check_logical_expression_literal(ex::_LogicalExpr)
+    if _isa_literal(ex)
+        error("Cannot define constraint on single logical variable, use `fix` instead.")
+    end
+end
+function _check_logical_expression_operator(ex)
     return
 end
-function _check_logical_expression(ex::_LogicalExpr)
+function _check_logical_expression_operator(ex::_LogicalExpr)
     if !(ex.head in _LogicalOperatorHeads)
         error("Unrecognized logical operator `$(ex.head)`.")
     end
     for a in ex.args
-        _check_logical_expression(a)
+        _check_logical_expression_operator(a)
     end
     return
 end

test/constraints/proposition.jl

@@ -9,6 +9,8 @@ function test_proposition_add_fail()
     m = GDPModel()
     @variable(m, y[1:3], Logical)
     @test_throws ErrorException @constraint(m, y[1] := true)
+    @test_throws ErrorException @constraint(m, ¬y[1] := true)
+    @test_throws ErrorException @constraint(m, logical_not(y[1]) := true)
     @test_throws ErrorException @constraint(Model(), logical_or(y...) := true)
     @test_throws ErrorException @constraint(m, logical_or(y...) == 2)
     @test_throws ErrorException @constraint(m, logical_or(y...) <= 1)
@@ -22,33 +24,6 @@ function test_proposition_add_fail()
     @test_throws AssertionError add_constraint(m, ScalarConstraint(logical_or(y...), MOI.LessThan(42)))
 end
 
-function test_negation_add_success()
-    model = GDPModel()
-    @variable(model, y, Logical)
-    c1 = @constraint(model, logical_not(y) := true)
-    @constraint(model, c2, ¬y := true)
-    @test is_valid(model, c1)
-    @test is_valid(model, c2)
-    @test owner_model(c1) == model
-    @test owner_model(c2) == model
-    @test name(c1) == ""
-    @test name(c2) == "c2"
-    @test index(c1) == LogicalConstraintIndex(1)
-    @test index(c2) == LogicalConstraintIndex(2)
-    @test haskey(DP._logical_constraints(model), index(c1))
-    @test haskey(DP._logical_constraints(model), index(c2))
-    @test DP._logical_constraints(model)[index(c1)] == DP._constraint_data(c1)
-    @test constraint_object(c1).func isa DP._LogicalExpr
-    @test constraint_object(c2).func isa DP._LogicalExpr
-    @test constraint_object(c1).func.head == 
-            constraint_object(c2).func.head == :!
-    @test constraint_object(c1).func.args ==
-            constraint_object(c2).func.args == Any[y]
-    @test constraint_object(c1).set == 
-            constraint_object(c2).set == MOI.EqualTo{Bool}(true)
-    @test c1 == copy(c1)
-end
-
 function test_implication_add_success()
     model = GDPModel()
     @variable(model, y[1:2], Logical)
@@ -168,18 +143,6 @@ function test_proposition_delete()
     @test !DP._ready_to_optimize(model)
 end
 
-function test_negation_reformulation()
-    model = GDPModel()
-    @variable(model, y, Logical)
-    @constraint(model, ¬y := true) 
-    reformulate_model(model, DummyReformulation())
-    ref_con = DP._reformulation_constraints(model)[1]
-    @test is_valid(model, ref_con)
-    ref_con_obj = constraint_object(ref_con)
-    @test ref_con_obj.set == MOI.GreaterThan(0.0)
-    @test ref_con_obj.func == -DP._indicator_to_binary(model)[y]
-end
-
 function test_implication_reformulation()
     model = GDPModel()
     @variable(model, y[1:2], Logical)
@@ -222,17 +185,18 @@ end
 function test_intersection_reformulation()
     model = GDPModel()
     @variable(model, y[1:2], Logical)
-    @constraint(model, ∧(y[1], y[2]) := true)
+    @constraint(model, y[1] ∧ ¬y[2] := true)
     reformulate_model(model, DummyReformulation())
     ref_cons = DP._reformulation_constraints(model)
     @test all(is_valid.(model, ref_cons))
     ref_con_objs = constraint_object.(ref_cons)
-    @test ref_con_objs[1].set == 
-            ref_con_objs[2].set == MOI.GreaterThan(1.0)
+    sets = [ref_con_objs[1].set, ref_con_objs[2].set]
+    @test MOI.GreaterThan(1.0) in sets
+    @test MOI.GreaterThan(0.0) in sets
     bvars = DP._indicator_to_binary(model)
     funcs = [ref_con_objs[1].func, ref_con_objs[2].func]
     @test 1bvars[y[1]] in funcs
-    @test 1bvars[y[2]] in funcs
+    @test -1bvars[y[2]] in funcs
 end
 
 function test_implication_reformulation()
@@ -530,7 +494,6 @@ end
     end
     @testset "Add Proposition" begin
         test_proposition_add_fail()
-        test_negation_add_success()
         test_implication_add_success()
         test_equivalence_add_success()
         test_intersection_and_flatten_add_success()
@@ -540,7 +503,6 @@ end
         test_proposition_add_sparse_axis()
     end
     @testset "Reformulate Proposition" begin
-        test_negation_reformulation()
         test_implication_reformulation()
         test_implication_reformulation_fail()
         test_equivalence_reformulation()