bug fix in propositional logic

Author: hdavid16

Project.toml

@@ -1,7 +1,7 @@
 name = "DisjunctiveProgramming"
 uuid = "0d27d021-0159-4c7d-b4a7-9ccb5d9366cf"
 authors = ["hdavid16 <[email protected]>"]
-version = "0.2.1"
+version = "0.3.0"
 
 [deps]
 IntervalArithmetic = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253"

src/logic.jl

@@ -1,17 +1,19 @@
+"""
+
+"""
+function select()
+    
+end
+
 """
     to_cnf!(m::Model, expr::Expr)
 
 Convert logical proposition expression into conjunctive normal form.
 """
 function to_cnf!(m::Model, expr::Expr)
-    expr_name = Symbol(expr) #get name to register reformulated logical proposition
+    expr_name = Symbol("{$expr}") #get name to register reformulated logical proposition
     replace_Symvars!(expr, m; logical_proposition = true) #replace all JuMP variables with Symbolic variables
-    check_logical_proposition(expr) #check that valid boolean symbols and variables are used in the logical proposition
-    eliminate_equivalence!(expr) #eliminate ⇔
-    eliminate_implication!(expr) #eliminmate ⇒
-    move_negations_inwards!(expr) #expand ¬
-    clause_list = distribute_and_over_or_recursively!(expr) #distribute ∧ over ∨ recursively
-    @assert !isempty(clause_list) "Conversion to CNF failed."
+    clause_list = to_cnf!(expr)
     #replace symbolic variables with JuMP variables and boolean operators with their algebraic counterparts
     for clause in clause_list
         replace_JuMPvars!(clause, m)
@@ -29,6 +31,22 @@ function to_cnf!(m::Model, expr::Expr)
     end
 end
 
+"""
+    to_cnf!(expr::Expr)
+
+Convert an expression of symbolic Boolean variables and operators to CNF.
+"""
+function to_cnf!(expr::Expr)
+    check_logical_proposition(expr) #check that valid boolean symbols and variables are used in the logical proposition
+    eliminate_equivalence!(expr) #eliminate ⇔
+    eliminate_implication!(expr) #eliminmate ⇒
+    move_negations_inwards!(expr) #expand ¬
+    clause_list = distribute_and_over_or_recursively!(expr) #distribute ∧ over ∨ recursively
+    @assert !isempty(clause_list) "Conversion to CNF failed."
+
+    return clause_list
+end
+
 """
     check_logical_proposition(expr::Expr)
 
@@ -53,11 +71,13 @@ function eliminate_equivalence!(expr)
     if expr isa Expr
         if expr.args[1] == :⇔
             @assert length(expr.args) == 3 "Double implication cannot have more than two clauses."
-            A = expr.args[2]
-            B = expr.args[3]
+            A1 = expr.args[2]
+            B1 = expr.args[3]
+            A2 = A1 isa Expr ? copy(A1) : A1
+            B2 = B1 isa Expr ? copy(B1) : B1
             expr.args[1] = :∧
-            expr.args[2] = :($A ⇒ $B)
-            expr.args[3] = :($B ⇒ $A)
+            expr.args[2] = :($A1 ⇒ $B1)
+            expr.args[3] = :($B2 ⇒ $A2)
         end
         for i in eachindex(expr.args)
             expr.args[i] = eliminate_equivalence!(expr.args[i])

src/macros.jl

@@ -135,17 +135,7 @@ Add logical proposition macro.
 macro proposition(m, expr)
     #get args
     expr = QuoteNode(expr)
-    code = :(add_proposition!($m, $expr))
-
+    code = :(DisjunctiveProgramming.to_cnf!($m, $expr))
+    
     return esc(code)
 end
-
-"""
-    add_proposition!(m::Model, expr::Expr)
-
-Add logical proposition expression to a JuMP model.
-"""
-function add_proposition!(m::Model, expr::Expr)
-    @assert m isa Model "A valid JuMP Model must be provided."
-    to_cnf!(m, expr)
-end