diff --git a/conjure_oxide/src/main.rs b/conjure_oxide/src/main.rs index 6347e809de..548f93f903 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 bd2f38feb2..5397f3040b 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)?; @@ -240,6 +252,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), } } @@ -282,24 +298,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(_) => { @@ -314,10 +352,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 e2362000ae..c448863e01 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -79,27 +79,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..0b90842879 100644 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ b/crates/conjure_core/src/solver/adaptors/minion.rs @@ -248,7 +248,40 @@ 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)) => { + parse_expr( + Expr::Eq( + Metadata::new(), + Box::new(Expr::Constant(Metadata::new(), Constant::Int(1))), + Box::new(Expr::Constant(Metadata::new(), Constant::Int(2))), + ), + minion_model, + )?; + } + // top level true + Expr::Constant(_, Constant::Bool(true)) => { + parse_expr( + Expr::Eq( + Metadata::new(), + Box::new(Expr::Constant(Metadata::new(), Constant::Int(1))), + Box::new(Expr::Constant(Metadata::new(), Constant::Int(1))), + ), + minion_model, + )?; + } + + _ => { + parse_expr(expr.to_owned(), minion_model)?; + } + } } Ok(()) }