diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index 671c3a9120..0a936bdfbe 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -54,7 +54,10 @@ fn integration_test(path: &str, essence_base: &str) -> Result<(), Box assert_eq!(model, expected_model); // Stage 2: Rewrite the model using the rule engine and check that the result is as expected - let rule_sets = resolve_rule_sets(SolverFamily::Minion, &vec!["Constant".to_string()])?; + let rule_sets = resolve_rule_sets( + SolverFamily::Minion, + &vec!["Constant".to_string(), "Bubble".to_string()], + )?; let model = rewrite_model(&model, &rule_sets)?; if verbose { println!("Rewritten model: {:#?}", model) diff --git a/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-rewrite.serialised.json index 29b1c529e1..b95b81b273 100644 --- a/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-rewrite.serialised.json @@ -1,31 +1,29 @@ { "constraints": { - "AllDiff": [ + "Neq": [ { "clean": false }, - [ - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "x" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "y" - } - ] - } - ] + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "y" + } + ] + } ] }, "next_var": 0, diff --git a/conjure_oxide/tests/integration/basic/div/01/input.essence.disabled b/conjure_oxide/tests/integration/basic/div/01/input.essence similarity index 100% rename from conjure_oxide/tests/integration/basic/div/01/input.essence.disabled rename to conjure_oxide/tests/integration/basic/div/01/input.essence 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 cf7b686f30..44371266d0 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,18 +1,22 @@ [ { - "a": 1, - "b": 1 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 1 }, { - "a": 2, - "b": 2 + "MachineName(0)": 1, + "UserName(a)": 2, + "UserName(b)": 2 }, { - "a": 3, - "b": 2 + "MachineName(0)": 1, + "UserName(a)": 3, + "UserName(b)": 2 }, { - "a": 3, - "b": 3 + "MachineName(0)": 1, + "UserName(a)": 3, + "UserName(b)": 3 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/01/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/div/01/input.expected-parse.serialised.json index 54e3a18b85..7d53ee1ef8 100644 --- a/conjure_oxide/tests/integration/basic/div/01/input.expected-parse.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/01/input.expected-parse.serialised.json @@ -2,17 +2,17 @@ "constraints": { "Eq": [ { - "dirtyclean": false + "clean": false }, { - "Div": [ + "UnsafeDiv": [ { - "dirtyclean": false + "clean": false }, { "Reference": [ { - "dirtyclean": false + "clean": false }, { "UserName": "a" @@ -22,7 +22,7 @@ { "Reference": [ { - "dirtyclean": false + "clean": false }, { "UserName": "b" @@ -34,7 +34,7 @@ { "Constant": [ { - "dirtyclean": false + "clean": false }, { "Int": 1 @@ -43,6 +43,7 @@ } ] }, + "next_var": 0, "variables": [ [ { 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 6a967cc812..66a692476f 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 @@ -2,28 +2,45 @@ "constraints": { "And": [ { - "dirtyclean": false + "clean": false }, [ { - "DivEq": [ + "Eq": [ { - "dirtyclean": false + "clean": false }, { "Reference": [ { - "dirtyclean": false + "clean": false }, { - "UserName": "a" + "MachineName": 0 } ] }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 1 + } + ] + } + ] + }, + { + "Neq": [ + { + "clean": false + }, { "Reference": [ { - "dirtyclean": false + "clean": false }, { "UserName": "b" @@ -33,48 +50,74 @@ { "Constant": [ { - "dirtyclean": false + "clean": false }, { - "Int": 1 + "Int": 0 } ] } ] }, { - "AllDiff": [ + "DivEq": [ + { + "clean": false + }, { - "dirtyclean": false + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "b" + } + ] }, - [ - { - "Reference": [ - { - "dirtyclean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "dirtyclean": false - }, - { - "Int": 0 - } - ] - } - ] + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } ] } ] ] }, + "next_var": 1, "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], [ { "UserName": "a" diff --git a/conjure_oxide/tests/integration/basic/div/02/input.essence b/conjure_oxide/tests/integration/basic/div/02/input.essence new file mode 100644 index 0000000000..5af6af6221 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/02/input.essence @@ -0,0 +1,2 @@ +find a : int(0..3) +such that a >= 4 / 2 $ should be simplified to constant diff --git a/conjure_oxide/tests/integration/basic/div/02/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/02/input.expected-minion.solutions.json new file mode 100644 index 0000000000..abd081d23b --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/02/input.expected-minion.solutions.json @@ -0,0 +1,8 @@ +[ + { + "UserName(a)": 2 + }, + { + "UserName(a)": 3 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/02/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/div/02/input.expected-parse.serialised.json new file mode 100644 index 0000000000..393aeee372 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/02/input.expected-parse.serialised.json @@ -0,0 +1,66 @@ +{ + "constraints": { + "Geq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "UnsafeDiv": [ + { + "clean": false + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 4 + } + ] + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 2 + } + ] + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..3db21fb5fe --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json @@ -0,0 +1,59 @@ +{ + "constraints": { + "Ineq": [ + { + "clean": false + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 2 + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 0 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/03/input.essence b/conjure_oxide/tests/integration/basic/div/03/input.essence new file mode 100644 index 0000000000..9c12c8ad39 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/03/input.essence @@ -0,0 +1,2 @@ +find a : int(0..9) +such that 2 = 8 / 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 new file mode 100644 index 0000000000..350becd8be --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json @@ -0,0 +1,10 @@ +[ + { + "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-parse.serialised.json b/conjure_oxide/tests/integration/basic/div/03/input.expected-parse.serialised.json new file mode 100644 index 0000000000..c2106cf366 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/03/input.expected-parse.serialised.json @@ -0,0 +1,66 @@ +{ + "constraints": { + "Eq": [ + { + "clean": false + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 2 + } + ] + }, + { + "UnsafeDiv": [ + { + "clean": false + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 8 + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 9 + ] + } + ] + } + } + ] + ] +} \ 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 new file mode 100644 index 0000000000..5af8c49c8c --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json @@ -0,0 +1,139 @@ +{ + "constraints": { + "And": [ + { + "clean": false + }, + [ + { + "Eq": [ + { + "clean": false + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 2 + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } + ] + }, + { + "Neq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 0 + } + ] + } + ] + }, + { + "DivEq": [ + { + "clean": false + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 8 + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } + ] + } + ] + ] + }, + "next_var": 1, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 8 + ] + } + ] + } + } + ], + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 9 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/04/input.essence b/conjure_oxide/tests/integration/basic/div/04/input.essence new file mode 100644 index 0000000000..e87f024224 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/04/input.essence @@ -0,0 +1,2 @@ +find a,b,c : int(0..3) +such that !(a = b/c) 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 new file mode 100644 index 0000000000..20823a766c --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/04/input.expected-minion.solutions.json @@ -0,0 +1,314 @@ +[ + { + "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)": 2, + "UserName(c)": 0 + }, + { + "MachineName(0)": 0, + "UserName(a)": 0, + "UserName(b)": 3, + "UserName(c)": 0 + }, + { + "MachineName(0)": 0, + "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)": 3 + }, + { + "MachineName(0)": 0, + "UserName(a)": 1, + "UserName(b)": 3, + "UserName(c)": 0 + }, + { + "MachineName(0)": 0, + "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)": 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)": 3 + }, + { + "MachineName(0)": 0, + "UserName(a)": 2, + "UserName(b)": 3, + "UserName(c)": 0 + }, + { + "MachineName(0)": 0, + "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)": 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(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(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 + }, + { + "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-parse.serialised.json b/conjure_oxide/tests/integration/basic/div/04/input.expected-parse.serialised.json new file mode 100644 index 0000000000..f3289ecca1 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/04/input.expected-parse.serialised.json @@ -0,0 +1,107 @@ +{ + "constraints": { + "Not": [ + { + "clean": false + }, + { + "Eq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "UnsafeDiv": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "b" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "c" + } + ] + } + ] + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ] + ] +} \ 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 new file mode 100644 index 0000000000..a7abc09a77 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json @@ -0,0 +1,182 @@ +{ + "constraints": { + "And": [ + { + "clean": false + }, + [ + { + "Or": [ + { + "clean": false + }, + [ + { + "Neq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } + ] + }, + { + "Eq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 0 + } + ] + } + ] + } + ] + ] + }, + { + "DivEq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "b" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "c" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } + ] + } + ] + ] + }, + "next_var": 1, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/05/input.essence b/conjure_oxide/tests/integration/basic/div/05/input.essence new file mode 100644 index 0000000000..8b759e332b --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/05/input.essence @@ -0,0 +1,2 @@ +find a,b,c : int(0..3) +such that (a != b/c) diff --git a/conjure_oxide/tests/integration/basic/div/05/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/05/input.expected-minion.solutions.json new file mode 100644 index 0000000000..1bde989707 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/05/input.expected-minion.solutions.json @@ -0,0 +1,218 @@ +[ + { + "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)": 2 + }, + { + "MachineName(0)": 0, + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 3 + }, + { + "MachineName(0)": 0, + "UserName(a)": 1, + "UserName(b)": 2, + "UserName(c)": 3 + }, + { + "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)": 2 + }, + { + "MachineName(0)": 0, + "UserName(a)": 2, + "UserName(b)": 1, + "UserName(c)": 3 + }, + { + "MachineName(0)": 0, + "UserName(a)": 2, + "UserName(b)": 2, + "UserName(c)": 3 + }, + { + "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)": 2 + }, + { + "MachineName(0)": 0, + "UserName(a)": 3, + "UserName(b)": 1, + "UserName(c)": 3 + }, + { + "MachineName(0)": 0, + "UserName(a)": 3, + "UserName(b)": 2, + "UserName(c)": 3 + }, + { + "MachineName(0)": 1, + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 0, + "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(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 + }, + { + "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/05/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/div/05/input.expected-parse.serialised.json new file mode 100644 index 0000000000..f97a808245 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/05/input.expected-parse.serialised.json @@ -0,0 +1,100 @@ +{ + "constraints": { + "Neq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "UnsafeDiv": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "b" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "c" + } + ] + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/div/05/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/05/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..4a2e9cbd22 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/div/05/input.expected-rewrite.serialised.json @@ -0,0 +1,173 @@ +{ + "constraints": { + "And": [ + { + "clean": false + }, + [ + { + "Neq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } + ] + }, + { + "Neq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false + }, + { + "Int": 0 + } + ] + } + ] + }, + { + "DivEq": [ + { + "clean": false + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "b" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "UserName": "c" + } + ] + }, + { + "Reference": [ + { + "clean": false + }, + { + "MachineName": 0 + } + ] + } + ] + } + ] + ] + }, + "next_var": 1, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json index ddde4ec5d5..5ccb315ed0 100644 --- a/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json @@ -123,7 +123,7 @@ }, [ { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -146,67 +146,11 @@ "UserName": "a" } ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] }, { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -220,33 +164,6 @@ } ] }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, { "Reference": [ { @@ -256,192 +173,6 @@ "UserName": "b" } ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] } diff --git a/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json index bb5392dbfe..b52587ef1b 100644 --- a/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json @@ -123,7 +123,7 @@ }, [ { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -146,67 +146,11 @@ "UserName": "a" } ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] }, { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -220,33 +164,6 @@ } ] }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, { "Reference": [ { @@ -256,192 +173,6 @@ "UserName": "b" } ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] } diff --git a/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json index c7e8483ff2..5db97498a9 100644 --- a/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json @@ -123,7 +123,7 @@ }, [ { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -146,67 +146,11 @@ "UserName": "a" } ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] }, { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -220,33 +164,6 @@ } ] }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, { "Reference": [ { @@ -256,192 +173,6 @@ "UserName": "b" } ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] } diff --git a/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json index f7af2402c3..0e92794bad 100644 --- a/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json @@ -123,7 +123,7 @@ }, [ { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -146,67 +146,11 @@ "UserName": "a" } ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] }, { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -220,33 +164,6 @@ } ] }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, { "Reference": [ { @@ -256,192 +173,6 @@ "UserName": "b" } ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] } diff --git a/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json index 2f42044ffe..aa1cbd1cbb 100644 --- a/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json @@ -123,7 +123,7 @@ }, [ { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -146,67 +146,11 @@ "UserName": "a" } ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] }, { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ + "Eq": [ { "clean": false }, @@ -220,33 +164,6 @@ } ] }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, { "Reference": [ { @@ -256,192 +173,6 @@ "UserName": "b" } ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - } - ] - ] - }, - { - "Or": [ - { - "clean": false - }, - [ - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "a" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false - }, - { - "Reference": [ - { - "clean": false - }, - { - "UserName": "b" - } - ] - }, - { - "Reference": [ - { - "clean": false - }, - { - "MachineName": 0 - } - ] - }, - { - "Constant": [ - { - "clean": false - }, - { - "Int": 0 - } - ] } ] } diff --git a/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json index 79ee6ea133..53d689cef2 100644 --- a/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json @@ -45,7 +45,7 @@ { "Constant": [ { - "clean": true + "clean": false }, { "Int": 4 @@ -94,7 +94,7 @@ { "Constant": [ { - "clean": true + "clean": false }, { "Int": 4 diff --git a/crates/conjure_core/src/ast/constants.rs b/crates/conjure_core/src/ast/constants.rs index 50eeed65ed..853980a74f 100644 --- a/crates/conjure_core/src/ast/constants.rs +++ b/crates/conjure_core/src/ast/constants.rs @@ -29,6 +29,18 @@ impl TryFrom for bool { } } +impl From for Constant { + fn from(i: i32) -> Self { + Constant::Int(i) + } +} + +impl From for Constant { + fn from(b: bool) -> Self { + Constant::Bool(b) + } +} + impl Display for Constant { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { match &self { diff --git a/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index 65da421b9d..e17244f306 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -9,6 +9,7 @@ use uniplate_derive::Uniplate; use crate::ast::constants::Constant; use crate::ast::symbol_table::{Name, SymbolTable}; +use crate::ast::ReturnType; use crate::metadata::Metadata; #[document_compatibility] @@ -21,6 +22,10 @@ pub enum Expression { */ Nothing, + /// An expression representing "A is valid as long as B is true" + /// Turns into a conjunction when it reaches a boolean context + Bubble(Metadata, Box, Box), + #[compatible(Minion, JsonInput)] Constant(Metadata, Constant), @@ -66,6 +71,13 @@ pub enum Expression { #[compatible(JsonInput)] Lt(Metadata, Box, Box), + /// Division after preventing division by zero, usually with a bubble + SafeDiv(Metadata, Box, Box), + + /// Division with a possibly undefined value (division by 0) + #[compatible(JsonInput)] + UnsafeDiv(Metadata, Box, Box), + /* Flattened SumEq. * * Note: this is an intermediary step that's used in the process of converting from conjure model to minion. @@ -82,17 +94,19 @@ pub enum Expression { #[compatible(Minion)] SumLeq(Metadata, Vec, Box), + #[compatible(Minion)] + DivEq(Metadata, Box, Box, Box), + #[compatible(Minion)] Ineq(Metadata, Box, Box, Box), - // #[compatible(Minion)] - // DivEq(Metadata, Box, Box, Box), #[compatible(Minion)] AllDiff(Metadata, Vec), } impl Expression { pub fn bounds(&self, vars: &SymbolTable) -> Option<(i32, i32)> { + // TODO: (flm8) change this to return full Domains rather than just bounds match self { Expression::Reference(_, name) => vars.get(name).and_then(|v| v.domain.min_max_i32()), Expression::Constant(_, Constant::Int(i)) => Some((*i, *i)), @@ -124,10 +138,63 @@ impl Expression { bounds.iter().map(|(_, max)| *max).min()?, )) } + Expression::UnsafeDiv(_, a, b) | Expression::SafeDiv(_, a, b) => { + let (a_min, a_max) = a.bounds(vars)?; + let (mut b_min, mut b_max) = b.bounds(vars)?; + if b_min == 0 && b_max == 0 { + return None; + } + if b_min == 0 { + b_min += 1; // Smallest number which avoids division by zero + } + if b_max == 0 { + b_max -= 1; // Largest number which avoids division by zero + } + Some((a_min / b_max, a_max / b_min)) // TODO: calculate bounds considering negativ values + } _ => todo!(), } } + pub fn can_be_undefined(&self) -> bool { + // TODO: there will be more false cases but we are being conservative + match self { + Expression::Reference(_, _) => false, + Expression::Constant(_, Constant::Bool(_)) => false, + Expression::Constant(_, Constant::Int(_)) => false, + _ => true, + } + } + + pub fn return_type(&self) -> Option { + match self { + Expression::Constant(_, Constant::Int(_)) => Some(ReturnType::Int), + Expression::Constant(_, Constant::Bool(_)) => Some(ReturnType::Bool), + Expression::Reference(_, _) => None, + Expression::Sum(_, _) => Some(ReturnType::Int), + Expression::Min(_, _) => Some(ReturnType::Int), + Expression::Not(_, _) => Some(ReturnType::Bool), + Expression::Or(_, _) => Some(ReturnType::Bool), + Expression::And(_, _) => Some(ReturnType::Bool), + Expression::Eq(_, _, _) => Some(ReturnType::Bool), + Expression::Neq(_, _, _) => Some(ReturnType::Bool), + Expression::Geq(_, _, _) => Some(ReturnType::Bool), + Expression::Leq(_, _, _) => Some(ReturnType::Bool), + Expression::Gt(_, _, _) => Some(ReturnType::Bool), + Expression::Lt(_, _, _) => Some(ReturnType::Bool), + Expression::SafeDiv(_, _, _) => Some(ReturnType::Int), + Expression::UnsafeDiv(_, _, _) => Some(ReturnType::Int), + Expression::SumEq(_, _, _) => Some(ReturnType::Bool), + Expression::SumGeq(_, _, _) => Some(ReturnType::Bool), + Expression::SumLeq(_, _, _) => Some(ReturnType::Bool), + Expression::DivEq(_, _, _, _) => Some(ReturnType::Bool), + Expression::Ineq(_, _, _, _) => Some(ReturnType::Bool), + Expression::AllDiff(_, _) => Some(ReturnType::Bool), + Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool? + Expression::Nothing => None, + } + } + pub fn is_clean(&self) -> bool { match self { Expression::Nothing => true, @@ -203,8 +270,6 @@ impl Expression { } Expression::Eq(metadata, box1, box2) => { metadata.clean = bool_value; - box1.set_clean(bool_value); - box2.set_clean(bool_value); } Expression::Neq(metadata, _box1, _box2) => { metadata.clean = bool_value; @@ -236,93 +301,143 @@ impl Expression { Expression::SumEq(metadata, _exprs, _expr) => { metadata.clean = bool_value; } + Expression::Bubble(metadata, box1, box2) => { + metadata.clean = bool_value; + } + Expression::SafeDiv(metadata, box1, box2) => { + metadata.clean = bool_value; + } + Expression::UnsafeDiv(metadata, box1, box2) => { + metadata.clean = bool_value; + } + Expression::DivEq(metadata, box1, box2, box3) => { + metadata.clean = bool_value; + } } } } fn display_expressions(expressions: &[Expression]) -> String { - if expressions.len() <= 3 { - format!( - "[{}]", - expressions - .iter() - .map(|e| e.to_string()) - .collect::>() - .join(", ") - ) - } else { - format!( - "[{}..{}]", - expressions[0], - expressions[expressions.len() - 1] - ) + // if expressions.len() <= 3 { + format!( + "[{}]", + expressions + .iter() + .map(|e| e.to_string()) + .collect::>() + .join(", ") + ) + // } else { + // format!( + // "[{}..{}]", + // expressions[0], + // expressions[expressions.len() - 1] + // ) + // } +} + +impl From for Expression { + fn from(i: i32) -> Self { + Expression::Constant(Metadata::new(), Constant::Int(i)) + } +} + +impl From for Expression { + fn from(b: bool) -> Self { + Expression::Constant(Metadata::new(), Constant::Bool(b)) } } impl Display for Expression { + // TODO: (flm8) this will change once we implement a parser (two-way conversion) fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { match &self { - Expression::Constant(metadata, c) => write!(f, "Constant({}, {})", metadata, c), - Expression::Reference(metadata, name) => write!(f, "Reference({}, {})", metadata, name), + Expression::Constant(_, c) => match c { + Constant::Bool(b) => write!(f, "{}", b), + Constant::Int(i) => write!(f, "{}", i), + }, + Expression::Reference(_, name) => match name { + Name::MachineName(n) => write!(f, "_{}", n), + Name::UserName(s) => write!(f, "{}", s), + }, Expression::Nothing => write!(f, "Nothing"), - Expression::Sum(metadata, expressions) => { - write!(f, "Sum({}, {})", metadata, display_expressions(expressions)) + Expression::Sum(_, expressions) => { + write!(f, "Sum({})", display_expressions(expressions)) } - Expression::Not(metadata, expr_box) => { - write!(f, "Not({}, {})", metadata, expr_box.clone()) + Expression::Min(_, expressions) => { + write!(f, "Min({})", display_expressions(expressions)) } - Expression::Or(metadata, expressions) => { - write!(f, "Not({}, {})", metadata, display_expressions(expressions)) + Expression::Not(_, expr_box) => { + write!(f, "Not({})", expr_box.clone()) } - Expression::And(metadata, expressions) => { - write!(f, "And({}, {})", metadata, display_expressions(expressions)) + Expression::Or(_, expressions) => { + write!(f, "Or({})", display_expressions(expressions)) } - Expression::Eq(metadata, box1, box2) => { - write!(f, "Eq({}, {}, {})", metadata, box1.clone(), box2.clone()) + Expression::And(_, expressions) => { + write!(f, "And({})", display_expressions(expressions)) } - Expression::Neq(metadata, box1, box2) => { - write!(f, "Neq({}, {}, {})", metadata, box1.clone(), box2.clone()) + Expression::Eq(_, box1, box2) => { + write!(f, "({} = {})", box1.clone(), box2.clone()) } - Expression::Geq(metadata, box1, box2) => { - write!(f, "Geq({}, {}, {})", metadata, box1.clone(), box2.clone()) + Expression::Neq(_, box1, box2) => { + write!(f, "({} != {})", box1.clone(), box2.clone()) } - Expression::Leq(metadata, box1, box2) => { - write!(f, "Leq({}, {}, {})", metadata, box1.clone(), box2.clone()) + Expression::Geq(_, box1, box2) => { + write!(f, "({} >= {})", box1.clone(), box2.clone()) } - Expression::Gt(metadata, box1, box2) => { - write!(f, "Gt({}, {}, {})", metadata, box1.clone(), box2.clone()) + Expression::Leq(_, box1, box2) => { + write!(f, "({} <= {})", box1.clone(), box2.clone()) } - Expression::Lt(metadata, box1, box2) => { - write!(f, "Lt({}, {}, {})", metadata, box1.clone(), box2.clone()) + Expression::Gt(_, box1, box2) => { + write!(f, "({} > {})", box1.clone(), box2.clone()) } - Expression::SumGeq(metadata, box1, box2) => { - write!( - f, - "SumGeq({}, {}. {})", - metadata, - display_expressions(box1), - box2.clone() - ) + Expression::Lt(_, box1, box2) => { + write!(f, "({} < {})", box1.clone(), box2.clone()) } - Expression::SumLeq(metadata, box1, box2) => { + Expression::SumEq(_, expressions, expr_box) => { write!( f, - "SumLeq({}, {}, {})", - metadata, - display_expressions(box1), - box2.clone() + "SumEq({}, {})", + display_expressions(expressions), + expr_box.clone() ) } - Expression::Ineq(metadata, box1, box2, box3) => write!( + Expression::SumGeq(_, box1, box2) => { + write!(f, "SumGeq({}, {})", display_expressions(box1), box2.clone()) + } + Expression::SumLeq(_, box1, box2) => { + write!(f, "SumLeq({}, {})", display_expressions(box1), box2.clone()) + } + Expression::Ineq(_, box1, box2, box3) => write!( f, - "Ineq({}, {}, {}, {})", - metadata, + "Ineq({}, {}, {})", box1.clone(), box2.clone(), box3.clone() ), + Expression::AllDiff(_, expressions) => { + write!(f, "AllDiff({})", display_expressions(expressions)) + } + Expression::Bubble(_, box1, box2) => { + write!(f, "{{{} @ {}}}", box1.clone(), box2.clone()) + } + Expression::SafeDiv(_, box1, box2) => { + write!(f, "SafeDiv({}, {})", box1.clone(), box2.clone()) + } + Expression::UnsafeDiv(_, box1, box2) => { + write!(f, "UnsafeDiv({}, {})", box1.clone(), box2.clone()) + } + Expression::DivEq(_, box1, box2, box3) => { + write!( + f, + "DivEq({}, {}, {})", + box1.clone(), + box2.clone(), + box3.clone() + ) + } #[allow(unreachable_patterns)] - _ => write!(f, "Expression::Unknown"), + other => todo!("Implement display for {:?}", other), } } } diff --git a/crates/conjure_core/src/ast/mod.rs b/crates/conjure_core/src/ast/mod.rs index 6715346725..26c214e0da 100644 --- a/crates/conjure_core/src/ast/mod.rs +++ b/crates/conjure_core/src/ast/mod.rs @@ -1,13 +1,15 @@ +mod constants; +mod domains; +mod expressions; +mod symbol_table; +mod types; +mod variables; + pub use constants::Constant; pub use domains::Domain; pub use domains::Range; pub use expressions::Expression; pub use symbol_table::Name; pub use symbol_table::SymbolTable; +pub use types::ReturnType; pub use variables::DecisionVariable; - -mod constants; -mod domains; -mod expressions; -mod symbol_table; -mod variables; diff --git a/crates/conjure_core/src/ast/types.rs b/crates/conjure_core/src/ast/types.rs new file mode 100644 index 0000000000..d9389420bc --- /dev/null +++ b/crates/conjure_core/src/ast/types.rs @@ -0,0 +1,5 @@ +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum ReturnType { + Int, + Bool, +} diff --git a/crates/conjure_core/src/parse/parse_model.rs b/crates/conjure_core/src/parse/parse_model.rs index 694ecd0ab8..ad1803d19a 100644 --- a/crates/conjure_core/src/parse/parse_model.rs +++ b/crates/conjure_core/src/parse/parse_model.rs @@ -178,10 +178,10 @@ fn parse_expression(obj: &JsonValue) -> Option { "MkOpLt", Box::new(Expression::Lt) as Box _>, ), - // ( - // "MkOpDiv", - // Box::new(Expression::Div) as Box _>, - // ), + ( + "MkOpDiv", + Box::new(Expression::UnsafeDiv) as Box _>, + ), ] .into_iter() .collect(); diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs index 70423df676..5399b76bc6 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -399,22 +399,6 @@ fn evaluate_constant_not(expr: &Expr, _: &Model) -> ApplicationResult { } } -// /** Turn a Div into a SafeDiv and post a global constraint to avoid undefined. */ -// #[register_rule(("Base", 100))] -// fn ensure_div(expr: &Expr, _: &Model) -> ApplicationResult { -// match expr { -// Expr::Div(metadata, a, b) => Ok(Reduction::with_top( -// Expr::SafeDiv(metadata.clone(), a.clone(), b.clone()), -// Expr::Neq( -// Metadata::new(), -// b.clone(), -// Box::new(Expr::Constant(Metadata::new(), Const::Int(0))), -// ), -// )), -// _ => Err(ApplicationError::RuleNotApplicable), -// } -// } - /** * Turn a Min into a new variable and post a global constraint to ensure the new variable is the minimum. * ```text @@ -435,21 +419,10 @@ fn min_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult { Box::new(Expr::Reference(Metadata::new(), new_name.clone())), Box::new(e.clone()), )); - disjunction.push(Expr::And( - // TODO: change to an Eq once we figure out how to apply them later + disjunction.push(Expr::Eq( Metadata::new(), - vec![ - Expr::Leq( - Metadata::new(), - Box::new(Expr::Reference(Metadata::new(), new_name.clone())), - Box::new(e.clone()), - ), - Expr::Geq( - Metadata::new(), - Box::new(Expr::Reference(Metadata::new(), new_name.clone())), - Box::new(e.clone()), - ), - ], + Box::new(Expr::Reference(Metadata::new(), new_name.clone())), + Box::new(e.clone()), )); } new_top.push(Expr::Or(Metadata::new(), disjunction)); @@ -522,3 +495,65 @@ fn distribute_or_over_and(expr: &Expr, _: &Model) -> ApplicationResult { _ => Err(ApplicationError::RuleNotApplicable), } } + +/** +* Distribute `not` over `and` (De Morgan's Law): + +* ```text +* not(and(a, b)) = or(not a, not b) +* ``` + */ +#[register_rule(("Base", 100))] +fn distribute_not_over_and(expr: &Expr, _: &Model) -> ApplicationResult { + match expr { + Expr::Not(_, contents) => match contents.as_ref() { + Expr::And(metadata, exprs) => { + if exprs.len() == 1 { + let single_expr = exprs[0].clone(); + return Ok(Reduction::pure(Expr::Not( + Metadata::new(), + Box::new(single_expr.clone()), + ))); + } + let mut new_exprs = Vec::new(); + for e in exprs { + new_exprs.push(Expr::Not(metadata.clone(), Box::new(e.clone()))); + } + Ok(Reduction::pure(Expr::Or(metadata.clone(), new_exprs))) + } + _ => Err(ApplicationError::RuleNotApplicable), + }, + _ => Err(ApplicationError::RuleNotApplicable), + } +} + +/** +* Distribute `not` over `or` (De Morgan's Law): + +* ```text +* not(or(a, b)) = and(not a, not b) +* ``` + */ +#[register_rule(("Base", 100))] +fn distribute_not_over_or(expr: &Expr, _: &Model) -> ApplicationResult { + match expr { + Expr::Not(_, contents) => match contents.as_ref() { + Expr::Or(metadata, exprs) => { + if exprs.len() == 1 { + let single_expr = exprs[0].clone(); + return Ok(Reduction::pure(Expr::Not( + Metadata::new(), + Box::new(single_expr.clone()), + ))); + } + let mut new_exprs = Vec::new(); + for e in exprs { + new_exprs.push(Expr::Not(metadata.clone(), Box::new(e.clone()))); + } + Ok(Reduction::pure(Expr::And(metadata.clone(), new_exprs))) + } + _ => Err(ApplicationError::RuleNotApplicable), + }, + _ => Err(ApplicationError::RuleNotApplicable), + } +} diff --git a/crates/conjure_core/src/rules/bubble.rs b/crates/conjure_core/src/rules/bubble.rs new file mode 100644 index 0000000000..f2c51503f8 --- /dev/null +++ b/crates/conjure_core/src/rules/bubble.rs @@ -0,0 +1,86 @@ +use conjure_core::ast::{Expression, ReturnType}; +use conjure_core::metadata::Metadata; +use conjure_core::rule_engine::{ + register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction, +}; +use conjure_core::Model; +use uniplate::uniplate::Uniplate; + +register_rule_set!("Bubble", 254, ("Base")); + +// Bubble reduction rules + +/* + Reduce bubbles with a boolean expression to a conjunction with their condition. + + e.g. (a / b = c) @ (b != 0) => (a / b = c) & (b != 0) +*/ +#[register_rule(("Bubble", 100))] +fn expand_bubble(expr: &Expression, _: &Model) -> ApplicationResult { + match expr { + Expression::Bubble(_, a, b) if a.return_type() == Some(ReturnType::Bool) => { + Ok(Reduction::pure(Expression::And( + Metadata::new(), + vec![*a.clone(), *b.clone()], + ))) + } + _ => Err(ApplicationError::RuleNotApplicable), + } +} + +/* + Bring bubbles with a non-boolean expression higher up the tree. + + E.g. ((a / b) @ (b != 0)) = c => (a / b = c) @ (b != 0) +*/ +#[register_rule(("Bubble", 100))] +fn bubble_up(expr: &Expression, _: &Model) -> ApplicationResult { + let mut sub = expr.children(); + let mut bubbled_conditions = vec![]; + for e in sub.iter_mut() { + if let Expression::Bubble(_, a, b) = e { + if a.return_type() != Some(ReturnType::Bool) { + bubbled_conditions.push(*b.clone()); + *e = *a.clone(); + } + } + } + if bubbled_conditions.is_empty() { + return Err(ApplicationError::RuleNotApplicable); + } + return Ok(Reduction::pure(Expression::Bubble( + Metadata::new(), + Box::new( + expr.with_children(sub) + .or(Err(ApplicationError::RuleNotApplicable))?, + ), + Box::new(Expression::And(Metadata::new(), bubbled_conditions)), + ))); +} + +// Bubble applications + +/* + Convert an unsafe division to a safe division with a bubble condition. + + Division by zero is undefined and therefore not allowed, so we add a condition to check for it. + This condition is brought up the tree and expanded into a conjunction with the first boolean-type expression it is paired with. + + E.g. a / b => (a / b) @ (b != 0) + +*/ +#[register_rule(("Bubble", 100))] +fn div_to_bubble(expr: &Expression, _: &Model) -> ApplicationResult { + if let Expression::UnsafeDiv(_, a, b) = expr { + return Ok(Reduction::pure(Expression::Bubble( + Metadata::new(), + Box::new(Expression::SafeDiv(Metadata::new(), a.clone(), b.clone())), + Box::new(Expression::Neq( + Metadata::new(), + b.clone(), + Box::new(Expression::from(0)), + )), + ))); + } + return Err(ApplicationError::RuleNotApplicable); +} diff --git a/crates/conjure_core/src/rules/cnf.rs b/crates/conjure_core/src/rules/cnf.rs index 7d88a684d1..33c3d9272c 100644 --- a/crates/conjure_core/src/rules/cnf.rs +++ b/crates/conjure_core/src/rules/cnf.rs @@ -10,51 +10,3 @@ use conjure_core::solver::SolverFamily; use conjure_core::Model; register_rule_set!("CNF", 100, ("Base"), (SolverFamily::SAT)); - -/** -* Distribute `not` over `and` (De Morgan's Law): - -* ```text -* not(and(a, b)) = or(not a, not b) -* ``` - */ -#[register_rule(("CNF", 100))] -fn distribute_not_over_and(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Not(_, contents) => match contents.as_ref() { - Expr::And(metadata, exprs) => { - let mut new_exprs = Vec::new(); - for e in exprs { - new_exprs.push(Expr::Not(metadata.clone(), Box::new(e.clone()))); - } - Ok(Reduction::pure(Expr::Or(metadata.clone(), new_exprs))) - } - _ => Err(ApplicationError::RuleNotApplicable), - }, - _ => Err(ApplicationError::RuleNotApplicable), - } -} - -/** -* Distribute `not` over `or` (De Morgan's Law): - -* ```text -* not(or(a, b)) = and(not a, not b) -* ``` - */ -#[register_rule(("CNF", 100))] -fn distribute_not_over_or(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Not(_, contents) => match contents.as_ref() { - Expr::Or(metadata, exprs) => { - let mut new_exprs = Vec::new(); - for e in exprs { - new_exprs.push(Expr::Not(metadata.clone(), Box::new(e.clone()))); - } - Ok(Reduction::pure(Expr::And(metadata.clone(), new_exprs))) - } - _ => Err(ApplicationError::RuleNotApplicable), - }, - _ => Err(ApplicationError::RuleNotApplicable), - } -} diff --git a/crates/conjure_core/src/rules/constant.rs b/crates/conjure_core/src/rules/constant.rs index 9693307546..543149416c 100644 --- a/crates/conjure_core/src/rules/constant.rs +++ b/crates/conjure_core/src/rules/constant.rs @@ -60,6 +60,16 @@ pub fn eval_constant(expr: &Expr) -> Option { Expr::Min(_, exprs) => { opt_vec_op::(|e| e.iter().min().copied(), exprs).map(Const::Int) } + Expr::UnsafeDiv(_, a, b) | Expr::SafeDiv(_, a, b) => { + if unwrap_expr::(b)? == 0 { + return None; + } + bin_op::(|a, b| a / b, a, b).map(Const::Int) + } + Expr::DivEq(_, a, b, c) => { + tern_op::(|a, b, c| a == b * c, a, b, c).map(Const::Bool) + } + Expr::Bubble(_, a, b) => bin_op::(|a, b| a && b, a, b).map(Const::Bool), _ => { println!("WARNING: Unimplemented constant eval: {:?}", expr); None @@ -123,3 +133,28 @@ fn unwrap_expr>(expr: &Expr) -> Option { let c = eval_constant(expr)?; TryInto::::try_into(c).ok() } + +#[cfg(test)] +mod tests { + use conjure_core::ast::{Constant, Expression}; + + #[test] + fn div_by_zero() { + let expr = Expression::UnsafeDiv( + Default::default(), + Box::new(Expression::Constant(Default::default(), Constant::Int(1))), + Box::new(Expression::Constant(Default::default(), Constant::Int(0))), + ); + assert_eq!(super::eval_constant(&expr), None); + } + + #[test] + fn safediv_by_zero() { + let expr = Expression::SafeDiv( + Default::default(), + Box::new(Expression::Constant(Default::default(), Constant::Int(1))), + Box::new(Expression::Constant(Default::default(), Constant::Int(0))), + ); + assert_eq!(super::eval_constant(&expr), None); + } +} diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index d0ae7e37b0..81398e4c9a 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -2,7 +2,11 @@ /* Rules for translating to Minion-supported constraints */ /************************************************************************/ -use crate::ast::{Constant as Const, Expression as Expr}; +use uniplate::uniplate::Uniplate; + +use crate::ast::{ + Constant as Const, DecisionVariable, Domain, Expression as Expr, Range, SymbolTable, +}; use crate::metadata::Metadata; use crate::rule_engine::{ register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction, @@ -109,12 +113,21 @@ fn sum_leq_to_sumleq(expr: &Expr, _: &Model) -> ApplicationResult { fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Eq(metadata, a, b) => { - let exprs = sum_to_vector(a)?; - Ok(Reduction::pure(Expr::SumEq( - metadata.clone(), - exprs, - b.clone(), - ))) + if let Ok(exprs) = sum_to_vector(a) { + Ok(Reduction::pure(Expr::SumEq( + metadata.clone(), + exprs, + b.clone(), + ))) + } else if let Ok(exprs) = sum_to_vector(b) { + Ok(Reduction::pure(Expr::SumEq( + metadata.clone(), + exprs, + a.clone(), + ))) + } else { + Err(ApplicationError::RuleNotApplicable) + } } _ => Err(ApplicationError::RuleNotApplicable), } @@ -229,63 +242,91 @@ fn leq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { } } -// #[register_rule(("Minion", 100))] -// fn safediv_eq_to_diveq(expr: &Expr, _: &Model) -> ApplicationResult { +// #[register_rule(("Minion", 99))] +// fn eq_to_leq_geq(expr: &Expr, _: &Model) -> ApplicationResult { // match expr { // Expr::Eq(metadata, a, b) => { -// if let Expr::SafeDiv(_, x, y) = a.as_ref() { -// if !(b.is_reference() || b.is_constant()) { -// return Err(ApplicationError::RuleNotApplicable); -// } -// Ok(Reduction::pure(Expr::DivEq( -// metadata.clone(), -// x.clone(), -// y.clone(), -// b.clone(), -// ))) -// } else if let Expr::SafeDiv(_, x, y) = b.as_ref() { -// if !(a.is_reference() || a.is_constant()) { -// return Err(ApplicationError::RuleNotApplicable); -// } -// Ok(Reduction::pure(Expr::DivEq( -// metadata.clone(), -// x.clone(), -// y.clone(), -// a.clone(), -// ))) -// } else { -// Err(ApplicationError::RuleNotApplicable) -// } +// return Ok(Reduction::pure(Expr::And( +// metadata.clone(), +// vec![ +// Expr::Leq(metadata.clone(), a.clone(), b.clone()), +// Expr::Geq(metadata.clone(), a.clone(), b.clone()), +// ], +// ))); // } // _ => Err(ApplicationError::RuleNotApplicable), // } // } -#[register_rule(("Minion", 100))] -fn neq_to_alldiff(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Neq(metadata, a, b) => Ok(Reduction::pure(Expr::AllDiff( - metadata.clone(), - vec![*a.clone(), *b.clone()], - ))), - _ => Err(ApplicationError::RuleNotApplicable), +/** + * 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))] +fn flatten_safediv(expr: &Expr, mdl: &Model) -> ApplicationResult { + if expr.is_eq() || expr.is_leq() || expr.is_geq() || expr.is_neq() { + let mut sub = expr.children(); + + let mut new_vars = SymbolTable::new(); + let mut new_top = vec![]; + + // replace every safe div child with a reference to a new variable + for c in sub.iter_mut() { + if let Expr::SafeDiv(_, a, b) = c.clone() { + let new_name = mdl.gensym(); + let bound = c + .bounds(&mdl.variables) + .ok_or(ApplicationError::BoundError)?; + new_vars.insert( + new_name.clone(), + DecisionVariable::new(Domain::IntDomain(vec![Range::Bounded( + bound.0, bound.1, + )])), + ); + + new_top.push(Expr::DivEq( + Metadata::new(), + a.clone(), + b.clone(), + Box::new(Expr::Reference(Metadata::new(), new_name.clone())), + )); + + *c = Expr::Reference(Metadata::new(), new_name.clone()); + } + } + if !new_top.is_empty() { + return Ok(Reduction::new( + expr.with_children(sub) + .or(Err(ApplicationError::RuleNotApplicable))?, + Expr::And(Metadata::new(), new_top), + new_vars, + )); + } } + Err(ApplicationError::RuleNotApplicable) } -#[register_rule(("Minion", 99))] -fn eq_to_leq_geq(expr: &Expr, _: &Model) -> ApplicationResult { +#[register_rule(("Minion", 100))] +fn div_eq_to_diveq(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Eq(metadata, a, b) => { - if let Ok(exprs) = sum_to_vector(a) { - Ok(Reduction::pure(Expr::SumEq( + if let Expr::SafeDiv(_, x, y) = a.as_ref() { + if !(b.is_reference() || b.is_constant()) { + return Err(ApplicationError::RuleNotApplicable); + } + Ok(Reduction::pure(Expr::DivEq( metadata.clone(), - exprs, + x.clone(), + y.clone(), b.clone(), ))) - } else if let Ok(exprs) = sum_to_vector(b) { - Ok(Reduction::pure(Expr::SumEq( + } else if let Expr::SafeDiv(_, x, y) = b.as_ref() { + if !(a.is_reference() || a.is_constant()) { + return Err(ApplicationError::RuleNotApplicable); + } + Ok(Reduction::pure(Expr::DivEq( metadata.clone(), - exprs, + x.clone(), + y.clone(), a.clone(), ))) } else { @@ -295,3 +336,45 @@ fn eq_to_leq_geq(expr: &Expr, _: &Model) -> ApplicationResult { _ => Err(ApplicationError::RuleNotApplicable), } } + +#[register_rule(("Minion", 100))] +fn negated_neq_to_eq(expr: &Expr, _: &Model) -> ApplicationResult { + match expr { + Expr::Not(_, a) => match a.as_ref() { + Expr::Neq(_, b, c) => { + if !b.can_be_undefined() && !c.can_be_undefined() { + Ok(Reduction::pure(Expr::Eq( + Metadata::new(), + b.clone(), + c.clone(), + ))) + } else { + Err(ApplicationError::RuleNotApplicable) + } + } + _ => Err(ApplicationError::RuleNotApplicable), + }, + _ => Err(ApplicationError::RuleNotApplicable), + } +} + +#[register_rule(("Minion", 100))] +fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult { + match expr { + Expr::Not(_, a) => match a.as_ref() { + Expr::Eq(_, b, c) => { + if !b.can_be_undefined() && !c.can_be_undefined() { + Ok(Reduction::pure(Expr::Neq( + Metadata::new(), + b.clone(), + c.clone(), + ))) + } else { + Err(ApplicationError::RuleNotApplicable) + } + } + _ => Err(ApplicationError::RuleNotApplicable), + }, + _ => Err(ApplicationError::RuleNotApplicable), + } +} diff --git a/crates/conjure_core/src/rules/mod.rs b/crates/conjure_core/src/rules/mod.rs index c4435a41b3..e65f659901 100644 --- a/crates/conjure_core/src/rules/mod.rs +++ b/crates/conjure_core/src/rules/mod.rs @@ -1,6 +1,7 @@ pub use constant::eval_constant; mod base; +mod bubble; mod cnf; mod constant; mod minion; diff --git a/crates/conjure_core/src/solver/adaptors/minion.rs b/crates/conjure_core/src/solver/adaptors/minion.rs index 171d3c3b2d..2362976aeb 100644 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ b/crates/conjure_core/src/solver/adaptors/minion.rs @@ -276,26 +276,21 @@ fn read_expr(expr: conjure_ast::Expression) -> Result Ok(minion_ast::Constraint::AllDiff(vec![ - read_var(*a)?, - read_var(*b)?, - ])), - // conjure_ast::Expression::DivEq(_metadata, a, b, c) => { - // minion_model.constraints.push(minion_ast::Constraint::Div( - // (read_var(*a)?, read_var(*b)?), - // read_var(*c)?, - // )); - // Ok(()) - // } - conjure_ast::Expression::AllDiff(_metadata, vars) => { - Ok(minion_ast::Constraint::AllDiff(read_vars(vars)?)) + conjure_ast::Expression::Neq(_metadata, a, b) => { + Ok(minion_ast::Constraint::DisEq(read_var(*a)?, read_var(*b)?)) } + conjure_ast::Expression::DivEq(_metadata, a, b, c) => Ok( + minion_ast::Constraint::DivUndefZero((read_var(*a)?, read_var(*b)?), read_var(*c)?), + ), conjure_ast::Expression::Or(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedOr( 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)?)) + } x => Err(ModelFeatureNotSupported(format!("{:?}", x))), } } diff --git a/solvers/minion/src/run.rs b/solvers/minion/src/run.rs index fac7b105e9..e31114c809 100644 --- a/solvers/minion/src/run.rs +++ b/solvers/minion/src/run.rs @@ -574,7 +574,11 @@ unsafe fn constraint_add_args( //Constraint::WNotInRange(_, _) => todo!(), //Constraint::WNotInset(_, _) => todo!(), //Constraint::Abs(_, _) => todo!(), - //Constraint::DisEq(_, _) => todo!(), + Constraint::DisEq(a, b) => { + read_var(i, r_constr, a)?; + read_var(i, r_constr, b)?; + Ok(()) + } //Constraint::MinusEq(_, _) => todo!(), //Constraint::GacEq(_, _) => todo!(), //Constraint::WatchLess(_, _) => todo!(),