From 28be2b7220270ea7aba67bf0c9ad0c6eb7c3d81e Mon Sep 17 00:00:00 2001
From: Niklas Dewally <niklas@dewally.com>
Date: Fri, 11 Oct 2024 21:21:36 +0100
Subject: [PATCH] wip: implement not(x) ~> w-lit(x,0)

---
 crates/conjure_core/src/rules/minion.rs | 32 +++++++++++++++++++------
 1 file changed, 25 insertions(+), 7 deletions(-)

diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs
index 653dfd81ff..cc74026e33 100644
--- a/crates/conjure_core/src/rules/minion.rs
+++ b/crates/conjure_core/src/rules/minion.rs
@@ -2,10 +2,7 @@
 /*        Rules for translating to Minion-supported constraints         */
 /************************************************************************/
 
-
-use crate::ast::{
-    Constant as Const, DecisionVariable, Domain, Expression as Expr, SymbolTable,
-};
+use crate::ast::{Constant as Const, DecisionVariable, Domain, Expression as Expr, SymbolTable};
 use crate::metadata::Metadata;
 use crate::rule_engine::{
     register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,
@@ -397,6 +394,7 @@ fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult {
 /// ```text
 /// and([x,...]) ~> and([w-literal(x,1),..])
 ///  or([x,...]) ~>  or([w-literal(x,1),..])
+///  not(x)      ~>  w-literal(x,0)
 /// ```
 ///
 /// ## Rationale
@@ -407,8 +405,8 @@ fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult {
 ///
 #[register_rule(("Minion", 50))]
 fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult {
-    use Expr::*;
     use Domain::BoolDomain;
+    use Expr::*;
     match expr {
         Or(m, vec) => {
             let mut changed = false;
@@ -416,7 +414,9 @@ fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult {
             for expr in vec {
                 new_vec.push(match expr {
                     Reference(m, name)
-                        if mdl.get_domain(name).is_some_and(|x| matches!(x,BoolDomain)) =>
+                        if mdl
+                            .get_domain(name)
+                            .is_some_and(|x| matches!(x, BoolDomain)) =>
                     {
                         changed = true;
                         WatchedLiteral(m.clone_dirty(), name.clone(), Const::Bool(true))
@@ -437,7 +437,9 @@ fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult {
             for expr in vec {
                 new_vec.push(match expr {
                     Reference(m, name)
-                        if mdl.get_domain(name).is_some_and(|x| matches!(x,BoolDomain)) =>
+                        if mdl
+                            .get_domain(name)
+                            .is_some_and(|x| matches!(x, BoolDomain)) =>
                     {
                         changed = true;
                         WatchedLiteral(m.clone_dirty(), name.clone(), Const::Bool(true))
@@ -452,6 +454,22 @@ fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult {
 
             Ok(Reduction::pure(And(m.clone_dirty(), new_vec)))
         }
+
+        Not(m, expr) => {
+            if let Reference(_, name) = (**expr).clone() {
+                if mdl
+                    .get_domain(&name)
+                    .is_some_and(|x| matches!(x, BoolDomain))
+                {
+                    return Ok(Reduction::pure(WatchedLiteral(
+                        m.clone_dirty(),
+                        name.clone(),
+                        Const::Bool(false),
+                    )));
+                }
+            }
+            Err(RuleNotApplicable)
+        }
         _ => Err(RuleNotApplicable),
     }
 }