From 3394b925ea67a28896cf83c1941842a4f973b4ef Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 11 Oct 2024 15:08:15 +0100 Subject: [PATCH 1/9] add partial evaluator For expressions containing both constants and nested expressions, the partial evaluator collapses constant values into a single value. For example, x + 1 + y + 2 + 3 ~> x + y + 6. In some cases, the partial evaluator replaces the constraint with a truth value. Currently, this is done when two identical constants are in an all-different constraint, and for the boolean clauses ` M or true` and `M and false`. The difference between this and the existing evaluator is that the latter only evaluates expressions made entirely of constants. Having both is useful: the total evaluator is useful for solutions checking (amongst other things), and the partial evaluator for model Optimisation. --- conjure_oxide/tests/generated_tests.rs | 4 +- .../{input.eprime.disabled => input.eprime} | 0 .../input.expected-minion.solutions.json | 146 +++++++++ .../input.expected-parse.serialised.json | 153 ++++++++++ .../input.expected-rewrite.serialised.json | 135 +++++++++ crates/conjure_core/src/rules/mod.rs | 1 + crates/conjure_core/src/rules/partial_eval.rs | 277 ++++++++++++++++++ 7 files changed, 715 insertions(+), 1 deletion(-) rename conjure_oxide/tests/integration/eprime-minion/partial-eval-add/{input.eprime.disabled => input.eprime} (100%) create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json create mode 100644 crates/conjure_core/src/rules/partial_eval.rs diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index 698e3ac330..c95c32b94f 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -171,7 +171,9 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) SumLeq(_, vec, _) => assert_constants_leq_one(&x, vec), DivEq(_, _, _, _) => (), Ineq(_, _, _, _) => (), - AllDiff(_, vec) => assert_constants_leq_one(&x, vec), + // this is a vector operation, but we don't want to fold values into each-other in this + // one + AllDiff(_, _) => (), }; x.clone() })); diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime.disabled b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime similarity index 100% rename from conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime.disabled rename to conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-minion.solutions.json new file mode 100644 index 0000000000..655db490bb --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-minion.solutions.json @@ -0,0 +1,146 @@ +[ + { + "UserName(x)": 15, + "UserName(y)": 50 + }, + { + "UserName(x)": 16, + "UserName(y)": 49 + }, + { + "UserName(x)": 17, + "UserName(y)": 48 + }, + { + "UserName(x)": 18, + "UserName(y)": 47 + }, + { + "UserName(x)": 19, + "UserName(y)": 46 + }, + { + "UserName(x)": 20, + "UserName(y)": 45 + }, + { + "UserName(x)": 21, + "UserName(y)": 44 + }, + { + "UserName(x)": 22, + "UserName(y)": 43 + }, + { + "UserName(x)": 23, + "UserName(y)": 42 + }, + { + "UserName(x)": 24, + "UserName(y)": 41 + }, + { + "UserName(x)": 25, + "UserName(y)": 40 + }, + { + "UserName(x)": 26, + "UserName(y)": 39 + }, + { + "UserName(x)": 27, + "UserName(y)": 38 + }, + { + "UserName(x)": 28, + "UserName(y)": 37 + }, + { + "UserName(x)": 29, + "UserName(y)": 36 + }, + { + "UserName(x)": 30, + "UserName(y)": 35 + }, + { + "UserName(x)": 31, + "UserName(y)": 34 + }, + { + "UserName(x)": 32, + "UserName(y)": 33 + }, + { + "UserName(x)": 33, + "UserName(y)": 32 + }, + { + "UserName(x)": 34, + "UserName(y)": 31 + }, + { + "UserName(x)": 35, + "UserName(y)": 30 + }, + { + "UserName(x)": 36, + "UserName(y)": 29 + }, + { + "UserName(x)": 37, + "UserName(y)": 28 + }, + { + "UserName(x)": 38, + "UserName(y)": 27 + }, + { + "UserName(x)": 39, + "UserName(y)": 26 + }, + { + "UserName(x)": 40, + "UserName(y)": 25 + }, + { + "UserName(x)": 41, + "UserName(y)": 24 + }, + { + "UserName(x)": 42, + "UserName(y)": 23 + }, + { + "UserName(x)": 43, + "UserName(y)": 22 + }, + { + "UserName(x)": 44, + "UserName(y)": 21 + }, + { + "UserName(x)": 45, + "UserName(y)": 20 + }, + { + "UserName(x)": 46, + "UserName(y)": 19 + }, + { + "UserName(x)": 47, + "UserName(y)": 18 + }, + { + "UserName(x)": 48, + "UserName(y)": 17 + }, + { + "UserName(x)": 49, + "UserName(y)": 16 + }, + { + "UserName(x)": 50, + "UserName(y)": 15 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json new file mode 100644 index 0000000000..b170804ab9 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json @@ -0,0 +1,153 @@ +{ + "constraints": { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 20 + } + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 100 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..09d6631b44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json @@ -0,0 +1,135 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "SumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 65 + } + ] + } + ] + }, + { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 65 + } + ] + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/crates/conjure_core/src/rules/mod.rs b/crates/conjure_core/src/rules/mod.rs index e65f659901..900402d6c4 100644 --- a/crates/conjure_core/src/rules/mod.rs +++ b/crates/conjure_core/src/rules/mod.rs @@ -5,3 +5,4 @@ mod bubble; mod cnf; mod constant; mod minion; +mod partial_eval; diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs new file mode 100644 index 0000000000..3f6d6409a4 --- /dev/null +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -0,0 +1,277 @@ +use std::collections::HashSet; + +use conjure_macros::register_rule; + +use crate::ast::{Constant as Const, Expression as Expr}; +use crate::rule_engine::{ApplicationResult, Reduction}; +use crate::Model; + +#[register_rule(("Base",200))] +fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { + use conjure_core::rule_engine::ApplicationError::RuleNotApplicable; + use Expr::*; + + // NOTE: If nothing changes, we must return RuleNotApplicable, or the rewriter will try this + // rule infinitely! + // This is why we always check whether we found a constant or not. + match expr.clone() { + Nothing => Err(RuleNotApplicable), + Bubble(_, _, _) => Err(RuleNotApplicable), + Constant(_, _) => Err(RuleNotApplicable), + Reference(_, _) => Err(RuleNotApplicable), + Sum(m, vec) => { + let mut acc = 0; + let mut n_consts = 0; + let mut new_vec: Vec = Vec::new(); + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + acc += x; + n_consts += 1; + } else { + new_vec.push(expr); + } + } + if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Sum(m, new_vec))) + } + } + Min(m, vec) => { + let mut acc: Option = None; + let mut n_consts = 0; + let mut new_vec: Vec = Vec::new(); + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc = match acc { + Some(i) => { + if i > x { + Some(x) + } else { + Some(i) + } + } + None => Some(x), + }; + } else { + new_vec.push(expr); + } + } + + if let Some(i) = acc { + new_vec.push(Constant(Default::default(), Const::Int(i))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Min(m, new_vec))) + } + } + Max(m, vec) => { + let mut acc: Option = None; + let mut n_consts = 0; + let mut new_vec: Vec = Vec::new(); + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc = match acc { + Some(i) => { + if i < x { + Some(x) + } else { + Some(i) + } + } + None => Some(x), + }; + } else { + new_vec.push(expr); + } + } + + if let Some(i) = acc { + new_vec.push(Constant(Default::default(), Const::Int(i))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Max(m, new_vec))) + } + } + Not(_, _) => Err(RuleNotApplicable), + Or(m, vec) => { + let mut new_vec: Vec = Vec::new(); + let mut has_const: bool = false; + for expr in vec { + if let Constant(_, Const::Bool(x)) = expr { + has_const = true; + if x { + return Ok(Reduction::pure(Constant( + Default::default(), + Const::Bool(true), + ))); + } + } else { + new_vec.push(expr); + } + } + + if !has_const { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Or(m, new_vec))) + } + } + And(m, vec) => { + let mut new_vec: Vec = Vec::new(); + let mut has_const: bool = false; + for expr in vec { + if let Constant(_, Const::Bool(x)) = expr { + has_const = true; + if !x { + return Ok(Reduction::pure(Constant( + Default::default(), + Const::Bool(false), + ))); + } + } else { + new_vec.push(expr); + } + } + + if !has_const { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(And(m, new_vec))) + } + } + Eq(_, _, _) => Err(RuleNotApplicable), + Neq(_, _, _) => Err(RuleNotApplicable), + Geq(_, _, _) => Err(RuleNotApplicable), + Leq(_, _, _) => Err(RuleNotApplicable), + Gt(_, _, _) => Err(RuleNotApplicable), + Lt(_, _, _) => Err(RuleNotApplicable), + SafeDiv(_, _, _) => Err(RuleNotApplicable), + UnsafeDiv(_, _, _) => Err(RuleNotApplicable), + SumEq(m, vec, eq) => { + let mut acc = 0; + let mut new_vec: Vec = Vec::new(); + let mut n_consts = 0; + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc += x; + } else { + new_vec.push(expr); + } + } + + if let Constant(_, Const::Int(x)) = *eq { + if acc != 0 { + // when rhs is a constant, move lhs constants to rhs + return Ok(Reduction::pure(SumEq( + m, + new_vec, + Box::new(Constant(Default::default(), Const::Int(x - acc))), + ))); + } + } else if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(SumEq(m, new_vec, eq))) + } + } + SumGeq(m, vec, geq) => { + let mut acc = 0; + let mut new_vec: Vec = Vec::new(); + let mut n_consts = 0; + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc += x; + } else { + new_vec.push(expr); + } + } + + if let Constant(_, Const::Int(x)) = *geq { + if acc != 0 { + // when rhs is a constant, move lhs constants to rhs + return Ok(Reduction::pure(SumGeq( + m, + new_vec, + Box::new(Constant(Default::default(), Const::Int(x - acc))), + ))); + } + } else if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(SumGeq(m, new_vec, geq))) + } + } + SumLeq(m, vec, leq) => { + let mut acc = 0; + let mut new_vec: Vec = Vec::new(); + let mut n_consts = 0; + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc += x; + } else { + new_vec.push(expr); + } + } + + if let Constant(_, Const::Int(x)) = *leq { + // when rhs is a constant, move lhs constants to rhs + if acc != 0 { + return Ok(Reduction::pure(SumLeq( + m, + new_vec, + Box::new(Constant(Default::default(), Const::Int(x - acc))), + ))); + } + } else if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(SumLeq(m, new_vec, leq))) + } + } + DivEq(_, _, _, _) => Err(RuleNotApplicable), + Ineq(_, _, _, _) => Err(RuleNotApplicable), + AllDiff(m, vec) => { + let mut consts: HashSet = HashSet::new(); + + // check for duplicate constant values which would fail the constraint + for expr in &vec { + if let Constant(_, Const::Int(x)) = expr { + if !consts.insert(*x) { + return Ok(Reduction::pure(Constant(m, Const::Bool(false)))); + } + } + } + + // nothing has changed + Err(RuleNotApplicable) + } + } +} From 4c2e1d70362cb4fdf49ca944642ae9d209322cbb Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 11 Oct 2024 16:52:35 +0100 Subject: [PATCH 2/9] parser: add boolean constants --- crates/conjure_core/src/parse/parse_model.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/crates/conjure_core/src/parse/parse_model.rs b/crates/conjure_core/src/parse/parse_model.rs index 2ae9fe501b..7265928f2e 100644 --- a/crates/conjure_core/src/parse/parse_model.rs +++ b/crates/conjure_core/src/parse/parse_model.rs @@ -211,6 +211,10 @@ fn parse_expression(obj: &JsonValue) -> Option { "MkOpMax", Box::new(Expression::Max) as Box _>, ), + ( + "MkOpAllDiff", + Box::new(Expression::AllDiff) as Box _>, + ), ] .into_iter() .collect(); @@ -313,6 +317,11 @@ fn parse_constant(constant: &serde_json::Map) -> Option { + let b: bool = b["ConstantBool"].as_bool().unwrap(); + Some(Expression::Constant(Metadata::new(), Constant::Bool(b))) + } otherwise => panic!("Unhandled parse_constant {:#?}", otherwise), } } From 40ce5a97428c456c60f017d066e7d25409be1159 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 11 Oct 2024 17:55:49 +0100 Subject: [PATCH 3/9] add w-lit constraint, enabling support for variables in and/or clauses - Add w-lit constraint, allowing variables to be found at the top level of and and or clauses. `And` and `or` convert to the watched-and and watched-or Minion constraints. These only take constraints as arguments, not variables. W-lit(x,1) is SAT iff x is true; using this fact, variables can be converted to constraints, solving this limitation. Conjure Oxide's W-lit expression is more strongly typed than other expressions. My intention is for this to be a low-level, Minion-specific expression that is only used at the end of the rewriting process. As far as I can see, it doesn't have any modelling uses, and is only useful to allow the use of variables in watched-or / watched-and. --- conjure_oxide/tests/generated_tests.rs | 3 +- crates/conjure_core/src/ast/expressions.rs | 16 ++++ crates/conjure_core/src/rules/base.rs | 7 +- crates/conjure_core/src/rules/minion.rs | 74 ++++++++++++++++++- crates/conjure_core/src/rules/partial_eval.rs | 2 + .../src/solver/adaptors/minion.rs | 21 +++++- solvers/minion/src/run.rs | 6 +- 7 files changed, 122 insertions(+), 7 deletions(-) diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index c95c32b94f..f418cee637 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -145,7 +145,7 @@ fn integration_test_inner( } fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) { - model.constraints.descend(Arc::new(|x| { + model.constraints.transform(Arc::new(|x| { use conjure_core::ast::Expression::*; match &x { Nothing => (), @@ -174,6 +174,7 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) // this is a vector operation, but we don't want to fold values into each-other in this // one AllDiff(_, _) => (), + WatchedLiteral(_, _, _) => (), }; x.clone() })); diff --git a/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index 620c835bd6..da34e18bd8 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -110,6 +110,18 @@ pub enum Expression { #[compatible(Minion)] AllDiff(Metadata, Vec), + + /// w-literal(x,k) is SAT iff x == k, where x is a variable and k a constant. + /// + /// This is a low-level Minion constraint and you should (probably) use Eq instead. The main + /// use of w-literal is to convert boolean variables to constraints so that they can be used + /// inside watched-and and watched-or. + /// + /// See `rules::minion::boolean_literal_to_wliteral`. + /// + /// + #[compatible(Minion)] + WatchedLiteral(Metadata, Name, Constant), } fn expr_vec_to_domain_i32( @@ -223,6 +235,7 @@ impl Expression { Expression::AllDiff(_, _) => Some(ReturnType::Bool), Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool? Expression::Nothing => None, + Expression::WatchedLiteral(_, _, _) => Some(ReturnType::Bool), } } @@ -320,6 +333,9 @@ impl Expression { Expression::DivEq(metadata, box1, box2, box3) => { metadata.clean = bool_value; } + Expression::WatchedLiteral(metadata, name, constant) => { + metadata.clean = bool_value; + } } } } diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs index eb38852ad4..3382d0fa30 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -86,9 +86,10 @@ fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult { #[register_rule(("Base", 100))] fn empty_to_nothing(expr: &Expr, _: &Model) -> ApplicationResult { match expr { - Expr::Nothing | Expr::Reference(_, _) | Expr::Constant(_, _) => { - Err(ApplicationError::RuleNotApplicable) - } + Expr::Nothing + | Expr::Reference(_, _) + | Expr::Constant(_, _) + | Expr::WatchedLiteral(_, _, _) => Err(ApplicationError::RuleNotApplicable), _ => { if expr.children().is_empty() { Ok(Reduction::pure(Expr::Nothing)) diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index 1e265be0bf..d59160a85b 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -2,14 +2,17 @@ /* Rules for translating to Minion-supported constraints */ /************************************************************************/ -use crate::ast::{Constant as Const, DecisionVariable, 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, }; + use crate::solver::SolverFamily; use crate::Model; use uniplate::Uniplate; +use ApplicationError::RuleNotApplicable; register_rule_set!("Minion", 100, ("Base"), (SolverFamily::Minion)); @@ -385,3 +388,72 @@ fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult { _ => Err(ApplicationError::RuleNotApplicable), } } + +/// Flattening rule that converts boolean variables to watched-literal constraints. +/// +/// For some boolean variable x: +/// ```text +/// and([x,...]) ~> and([w-literal(x,1),..]) +/// or([x,...]) ~> or([w-literal(x,1),..]) +/// ``` +/// +/// ## Rationale +/// +/// Minion's watched-and and watched-or constraints only takes other constraints as arguments. +/// +/// This restates boolean variables as the equivalent constraint "SAT if x is true". +/// +#[register_rule(("Minion", 50))] +fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult { + use Domain::BoolDomain; + use Expr::*; + match expr { + Or(m, vec) => { + let mut changed = false; + let mut new_vec = Vec::new(); + for expr in vec { + new_vec.push(match expr { + Reference(m, name) + if mdl + .get_domain(name) + .is_some_and(|x| matches!(x, BoolDomain)) => + { + changed = true; + WatchedLiteral(m.clone_dirty(), name.clone(), Const::Bool(true)) + } + e => e.clone(), + }); + } + + if !changed { + return Err(RuleNotApplicable); + } + + Ok(Reduction::pure(Or(m.clone_dirty(), new_vec))) + } + And(m, vec) => { + let mut changed = false; + let mut new_vec = Vec::new(); + for expr in vec { + new_vec.push(match expr { + Reference(m, name) + if mdl + .get_domain(name) + .is_some_and(|x| matches!(x, BoolDomain)) => + { + changed = true; + WatchedLiteral(m.clone_dirty(), name.clone(), Const::Bool(true)) + } + e => e.clone(), + }); + } + + if !changed { + return Err(RuleNotApplicable); + } + + Ok(Reduction::pure(And(m.clone_dirty(), new_vec))) + } + _ => Err(RuleNotApplicable), + } +} diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs index 3f6d6409a4..73641542c4 100644 --- a/crates/conjure_core/src/rules/partial_eval.rs +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -273,5 +273,7 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { // nothing has changed Err(RuleNotApplicable) } + + WatchedLiteral(_, _, _) => Err(RuleNotApplicable), } } diff --git a/crates/conjure_core/src/solver/adaptors/minion.rs b/crates/conjure_core/src/solver/adaptors/minion.rs index 2362976aeb..8e1811046e 100644 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ b/crates/conjure_core/src/solver/adaptors/minion.rs @@ -291,6 +291,13 @@ fn read_expr(expr: conjure_ast::Expression) -> Result { Ok(minion_ast::Constraint::Eq(read_var(*a)?, read_var(*b)?)) } + + conjure_ast::Expression::WatchedLiteral(_metadata, name, k) => { + Ok(minion_ast::Constraint::WLiteral( + minion_ast::Var::NameRef(_name_to_string(name)), + minion_ast::Constant::Integer(read_const_1(k)?), + )) + } x => Err(ModelFeatureNotSupported(format!("{:?}", x))), } } @@ -329,7 +336,19 @@ fn _read_ref(e: conjure_ast::Expression) -> Result { fn read_const(e: conjure_ast::Expression) -> Result { match e { - conjure_ast::Expression::Constant(_, conjure_ast::Constant::Int(n)) => Ok(n), + conjure_ast::Expression::Constant(_, x) => Ok(read_const_1(x)?), + x => Err(ModelInvalid(format!( + "expected a constant, but got `{0:?}`", + x + ))), + } +} + +fn read_const_1(k: conjure_ast::Constant) -> Result { + match k { + conjure_ast::Constant::Int(n) => Ok(n), + conjure_ast::Constant::Bool(true) => Ok(1), + conjure_ast::Constant::Bool(false) => Ok(0), x => Err(ModelInvalid(format!( "expected a constant, but got `{0:?}`", x diff --git a/solvers/minion/src/run.rs b/solvers/minion/src/run.rs index e31114c809..2cedf739af 100644 --- a/solvers/minion/src/run.rs +++ b/solvers/minion/src/run.rs @@ -562,7 +562,11 @@ unsafe fn constraint_add_args( //Constraint::WatchElementOne(_, _, _) => todo!(), //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(), //Constraint::WatchElementUndefZero(_, _, _) => todo!(), - //Constraint::WLiteral(_, _) => todo!(), + Constraint::WLiteral(a, b) => { + read_var(i, r_constr, a)?; + read_constant(r_constr, b)?; + Ok(()) + } //Constraint::WNotLiteral(_, _) => todo!(), //Constraint::WInIntervalSet(_, _) => todo!(), //Constraint::WInRange(_, _) => todo!(), From 97739720ceb1ab89b2bab529024c01f7eace29ba Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 11 Oct 2024 16:29:25 +0100 Subject: [PATCH 4/9] add test for partial evaluation of or, and --- .../partial-eval-or-and/config.toml | 1 + .../partial-eval-or-and/input.eprime | 8 ++ .../input.expected-minion.solutions.json | 17 +++ .../input.expected-parse.serialised.json | 124 ++++++++++++++++++ .../input.expected-rewrite.serialised.json | 91 +++++++++++++ 5 files changed, 241 insertions(+) create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime new file mode 100644 index 0000000000..c69f546a71 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime @@ -0,0 +1,8 @@ +language ESSENCE' 1.0 + +find a,b,c : bool such that + +a \/ b \/ false, +$ this alldiff should not end up in the final model +allDiff([1,2,3]) \/ true, +(c /\ true) diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json new file mode 100644 index 0000000000..2357b354e3 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json @@ -0,0 +1,17 @@ +[ + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 0, + "UserName(c)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json new file mode 100644 index 0000000000..254436f7a4 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json @@ -0,0 +1,124 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": false + } + ] + } + ] + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..aa28296e44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json @@ -0,0 +1,91 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file From 14607885589fa8705b979567837664616429ce6c Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 11 Oct 2024 21:21:36 +0100 Subject: [PATCH 5/9] implement not(x) ~> w-lit(x,0) --- .gitignore | 1 + .../bool/literals-to-wlit-1/config.toml | 1 + .../bool/literals-to-wlit-1/input.eprime | 12 + .../input.expected-minion.solutions.json | 26 +++ .../input.expected-parse.serialised.json | 183 +++++++++++++++ .../input.expected-rewrite.serialised.json | 213 ++++++++++++++++++ crates/conjure_core/src/rules/minion.rs | 18 +- 7 files changed, 453 insertions(+), 1 deletion(-) create mode 100644 conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml create mode 100644 conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime create mode 100644 conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json diff --git a/.gitignore b/.gitignore index f1a67c9948..090c8762c9 100644 --- a/.gitignore +++ b/.gitignore @@ -180,4 +180,5 @@ fabric.properties *.eprime.infor *.eprime.minion *.eprime.solution +*.eprime.solution.* *.eprime.info diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime new file mode 100644 index 0000000000..66675954ea --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime @@ -0,0 +1,12 @@ +$ top level variables in and's and or's should be converted to wlit(x,1). +$ negations should be converted to wlit(x,0) + +language ESSENCE' 1.0 + +find a,b,c,d: bool +such that + a \/ b, + !c \/ (b /\ d), + b, + d \/ c + diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json new file mode 100644 index 0000000000..15ef0b1e30 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json @@ -0,0 +1,26 @@ +[ + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 0, + "UserName(d)": 1 + }, + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1, + "UserName(d)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 0, + "UserName(d)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 1, + "UserName(d)": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json new file mode 100644 index 0000000000..49ac787ba2 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json @@ -0,0 +1,183 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Not": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + } + ] + } + ] + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "d" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..696ccc0df2 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json @@ -0,0 +1,213 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": false + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": false + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": true + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "d" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index d59160a85b..cc74026e33 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -3,7 +3,6 @@ /************************************************************************/ 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, @@ -395,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 @@ -454,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), } } From 033355095a8d4fc1b4bd1bb57c43d40caa45ff51 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 12 Oct 2024 12:48:08 +0100 Subject: [PATCH 6/9] add broken complex partial evaluator test (arithmetic, nesting, min) Add more complex test case for the partial evaluator. This currently never terminates, so has been disabled. --- .../partial-eval-03/input.eprime.disabled | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled b/conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled new file mode 100644 index 0000000000..b327bb9231 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled @@ -0,0 +1,16 @@ +language ESSENCE' 1.0 + + +$ nesting, sumleqs, and mins + +find x,y,z : int(1..5) +find a: bool + +such that + 20 + x + 5 + y + min([(z + y),(y + x),(z + x + 5),50]) <= 40, + a = allDiff([x,y,z]), + + $ narrow down solutions a bit + y <= z, + x <= y + From 6c6d511be68fa09bfb7c8cdc3f6747c38ab503e1 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 12 Oct 2024 09:56:15 +0100 Subject: [PATCH 7/9] change rule priorities to run simplifiers first; add reify Create a rule priority taxonomy, and refactor rules to follow this new convention. In particular, ensure that partial and total evaluation and simplification rules happen before representation changes and solver specific rules. DESCRIPTION Simplifying a model before applying representation changes should ensure that nested sums do not get propagated across the model. For example, the transformation for min turns it into many binary constraints. If simplification was not done first, simplification steps would have to be ran on each of these binary constraints, instead of just on the input model. Ensuring that everything is always in canonical forms should stop rules looping, and help with pattern matching. The implementation of canonical forms is incomplete and outside the scope of this patch. These rule changes caused basic-div-04 to fail. To fix this, this patch also does the following: - add reify constraint (reify(X,1) if constraint X is SAT, reify(X,0) if constraint X is UNSAT) - add rule not(X) ~> reify(X,0) (where X is a constraint), allowing negated constraints to be passed to Minion. MOTIVATION The commit c2b74602c (add broken complex partial evaluator test (arithmetic, nesting, min), 2024-10-12) added a test case for the partial evaluator that never terminated. Simplification steps should be ran before the decomposition of the min constraint and the conversion of expressions into more specialised / solver specific forms (such as ineq, sumgeq, etc); however, this was not the case in this test. In this test, ineq / sumgeq were being applied before the sums had been flattened. After this refactor, this test now terminates with failure. A flattening rule for ineq is needed before this test passes and will be added in a later commit. --- .gitignore | 2 + conjure_oxide/tests/generated_tests.rs | 1 + .../01/input.expected-minion.solutions.json | 4 - .../01/input.expected-rewrite.serialised.json | 59 +----- .../03/input.expected-minion.solutions.json | 2 - .../03/input.expected-rewrite.serialised.json | 59 +----- .../04/input.expected-minion.solutions.json | 200 +++++++----------- .../04/input.expected-rewrite.serialised.json | 180 +++++++--------- .../partial-eval-01-add/config.toml | 1 + .../partial-eval-01-add/input.eprime | 3 + .../input.expected-minion.solutions.json | 146 +++++++++++++ .../input.expected-parse.serialised.json | 153 ++++++++++++++ .../input.expected-rewrite.serialised.json | 135 ++++++++++++ .../partial-eval-02-or-and/config.toml | 1 + .../partial-eval-02-or-and/input.eprime | 8 + .../input.expected-minion.solutions.json | 17 ++ .../input.expected-parse.serialised.json | 124 +++++++++++ .../input.expected-rewrite.serialised.json | 91 ++++++++ conjure_oxide/tests/rewrite_tests.rs | 116 +--------- crates/conjure_core/src/ast/expressions.rs | 9 +- .../src/rule_engine/resolve_rules.rs | 10 +- crates/conjure_core/src/rule_engine/rule.rs | 4 +- .../conjure_core/src/rule_engine/rule_set.rs | 14 +- crates/conjure_core/src/rules/base.rs | 64 ++---- crates/conjure_core/src/rules/bubble.rs | 8 +- crates/conjure_core/src/rules/constant.rs | 4 +- crates/conjure_core/src/rules/minion.rs | 53 +++-- crates/conjure_core/src/rules/mod.rs | 6 + crates/conjure_core/src/rules/partial_eval.rs | 3 +- .../conjure_core/src/rules/rule_semantics.md | 16 ++ .../src/solver/adaptors/minion.rs | 10 + crates/conjure_macros/src/lib.rs | 2 +- 32 files changed, 960 insertions(+), 545 deletions(-) create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/config.toml create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.eprime create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/config.toml create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.eprime create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json create mode 100644 crates/conjure_core/src/rules/rule_semantics.md diff --git a/.gitignore b/.gitignore index 090c8762c9..53c9ba7e86 100644 --- a/.gitignore +++ b/.gitignore @@ -182,3 +182,5 @@ fabric.properties *.eprime.solution *.eprime.solution.* *.eprime.info + +.MINION* diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index f418cee637..6619c90069 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -175,6 +175,7 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) // one AllDiff(_, _) => (), WatchedLiteral(_, _, _) => (), + Reify(_, _, _) => (), }; x.clone() })); diff --git a/conjure_oxide/tests/integration/basic/div/01/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/01/input.expected-minion.solutions.json index 44371266d0..c3f9f2e1ac 100644 --- a/conjure_oxide/tests/integration/basic/div/01/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/div/01/input.expected-minion.solutions.json @@ -1,21 +1,17 @@ [ { - "MachineName(0)": 1, "UserName(a)": 1, "UserName(b)": 1 }, { - "MachineName(0)": 1, "UserName(a)": 2, "UserName(b)": 2 }, { - "MachineName(0)": 1, "UserName(a)": 3, "UserName(b)": 2 }, { - "MachineName(0)": 1, "UserName(a)": 3, "UserName(b)": 3 } diff --git a/conjure_oxide/tests/integration/basic/div/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/01/input.expected-rewrite.serialised.json index 1110d162b6..d37d18e9b1 100644 --- a/conjure_oxide/tests/integration/basic/div/01/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/01/input.expected-rewrite.serialised.json @@ -7,7 +7,7 @@ }, [ { - "Eq": [ + "DivEq": [ { "clean": false, "etype": null @@ -19,28 +19,9 @@ "etype": null }, { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false, - "etype": null - }, - { - "Int": 1 + "UserName": "a" } ] - } - ] - }, - { - "Neq": [ - { - "clean": false, - "etype": null }, { "Reference": [ @@ -60,29 +41,18 @@ "etype": null }, { - "Int": 0 + "Int": 1 } ] } ] }, { - "DivEq": [ + "Neq": [ { "clean": false, "etype": null }, - { - "Reference": [ - { - "clean": false, - "etype": null - }, - { - "UserName": "a" - } - ] - }, { "Reference": [ { @@ -95,13 +65,13 @@ ] }, { - "Reference": [ + "Constant": [ { "clean": false, "etype": null }, { - "MachineName": 0 + "Int": 0 } ] } @@ -112,23 +82,6 @@ }, "next_var": 1, "variables": [ - [ - { - "MachineName": 0 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - 0, - 3 - ] - } - ] - } - } - ], [ { "UserName": "a" diff --git a/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json index 350becd8be..3d02c55645 100644 --- a/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json @@ -1,10 +1,8 @@ [ { - "MachineName(0)": 2, "UserName(a)": 3 }, { - "MachineName(0)": 2, "UserName(a)": 4 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json index e3a12533d7..1e9f1a4c71 100644 --- a/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json @@ -7,7 +7,7 @@ }, [ { - "Eq": [ + "DivEq": [ { "clean": false, "etype": null @@ -19,29 +19,10 @@ "etype": null }, { - "Int": 2 + "Int": 8 } ] }, - { - "Reference": [ - { - "clean": false, - "etype": null - }, - { - "MachineName": 0 - } - ] - } - ] - }, - { - "Neq": [ - { - "clean": false, - "etype": null - }, { "Reference": [ { @@ -60,29 +41,18 @@ "etype": null }, { - "Int": 0 + "Int": 2 } ] } ] }, { - "DivEq": [ + "Neq": [ { "clean": false, "etype": null }, - { - "Constant": [ - { - "clean": false, - "etype": null - }, - { - "Int": 8 - } - ] - }, { "Reference": [ { @@ -95,13 +65,13 @@ ] }, { - "Reference": [ + "Constant": [ { "clean": false, "etype": null }, { - "MachineName": 0 + "Int": 0 } ] } @@ -112,23 +82,6 @@ }, "next_var": 1, "variables": [ - [ - { - "MachineName": 0 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - 0, - 8 - ] - } - ] - } - } - ], [ { "UserName": "a" diff --git a/conjure_oxide/tests/integration/basic/div/04/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/04/input.expected-minion.solutions.json index 20823a766c..7f70b0739d 100644 --- a/conjure_oxide/tests/integration/basic/div/04/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/div/04/input.expected-minion.solutions.json @@ -1,314 +1,262 @@ [ { - "MachineName(0)": 0, "UserName(a)": 0, "UserName(b)": 0, "UserName(c)": 0 }, { - "MachineName(0)": 0, "UserName(a)": 0, "UserName(b)": 1, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { "UserName(a)": 0, "UserName(b)": 2, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 0, + "UserName(b)": 2, + "UserName(c)": 1 + }, + { + "UserName(a)": 0, + "UserName(b)": 2, + "UserName(c)": 2 + }, + { "UserName(a)": 0, "UserName(b)": 3, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 0, + "UserName(b)": 3, + "UserName(c)": 1 + }, + { + "UserName(a)": 0, + "UserName(b)": 3, + "UserName(c)": 2 + }, + { + "UserName(a)": 0, + "UserName(b)": 3, + "UserName(c)": 3 + }, + { "UserName(a)": 1, "UserName(b)": 0, "UserName(c)": 0 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 0, "UserName(c)": 1 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 0, "UserName(c)": 2 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 0, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 1, "UserName(c)": 0 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 1, "UserName(c)": 2 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 1, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 2, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 1, + "UserName(b)": 2, + "UserName(c)": 1 + }, + { "UserName(a)": 1, "UserName(b)": 2, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 1, "UserName(b)": 3, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 1, + "UserName(b)": 3, + "UserName(c)": 1 + }, + { "UserName(a)": 2, "UserName(b)": 0, "UserName(c)": 0 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 0, "UserName(c)": 1 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 0, "UserName(c)": 2 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 0, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 1, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 2, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { "UserName(a)": 2, "UserName(b)": 1, "UserName(c)": 2 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 1, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 2, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 2, + "UserName(b)": 2, + "UserName(c)": 2 + }, + { "UserName(a)": 2, "UserName(b)": 2, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 2, "UserName(b)": 3, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 2, + "UserName(b)": 3, + "UserName(c)": 1 + }, + { + "UserName(a)": 2, + "UserName(b)": 3, + "UserName(c)": 2 + }, + { + "UserName(a)": 2, + "UserName(b)": 3, + "UserName(c)": 3 + }, + { "UserName(a)": 3, "UserName(b)": 0, "UserName(c)": 0 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 0, "UserName(c)": 1 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 0, "UserName(c)": 2 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 0, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 1, "UserName(c)": 0 }, { - "MachineName(0)": 0, + "UserName(a)": 3, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { "UserName(a)": 3, "UserName(b)": 1, "UserName(c)": 2 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 1, "UserName(c)": 3 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 2, "UserName(c)": 0 }, { - "MachineName(0)": 0, "UserName(a)": 3, "UserName(b)": 2, - "UserName(c)": 3 - }, - { - "MachineName(0)": 0, - "UserName(a)": 3, - "UserName(b)": 3, - "UserName(c)": 0 - }, - { - "MachineName(0)": 1, - "UserName(a)": 0, - "UserName(b)": 1, "UserName(c)": 1 }, { - "MachineName(0)": 1, - "UserName(a)": 0, + "UserName(a)": 3, "UserName(b)": 2, "UserName(c)": 2 }, { - "MachineName(0)": 1, - "UserName(a)": 0, - "UserName(b)": 3, - "UserName(c)": 2 - }, - { - "MachineName(0)": 1, - "UserName(a)": 0, - "UserName(b)": 3, - "UserName(c)": 3 - }, - { - "MachineName(0)": 1, - "UserName(a)": 2, - "UserName(b)": 1, - "UserName(c)": 1 - }, - { - "MachineName(0)": 1, - "UserName(a)": 2, + "UserName(a)": 3, "UserName(b)": 2, - "UserName(c)": 2 - }, - { - "MachineName(0)": 1, - "UserName(a)": 2, - "UserName(b)": 3, - "UserName(c)": 2 - }, - { - "MachineName(0)": 1, - "UserName(a)": 2, - "UserName(b)": 3, "UserName(c)": 3 }, { - "MachineName(0)": 1, - "UserName(a)": 3, - "UserName(b)": 1, - "UserName(c)": 1 - }, - { - "MachineName(0)": 1, "UserName(a)": 3, - "UserName(b)": 2, - "UserName(c)": 2 + "UserName(b)": 3, + "UserName(c)": 0 }, { - "MachineName(0)": 1, "UserName(a)": 3, "UserName(b)": 3, "UserName(c)": 2 }, { - "MachineName(0)": 1, "UserName(a)": 3, "UserName(b)": 3, "UserName(c)": 3 - }, - { - "MachineName(0)": 2, - "UserName(a)": 0, - "UserName(b)": 2, - "UserName(c)": 1 - }, - { - "MachineName(0)": 2, - "UserName(a)": 1, - "UserName(b)": 2, - "UserName(c)": 1 - }, - { - "MachineName(0)": 2, - "UserName(a)": 3, - "UserName(b)": 2, - "UserName(c)": 1 - }, - { - "MachineName(0)": 3, - "UserName(a)": 0, - "UserName(b)": 3, - "UserName(c)": 1 - }, - { - "MachineName(0)": 3, - "UserName(a)": 1, - "UserName(b)": 3, - "UserName(c)": 1 - }, - { - "MachineName(0)": 3, - "UserName(a)": 2, - "UserName(b)": 3, - "UserName(c)": 1 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json index 729dff5584..0edb53f506 100644 --- a/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json @@ -1,144 +1,106 @@ { "constraints": { - "And": [ + "Reify": [ { "clean": false, "etype": null }, - [ - { - "Or": [ - { - "clean": false, - "etype": null - }, - [ - { - "Neq": [ - { - "clean": false, - "etype": null - }, - { - "Reference": [ - { - "clean": false, - "etype": null - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false, - "etype": null - }, - { - "MachineName": 0 - } - ] - } - ] - }, - { - "Eq": [ - { - "clean": false, - "etype": null - }, - { - "Reference": [ - { - "clean": false, - "etype": null - }, - { - "UserName": "c" - } - ] - }, - { - "Constant": [ - { - "clean": false, - "etype": null - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "DivEq": [ - { - "clean": false, - "etype": null - }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ { - "Reference": [ + "DivEq": [ { "clean": false, "etype": null }, { - "UserName": "b" - } - ] - }, - { - "Reference": [ + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, { - "clean": false, - "etype": null + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] }, { - "UserName": "c" + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] } ] }, { - "Reference": [ + "Neq": [ { "clean": false, "etype": null }, { - "MachineName": 0 + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 0 + } + ] } ] } ] - } - ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": false + } + ] + } ] }, "next_var": 1, "variables": [ - [ - { - "MachineName": 0 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - 0, - 3 - ] - } - ] - } - } - ], [ { "UserName": "a" diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/config.toml b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.eprime b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.eprime new file mode 100644 index 0000000000..94389448a2 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.eprime @@ -0,0 +1,3 @@ +language ESSENCE' 1.0 +given x,y :int(1..50) such that + x + 10 + 20 + y + 5 = 100 diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-minion.solutions.json new file mode 100644 index 0000000000..655db490bb --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-minion.solutions.json @@ -0,0 +1,146 @@ +[ + { + "UserName(x)": 15, + "UserName(y)": 50 + }, + { + "UserName(x)": 16, + "UserName(y)": 49 + }, + { + "UserName(x)": 17, + "UserName(y)": 48 + }, + { + "UserName(x)": 18, + "UserName(y)": 47 + }, + { + "UserName(x)": 19, + "UserName(y)": 46 + }, + { + "UserName(x)": 20, + "UserName(y)": 45 + }, + { + "UserName(x)": 21, + "UserName(y)": 44 + }, + { + "UserName(x)": 22, + "UserName(y)": 43 + }, + { + "UserName(x)": 23, + "UserName(y)": 42 + }, + { + "UserName(x)": 24, + "UserName(y)": 41 + }, + { + "UserName(x)": 25, + "UserName(y)": 40 + }, + { + "UserName(x)": 26, + "UserName(y)": 39 + }, + { + "UserName(x)": 27, + "UserName(y)": 38 + }, + { + "UserName(x)": 28, + "UserName(y)": 37 + }, + { + "UserName(x)": 29, + "UserName(y)": 36 + }, + { + "UserName(x)": 30, + "UserName(y)": 35 + }, + { + "UserName(x)": 31, + "UserName(y)": 34 + }, + { + "UserName(x)": 32, + "UserName(y)": 33 + }, + { + "UserName(x)": 33, + "UserName(y)": 32 + }, + { + "UserName(x)": 34, + "UserName(y)": 31 + }, + { + "UserName(x)": 35, + "UserName(y)": 30 + }, + { + "UserName(x)": 36, + "UserName(y)": 29 + }, + { + "UserName(x)": 37, + "UserName(y)": 28 + }, + { + "UserName(x)": 38, + "UserName(y)": 27 + }, + { + "UserName(x)": 39, + "UserName(y)": 26 + }, + { + "UserName(x)": 40, + "UserName(y)": 25 + }, + { + "UserName(x)": 41, + "UserName(y)": 24 + }, + { + "UserName(x)": 42, + "UserName(y)": 23 + }, + { + "UserName(x)": 43, + "UserName(y)": 22 + }, + { + "UserName(x)": 44, + "UserName(y)": 21 + }, + { + "UserName(x)": 45, + "UserName(y)": 20 + }, + { + "UserName(x)": 46, + "UserName(y)": 19 + }, + { + "UserName(x)": 47, + "UserName(y)": 18 + }, + { + "UserName(x)": 48, + "UserName(y)": 17 + }, + { + "UserName(x)": 49, + "UserName(y)": 16 + }, + { + "UserName(x)": 50, + "UserName(y)": 15 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-parse.serialised.json new file mode 100644 index 0000000000..b170804ab9 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-parse.serialised.json @@ -0,0 +1,153 @@ +{ + "constraints": { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 20 + } + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 100 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..09d6631b44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json @@ -0,0 +1,135 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "SumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 65 + } + ] + } + ] + }, + { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 65 + } + ] + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/config.toml b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.eprime b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.eprime new file mode 100644 index 0000000000..c69f546a71 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.eprime @@ -0,0 +1,8 @@ +language ESSENCE' 1.0 + +find a,b,c : bool such that + +a \/ b \/ false, +$ this alldiff should not end up in the final model +allDiff([1,2,3]) \/ true, +(c /\ true) diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-minion.solutions.json new file mode 100644 index 0000000000..2357b354e3 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-minion.solutions.json @@ -0,0 +1,17 @@ +[ + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 0, + "UserName(c)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json new file mode 100644 index 0000000000..254436f7a4 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json @@ -0,0 +1,124 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": false + } + ] + } + ] + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..aa28296e44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json @@ -0,0 +1,91 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/rewrite_tests.rs b/conjure_oxide/tests/rewrite_tests.rs index 7c96c29be0..607698a801 100644 --- a/conjure_oxide/tests/rewrite_tests.rs +++ b/conjure_oxide/tests/rewrite_tests.rs @@ -137,7 +137,7 @@ fn simplify_expression(expr: Expression) -> Expression { #[test] fn rule_sum_constants() { - let sum_constants = get_rule_by_name("sum_constants").unwrap(); + let sum_constants = get_rule_by_name("partial_evaluator").unwrap(); let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap(); let mut expr = Expression::Sum( @@ -164,36 +164,6 @@ fn rule_sum_constants() { ); } -#[test] -fn rule_sum_mixed() { - let sum_constants = get_rule_by_name("sum_constants").unwrap(); - - let mut expr = Expression::Sum( - Metadata::new(), - vec![ - Expression::Constant(Metadata::new(), Constant::Int(1)), - Expression::Constant(Metadata::new(), Constant::Int(2)), - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - ], - ); - - expr = sum_constants - .apply(&expr, &Model::new_empty(Default::default())) - .unwrap() - .new_expression; - - assert_eq!( - expr, - Expression::Sum( - Metadata::new(), - vec![ - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - Expression::Constant(Metadata::new(), Constant::Int(3)), - ] - ) - ); -} - #[test] fn rule_sum_geq() { let flatten_sum_geq = get_rule_by_name("flatten_sum_geq").unwrap(); @@ -238,7 +208,7 @@ fn rule_sum_geq() { #[test] fn reduce_solve_xyz() { println!("Rules: {:?}", get_rules()); - let sum_constants = get_rule_by_name("sum_constants").unwrap(); + let sum_constants = get_rule_by_name("partial_evaluator").unwrap(); let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap(); let lt_to_ineq = get_rule_by_name("lt_to_ineq").unwrap(); let sum_leq_to_sumleq = get_rule_by_name("sum_leq_to_sumleq").unwrap(); @@ -519,88 +489,6 @@ fn remove_trivial_and_or() { ); } -#[test] -fn rule_remove_constants_from_or() { - let remove_constants_from_or = get_rule_by_name("remove_constants_from_or").unwrap(); - - let mut expr = Expression::Or( - Metadata::new(), - vec![ - Expression::Constant(Metadata::new(), Constant::Bool(true)), - Expression::Constant(Metadata::new(), Constant::Bool(false)), - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - ], - ); - - expr = remove_constants_from_or - .apply(&expr, &Model::new_empty(Default::default())) - .unwrap() - .new_expression; - - assert_eq!( - expr, - Expression::Constant(Metadata::new(), Constant::Bool(true)) - ); -} - -#[test] -fn rule_remove_constants_from_and() { - let remove_constants_from_and = get_rule_by_name("remove_constants_from_and").unwrap(); - - let mut expr = Expression::And( - Metadata::new(), - vec![ - Expression::Constant(Metadata::new(), Constant::Bool(true)), - Expression::Constant(Metadata::new(), Constant::Bool(false)), - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - ], - ); - - expr = remove_constants_from_and - .apply(&expr, &Model::new_empty(Default::default())) - .unwrap() - .new_expression; - - assert_eq!( - expr, - Expression::Constant(Metadata::new(), Constant::Bool(false)) - ); -} - -#[test] -fn remove_constants_from_or_not_changed() { - let remove_constants_from_or = get_rule_by_name("remove_constants_from_or").unwrap(); - - let expr = Expression::Or( - Metadata::new(), - vec![ - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - Expression::Reference(Metadata::new(), Name::UserName(String::from("b"))), - ], - ); - - let result = remove_constants_from_or.apply(&expr, &Model::new_empty(Default::default())); - - assert!(result.is_err()); -} - -#[test] -fn remove_constants_from_and_not_changed() { - let remove_constants_from_and = get_rule_by_name("remove_constants_from_and").unwrap(); - - let expr = Expression::And( - Metadata::new(), - vec![ - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - Expression::Reference(Metadata::new(), Name::UserName(String::from("b"))), - ], - ); - - let result = remove_constants_from_and.apply(&expr, &Model::new_empty(Default::default())); - - assert!(result.is_err()); -} - #[test] fn rule_distribute_not_over_and() { let distribute_not_over_and = get_rule_by_name("distribute_not_over_and").unwrap(); diff --git a/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index da34e18bd8..bd34ef5996 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -122,10 +122,13 @@ pub enum Expression { /// #[compatible(Minion)] WatchedLiteral(Metadata, Name, Constant), + + #[compatible(Minion)] + Reify(Metadata, Box, Box), } fn expr_vec_to_domain_i32( - exprs: &Vec, + exprs: &[Expression], op: fn(i32, i32) -> Option, vars: &SymbolTable, ) -> Option { @@ -236,6 +239,7 @@ impl Expression { Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool? Expression::Nothing => None, Expression::WatchedLiteral(_, _, _) => Some(ReturnType::Bool), + Expression::Reify(_, _, _) => Some(ReturnType::Bool), } } @@ -336,6 +340,9 @@ impl Expression { Expression::WatchedLiteral(metadata, name, constant) => { metadata.clean = bool_value; } + Expression::Reify(metadata, _, _) => { + metadata.clean = bool_value; + } } } } diff --git a/crates/conjure_core/src/rule_engine/resolve_rules.rs b/crates/conjure_core/src/rule_engine/resolve_rules.rs index deb4d55a37..c2ee869b1e 100644 --- a/crates/conjure_core/src/rule_engine/resolve_rules.rs +++ b/crates/conjure_core/src/rule_engine/resolve_rules.rs @@ -89,8 +89,8 @@ pub fn resolve_rule_sets<'a>( /// - A map of rules to their priorities. pub fn get_rule_priorities<'a>( rule_sets: &Vec<&'a RuleSet<'a>>, -) -> Result, u8>, ResolveRulesError> { - let mut rule_priorities: HashMap<&'a Rule<'a>, (&'a RuleSet<'a>, u8)> = HashMap::new(); +) -> Result, u16>, ResolveRulesError> { + let mut rule_priorities: HashMap<&'a Rule<'a>, (&'a RuleSet<'a>, u16)> = HashMap::new(); for rs in rule_sets { for (rule, priority) in rs.get_rules() { @@ -104,7 +104,7 @@ pub fn get_rule_priorities<'a>( } } - let mut ans: HashMap<&'a Rule<'a>, u8> = HashMap::new(); + let mut ans: HashMap<&'a Rule<'a>, u16> = HashMap::new(); for (rule, (_, priority)) in rule_priorities { ans.insert(rule, priority); } @@ -128,7 +128,7 @@ pub fn get_rule_priorities<'a>( pub fn rule_cmp<'a>( a: &Rule<'a>, b: &Rule<'a>, - rule_priorities: &HashMap<&'a Rule<'a>, u8>, + rule_priorities: &HashMap<&'a Rule<'a>, u16>, ) -> std::cmp::Ordering { let a_priority = *rule_priorities.get(a).unwrap_or(&0); let b_priority = *rule_priorities.get(b).unwrap_or(&0); @@ -147,7 +147,7 @@ pub fn rule_cmp<'a>( /// /// # Returns /// - A list of rules sorted by their priorities and names. -pub fn get_rules_vec<'a>(rule_priorities: &HashMap<&'a Rule<'a>, u8>) -> Vec<&'a Rule<'a>> { +pub fn get_rules_vec<'a>(rule_priorities: &HashMap<&'a Rule<'a>, u16>) -> Vec<&'a Rule<'a>> { let mut rules: Vec<&'a Rule<'a>> = rule_priorities.keys().copied().collect(); rules.sort_by(|a, b| rule_cmp(a, b, rule_priorities)); rules diff --git a/crates/conjure_core/src/rule_engine/rule.rs b/crates/conjure_core/src/rule_engine/rule.rs index 99a698429f..14675dfaed 100644 --- a/crates/conjure_core/src/rule_engine/rule.rs +++ b/crates/conjure_core/src/rule_engine/rule.rs @@ -131,14 +131,14 @@ impl Reduction { pub struct Rule<'a> { pub name: &'a str, pub application: fn(&Expression, &Model) -> ApplicationResult, - pub rule_sets: &'a [(&'a str, u8)], // (name, priority). At runtime, we add the rule to rulesets + pub rule_sets: &'a [(&'a str, u16)], // (name, priority). At runtime, we add the rule to rulesets } impl<'a> Rule<'a> { pub const fn new( name: &'a str, application: fn(&Expression, &Model) -> ApplicationResult, - rule_sets: &'a [(&'static str, u8)], + rule_sets: &'a [(&'static str, u16)], ) -> Self { Self { name, diff --git a/crates/conjure_core/src/rule_engine/rule_set.rs b/crates/conjure_core/src/rule_engine/rule_set.rs index f290abdacc..aeece6df99 100644 --- a/crates/conjure_core/src/rule_engine/rule_set.rs +++ b/crates/conjure_core/src/rule_engine/rule_set.rs @@ -33,9 +33,9 @@ pub struct RuleSet<'a> { pub name: &'a str, /// Order of the RuleSet. Used to establish a consistent order of operations when resolving rules. /// If two RuleSets overlap (contain the same rule but with different priorities), the RuleSet with the higher order will be used as the source of truth. - pub order: u8, + pub order: u16, /// A map of rules to their priorities. This will be lazily initialized at runtime. - rules: OnceLock, u8>>, + rules: OnceLock, u16>>, /// The names of the rule sets that this rule set depends on. dependency_rs_names: &'a [&'a str], dependencies: OnceLock>>, @@ -46,7 +46,7 @@ pub struct RuleSet<'a> { impl<'a> RuleSet<'a> { pub const fn new( name: &'a str, - order: u8, + order: u16, dependencies: &'a [&'a str], solver_families: &'a [SolverFamily], ) -> Self { @@ -61,8 +61,8 @@ impl<'a> RuleSet<'a> { } /// Get the rules of this rule set, evaluating them lazily if necessary - /// Returns a `&HashMap<&Rule, u8>` where the key is the rule and the value is the priority of the rule. - pub fn get_rules(&self) -> &HashMap<&'a Rule<'a>, u8> { + /// Returns a `&HashMap<&Rule, u16>` where the key is the rule and the value is the priority of the rule. + pub fn get_rules(&self) -> &HashMap<&'a Rule<'a>, u16> { match self.rules.get() { None => { let rules = self.resolve_rules(); @@ -104,12 +104,12 @@ impl<'a> RuleSet<'a> { } /// Resolve the rules of this rule set ("reverse the arrows") - fn resolve_rules(&self) -> HashMap<&'a Rule<'a>, u8> { + fn resolve_rules(&self) -> HashMap<&'a Rule<'a>, u16> { let mut rules = HashMap::new(); for rule in get_rules() { let mut found = false; - let mut priority: u8 = 0; + let mut priority: u16 = 0; for (name, p) in rule.rule_sets { if *name == self.name { diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs index 3382d0fa30..73914893f7 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -10,7 +10,7 @@ use uniplate::Uniplate; /* This file contains basic rules for simplifying expressions */ /*****************************************************************************/ -register_rule_set!("Base", 150, ()); +register_rule_set!("Base", 100, ()); /** * Remove nothing's from expressions: @@ -21,7 +21,7 @@ register_rule_set!("Base", 150, ()); * ... * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult { fn remove_nothings(exprs: Vec) -> Result, ApplicationError> { let mut changed = false; @@ -83,7 +83,7 @@ fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult { * [] = Nothing * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn empty_to_nothing(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Nothing @@ -100,46 +100,13 @@ fn empty_to_nothing(expr: &Expr, _: &Model) -> ApplicationResult { } } -/** - * Evaluate sum of constants: - * ```text - * sum([1, 2, 3]) = 6 - * ``` - */ -#[register_rule(("Base", 100))] -fn sum_constants(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Sum(_, exprs) => { - let mut sum = 0; - let mut new_exprs = Vec::new(); - let mut changed = false; - for e in exprs { - match e { - Expr::Constant(_metadata, Const::Int(i)) => { - sum += i; - changed = true; - } - _ => new_exprs.push(e.clone()), - } - } - if !changed { - return Err(ApplicationError::RuleNotApplicable); - } - // TODO (kf77): Get existing metadata instead of creating a new one - new_exprs.push(Expr::Constant(Metadata::new(), Const::Int(sum))); - Ok(Reduction::pure(Expr::Sum(Metadata::new(), new_exprs))) // Let other rules handle only one Expr being contained in the sum - } - _ => Err(ApplicationError::RuleNotApplicable), - } -} - /** * Unwrap trivial sums: * ```text * sum([a]) = a * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn unwrap_sum(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Sum(_, exprs) if (exprs.len() == 1) => Ok(Reduction::pure(exprs[0].clone())), @@ -153,7 +120,7 @@ fn unwrap_sum(expr: &Expr, _: &Model) -> ApplicationResult { * sum(sum(a, b), c) = sum(a, b, c) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] pub fn flatten_nested_sum(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Sum(metadata, exprs) => { @@ -189,7 +156,7 @@ pub fn flatten_nested_sum(expr: &Expr, _: &Model) -> ApplicationResult { * or(or(a, b), c) = or(a, b, c) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn unwrap_nested_or(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Or(metadata, exprs) => { @@ -222,7 +189,7 @@ fn unwrap_nested_or(expr: &Expr, _: &Model) -> ApplicationResult { * and(and(a, b), c) = and(a, b, c) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn unwrap_nested_and(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::And(metadata, exprs) => { @@ -258,7 +225,7 @@ fn unwrap_nested_and(expr: &Expr, _: &Model) -> ApplicationResult { * not(not(a)) = a * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8400))] fn remove_double_negation(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Not(_, contents) => match contents.as_ref() { @@ -275,7 +242,7 @@ fn remove_double_negation(expr: &Expr, _: &Model) -> ApplicationResult { * and([a]) = a * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn remove_trivial_and(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::And(_, exprs) => { @@ -294,7 +261,7 @@ fn remove_trivial_and(expr: &Expr, _: &Model) -> ApplicationResult { * or([a]) = a * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn remove_trivial_or(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Or(_, exprs) => { @@ -308,6 +275,7 @@ fn remove_trivial_or(expr: &Expr, _: &Model) -> ApplicationResult { } /** +<<<<<<< HEAD * Remove constant bools from or expressions * ```text * or([true, a]) = true @@ -410,12 +378,12 @@ fn evaluate_constant_not(expr: &Expr, _: &Model) -> ApplicationResult { } /** - * Turn a Min into a new variable and post a top level constraint to ensure the new variable is the minimum. + * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum. * ```text * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 2000))] fn min_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult { match expr { Expr::Min(metadata, exprs) => { @@ -504,7 +472,7 @@ fn max_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult { * or(and(a, b), c) = and(or(a, c), or(b, c)) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8400))] fn distribute_or_over_and(expr: &Expr, _: &Model) -> ApplicationResult { fn find_and(exprs: &[Expr]) -> Option { // ToDo: may be better to move this to some kind of utils module? @@ -554,7 +522,7 @@ fn distribute_or_over_and(expr: &Expr, _: &Model) -> ApplicationResult { * not(and(a, b)) = or(not a, not b) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8400))] fn distribute_not_over_and(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Not(_, contents) => match contents.as_ref() { @@ -585,7 +553,7 @@ fn distribute_not_over_and(expr: &Expr, _: &Model) -> ApplicationResult { * not(or(a, b)) = and(not a, not b) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8400))] fn distribute_not_over_or(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Not(_, contents) => match contents.as_ref() { diff --git a/crates/conjure_core/src/rules/bubble.rs b/crates/conjure_core/src/rules/bubble.rs index d94a6b0483..f9b17c0edc 100644 --- a/crates/conjure_core/src/rules/bubble.rs +++ b/crates/conjure_core/src/rules/bubble.rs @@ -6,7 +6,7 @@ use conjure_core::rule_engine::{ use conjure_core::Model; use uniplate::Uniplate; -register_rule_set!("Bubble", 254, ("Base")); +register_rule_set!("Bubble", 100, ("Base")); // Bubble reduction rules @@ -15,7 +15,7 @@ register_rule_set!("Bubble", 254, ("Base")); e.g. (a / b = c) @ (b != 0) => (a / b = c) & (b != 0) */ -#[register_rule(("Bubble", 100))] +#[register_rule(("Bubble", 8900))] fn expand_bubble(expr: &Expression, _: &Model) -> ApplicationResult { match expr { Expression::Bubble(_, a, b) if a.return_type() == Some(ReturnType::Bool) => { @@ -33,7 +33,7 @@ fn expand_bubble(expr: &Expression, _: &Model) -> ApplicationResult { E.g. ((a / b) @ (b != 0)) = c => (a / b = c) @ (b != 0) */ -#[register_rule(("Bubble", 100))] +#[register_rule(("Bubble", 8900))] fn bubble_up(expr: &Expression, _: &Model) -> ApplicationResult { let mut sub = expr.children(); let mut bubbled_conditions = vec![]; @@ -66,7 +66,7 @@ fn bubble_up(expr: &Expression, _: &Model) -> ApplicationResult { E.g. a / b => (a / b) @ (b != 0) */ -#[register_rule(("Bubble", 100))] +#[register_rule(("Bubble", 6000))] fn div_to_bubble(expr: &Expression, _: &Model) -> ApplicationResult { if let Expression::UnsafeDiv(_, a, b) = expr { return Ok(Reduction::pure(Expression::Bubble( diff --git a/crates/conjure_core/src/rules/constant.rs b/crates/conjure_core/src/rules/constant.rs index aacbe10bb7..d072cb3b29 100644 --- a/crates/conjure_core/src/rules/constant.rs +++ b/crates/conjure_core/src/rules/constant.rs @@ -5,9 +5,9 @@ use conjure_core::rule_engine::{ }; use conjure_core::Model; -register_rule_set!("Constant", 255, ()); +register_rule_set!("Constant", 100, ()); -#[register_rule(("Constant", 255))] +#[register_rule(("Constant", 9001))] fn apply_eval_constant(expr: &Expr, _: &Model) -> ApplicationResult { if let Expr::Constant(_, _) = expr { return Err(ApplicationError::RuleNotApplicable); diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index cc74026e33..5320499c2f 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -66,7 +66,7 @@ fn sum_to_vector(expr: &Expr) -> Result, ApplicationError> { * sum([a, b, c]) >= d => sum_geq([a, b, c], d) * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn flatten_sum_geq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Geq(metadata, a, b) => { @@ -87,7 +87,7 @@ fn flatten_sum_geq(expr: &Expr, _: &Model) -> ApplicationResult { * sum([a, b, c]) <= d => sum_leq([a, b, c], d) * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn sum_leq_to_sumleq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Leq(metadata, a, b) => { @@ -108,7 +108,7 @@ fn sum_leq_to_sumleq(expr: &Expr, _: &Model) -> ApplicationResult { * eq(sum([a, b]), c) => sumeq([a, b], c) * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Eq(metadata, a, b) => { @@ -147,7 +147,7 @@ fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { * a + b = c * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn sumeq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::SumEq(metadata, exprs, eq_to) => Ok(Reduction::pure(Expr::And( @@ -168,7 +168,7 @@ fn sumeq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult { * a < b => a - b < -1 * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4100))] fn lt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Lt(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq( @@ -188,7 +188,7 @@ fn lt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { * a > b => b - a < -1 * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4100))] fn gt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Gt(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq( @@ -208,7 +208,7 @@ fn gt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { * a >= b => b - a < 0 * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4100))] fn geq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Geq(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq( @@ -228,7 +228,7 @@ fn geq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { * a <= b => a - b < 0 * ``` */ -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4100))] fn leq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Leq(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq( @@ -260,7 +260,7 @@ fn leq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { /** * Since Minion doesn't support some constraints with div (e.g. leq, neq), we add an auxiliary variable to represent the division result. */ -#[register_rule(("Minion", 101))] +#[register_rule(("Minion", 4400))] fn flatten_safediv(expr: &Expr, mdl: &Model) -> ApplicationResult { use Expr::*; match expr { @@ -307,7 +307,7 @@ fn flatten_safediv(expr: &Expr, mdl: &Model) -> ApplicationResult { Err(ApplicationError::RuleNotApplicable) } -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn div_eq_to_diveq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Eq(metadata, a, b) => { @@ -346,7 +346,7 @@ fn div_eq_to_diveq(expr: &Expr, _: &Model) -> ApplicationResult { } } -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn negated_neq_to_eq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Not(_, a) => match a.as_ref() { @@ -367,7 +367,7 @@ fn negated_neq_to_eq(expr: &Expr, _: &Model) -> ApplicationResult { } } -#[register_rule(("Minion", 100))] +#[register_rule(("Minion", 4400))] fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Not(_, a) => match a.as_ref() { @@ -403,7 +403,7 @@ fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult { /// /// This restates boolean variables as the equivalent constraint "SAT if x is true". /// -#[register_rule(("Minion", 50))] +#[register_rule(("Minion", 4100))] fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult { use Domain::BoolDomain; use Expr::*; @@ -473,3 +473,30 @@ fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult { _ => Err(RuleNotApplicable), } } + +/// Flattening rule for not(X) in Minion, where X is a constraint. +/// +/// ```text +/// not(X) ~> reify(X,0) +/// ``` +/// +/// This rule has lower priority than boolean_literal_to_wliteral so that we can assume that the +/// nested expressions are constraints not variables. + +#[register_rule(("Minion", 4090))] +fn not_constraint_to_reify(expr: &Expr, _: &Model) -> ApplicationResult { + use Expr::*; + if !matches!(expr, Not(_,c) if !matches!(**c, Reference(_,_)|Constant(_,_))) { + return Err(RuleNotApplicable); + } + + let Not(m, e) = expr else { + unreachable!(); + }; + + Ok(Reduction::pure(Reify( + m.clone(), + e.clone(), + Box::new(Constant(Metadata::new(), Const::Bool(false))), + ))) +} diff --git a/crates/conjure_core/src/rules/mod.rs b/crates/conjure_core/src/rules/mod.rs index 900402d6c4..825a81c036 100644 --- a/crates/conjure_core/src/rules/mod.rs +++ b/crates/conjure_core/src/rules/mod.rs @@ -1,3 +1,9 @@ +//! This module contains the rewrite rules for Conjure Oxides and it's solvers. +//! +//! # Rule Semantics +//! +#![doc = include_str!("./rule_semantics.md")] + pub use constant::eval_constant; mod base; diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs index 73641542c4..208013ce60 100644 --- a/crates/conjure_core/src/rules/partial_eval.rs +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -6,7 +6,7 @@ use crate::ast::{Constant as Const, Expression as Expr}; use crate::rule_engine::{ApplicationResult, Reduction}; use crate::Model; -#[register_rule(("Base",200))] +#[register_rule(("Base",9000))] fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { use conjure_core::rule_engine::ApplicationError::RuleNotApplicable; use Expr::*; @@ -275,5 +275,6 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { } WatchedLiteral(_, _, _) => Err(RuleNotApplicable), + Reify(_, _, _) => Err(RuleNotApplicable), } } diff --git a/crates/conjure_core/src/rules/rule_semantics.md b/crates/conjure_core/src/rules/rule_semantics.md new file mode 100644 index 0000000000..abd0cd5e6d --- /dev/null +++ b/crates/conjure_core/src/rules/rule_semantics.md @@ -0,0 +1,16 @@ +## Priorities + +Rule are applied in priority order (highest number first). + +Rule priority levels are currently the following: + +| Priority level | Usage | +| --- | ----- | +| **9001** | **Total evaluation** | +| **9000** | **Partial evaluation** | +| 8800 | Trivial simplifications: removing nesting, removing empty / unit constraints | +| 8400 | Transformation into canonical forms: (distributivity, associativity, commutativity, etc.) | +| **8000** | **Simplifications** | +| **6000** | **Modelling enhancing reformulations** | +| **4000** | **Solver Specific** | +| **2000** | **Non solver specific, non enhancing reformulations** (e.g. restate a constraint using simpler constraints when needed for solver compatability) | diff --git a/crates/conjure_core/src/solver/adaptors/minion.rs b/crates/conjure_core/src/solver/adaptors/minion.rs index 8e1811046e..298a12679e 100644 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ b/crates/conjure_core/src/solver/adaptors/minion.rs @@ -288,6 +288,12 @@ fn read_expr(expr: conjure_ast::Expression) -> Result, SolverError>>()?, )), + conjure_ast::Expression::And(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedAnd( + exprs + .iter() + .map(|x| read_expr(x.to_owned())) + .collect::, SolverError>>()?, + )), conjure_ast::Expression::Eq(_metadata, a, b) => { Ok(minion_ast::Constraint::Eq(read_var(*a)?, read_var(*b)?)) } @@ -298,6 +304,10 @@ fn read_expr(expr: conjure_ast::Expression) -> Result Ok(minion_ast::Constraint::Reify( + Box::new(read_expr(*e)?), + read_var(*v)?, + )), x => Err(ModelFeatureNotSupported(format!("{:?}", x))), } } diff --git a/crates/conjure_macros/src/lib.rs b/crates/conjure_macros/src/lib.rs index b0c39595fb..4258a6ce84 100644 --- a/crates/conjure_macros/src/lib.rs +++ b/crates/conjure_macros/src/lib.rs @@ -58,7 +58,7 @@ pub fn register_rule(arg_tokens: TokenStream, item: TokenStream) -> TokenStream let rule_set_name = &rule_set.rule_set; let priority = &rule_set.priority; quote! { - (#rule_set_name, #priority as u8) + (#rule_set_name, #priority as u16) } }) .collect::>(); From 9f326e46f50bf6a9b6442dc771fa2514ea25db90 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 12 Oct 2024 13:46:39 +0100 Subject: [PATCH 8/9] fix: add test case for soph's non-terminating min problem Soph (sm600) reported that the added model never terminated. Recent changes to the rule system (likely b25c3bbe2 (change rule priorities to run simplifiers first; add reify, 2024-10-12)) has fixed this. Co-authored-by: Soph --- .../sm600-non-terminating-min/config.toml | 1 + .../sm600-non-terminating-min/input.essence | 5 + .../input.expected-minion.solutions.json | 202 ++++++++++++++ .../input.expected-parse.serialised.json | 111 ++++++++ .../input.expected-rewrite.serialised.json | 250 ++++++++++++++++++ 5 files changed, 569 insertions(+) create mode 100644 conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml create mode 100644 conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence create mode 100644 conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence new file mode 100644 index 0000000000..29087c0d99 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence @@ -0,0 +1,5 @@ +$ test case by sm600, 11/10/2024 +$ this would never terminate + +find a,b : int(1..7) +such that min([a,b]) + 6 <= 10 diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json new file mode 100644 index 0000000000..f8773303c0 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json @@ -0,0 +1,202 @@ +[ + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 2 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 3 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 4 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 5 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 6 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 7 + }, + { + "MachineName(0)": 1, + "UserName(a)": 2, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 3, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 4, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 5, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 6, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 7, + "UserName(b)": 1 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 3 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 4 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 5 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 6 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 7 + }, + { + "MachineName(0)": 2, + "UserName(a)": 3, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 4, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 5, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 6, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 7, + "UserName(b)": 2 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 4 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 5 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 6 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 7 + }, + { + "MachineName(0)": 3, + "UserName(a)": 4, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 5, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 6, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 7, + "UserName(b)": 3 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 4 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 5 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 6 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 7 + }, + { + "MachineName(0)": 4, + "UserName(a)": 5, + "UserName(b)": 4 + }, + { + "MachineName(0)": 4, + "UserName(a)": 6, + "UserName(b)": 4 + }, + { + "MachineName(0)": 4, + "UserName(a)": 7, + "UserName(b)": 4 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json new file mode 100644 index 0000000000..08be1f5ad8 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json @@ -0,0 +1,111 @@ +{ + "constraints": { + "Leq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Min": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 6 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..a6a1af1be3 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json @@ -0,0 +1,250 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 4 + } + ] + } + ] + }, + { + "Ineq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 0 + } + ] + } + ] + }, + { + "Ineq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 0 + } + ] + } + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + } + ] + }, + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 1, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ], + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file From a9b71f1a760060f2aefd28f5a11c25d55ad26dc1 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Mon, 14 Oct 2024 15:43:52 +0100 Subject: [PATCH 9/9] fix: empty or([]) being parsed as nothing Constant matrices inside operations were not recognised by our parser, so were ignored. This includes expressions like or([]) and min([1,2,3]). - Add parsing support for constant matrices inside operations. - Add support for top level "false" and "true" with Minion. Ideally, these models would never get passed to the solver; however, this would require solution evaluation and a refactor of our tester, so I have left this for future work. Fixes #366. --- conjure_oxide/src/main.rs | 6 +- .../input.essence | 7 ++ .../input.expected-minion.solutions.json | 1 + .../input.expected-parse.serialised.json | 31 ++++++ .../input.expected-rewrite.serialised.json | 33 +++++++ .../input.essence | 5 + .../input.expected-minion.solutions.json | 17 ++++ .../input.expected-parse.serialised.json | 94 +++++++++++++++++++ .../input.expected-rewrite.serialised.json | 54 +++++++++++ .../input.expected-parse.serialised.json | 64 +++++++++++++ .../input.expected-parse.serialised.json | 64 +++++++++++++ crates/conjure_core/src/parse/parse_model.rs | 78 +++++++++++++-- crates/conjure_core/src/rules/base.rs | 44 +++++---- .../src/solver/adaptors/minion.rs | 23 ++++- solvers/minion/src/ast.rs | 2 + solvers/minion/src/run.rs | 5 + 16 files changed, 497 insertions(+), 31 deletions(-) create mode 100644 conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.essence create mode 100644 conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json create mode 100644 conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence create mode 100644 conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json diff --git a/conjure_oxide/src/main.rs b/conjure_oxide/src/main.rs index b37910c6cf..00da3b4737 100644 --- a/conjure_oxide/src/main.rs +++ b/conjure_oxide/src/main.rs @@ -97,10 +97,10 @@ pub fn main() -> AnyhowResult<()> { .append(true) .open("conjure_oxide.log")?; - //Builder::with_level("Trace") - Builder::new() + Builder::with_level("TRACE") + //Builder::new() .with_target_writer("info", new_writer(stdout())) - .with_target_writer("file", new_writer(log_file)) + .with_target_writer("file,jsonparser", new_writer(log_file)) .init(); if target_family != SolverFamily::Minion { diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.essence b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.essence new file mode 100644 index 0000000000..f471740fb1 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.essence @@ -0,0 +1,7 @@ + +$ "By mathematical tradition (and Essence semantics), an 'empty or' is false, however, this model has 5 answers (one for each value of a)" +$ -- https://github.com/conjure-cp/conjure-oxide/issues/366 + +find a : int(1..5) +such that +or([]) diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json new file mode 100644 index 0000000000..0637a088a0 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json @@ -0,0 +1 @@ +[] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json new file mode 100644 index 0000000000..081ff69222 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json @@ -0,0 +1,31 @@ +{ + "constraints": { + "Or": [ + { + "clean": false, + "etype": null + }, + [] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..6d33b6e63d --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json @@ -0,0 +1,33 @@ +{ + "constraints": { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": false + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence new file mode 100644 index 0000000000..094a8cfefb --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence @@ -0,0 +1,5 @@ +$ the parser would read the min as Nothing... +$ related: issue-366 + +find c : int(1..7) +such that min([5,7]) + c <= 10 diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json new file mode 100644 index 0000000000..7509f68790 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json @@ -0,0 +1,17 @@ +[ + { + "UserName(c)": 1 + }, + { + "UserName(c)": 2 + }, + { + "UserName(c)": 3 + }, + { + "UserName(c)": 4 + }, + { + "UserName(c)": 5 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json new file mode 100644 index 0000000000..299cb30c6c --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json @@ -0,0 +1,94 @@ +{ + "constraints": { + "Leq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Min": [ + { + "clean": false, + "etype": null + }, + [ + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 7 + } + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..11311f4a71 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json @@ -0,0 +1,54 @@ +{ + "constraints": { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + } + ] + }, + "next_var": 1, + "variables": [ + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json index 254436f7a4..4dcc11f11c 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json @@ -59,6 +59,70 @@ ] ] }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "AllDiff": [ + { + "clean": false, + "etype": null + }, + [ + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 1 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 2 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 3 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + }, { "And": [ { diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json index 254436f7a4..4dcc11f11c 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json @@ -59,6 +59,70 @@ ] ] }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "AllDiff": [ + { + "clean": false, + "etype": null + }, + [ + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 1 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 2 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 3 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + }, { "And": [ { diff --git a/crates/conjure_core/src/parse/parse_model.rs b/crates/conjure_core/src/parse/parse_model.rs index 7265928f2e..1ec2889ab7 100644 --- a/crates/conjure_core/src/parse/parse_model.rs +++ b/crates/conjure_core/src/parse/parse_model.rs @@ -10,6 +10,18 @@ use crate::error::{Error, Result}; use crate::metadata::Metadata; use crate::Model; +macro_rules! parser_trace { + ($($arg:tt)+) => { + log::trace!(target:"jsonparser",$($arg)+) + }; +} + +macro_rules! parser_debug { + ($($arg:tt)+) => { + log::debug!(target:"jsonparser",$($arg)+) + }; +} + pub fn model_from_json(str: &str, context: Arc>>) -> Result { let mut m = Model::new_empty(context); let v: JsonValue = serde_json::from_str(str)?; @@ -244,6 +256,10 @@ fn parse_expression(obj: &JsonValue) -> Option { )) } Value::Object(constant) if constant.contains_key("Constant") => parse_constant(constant), + Value::Object(constant) if constant.contains_key("ConstantInt") => parse_constant(constant), + Value::Object(constant) if constant.contains_key("ConstantBool") => { + parse_constant(constant) + } otherwise => panic!("Unhandled Expression {:#?}", otherwise), } } @@ -286,24 +302,46 @@ fn parse_vec_op( let (key, value) = vec_op.into_iter().next()?; let constructor = vec_operators.get(key.as_str())?; - let args_parsed: Vec> = value["AbstractLiteral"]["AbsLitMatrix"][1] - .as_array()? - .iter() - .map(parse_expression) - .collect(); + parser_debug!("Trying to parse vec_op: {key} ..."); + + let mut args_parsed: Option>> = None; + if let Some(abs_lit_matrix) = value.pointer("/AbstractLiteral/AbsLitMatrix/1") { + parser_trace!("... containing a matrix of literals"); + args_parsed = abs_lit_matrix.as_array().map(|x| { + x.iter() + .map(parse_expression) + .collect::>>() + }); + } + // the input of this expression is constant - e.g. or([]), or([false]), min([2]), etc. + else if let Some(const_abs_lit_matrix) = + value.pointer("/Constant/ConstantAbstract/AbsLitMatrix/1") + { + parser_trace!("... containing a matrix of constants"); + args_parsed = const_abs_lit_matrix.as_array().map(|x| { + x.iter() + .map(parse_expression) + .collect::>>() + }); + } + + let args_parsed = args_parsed?; let number_of_args = args_parsed.len(); + parser_debug!("... with {number_of_args} args {args_parsed:#?}"); + let valid_args: Vec = args_parsed.into_iter().flatten().collect(); if number_of_args != valid_args.len() { None } else { + parser_debug!("... success!"); Some(constructor(Metadata::new(), valid_args)) } } fn parse_constant(constant: &serde_json::Map) -> Option { - match &constant["Constant"] { - Value::Object(int) if int.contains_key("ConstantInt") => { + match &constant.get("Constant") { + Some(Value::Object(int)) if int.contains_key("ConstantInt") => { let int_32: i32 = match int["ConstantInt"].as_array()?[1].as_i64()?.try_into() { Ok(x) => x, Err(_) => { @@ -318,10 +356,34 @@ fn parse_constant(constant: &serde_json::Map) -> Option { + Some(Value::Object(b)) if b.contains_key("ConstantBool") => { let b: bool = b["ConstantBool"].as_bool().unwrap(); Some(Expression::Constant(Metadata::new(), Constant::Bool(b))) } + + // sometimes (e.g. constant matrices) we can have a ConstantInt / Constant bool that is + // not wrapped in Constant + None => { + let int_expr = constant["ConstantInt"] + .as_array() + .and_then(|x| x[1].as_i64()) + .and_then(|x| x.try_into().ok()) + .map(|x| Expression::Constant(Metadata::new(), Constant::Int(x))); + + if let e @ Some(_) = int_expr { + return e; + } + + let bool_expr = constant["ConstantBool"] + .as_bool() + .map(|x| Expression::Constant(Metadata::new(), Constant::Bool(x))); + + if let e @ Some(_) = bool_expr { + return e; + } + + panic!("Unhandled parse_constant {:#?}", constant); + } otherwise => panic!("Unhandled parse_constant {:#?}", otherwise), } } diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs index 73914893f7..e2662b971e 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -77,27 +77,33 @@ fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult { } } -/** - * Remove empty expressions: - * ```text - * [] = Nothing - * ``` - */ +/// Remove empty expressions: +/// ```text +/// or([]) ~> false +/// X([]) ~> Nothing +/// ``` #[register_rule(("Base", 8800))] -fn empty_to_nothing(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Nothing - | Expr::Reference(_, _) - | Expr::Constant(_, _) - | Expr::WatchedLiteral(_, _, _) => Err(ApplicationError::RuleNotApplicable), - _ => { - if expr.children().is_empty() { - Ok(Reduction::pure(Expr::Nothing)) - } else { - Err(ApplicationError::RuleNotApplicable) - } - } +fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult { + use Expr::*; + + // excluded expressions + if matches!( + expr, + Nothing | Reference(_, _) | Constant(_, _) | WatchedLiteral(_, _, _) + ) { + return Err(ApplicationError::RuleNotApplicable); + } + + if !expr.children().is_empty() { + return Err(ApplicationError::RuleNotApplicable); } + + let new_expr = match expr { + Or(_, _) => Constant(Metadata::new(), Const::Bool(false)), + _ => Nothing, + }; + + Ok(Reduction::pure(new_expr)) } /** diff --git a/crates/conjure_core/src/solver/adaptors/minion.rs b/crates/conjure_core/src/solver/adaptors/minion.rs index 298a12679e..26b337161e 100644 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ b/crates/conjure_core/src/solver/adaptors/minion.rs @@ -248,7 +248,28 @@ fn parse_exprs( minion_model: &mut MinionModel, ) -> Result<(), SolverError> { for expr in conjure_model.get_constraints_vec().iter() { - parse_expr(expr.to_owned(), minion_model)?; + // TODO: top level false / trues should not go to the solver to begin with + // ... but changing this at this stage would require rewriting the tester + use crate::metadata::Metadata; + use conjure_ast::Constant; + use conjure_ast::Expression as Expr; + + match expr { + // top level false + Expr::Constant(_, Constant::Bool(false)) => { + minion_model.constraints.push(minion_ast::Constraint::False); + return Ok(()); + } + // top level true + Expr::Constant(_, Constant::Bool(true)) => { + minion_model.constraints.push(minion_ast::Constraint::True); + return Ok(()); + } + + _ => { + parse_expr(expr.to_owned(), minion_model)?; + } + } } Ok(()) } diff --git a/solvers/minion/src/ast.rs b/solvers/minion/src/ast.rs index 44bba6e441..09f6c299f4 100644 --- a/solvers/minion/src/ast.rs +++ b/solvers/minion/src/ast.rs @@ -111,6 +111,8 @@ pub enum Constraint { WatchLess(Var, Var), WatchNeq(Var, Var), Ineq(Var, Var, Constant), + False, + True, } /// Representation of a Minion Variable. diff --git a/solvers/minion/src/run.rs b/solvers/minion/src/run.rs index 2cedf739af..8c01aaae89 100644 --- a/solvers/minion/src/run.rs +++ b/solvers/minion/src/run.rs @@ -372,6 +372,8 @@ unsafe fn get_constraint_type(constraint: &Constraint) -> Result Ok(ffi::ConstraintType_CT_GACEQ), Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS), Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ), + Constraint::True => Ok(ffi::ConstraintType_CT_TRUE), + Constraint::False => Ok(ffi::ConstraintType_CT_FALSE), #[allow(unreachable_patterns)] x => Err(MinionError::NotImplemented(format!( @@ -592,6 +594,9 @@ unsafe fn constraint_add_args( read_var(i, r_constr, b)?; Ok(()) } + + Constraint::True => Ok(()), + Constraint::False => Ok(()), #[allow(unreachable_patterns)] x => Err(MinionError::NotImplemented(format!("{:?}", x))), }