From 49e70404286e6ebd9df0f8a26550ca4102c7fc0d Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 12 Oct 2024 11:17:01 +0100 Subject: [PATCH] wip: change rule priorities to do simplifiers first --- COMMITMSG | 6 + 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 ++++++++ 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 | 165 ++------------- 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 +- 31 files changed, 961 insertions(+), 533 deletions(-) create mode 100644 COMMITMSG 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/COMMITMSG b/COMMITMSG new file mode 100644 index 0000000000..faa20cb63c --- /dev/null +++ b/COMMITMSG @@ -0,0 +1,6 @@ + - dont want to do ineq of a sum when we can do a leq! + before this patch, a leq was being rewritten to ineq(sum(...)) causing + partial-eval-03 to fail. Also, this was being done before the sums were + flattened. + - now have not(X) ~ reify(X,0) where X is a constraint + diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index 585da86989..a49e3cc1b8 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -174,6 +174,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/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index 53357de496..074bc244b0 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -120,10 +120,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 { @@ -230,6 +233,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), } } @@ -326,6 +330,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 1c70a20dc6..e2362000ae 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -12,7 +12,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: @@ -23,7 +23,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; @@ -85,7 +85,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 @@ -102,46 +102,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())), @@ -155,7 +122,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) => { @@ -191,7 +158,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) => { @@ -224,7 +191,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) => { @@ -260,7 +227,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() { @@ -277,7 +244,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) => { @@ -296,7 +263,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) => { @@ -310,114 +277,12 @@ fn remove_trivial_or(expr: &Expr, _: &Model) -> ApplicationResult { } /** - * Remove constant bools from or expressions - * ```text - * or([true, a]) = true - * or([false, a]) = a - * ``` - */ -#[register_rule(("Base", 100))] -fn remove_constants_from_or(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Or(metadata, exprs) => { - let mut new_exprs = Vec::new(); - let mut changed = false; - for e in exprs { - match e { - Expr::Constant(metadata, Const::Bool(val)) => { - if *val { - // If we find a true, the whole expression is true - return Ok(Reduction::pure(Expr::Constant( - metadata.clone_dirty(), - Const::Bool(true), - ))); - } else { - // If we find a false, we can ignore it - changed = true; - } - } - _ => new_exprs.push(e.clone()), - } - } - if !changed { - return Err(ApplicationError::RuleNotApplicable); - } - Ok(Reduction::pure(Expr::Or(metadata.clone_dirty(), new_exprs))) - } - _ => Err(ApplicationError::RuleNotApplicable), - } -} - -/** - * Remove constant bools from and expressions - * ```text - * and([true, a]) = a - * and([false, a]) = false - * ``` - */ -#[register_rule(("Base", 100))] -fn remove_constants_from_and(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::And(metadata, exprs) => { - let mut new_exprs = Vec::new(); - let mut changed = false; - for e in exprs { - match e { - Expr::Constant(metadata, Const::Bool(val)) => { - if !*val { - // If we find a false, the whole expression is false - return Ok(Reduction::pure(Expr::Constant( - metadata.clone_dirty(), - Const::Bool(false), - ))); - } else { - // If we find a true, we can ignore it - changed = true; - } - } - _ => new_exprs.push(e.clone()), - } - } - if !changed { - return Err(ApplicationError::RuleNotApplicable); - } - Ok(Reduction::pure(Expr::And( - metadata.clone_dirty(), - new_exprs, - ))) - } - _ => Err(ApplicationError::RuleNotApplicable), - } -} - -/** - * Evaluate Not expressions with constant bools - * ```text - * not(true) = false - * not(false) = true - * ``` - */ -#[register_rule(("Base", 100))] -fn evaluate_constant_not(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Not(_, contents) => match contents.as_ref() { - Expr::Constant(metadata, Const::Bool(val)) => Ok(Reduction::pure(Expr::Constant( - metadata.clone_dirty(), - Const::Bool(!val), - ))), - _ => Err(ApplicationError::RuleNotApplicable), - }, - _ => Err(ApplicationError::RuleNotApplicable), - } -} - -/** - * Turn a Min into a new variable and post a global 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) => { @@ -462,7 +327,7 @@ fn min_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? @@ -512,7 +377,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() { @@ -543,7 +408,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 866f3b655b..8295a4cb81 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..cca773aba4 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. +/// +/// ``` +/// 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 32a4626ed9..b6718a9419 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::*; @@ -243,5 +243,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..09a157afd3 --- /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::>();