From eaf65adc3afb6ef87a07eda949701952c00a2848 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 10 Jan 2025 14:56:08 +0000 Subject: [PATCH] Add absolute values and convert to Minion Add support for absolute values, in particular: * Parsing from JSON. * The `Abs` expression variant. * The `FlatAbsEq` Minion constraint. * Flattening and conversion to Minion. As part of this change, a division domain bug is fixed. In our domain calculation we use truncating division, the default Rust integer division operator. However, the semantics of Essence Prime specify floor division. Truncating division has the effect of rounding towards 0. Truncating division does `-5 / 2 =-2` and `5/2 = 2`. However, we want `-5/2 = -3` and `5/2 = 2`. This caused the domains of variables containing negative divisions to sometimes be one too high. For abs-03, this caused Oxide to give different solutions than Conjure. --- .../basic/abs/0-simple/config.toml | 1 + .../input-expected-rule-trace-human.txt | 24 ++ .../basic/abs/0-simple/input.eprime | 6 + .../input.expected-minion.solutions.json | 8 + .../input.expected-parse.serialised.json | 66 +++ .../input.expected-rewrite.serialised.json | 42 ++ .../basic/abs/01-simple/config.toml | 2 + .../input-expected-rule-trace-human.txt | 65 +++ .../basic/abs/01-simple/input.eprime | 5 + .../input.expected-minion.solutions.json | 26 ++ .../input.expected-parse.serialised.json | 114 +++++ .../input.expected-rewrite.serialised.json | 171 ++++++++ .../integration/basic/abs/02-neg/config.toml | 2 + .../input-expected-rule-trace-human.txt | 77 ++++ .../integration/basic/abs/02-neg/input.eprime | 5 + .../input.expected-minion.solutions.json | 26 ++ .../input.expected-parse.serialised.json | 130 ++++++ .../input.expected-rewrite.serialised.json | 171 ++++++++ .../basic/abs/03-nested/config.toml | 2 + .../input-expected-rule-trace-human.txt | 284 +++++++++++++ .../basic/abs/03-nested/input.eprime | 7 + .../input.expected-minion.solutions.json | 90 ++++ .../input.expected-parse.serialised.json | 217 ++++++++++ .../input.expected-rewrite.serialised.json | 390 ++++++++++++++++++ .../basic/abs/04-bounds/config.toml | 1 + .../input-expected-rule-trace-human.txt | 43 ++ .../basic/abs/04-bounds/input.eprime | 8 + .../input.expected-minion.solutions.json | 22 + .../input.expected-parse.serialised.json | 106 +++++ .../input.expected-rewrite.serialised.json | 99 +++++ crates/conjure_core/src/ast/expressions.rs | 46 ++- crates/conjure_core/src/parse/parse_model.rs | 4 + crates/conjure_core/src/rules/base.rs | 1 + .../conjure_core/src/rules/constant_eval.rs | 7 + crates/conjure_core/src/rules/minion.rs | 55 +++ crates/conjure_core/src/rules/partial_eval.rs | 5 + .../src/solver/adaptors/minion/parse_model.rs | 3 + solvers/minion/src/run.rs | 6 +- 38 files changed, 2332 insertions(+), 5 deletions(-) create mode 100644 conjure_oxide/tests/integration/basic/abs/0-simple/config.toml create mode 100644 conjure_oxide/tests/integration/basic/abs/0-simple/input-expected-rule-trace-human.txt create mode 100644 conjure_oxide/tests/integration/basic/abs/0-simple/input.eprime create mode 100644 conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-rewrite.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/01-simple/config.toml create mode 100644 conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt create mode 100644 conjure_oxide/tests/integration/basic/abs/01-simple/input.eprime create mode 100644 conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-rewrite.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/02-neg/config.toml create mode 100644 conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt create mode 100644 conjure_oxide/tests/integration/basic/abs/02-neg/input.eprime create mode 100644 conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-rewrite.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/03-nested/config.toml create mode 100644 conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt create mode 100644 conjure_oxide/tests/integration/basic/abs/03-nested/input.eprime create mode 100644 conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-rewrite.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/04-bounds/config.toml create mode 100644 conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt create mode 100644 conjure_oxide/tests/integration/basic/abs/04-bounds/input.eprime create mode 100644 conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-minion.solutions.json create mode 100644 conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-parse.serialised.json create mode 100644 conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-rewrite.serialised.json diff --git a/conjure_oxide/tests/integration/basic/abs/0-simple/config.toml b/conjure_oxide/tests/integration/basic/abs/0-simple/config.toml new file mode 100644 index 0000000000..98e48e9c43 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/0-simple/config.toml @@ -0,0 +1 @@ +use_native_parser=false diff --git a/conjure_oxide/tests/integration/basic/abs/0-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/0-simple/input-expected-rule-trace-human.txt new file mode 100644 index 0000000000..9e3e5c712d --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/0-simple/input-expected-rule-trace-human.txt @@ -0,0 +1,24 @@ +Model before rewriting: + +find x: int(-2..3) + +such that + +(|x| = 1) + +-- + +(|x| = 1), + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(1,x) + +-- + +Final model: + +find x: int(-2..3) + +such that + +AbsEq(1,x) + diff --git a/conjure_oxide/tests/integration/basic/abs/0-simple/input.eprime b/conjure_oxide/tests/integration/basic/abs/0-simple/input.eprime new file mode 100644 index 0000000000..e4cf3f550d --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/0-simple/input.eprime @@ -0,0 +1,6 @@ +language ESSENCE' 1.0 + +find x : int(-2..3) + +such that +|x| = 1 diff --git a/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-minion.solutions.json new file mode 100644 index 0000000000..3f50c4f3ae --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-minion.solutions.json @@ -0,0 +1,8 @@ +[ + { + "x": -1 + }, + { + "x": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-parse.serialised.json new file mode 100644 index 0000000000..109e23fd19 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-parse.serialised.json @@ -0,0 +1,66 @@ +{ + "constraints": [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "x" + } + } + ] + } + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 1 + } + } + ] + } + ] + } + ], + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -2, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..ce12c68b6f --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/0-simple/input.expected-rewrite.serialised.json @@ -0,0 +1,42 @@ +{ + "constraints": [ + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 1 + } + }, + { + "Reference": { + "UserName": "x" + } + } + ] + } + ], + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -2, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/config.toml b/conjure_oxide/tests/integration/basic/abs/01-simple/config.toml new file mode 100644 index 0000000000..d0e6f9dce0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/01-simple/config.toml @@ -0,0 +1,2 @@ +run_solver=true +use_native_parser=false diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt new file mode 100644 index 0000000000..703aa4bd90 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt @@ -0,0 +1,65 @@ +Model before rewriting: + +find x: int(-5..5) +find y: int(-5..5) + +such that + +(Sum([|x|, |y|]) = 10) + +-- + +Sum([|x|, |y|]), + ~~> flatten_vecop ([("Minion", 4200)]) +Sum([__0, __1]) +new variables: + __0: int(0..5) + __1: int(0..5) +new constraints: + __0 =aux |x| + __1 =aux |y| +-- + +__0 =aux |x|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__0,x) + +-- + +__1 =aux |y|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__1,y) + +-- + +(Sum([__0, __1]) = 10), + ~~> sum_eq_to_inequalities ([("Minion", 4100)]) +And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)]) + +-- + +(Sum([__0, __1]) <= 10), + ~~> introduce_sumleq ([("Minion", 4400)]) +SumLeq([__0, __1], 10) + +-- + +(Sum([__0, __1]) >= 10), + ~~> introduce_sumgeq ([("Minion", 4400)]) +SumGeq([__0, __1], 10) + +-- + +Final model: + +find x: int(-5..5) +find y: int(-5..5) +find __0: int(0..5) +find __1: int(0..5) + +such that + +And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)]), +AbsEq(__0,x), +AbsEq(__1,y) + diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input.eprime b/conjure_oxide/tests/integration/basic/abs/01-simple/input.eprime new file mode 100644 index 0000000000..049c03b069 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/01-simple/input.eprime @@ -0,0 +1,5 @@ +language ESSENCE' 1.0 + +find x,y: int(-5..5) + +such that |x| + |y| = 10 diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-minion.solutions.json new file mode 100644 index 0000000000..db4650a1d0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-minion.solutions.json @@ -0,0 +1,26 @@ +[ + { + "__0": 5, + "__1": 5, + "x": -5, + "y": -5 + }, + { + "__0": 5, + "__1": 5, + "x": -5, + "y": 5 + }, + { + "__0": 5, + "__1": 5, + "x": 5, + "y": -5 + }, + { + "__0": 5, + "__1": 5, + "x": 5, + "y": 5 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-parse.serialised.json new file mode 100644 index 0000000000..3b85444ab2 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-parse.serialised.json @@ -0,0 +1,114 @@ +{ + "constraints": [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "x" + } + } + ] + } + ] + }, + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "y" + } + } + ] + } + ] + } + ] + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 10 + } + } + ] + } + ] + } + ], + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..c4278959b2 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-rewrite.serialised.json @@ -0,0 +1,171 @@ +{ + "constraints": [ + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "FlatSumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ], + { + "Literal": { + "Int": 10 + } + } + ] + }, + { + "FlatSumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ], + { + "Literal": { + "Int": 10 + } + } + ] + } + ] + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "UserName": "x" + } + } + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 1 + } + }, + { + "Reference": { + "UserName": "y" + } + } + ] + } + ], + "next_var": 2, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 5 + ] + } + ] + } + } + ], + [ + { + "MachineName": 1 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/config.toml b/conjure_oxide/tests/integration/basic/abs/02-neg/config.toml new file mode 100644 index 0000000000..d0e6f9dce0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/02-neg/config.toml @@ -0,0 +1,2 @@ +run_solver=true +use_native_parser=false diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt new file mode 100644 index 0000000000..e94addf01e --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt @@ -0,0 +1,77 @@ +Model before rewriting: + +find x: int(-5..5) +find y: int(-5..5) + +such that + +(Sum([|-(x)|, |-(y)|]) = 10) + +-- + +|-(x)|, + ~~> partial_evaluator ([("Base", 9000)]) +|x| + +-- + +|-(y)|, + ~~> partial_evaluator ([("Base", 9000)]) +|y| + +-- + +Sum([|x|, |y|]), + ~~> flatten_vecop ([("Minion", 4200)]) +Sum([__0, __1]) +new variables: + __0: int(0..5) + __1: int(0..5) +new constraints: + __0 =aux |x| + __1 =aux |y| +-- + +__0 =aux |x|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__0,x) + +-- + +__1 =aux |y|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__1,y) + +-- + +(Sum([__0, __1]) = 10), + ~~> sum_eq_to_inequalities ([("Minion", 4100)]) +And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)]) + +-- + +(Sum([__0, __1]) <= 10), + ~~> introduce_sumleq ([("Minion", 4400)]) +SumLeq([__0, __1], 10) + +-- + +(Sum([__0, __1]) >= 10), + ~~> introduce_sumgeq ([("Minion", 4400)]) +SumGeq([__0, __1], 10) + +-- + +Final model: + +find x: int(-5..5) +find y: int(-5..5) +find __0: int(0..5) +find __1: int(0..5) + +such that + +And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)]), +AbsEq(__0,x), +AbsEq(__1,y) + diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input.eprime b/conjure_oxide/tests/integration/basic/abs/02-neg/input.eprime new file mode 100644 index 0000000000..ff79ba7fdf --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/02-neg/input.eprime @@ -0,0 +1,5 @@ +language ESSENCE' 1.0 + +find x,y: int(-5..5) + +such that |-x| + |-y| = 10 diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-minion.solutions.json new file mode 100644 index 0000000000..db4650a1d0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-minion.solutions.json @@ -0,0 +1,26 @@ +[ + { + "__0": 5, + "__1": 5, + "x": -5, + "y": -5 + }, + { + "__0": 5, + "__1": 5, + "x": -5, + "y": 5 + }, + { + "__0": 5, + "__1": 5, + "x": 5, + "y": -5 + }, + { + "__0": 5, + "__1": 5, + "x": 5, + "y": 5 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-parse.serialised.json new file mode 100644 index 0000000000..4106ba1516 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-parse.serialised.json @@ -0,0 +1,130 @@ +{ + "constraints": [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Neg": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "x" + } + } + ] + } + ] + } + ] + }, + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Neg": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "y" + } + } + ] + } + ] + } + ] + } + ] + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 10 + } + } + ] + } + ] + } + ], + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..c4278959b2 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-rewrite.serialised.json @@ -0,0 +1,171 @@ +{ + "constraints": [ + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "FlatSumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ], + { + "Literal": { + "Int": 10 + } + } + ] + }, + { + "FlatSumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ], + { + "Literal": { + "Int": 10 + } + } + ] + } + ] + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "UserName": "x" + } + } + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 1 + } + }, + { + "Reference": { + "UserName": "y" + } + } + ] + } + ], + "next_var": 2, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 5 + ] + } + ] + } + } + ], + [ + { + "MachineName": 1 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/config.toml b/conjure_oxide/tests/integration/basic/abs/03-nested/config.toml new file mode 100644 index 0000000000..d0e6f9dce0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/03-nested/config.toml @@ -0,0 +1,2 @@ +run_solver=true +use_native_parser=false diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt new file mode 100644 index 0000000000..65309324be --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt @@ -0,0 +1,284 @@ +Model before rewriting: + +find x: int(-5..2) +find y: int(-5..2) +find z: int(-5..2) + +such that + +(Sum([|(Sum([UnsafeDiv(x, 2), y]) - z)|, UnsafeDiv(|y|, 2)]) = 10) + +-- + +(Sum([UnsafeDiv(x, 2), y]) - z), + ~~> minus_to_sum ([("Base", 8400)]) +Sum([Sum([UnsafeDiv(x, 2), y]), -(z)]) + +-- + +Sum([Sum([UnsafeDiv(x, 2), y]), -(z)]), + ~~> normalise_associative_commutative ([("Base", 8900)]) +Sum([UnsafeDiv(x, 2), y, -(z)]) + +-- + +UnsafeDiv(x, 2), + ~~> div_to_bubble ([("Bubble", 6000)]) +{SafeDiv(x, 2) @ (2 != 0)} + +-- + +(2 != 0), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +Sum([{SafeDiv(x, 2) @ true}, y, -(z)]), + ~~> bubble_up ([("Bubble", 8900)]) +{Sum([SafeDiv(x, 2), y, -(z)]) @ And([true])} + +-- + +And([true]), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +|{Sum([SafeDiv(x, 2), y, -(z)]) @ true}|, + ~~> bubble_up ([("Bubble", 8900)]) +{|Sum([SafeDiv(x, 2), y, -(z)])| @ And([true])} + +-- + +And([true]), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +Sum([{|Sum([SafeDiv(x, 2), y, -(z)])| @ true}, UnsafeDiv(|y|, 2)]), + ~~> bubble_up ([("Bubble", 8900)]) +{Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) @ And([true])} + +-- + +And([true]), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +({Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) @ true} = 10), + ~~> bubble_up ([("Bubble", 8900)]) +{(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10) @ And([true])} + +-- + +And([true]), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +{(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10) @ true}, + ~~> expand_bubble ([("Bubble", 8900)]) +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10), true]) + +-- + +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10), true]), + ~~> partial_evaluator ([("Base", 9000)]) +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10)]) + +-- + +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10)]), + ~~> remove_unit_vector_and ([("Base", 8800)]) +(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, UnsafeDiv(|y|, 2)]) = 10) + +-- + +UnsafeDiv(|y|, 2), + ~~> div_to_bubble ([("Bubble", 6000)]) +{SafeDiv(|y|, 2) @ (2 != 0)} + +-- + +(2 != 0), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, {SafeDiv(|y|, 2) @ true}]), + ~~> bubble_up ([("Bubble", 8900)]) +{Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) @ And([true])} + +-- + +And([true]), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +({Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) @ true} = 10), + ~~> bubble_up ([("Bubble", 8900)]) +{(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10) @ And([true])} + +-- + +And([true]), + ~~> apply_eval_constant ([("Constant", 9001)]) +true + +-- + +{(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10) @ true}, + ~~> expand_bubble ([("Bubble", 8900)]) +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10), true]) + +-- + +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10), true]), + ~~> partial_evaluator ([("Base", 9000)]) +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10)]) + +-- + +And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10)]), + ~~> remove_unit_vector_and ([("Base", 8800)]) +(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10) + +-- + +Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]), + ~~> flatten_vecop ([("Minion", 4200)]) +Sum([__0, __1]) +new variables: + __0: int(0..10) + __1: int(0..2) +new constraints: + __0 =aux |Sum([SafeDiv(x, 2), y, -(z)])| + __1 =aux SafeDiv(|y|, 2) +-- + +|Sum([SafeDiv(x, 2), y, -(z)])|, + ~~> flatten_unop ([("Minion", 4200)]) +|__2| +new variables: + __2: int(-10..8) +new constraints: + __2 =aux Sum([SafeDiv(x, 2), y, -(z)]) +-- + +__0 =aux |__2|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__0,__2) + +-- + +SafeDiv(|y|, 2), + ~~> flatten_binop ([("Minion", 4200)]) +SafeDiv(__3, 2) +new variables: + __3: int(0..5) +new constraints: + __3 =aux |y| +-- + +__3 =aux |y|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__3,y) + +-- + +__1 =aux SafeDiv(__3, 2), + ~~> introduce_diveq ([("Minion", 4200)]) +DivEq(__3, 2, __1) + +-- + +Sum([SafeDiv(x, 2), y, -(z)]), + ~~> flatten_vecop ([("Minion", 4200)]) +Sum([__4, y, __5]) +new variables: + __4: int(-3..1) + __5: int(-2..5) +new constraints: + __4 =aux SafeDiv(x, 2) + __5 =aux -(z) +-- + +__5 =aux -(z), + ~~> introduce_minuseq_from_aux_decl ([("Minion", 4400)]) +MinusEq(__5,z) + +-- + +__4 =aux SafeDiv(x, 2), + ~~> introduce_diveq ([("Minion", 4200)]) +DivEq(x, 2, __4) + +-- + +(Sum([__0, __1]) = 10), + ~~> sum_eq_to_inequalities ([("Minion", 4100)]) +And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)]) + +-- + +(Sum([__0, __1]) <= 10), + ~~> introduce_sumleq ([("Minion", 4400)]) +SumLeq([__0, __1], 10) + +-- + +(Sum([__0, __1]) >= 10), + ~~> introduce_sumgeq ([("Minion", 4400)]) +SumGeq([__0, __1], 10) + +-- + +__2 =aux Sum([__4, y, __5]), + ~~> sum_eq_to_inequalities ([("Minion", 4100)]) +And([(Sum([__4, y, __5]) <= __2), (Sum([__4, y, __5]) >= __2)]) + +-- + +(Sum([__4, y, __5]) <= __2), + ~~> introduce_sumleq ([("Minion", 4400)]) +SumLeq([__4, y, __5], __2) + +-- + +(Sum([__4, y, __5]) >= __2), + ~~> introduce_sumgeq ([("Minion", 4400)]) +SumGeq([__4, y, __5], __2) + +-- + +Final model: + +find x: int(-5..2) +find y: int(-5..2) +find z: int(-5..2) +find __0: int(0..10) +find __1: int(0..2) +find __2: int(-10..8) +find __3: int(0..5) +find __4: int(-3..1) +find __5: int(-2..5) + +such that + +And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)]), +AbsEq(__0,__2), +DivEq(__3, 2, __1), +And([SumLeq([__4, y, __5], __2), SumGeq([__4, y, __5], __2)]), +AbsEq(__3,y), +DivEq(x, 2, __4), +MinusEq(__5,z) + diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input.eprime b/conjure_oxide/tests/integration/basic/abs/03-nested/input.eprime new file mode 100644 index 0000000000..b43b98b906 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/03-nested/input.eprime @@ -0,0 +1,7 @@ +language ESSENCE' 1.0 + +find x,y,z: int(-5..2) + +$ 1. stuff inside the abs to be flattened +$ 2. the abs itself needs to be flattened +such that |((x/2)+y-z)| + (|y|/2) = 10 diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-minion.solutions.json new file mode 100644 index 0000000000..1824f6cb51 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-minion.solutions.json @@ -0,0 +1,90 @@ +[ + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 4, + "__4": -2, + "__5": -2, + "x": -3, + "y": -4, + "z": 2 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 4, + "__4": -2, + "__5": -2, + "x": -4, + "y": -4, + "z": 2 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 4, + "__4": -3, + "__5": -1, + "x": -5, + "y": -4, + "z": 1 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 5, + "__4": -1, + "__5": -2, + "x": -1, + "y": -5, + "z": 2 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 5, + "__4": -1, + "__5": -2, + "x": -2, + "y": -5, + "z": 2 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 5, + "__4": -2, + "__5": -1, + "x": -3, + "y": -5, + "z": 1 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 5, + "__4": -2, + "__5": -1, + "x": -4, + "y": -5, + "z": 1 + }, + { + "__0": 8, + "__1": 2, + "__2": -8, + "__3": 5, + "__4": -3, + "__5": 0, + "x": -5, + "y": -5, + "z": 0 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-parse.serialised.json new file mode 100644 index 0000000000..ec7b17294a --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-parse.serialised.json @@ -0,0 +1,217 @@ +{ + "constraints": [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Minus": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "UnsafeDiv": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "x" + } + } + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 2 + } + } + ] + } + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "y" + } + } + ] + } + ] + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "z" + } + } + ] + } + ] + } + ] + }, + { + "UnsafeDiv": [ + { + "clean": false, + "etype": null + }, + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "y" + } + } + ] + } + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 2 + } + } + ] + } + ] + } + ] + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 10 + } + } + ] + } + ] + } + ], + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 2 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 2 + ] + } + ] + } + } + ], + [ + { + "UserName": "z" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 2 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..9c274979cc --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/03-nested/input.expected-rewrite.serialised.json @@ -0,0 +1,390 @@ +{ + "constraints": [ + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "FlatSumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ], + { + "Literal": { + "Int": 10 + } + } + ] + }, + { + "FlatSumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ], + { + "Literal": { + "Int": 10 + } + } + ] + } + ] + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "MachineName": 2 + } + } + ] + }, + { + "MinionDivEqUndefZero": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 3 + } + }, + { + "Literal": { + "Int": 2 + } + }, + { + "Reference": { + "MachineName": 1 + } + } + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "FlatSumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 4 + } + }, + { + "Reference": { + "UserName": "y" + } + }, + { + "Reference": { + "MachineName": 5 + } + } + ], + { + "Reference": { + "MachineName": 2 + } + } + ] + }, + { + "FlatSumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": { + "MachineName": 4 + } + }, + { + "Reference": { + "UserName": "y" + } + }, + { + "Reference": { + "MachineName": 5 + } + } + ], + { + "Reference": { + "MachineName": 2 + } + } + ] + } + ] + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 3 + } + }, + { + "Reference": { + "UserName": "y" + } + } + ] + }, + { + "MinionDivEqUndefZero": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "x" + } + }, + { + "Literal": { + "Int": 2 + } + }, + { + "Reference": { + "MachineName": 4 + } + } + ] + }, + { + "FlatMinusEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 5 + } + }, + { + "Reference": { + "UserName": "z" + } + } + ] + } + ], + "next_var": 6, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 10 + ] + } + ] + } + } + ], + [ + { + "MachineName": 1 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 2 + ] + } + ] + } + } + ], + [ + { + "MachineName": 2 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -10, + 8 + ] + } + ] + } + } + ], + [ + { + "MachineName": 3 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 5 + ] + } + ] + } + } + ], + [ + { + "MachineName": 4 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -3, + 1 + ] + } + ] + } + } + ], + [ + { + "MachineName": 5 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -2, + 5 + ] + } + ] + } + } + ], + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 2 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 2 + ] + } + ] + } + } + ], + [ + { + "UserName": "z" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -5, + 2 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/config.toml b/conjure_oxide/tests/integration/basic/abs/04-bounds/config.toml new file mode 100644 index 0000000000..98e48e9c43 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/config.toml @@ -0,0 +1 @@ +use_native_parser=false diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt new file mode 100644 index 0000000000..085ec347a6 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt @@ -0,0 +1,43 @@ +Model before rewriting: + +find x: int(-2..3) +find y: int(1..3) + +such that + +(Product([y, |x|]) = 2) + +-- + +Product([y, |x|]), + ~~> flatten_vecop ([("Minion", 4200)]) +Product([y, __0]) +new variables: + __0: int(0..3) +new constraints: + __0 =aux |x| +-- + +__0 =aux |x|, + ~~> introduce_abseq ([("Minion", 4400)]) +AbsEq(__0,x) + +-- + +(Product([y, __0]) = 2), + ~~> introduce_producteq ([("Minion", 4200)]) +FlatProductEq(__0,y,2) + +-- + +Final model: + +find x: int(-2..3) +find y: int(1..3) +find __0: int(0..3) + +such that + +FlatProductEq(__0,y,2), +AbsEq(__0,x) + diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input.eprime b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.eprime new file mode 100644 index 0000000000..2524f4241a --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.eprime @@ -0,0 +1,8 @@ +language ESSENCE' 1.0 + +$ should get aux var with bounds int(0..3), not int(2..3) +find x : int(-2..3) +find y: int(1..3) + +such that +y * |x| = 2 diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-minion.solutions.json new file mode 100644 index 0000000000..a40e9ac4f0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-minion.solutions.json @@ -0,0 +1,22 @@ +[ + { + "__0": 1, + "x": -1, + "y": 2 + }, + { + "__0": 1, + "x": 1, + "y": 2 + }, + { + "__0": 2, + "x": -2, + "y": 1 + }, + { + "__0": 2, + "x": 2, + "y": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-parse.serialised.json new file mode 100644 index 0000000000..1ee6cc3e98 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-parse.serialised.json @@ -0,0 +1,106 @@ +{ + "constraints": [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Product": [ + { + "clean": false, + "etype": null + }, + [ + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "y" + } + } + ] + }, + { + "Abs": [ + { + "clean": false, + "etype": null + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "UserName": "x" + } + } + ] + } + ] + } + ] + ] + }, + { + "Atomic": [ + { + "clean": false, + "etype": null + }, + { + "Literal": { + "Int": 2 + } + } + ] + } + ] + } + ], + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -2, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 3 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..c22167f72b --- /dev/null +++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/input.expected-rewrite.serialised.json @@ -0,0 +1,99 @@ +{ + "constraints": [ + { + "FlatProductEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "UserName": "y" + } + }, + { + "Literal": { + "Int": 2 + } + } + ] + }, + { + "FlatAbsEq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": { + "MachineName": 0 + } + }, + { + "Reference": { + "UserName": "x" + } + } + ] + } + ], + "next_var": 1, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 0, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + -2, + 3 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 3 + ] + } + ] + } + } + ] + ] +} \ 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 77dd723a32..cdba8de76e 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -35,6 +35,10 @@ pub enum Expression { Atomic(Metadata, Atom), + /// `|x|` - absolute value of `x` + #[compatible(JsonInput)] + Abs(Metadata, Box), + #[compatible(JsonInput)] Sum(Metadata, Vec), @@ -101,6 +105,16 @@ pub enum Expression { #[compatible(JsonInput)] Minus(Metadata, Box, Box), + /// Ensures that x=|y| i.e. x is the absolute value of y. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#abs) + #[compatible(Minion)] + FlatAbsEq(Metadata, Atom, Atom), + /// Ensures that sum(vec) >= x. /// /// Low-level Minion constraint. @@ -288,12 +302,28 @@ impl Expression { expr_vec_to_domain_i32(exprs, |x, y| Some(if x > y { x } else { y }), vars) } Expression::UnsafeDiv(_, a, b) => a.domain_of(vars)?.apply_i32( - |x, y| if y != 0 { Some(x / y) } else { None }, + // rust integer division is truncating; however, we want to always round down, + // including for negative numbers. + |x, y| { + if y != 0 { + Some((x as f32 / y as f32).floor() as i32) + } else { + None + } + }, &b.domain_of(vars)?, ), Expression::SafeDiv(_, a, b) => { + // rust integer division is truncating; however, we want to always round down + // including for negative numbers. let domain = a.domain_of(vars)?.apply_i32( - |x, y| if y != 0 { Some(x / y) } else { None }, + |x, y| { + if y != 0 { + Some((x as f32 / y as f32).floor() as i32) + } else { + None + } + }, &b.domain_of(vars)?, ); @@ -340,6 +370,7 @@ impl Expression { Expression::Leq(_, _, _) => Some(Domain::BoolDomain), Expression::Gt(_, _, _) => Some(Domain::BoolDomain), Expression::Lt(_, _, _) => Some(Domain::BoolDomain), + Expression::FlatAbsEq(_, _, _) => Some(Domain::BoolDomain), Expression::FlatSumGeq(_, _, _) => Some(Domain::BoolDomain), Expression::FlatSumLeq(_, _, _) => Some(Domain::BoolDomain), Expression::MinionDivEqUndefZero(_, _, _, _) => Some(Domain::BoolDomain), @@ -370,8 +401,9 @@ impl Expression { Expression::FlatProductEq(_, _, _, _) => Some(Domain::BoolDomain), Expression::FlatWeightedSumLeq(_, _, _, _) => Some(Domain::BoolDomain), Expression::FlatWeightedSumGeq(_, _, _, _) => Some(Domain::BoolDomain), - // #[allow(unreachable_patterns)] - // _ => bug!("Cannot calculate domain of {:?}", self), + Expression::Abs(_, a) => a + .domain_of(vars)? + .apply_i32(|a, _| Some(a.abs()), &a.domain_of(vars)?), }; match ret { // TODO: (flm8) the Minion bindings currently only support single ranges for domains, so we use the min/max bounds @@ -416,6 +448,7 @@ impl Expression { Expression::Atomic(_, Atom::Literal(Literal::Int(_))) => Some(ReturnType::Int), Expression::Atomic(_, Atom::Literal(Literal::Bool(_))) => Some(ReturnType::Bool), Expression::Atomic(_, Atom::Reference(_)) => None, + Expression::Abs(_, _) => Some(ReturnType::Int), Expression::Sum(_, _) => Some(ReturnType::Int), Expression::Product(_, _) => Some(ReturnType::Int), Expression::Min(_, _) => Some(ReturnType::Int), @@ -445,6 +478,7 @@ impl Expression { Expression::MinionModuloEqUndefZero(_, _, _, _) => Some(ReturnType::Bool), Expression::Neg(_, _) => Some(ReturnType::Int), Expression::Minus(_, _, _) => Some(ReturnType::Int), + Expression::FlatAbsEq(_, _, _) => Some(ReturnType::Bool), Expression::FlatMinusEq(_, _, _) => Some(ReturnType::Bool), Expression::FlatProductEq(_, _, _, _) => Some(ReturnType::Bool), Expression::FlatWeightedSumLeq(_, _, _, _) => Some(ReturnType::Bool), @@ -497,6 +531,7 @@ impl Display for Expression { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { match &self { Expression::Atomic(_, atom) => atom.fmt(f), + Expression::Abs(_, a) => write!(f, "|{}|", a), Expression::Sum(_, expressions) => { write!(f, "Sum({})", pretty_vec(expressions)) } @@ -601,6 +636,9 @@ impl Display for Expression { Expression::Minus(_, a, b) => { write!(f, "({} - {})", a.clone(), b.clone()) } + Expression::FlatAbsEq(_, a, b) => { + write!(f, "AbsEq({},{})", a.clone(), b.clone()) + } Expression::FlatMinusEq(_, a, b) => { write!(f, "MinusEq({},{})", a.clone(), b.clone()) } diff --git a/crates/conjure_core/src/parse/parse_model.rs b/crates/conjure_core/src/parse/parse_model.rs index 07792d8801..e5bacf11a7 100644 --- a/crates/conjure_core/src/parse/parse_model.rs +++ b/crates/conjure_core/src/parse/parse_model.rs @@ -257,6 +257,10 @@ fn parse_expression(obj: &JsonValue) -> Option { "MkOpNegate", Box::new(Expression::Neg) as Box _>, ), + ( + "MkOpTwoBars", + Box::new(Expression::Abs) as Box _>, + ), ] .into_iter() .collect(); diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs index ec4eb37a17..9c611ea789 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -39,6 +39,7 @@ fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult { | MinionDivEqUndefZero(_, _, _, _) | MinionModuloEqUndefZero(_, _, _, _) | MinionReify(_, _, _) + | FlatAbsEq(_, _, _) ) { return Err(ApplicationError::RuleNotApplicable); } diff --git a/crates/conjure_core/src/rules/constant_eval.rs b/crates/conjure_core/src/rules/constant_eval.rs index 49a33571b9..7c4d5cd58e 100644 --- a/crates/conjure_core/src/rules/constant_eval.rs +++ b/crates/conjure_core/src/rules/constant_eval.rs @@ -28,6 +28,7 @@ pub fn eval_constant(expr: &Expr) -> Option { match expr { Expr::Atomic(_, Atom::Literal(c)) => Some(c.clone()), Expr::Atomic(_, Atom::Reference(_c)) => None, + Expr::Abs(_, e) => un_op::(|a| a.abs(), e).map(Lit::Int), Expr::Eq(_, a, b) => bin_op::(|a, b| a == b, a, b) .or_else(|| bin_op::(|a, b| a == b, a, b)) .map(Lit::Bool), @@ -206,6 +207,12 @@ pub fn eval_constant(expr: &Expr) -> Option { Some(Lit::Bool(sum >= total)) } + Expr::FlatAbsEq(_, x, y) => { + let x: i32 = x.try_into().ok()?; + let y: i32 = y.try_into().ok()?; + + Some(Lit::Bool(x == y.abs())) + } } } diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index 532d93b78a..6ed43e144c 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -405,6 +405,36 @@ fn introduce_modeq(expr: &Expr, _: &Model) -> ApplicationResult { ))) } +#[register_rule(("Minion", 4400))] +fn introduce_abseq(expr: &Expr, _: &Model) -> ApplicationResult { + let (x, abs_y): (Atom, Expr) = match expr.clone() { + Expr::Eq(_, a, b) => { + let a_atom: Option<&Atom> = (&*a).try_into().ok(); + let b_atom: Option<&Atom> = (&*b).try_into().ok(); + + if let Some(a_atom) = a_atom { + Ok((a_atom.clone(), *b)) + } else if let Some(b_atom) = b_atom { + Ok((b_atom.clone(), *a)) + } else { + Err(RuleNotApplicable) + } + } + + Expr::AuxDeclaration(_, a, b) => Ok((a.into(), *b)), + + _ => Err(RuleNotApplicable), + }?; + + let Expr::Abs(_, y) = abs_y else { + return Err(RuleNotApplicable); + }; + + let y: Atom = (*y).try_into().or(Err(RuleNotApplicable))?; + + Ok(Reduction::pure(Expr::FlatAbsEq(Metadata::new(), x, y))) +} + /// Introduces a Minion `MinusEq` constraint from `x = -y`, where x and y are atoms. /// /// ```text @@ -505,6 +535,31 @@ fn flatten_binop(expr: &Expr, model: &Model) -> ApplicationResult { Ok(Reduction::new(expr, new_tops, model.variables)) } +#[register_rule(("Minion", 4200))] +fn flatten_unop(expr: &Expr, model: &Model) -> ApplicationResult { + if !matches!(expr, Expr::Abs(_, _)) { + return Err(RuleNotApplicable); + } + + let mut children = expr.children(); + debug_assert_eq!(children.len(), 1); + let child = &mut children[0]; + + let mut model = model.clone(); + let mut new_tops: Vec = vec![]; + + if let Some(aux_var_info) = to_aux_var(child, &model) { + model = aux_var_info.model(); + new_tops.push(aux_var_info.top_level_expr()); + *child = aux_var_info.as_expr(); + } else { + return Err(RuleNotApplicable); + } + + let expr = expr.with_children(children); + Ok(Reduction::new(expr, new_tops, model.variables)) +} + #[register_rule(("Minion", 4200))] fn flatten_vecop(expr: &Expr, model: &Model) -> ApplicationResult { if !matches!(expr, Expr::Sum(_, _) | Expr::Product(_, _)) { diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs index 6f597b2640..52baed35b5 100644 --- a/crates/conjure_core/src/rules/partial_eval.rs +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -17,6 +17,10 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { match expr.clone() { Bubble(_, _, _) => Err(RuleNotApplicable), Atomic(_, _) => Err(RuleNotApplicable), + Abs(m, e) => match *e { + Neg(_, inner) => Ok(Reduction::pure(Abs(m, inner))), + _ => Err(RuleNotApplicable), + }, Sum(m, vec) => { let mut acc = 0; let mut n_consts = 0; @@ -222,6 +226,7 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { // As these are in a low level solver form, I'm assuming that these have already been // simplified and partially evaluated. + FlatAbsEq(_, _, _) => Err(RuleNotApplicable), FlatIneq(_, _, _, _) => Err(RuleNotApplicable), FlatMinusEq(_, _, _) => Err(RuleNotApplicable), FlatProductEq(_, _, _, _) => Err(RuleNotApplicable), diff --git a/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs b/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs index be10b287f7..c4198a8ab3 100644 --- a/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs +++ b/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs @@ -235,6 +235,9 @@ fn parse_expr(expr: conjure_ast::Expression) -> Result { + Ok(minion_ast::Constraint::Abs(parse_atom(x)?, parse_atom(y)?)) + } x => Err(ModelFeatureNotSupported(format!("{:?}", x))), } } diff --git a/solvers/minion/src/run.rs b/solvers/minion/src/run.rs index ebe51033ba..fea5aba0a3 100644 --- a/solvers/minion/src/run.rs +++ b/solvers/minion/src/run.rs @@ -582,7 +582,11 @@ unsafe fn constraint_add_args( } //Constraint::WNotInRange(_, _) => todo!(), //Constraint::WNotInset(_, _) => todo!(), - //Constraint::Abs(_, _) => todo!(), + Constraint::Abs(a, b) => { + read_var(i, r_constr, a)?; + read_var(i, r_constr, b)?; + Ok(()) + } Constraint::DisEq(a, b) => { read_var(i, r_constr, a)?; read_var(i, r_constr, b)?;