Define behaviour for empty expressions

conjure_oxide/tests/generated_tests.rs

@@ -232,7 +232,6 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
     model.constraints.transform(Arc::new(|x| {
         use conjure_core::ast::Expression::*;
         match &x {
-            Nothing => (),
             Bubble(_, _, _) => (),
             FactorE(_, _) => (),
             Sum(_, vec) => assert_constants_leq_one(&x, vec),

conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-parse.serialised.json

@@ -1,5 +1,13 @@
 {
-  "constraints": "Nothing",
+  "constraints": {
+    "And": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      []
+    ]
+  },
   "next_var": 0,
   "variables": [
     [

conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-rewrite.serialised.json

@@ -1,5 +1,17 @@
 {
-  "constraints": "Nothing",
+  "constraints": {
+    "FactorE": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      {
+        "Literal": {
+          "Bool": true
+        }
+      }
+    ]
+  },
   "next_var": 0,
   "variables": [
     [

conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-parse.serialised.json

@@ -1,5 +1,13 @@
 {
-  "constraints": "Nothing",
+  "constraints": {
+    "And": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      []
+    ]
+  },
   "next_var": 0,
   "variables": [
     [

conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-rewrite.serialised.json

@@ -1,5 +1,17 @@
 {
-  "constraints": "Nothing",
+  "constraints": {
+    "FactorE": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      {
+        "Literal": {
+          "Bool": true
+        }
+      }
+    ]
+  },
   "next_var": 0,
   "variables": [
     [

crates/conjure_core/src/ast/expressions.rs

@@ -27,12 +27,6 @@ use super::{Domain, Range};
 #[biplate(to=Factor)]
 #[biplate(to=Name)]
 pub enum Expression {
-    /**
-     * Represents an empty expression
-     * NB: we only expect this at the top level of a model (if there is no constraints)
-     */
-    Nothing,
-
     /// An expression representing "A is valid as long as B is true"
     /// Turns into a conjunction when it reaches a boolean context
     Bubble(Metadata, Box<Expression>, Box<Expression>),
@@ -245,7 +239,6 @@ impl Expression {
             Expression::Ineq(_, _, _, _) => Some(ReturnType::Bool),
             Expression::AllDiff(_, _) => Some(ReturnType::Bool),
             Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool?
-            Expression::Nothing => None,
             Expression::WatchedLiteral(_, _, _) => Some(ReturnType::Bool),
             Expression::Reify(_, _, _) => Some(ReturnType::Bool),
         }
@@ -306,7 +299,6 @@ impl Display for Expression {
                 Name::MachineName(n) => write!(f, "_{}", n),
                 Name::UserName(s) => write!(f, "{}", s),
             },
-            Expression::Nothing => write!(f, "Nothing"),
             Expression::Sum(_, expressions) => {
                 write!(f, "Sum({})", display_expressions(expressions))
             }

crates/conjure_core/src/model.rs

@@ -68,7 +68,11 @@ impl Model {
     }
 
     pub fn new_empty(context: Arc<RwLock<Context<'static>>>) -> Model {
-        Model::new(Default::default(), Expression::Nothing, context)
+        Model::new(
+            Default::default(),
+            Expression::And(Metadata::new(), Vec::new()),
+            context,
+        )
     }
     // Function to update a DecisionVariable based on its Name
     pub fn update_domain(&mut self, name: &Name, new_domain: Domain) {
@@ -89,14 +93,13 @@ impl Model {
     pub fn get_constraints_vec(&self) -> Vec<Expression> {
         match &self.constraints {
             Expression::And(_, constraints) => constraints.clone(),
-            Expression::Nothing => vec![],
             _ => vec![self.constraints.clone()],
         }
     }
 
     pub fn set_constraints(&mut self, constraints: Vec<Expression>) {
         if constraints.is_empty() {
-            self.constraints = Expression::Nothing;
+            self.constraints = Expression::And(Metadata::new(), Vec::new());
         } else if constraints.len() == 1 {
             self.constraints = constraints[0].clone();
         } else {

crates/conjure_core/src/rule_engine/rule.rs

@@ -75,7 +75,7 @@ impl Reduction {
     pub fn pure(new_expression: Expression) -> Self {
         Self {
             new_expression,
-            new_top: Expression::Nothing,
+            new_top: Expression::And(Metadata::new(), Vec::new()),
             symbols: SymbolTable::new(),
         }
     }
@@ -84,7 +84,7 @@ impl Reduction {
     pub fn with_symbols(new_expression: Expression, symbols: SymbolTable) -> Self {
         Self {
             new_expression,
-            new_top: Expression::Nothing,
+            new_top: Expression::And(Metadata::new(), Vec::new()),
             symbols,
         }
     }
@@ -101,21 +101,25 @@ impl Reduction {
     // Apply side-effects (e.g. symbol table updates
     pub fn apply(self, model: &mut Model) {
         model.variables.extend(self.symbols); // Add new assignments to the symbol table
-        if let Expression::Nothing = self.new_top {
-            model.constraints = self.new_expression.clone();
-        } else {
-            model.constraints = match self.new_expression {
-                Expression::And(metadata, mut exprs) => {
-                    // Avoid creating a nested conjunction
-                    exprs.push(self.new_top.clone());
-                    Expression::And(metadata.clone_dirty(), exprs)
-                }
-                _ => Expression::And(
-                    Metadata::new(),
-                    vec![self.new_expression.clone(), self.new_top],
-                ),
-            };
+                                              // TODO: (yb33) Remove it when we change constraints to a vector
+        if let Expression::And(_, exprs) = &self.new_top {
+            if exprs.is_empty() {
+                model.constraints = self.new_expression.clone();
+                return;
+            }
         }
+
+        model.constraints = match self.new_expression {
+            Expression::And(metadata, mut exprs) => {
+                // Avoid creating a nested conjunction
+                exprs.push(self.new_top.clone());
+                Expression::And(metadata.clone_dirty(), exprs)
+            }
+            _ => Expression::And(
+                Metadata::new(),
+                vec![self.new_expression.clone(), self.new_top],
+            ),
+        };
     }
 }
 

crates/conjure_core/src/rules/base.rs

@@ -18,82 +18,22 @@ use Lit::*;
 
 register_rule_set!("Base", 100, ());
 
-/**
- * Remove nothing's from expressions:
- * ```text
- * and([a, nothing, b]) = and([a, b])
- * sum([a, nothing, b]) = sum([a, b])
- * sum_leq([a, nothing, b], c) = sum_leq([a, b], c)
- * ...
- * ```
-*/
-#[register_rule(("Base", 8800))]
-fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult {
-    fn remove_nothings(exprs: Vec<Expr>) -> Result<Vec<Expr>, ApplicationError> {
-        let mut changed = false;
-        let mut new_exprs = Vec::new();
-
-        for e in exprs {
-            match e.clone() {
-                Nothing => {
-                    changed = true;
-                }
-                _ => new_exprs.push(e),
-            }
-        }
-
-        if changed {
-            Ok(new_exprs)
-        } else {
-            Err(ApplicationError::RuleNotApplicable)
-        }
-    }
-
-    fn get_lhs_rhs(sub: Vec<Expr>) -> (Vec<Expr>, Box<Expr>) {
-        if sub.is_empty() {
-            return (Vec::new(), Box::new(Nothing));
-        }
-
-        let lhs = sub[..(sub.len() - 1)].to_vec();
-        let rhs = Box::new(sub[sub.len() - 1].clone());
-        (lhs, rhs)
-    }
-
-    // FIXME (niklasdewally): temporary conversion until I get the Uniplate APIs figured out
-    // Uniplate *should* support Vec<> not im::Vector
-    let new_sub = remove_nothings(expr.children().into_iter().collect())?;
-
-    match expr {
-        And(md, _) => Ok(Reduction::pure(And(md.clone(), new_sub))),
-        Or(md, _) => Ok(Reduction::pure(Or(md.clone(), new_sub))),
-        Sum(md, _) => Ok(Reduction::pure(Sum(md.clone(), new_sub))),
-        SumEq(md, _, _) => {
-            let (lhs, rhs) = get_lhs_rhs(new_sub);
-            Ok(Reduction::pure(SumEq(md.clone(), lhs, rhs)))
-        }
-        SumLeq(md, _lhs, _rhs) => {
-            let (lhs, rhs) = get_lhs_rhs(new_sub);
-            Ok(Reduction::pure(SumLeq(md.clone(), lhs, rhs)))
-        }
-        SumGeq(md, _lhs, _rhs) => {
-            let (lhs, rhs) = get_lhs_rhs(new_sub);
-            Ok(Reduction::pure(SumGeq(md.clone(), lhs, rhs)))
-        }
-        _ => Err(ApplicationError::RuleNotApplicable),
-    }
-}
-
-/// Remove empty expressions:
-///  ```text
-///   or([]) ~> false
-///   X([])  ~> Nothing
-///  ```
+/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.
+///
+/// For example:
+/// - `or([])` simplifies to `false` since no disjunction exists.
+///
+/// **Applicable examples:**
+/// ```text
+/// or([])  ~> false
+/// X([]) ~> Nothing
+/// ```
 #[register_rule(("Base", 8800))]
 fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult {
     // excluded expressions
     if matches!(
         expr,
-        Nothing | FactorE(_, Reference(_,)) | FactorE(_, Literal(_)) | WatchedLiteral(_, _, _)
+        FactorE(_, Reference(_,)) | FactorE(_, Literal(_)) | WatchedLiteral(_, _, _)
     ) {
         return Err(ApplicationError::RuleNotApplicable);
     }
@@ -104,7 +44,7 @@ fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult {
 
     let new_expr = match expr {
         Or(_, _) => FactorE(Metadata::new(), Literal(Bool(false))),
-        _ => Nothing,
+        _ => And(Metadata::new(), vec![]), // TODO: (yb33) Change it to a simple vector after we refactor our model,
     };
 
     Ok(Reduction::pure(new_expr))

crates/conjure_core/src/rules/partial_eval.rs

@@ -15,7 +15,6 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult {
     // rule infinitely!
     // This is why we always check whether we found a constant or not.
     match expr.clone() {
-        Nothing => Err(RuleNotApplicable),
         Bubble(_, _, _) => Err(RuleNotApplicable),
         FactorE(_, _) => Err(RuleNotApplicable),
         Sum(m, vec) => {