diff --git a/.gitignore b/.gitignore index f1a67c9948..53c9ba7e86 100644 --- a/.gitignore +++ b/.gitignore @@ -180,4 +180,7 @@ fabric.properties *.eprime.infor *.eprime.minion *.eprime.solution +*.eprime.solution.* *.eprime.info + +.MINION* diff --git a/conjure_oxide/src/main.rs b/conjure_oxide/src/main.rs index b37910c6cf..00da3b4737 100644 --- a/conjure_oxide/src/main.rs +++ b/conjure_oxide/src/main.rs @@ -97,10 +97,10 @@ pub fn main() -> AnyhowResult<()> { .append(true) .open("conjure_oxide.log")?; - //Builder::with_level("Trace") - Builder::new() + Builder::with_level("TRACE") + //Builder::new() .with_target_writer("info", new_writer(stdout())) - .with_target_writer("file", new_writer(log_file)) + .with_target_writer("file,jsonparser", new_writer(log_file)) .init(); if target_family != SolverFamily::Minion { diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index 698e3ac330..6619c90069 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -145,7 +145,7 @@ fn integration_test_inner( } fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) { - model.constraints.descend(Arc::new(|x| { + model.constraints.transform(Arc::new(|x| { use conjure_core::ast::Expression::*; match &x { Nothing => (), @@ -171,7 +171,11 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) SumLeq(_, vec, _) => assert_constants_leq_one(&x, vec), DivEq(_, _, _, _) => (), Ineq(_, _, _, _) => (), - AllDiff(_, vec) => assert_constants_leq_one(&x, vec), + // this is a vector operation, but we don't want to fold values into each-other in this + // one + AllDiff(_, _) => (), + 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/bugs/issue-336-empty-or-should-be-false/input.essence b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.essence new file mode 100644 index 0000000000..f471740fb1 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.essence @@ -0,0 +1,7 @@ + +$ "By mathematical tradition (and Essence semantics), an 'empty or' is false, however, this model has 5 answers (one for each value of a)" +$ -- https://github.com/conjure-cp/conjure-oxide/issues/366 + +find a : int(1..5) +such that +or([]) diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json new file mode 100644 index 0000000000..0637a088a0 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-minion.solutions.json @@ -0,0 +1 @@ +[] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json new file mode 100644 index 0000000000..081ff69222 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-parse.serialised.json @@ -0,0 +1,31 @@ +{ + "constraints": { + "Or": [ + { + "clean": false, + "etype": null + }, + [] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..6d33b6e63d --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/issue-336-empty-or-should-be-false/input.expected-rewrite.serialised.json @@ -0,0 +1,33 @@ +{ + "constraints": { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": false + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 5 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence new file mode 100644 index 0000000000..29087c0d99 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.essence @@ -0,0 +1,5 @@ +$ test case by sm600, 11/10/2024 +$ this would never terminate + +find a,b : int(1..7) +such that min([a,b]) + 6 <= 10 diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json new file mode 100644 index 0000000000..f8773303c0 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-minion.solutions.json @@ -0,0 +1,202 @@ +[ + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 2 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 3 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 4 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 5 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 6 + }, + { + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 7 + }, + { + "MachineName(0)": 1, + "UserName(a)": 2, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 3, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 4, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 5, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 6, + "UserName(b)": 1 + }, + { + "MachineName(0)": 1, + "UserName(a)": 7, + "UserName(b)": 1 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 3 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 4 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 5 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 6 + }, + { + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 7 + }, + { + "MachineName(0)": 2, + "UserName(a)": 3, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 4, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 5, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 6, + "UserName(b)": 2 + }, + { + "MachineName(0)": 2, + "UserName(a)": 7, + "UserName(b)": 2 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 4 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 5 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 6 + }, + { + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 7 + }, + { + "MachineName(0)": 3, + "UserName(a)": 4, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 5, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 6, + "UserName(b)": 3 + }, + { + "MachineName(0)": 3, + "UserName(a)": 7, + "UserName(b)": 3 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 4 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 5 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 6 + }, + { + "MachineName(0)": 4, + "UserName(a)": 4, + "UserName(b)": 7 + }, + { + "MachineName(0)": 4, + "UserName(a)": 5, + "UserName(b)": 4 + }, + { + "MachineName(0)": 4, + "UserName(a)": 6, + "UserName(b)": 4 + }, + { + "MachineName(0)": 4, + "UserName(a)": 7, + "UserName(b)": 4 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json new file mode 100644 index 0000000000..08be1f5ad8 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-parse.serialised.json @@ -0,0 +1,111 @@ +{ + "constraints": { + "Leq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Min": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 6 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..a6a1af1be3 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json @@ -0,0 +1,250 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 4 + } + ] + } + ] + }, + { + "Ineq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 0 + } + ] + } + ] + }, + { + "Ineq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 0 + } + ] + } + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + } + ] + }, + { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "MachineName": 0 + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 1, + "variables": [ + [ + { + "MachineName": 0 + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ], + [ + { + "UserName": "a" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ], + [ + { + "UserName": "b" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence new file mode 100644 index 0000000000..094a8cfefb --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.essence @@ -0,0 +1,5 @@ +$ the parser would read the min as Nothing... +$ related: issue-366 + +find c : int(1..7) +such that min([5,7]) + c <= 10 diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json new file mode 100644 index 0000000000..7509f68790 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-minion.solutions.json @@ -0,0 +1,17 @@ +[ + { + "UserName(c)": 1 + }, + { + "UserName(c)": 2 + }, + { + "UserName(c)": 3 + }, + { + "UserName(c)": 4 + }, + { + "UserName(c)": 5 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json new file mode 100644 index 0000000000..299cb30c6c --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-parse.serialised.json @@ -0,0 +1,94 @@ +{ + "constraints": { + "Leq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Min": [ + { + "clean": false, + "etype": null + }, + [ + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 7 + } + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..11311f4a71 --- /dev/null +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input.expected-rewrite.serialised.json @@ -0,0 +1,54 @@ +{ + "constraints": { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + } + ] + }, + "next_var": 1, + "variables": [ + [ + { + "UserName": "c" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 7 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime new file mode 100644 index 0000000000..66675954ea --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.eprime @@ -0,0 +1,12 @@ +$ top level variables in and's and or's should be converted to wlit(x,1). +$ negations should be converted to wlit(x,0) + +language ESSENCE' 1.0 + +find a,b,c,d: bool +such that + a \/ b, + !c \/ (b /\ d), + b, + d \/ c + diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json new file mode 100644 index 0000000000..15ef0b1e30 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-minion.solutions.json @@ -0,0 +1,26 @@ +[ + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 0, + "UserName(d)": 1 + }, + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1, + "UserName(d)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 0, + "UserName(d)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 1, + "UserName(d)": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json new file mode 100644 index 0000000000..49ac787ba2 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-parse.serialised.json @@ -0,0 +1,183 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Not": [ + { + "clean": false, + "etype": null + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + } + ] + } + ] + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + } + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "d" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..696ccc0df2 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/bool/literals-to-wlit-1/input.expected-rewrite.serialised.json @@ -0,0 +1,213 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": false + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": false + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "d" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": true + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "d" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/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-add/input.eprime.disabled b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.eprime similarity index 100% rename from conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime.disabled rename to conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.eprime 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..4dcc11f11c --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-parse.serialised.json @@ -0,0 +1,188 @@ +{ + "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 + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "AllDiff": [ + { + "clean": false, + "etype": null + }, + [ + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 1 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 2 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 3 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..aa28296e44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-02-or-and/input.expected-rewrite.serialised.json @@ -0,0 +1,91 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled b/conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled new file mode 100644 index 0000000000..b327bb9231 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-03/input.eprime.disabled @@ -0,0 +1,16 @@ +language ESSENCE' 1.0 + + +$ nesting, sumleqs, and mins + +find x,y,z : int(1..5) +find a: bool + +such that + 20 + x + 5 + y + min([(z + y),(y + x),(z + x + 5),50]) <= 40, + a = allDiff([x,y,z]), + + $ narrow down solutions a bit + y <= z, + x <= y + diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.eprime new file mode 100644 index 0000000000..94389448a2 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-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-add/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-minion.solutions.json new file mode 100644 index 0000000000..655db490bb --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-minion.solutions.json @@ -0,0 +1,146 @@ +[ + { + "UserName(x)": 15, + "UserName(y)": 50 + }, + { + "UserName(x)": 16, + "UserName(y)": 49 + }, + { + "UserName(x)": 17, + "UserName(y)": 48 + }, + { + "UserName(x)": 18, + "UserName(y)": 47 + }, + { + "UserName(x)": 19, + "UserName(y)": 46 + }, + { + "UserName(x)": 20, + "UserName(y)": 45 + }, + { + "UserName(x)": 21, + "UserName(y)": 44 + }, + { + "UserName(x)": 22, + "UserName(y)": 43 + }, + { + "UserName(x)": 23, + "UserName(y)": 42 + }, + { + "UserName(x)": 24, + "UserName(y)": 41 + }, + { + "UserName(x)": 25, + "UserName(y)": 40 + }, + { + "UserName(x)": 26, + "UserName(y)": 39 + }, + { + "UserName(x)": 27, + "UserName(y)": 38 + }, + { + "UserName(x)": 28, + "UserName(y)": 37 + }, + { + "UserName(x)": 29, + "UserName(y)": 36 + }, + { + "UserName(x)": 30, + "UserName(y)": 35 + }, + { + "UserName(x)": 31, + "UserName(y)": 34 + }, + { + "UserName(x)": 32, + "UserName(y)": 33 + }, + { + "UserName(x)": 33, + "UserName(y)": 32 + }, + { + "UserName(x)": 34, + "UserName(y)": 31 + }, + { + "UserName(x)": 35, + "UserName(y)": 30 + }, + { + "UserName(x)": 36, + "UserName(y)": 29 + }, + { + "UserName(x)": 37, + "UserName(y)": 28 + }, + { + "UserName(x)": 38, + "UserName(y)": 27 + }, + { + "UserName(x)": 39, + "UserName(y)": 26 + }, + { + "UserName(x)": 40, + "UserName(y)": 25 + }, + { + "UserName(x)": 41, + "UserName(y)": 24 + }, + { + "UserName(x)": 42, + "UserName(y)": 23 + }, + { + "UserName(x)": 43, + "UserName(y)": 22 + }, + { + "UserName(x)": 44, + "UserName(y)": 21 + }, + { + "UserName(x)": 45, + "UserName(y)": 20 + }, + { + "UserName(x)": 46, + "UserName(y)": 19 + }, + { + "UserName(x)": 47, + "UserName(y)": 18 + }, + { + "UserName(x)": 48, + "UserName(y)": 17 + }, + { + "UserName(x)": 49, + "UserName(y)": 16 + }, + { + "UserName(x)": 50, + "UserName(y)": 15 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json new file mode 100644 index 0000000000..b170804ab9 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-parse.serialised.json @@ -0,0 +1,153 @@ +{ + "constraints": { + "Eq": [ + { + "clean": false, + "etype": null + }, + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Sum": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 10 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 20 + } + ] + } + ] + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 5 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 100 + } + ] + } + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..09d6631b44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json @@ -0,0 +1,135 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "SumGeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 65 + } + ] + } + ] + }, + { + "SumLeq": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "x" + } + ] + }, + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "y" + } + ] + } + ], + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 65 + } + ] + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "x" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ], + [ + { + "UserName": "y" + }, + { + "domain": { + "IntDomain": [ + { + "Bounded": [ + 1, + 50 + ] + } + ] + } + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml new file mode 100644 index 0000000000..aba59830c1 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/config.toml @@ -0,0 +1 @@ +extra_rewriter_asserts=["vector_operators_have_partially_evaluated"] diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime new file mode 100644 index 0000000000..c69f546a71 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.eprime @@ -0,0 +1,8 @@ +language ESSENCE' 1.0 + +find a,b,c : bool such that + +a \/ b \/ false, +$ this alldiff should not end up in the final model +allDiff([1,2,3]) \/ true, +(c /\ true) diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json new file mode 100644 index 0000000000..2357b354e3 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-minion.solutions.json @@ -0,0 +1,17 @@ +[ + { + "UserName(a)": 0, + "UserName(b)": 1, + "UserName(c)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 0, + "UserName(c)": 1 + }, + { + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 1 + } +] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json new file mode 100644 index 0000000000..4dcc11f11c --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-parse.serialised.json @@ -0,0 +1,188 @@ +{ + "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 + } + ] + } + ] + ] + }, + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "AllDiff": [ + { + "clean": false, + "etype": null + }, + [ + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 1 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 2 + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Int": 3 + } + ] + } + ] + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Reference": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + } + ] + }, + { + "Constant": [ + { + "clean": false, + "etype": null + }, + { + "Bool": true + } + ] + } + ] + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json new file mode 100644 index 0000000000..aa28296e44 --- /dev/null +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-or-and/input.expected-rewrite.serialised.json @@ -0,0 +1,91 @@ +{ + "constraints": { + "And": [ + { + "clean": false, + "etype": null + }, + [ + { + "Or": [ + { + "clean": false, + "etype": null + }, + [ + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "a" + }, + { + "Bool": true + } + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "b" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + { + "WatchedLiteral": [ + { + "clean": false, + "etype": null + }, + { + "UserName": "c" + }, + { + "Bool": true + } + ] + } + ] + ] + }, + "next_var": 0, + "variables": [ + [ + { + "UserName": "a" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "b" + }, + { + "domain": "BoolDomain" + } + ], + [ + { + "UserName": "c" + }, + { + "domain": "BoolDomain" + } + ] + ] +} \ No newline at end of file diff --git a/conjure_oxide/tests/rewrite_tests.rs b/conjure_oxide/tests/rewrite_tests.rs index 7c96c29be0..607698a801 100644 --- a/conjure_oxide/tests/rewrite_tests.rs +++ b/conjure_oxide/tests/rewrite_tests.rs @@ -137,7 +137,7 @@ fn simplify_expression(expr: Expression) -> Expression { #[test] fn rule_sum_constants() { - let sum_constants = get_rule_by_name("sum_constants").unwrap(); + let sum_constants = get_rule_by_name("partial_evaluator").unwrap(); let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap(); let mut expr = Expression::Sum( @@ -164,36 +164,6 @@ fn rule_sum_constants() { ); } -#[test] -fn rule_sum_mixed() { - let sum_constants = get_rule_by_name("sum_constants").unwrap(); - - let mut expr = Expression::Sum( - Metadata::new(), - vec![ - Expression::Constant(Metadata::new(), Constant::Int(1)), - Expression::Constant(Metadata::new(), Constant::Int(2)), - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - ], - ); - - expr = sum_constants - .apply(&expr, &Model::new_empty(Default::default())) - .unwrap() - .new_expression; - - assert_eq!( - expr, - Expression::Sum( - Metadata::new(), - vec![ - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - Expression::Constant(Metadata::new(), Constant::Int(3)), - ] - ) - ); -} - #[test] fn rule_sum_geq() { let flatten_sum_geq = get_rule_by_name("flatten_sum_geq").unwrap(); @@ -238,7 +208,7 @@ fn rule_sum_geq() { #[test] fn reduce_solve_xyz() { println!("Rules: {:?}", get_rules()); - let sum_constants = get_rule_by_name("sum_constants").unwrap(); + let sum_constants = get_rule_by_name("partial_evaluator").unwrap(); let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap(); let lt_to_ineq = get_rule_by_name("lt_to_ineq").unwrap(); let sum_leq_to_sumleq = get_rule_by_name("sum_leq_to_sumleq").unwrap(); @@ -519,88 +489,6 @@ fn remove_trivial_and_or() { ); } -#[test] -fn rule_remove_constants_from_or() { - let remove_constants_from_or = get_rule_by_name("remove_constants_from_or").unwrap(); - - let mut expr = Expression::Or( - Metadata::new(), - vec![ - Expression::Constant(Metadata::new(), Constant::Bool(true)), - Expression::Constant(Metadata::new(), Constant::Bool(false)), - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - ], - ); - - expr = remove_constants_from_or - .apply(&expr, &Model::new_empty(Default::default())) - .unwrap() - .new_expression; - - assert_eq!( - expr, - Expression::Constant(Metadata::new(), Constant::Bool(true)) - ); -} - -#[test] -fn rule_remove_constants_from_and() { - let remove_constants_from_and = get_rule_by_name("remove_constants_from_and").unwrap(); - - let mut expr = Expression::And( - Metadata::new(), - vec![ - Expression::Constant(Metadata::new(), Constant::Bool(true)), - Expression::Constant(Metadata::new(), Constant::Bool(false)), - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - ], - ); - - expr = remove_constants_from_and - .apply(&expr, &Model::new_empty(Default::default())) - .unwrap() - .new_expression; - - assert_eq!( - expr, - Expression::Constant(Metadata::new(), Constant::Bool(false)) - ); -} - -#[test] -fn remove_constants_from_or_not_changed() { - let remove_constants_from_or = get_rule_by_name("remove_constants_from_or").unwrap(); - - let expr = Expression::Or( - Metadata::new(), - vec![ - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - Expression::Reference(Metadata::new(), Name::UserName(String::from("b"))), - ], - ); - - let result = remove_constants_from_or.apply(&expr, &Model::new_empty(Default::default())); - - assert!(result.is_err()); -} - -#[test] -fn remove_constants_from_and_not_changed() { - let remove_constants_from_and = get_rule_by_name("remove_constants_from_and").unwrap(); - - let expr = Expression::And( - Metadata::new(), - vec![ - Expression::Reference(Metadata::new(), Name::UserName(String::from("a"))), - Expression::Reference(Metadata::new(), Name::UserName(String::from("b"))), - ], - ); - - let result = remove_constants_from_and.apply(&expr, &Model::new_empty(Default::default())); - - assert!(result.is_err()); -} - #[test] fn rule_distribute_not_over_and() { let distribute_not_over_and = get_rule_by_name("distribute_not_over_and").unwrap(); diff --git a/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index 620c835bd6..bd34ef5996 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -110,10 +110,25 @@ pub enum Expression { #[compatible(Minion)] AllDiff(Metadata, Vec), + + /// w-literal(x,k) is SAT iff x == k, where x is a variable and k a constant. + /// + /// This is a low-level Minion constraint and you should (probably) use Eq instead. The main + /// use of w-literal is to convert boolean variables to constraints so that they can be used + /// inside watched-and and watched-or. + /// + /// See `rules::minion::boolean_literal_to_wliteral`. + /// + /// + #[compatible(Minion)] + WatchedLiteral(Metadata, Name, Constant), + + #[compatible(Minion)] + Reify(Metadata, Box, Box), } fn expr_vec_to_domain_i32( - exprs: &Vec, + exprs: &[Expression], op: fn(i32, i32) -> Option, vars: &SymbolTable, ) -> Option { @@ -223,6 +238,8 @@ impl Expression { Expression::AllDiff(_, _) => Some(ReturnType::Bool), Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool? Expression::Nothing => None, + Expression::WatchedLiteral(_, _, _) => Some(ReturnType::Bool), + Expression::Reify(_, _, _) => Some(ReturnType::Bool), } } @@ -320,6 +337,12 @@ impl Expression { Expression::DivEq(metadata, box1, box2, box3) => { metadata.clean = bool_value; } + Expression::WatchedLiteral(metadata, name, constant) => { + metadata.clean = bool_value; + } + Expression::Reify(metadata, _, _) => { + metadata.clean = bool_value; + } } } } diff --git a/crates/conjure_core/src/parse/parse_model.rs b/crates/conjure_core/src/parse/parse_model.rs index 2ae9fe501b..1ec2889ab7 100644 --- a/crates/conjure_core/src/parse/parse_model.rs +++ b/crates/conjure_core/src/parse/parse_model.rs @@ -10,6 +10,18 @@ use crate::error::{Error, Result}; use crate::metadata::Metadata; use crate::Model; +macro_rules! parser_trace { + ($($arg:tt)+) => { + log::trace!(target:"jsonparser",$($arg)+) + }; +} + +macro_rules! parser_debug { + ($($arg:tt)+) => { + log::debug!(target:"jsonparser",$($arg)+) + }; +} + pub fn model_from_json(str: &str, context: Arc>>) -> Result { let mut m = Model::new_empty(context); let v: JsonValue = serde_json::from_str(str)?; @@ -211,6 +223,10 @@ fn parse_expression(obj: &JsonValue) -> Option { "MkOpMax", Box::new(Expression::Max) as Box _>, ), + ( + "MkOpAllDiff", + Box::new(Expression::AllDiff) as Box _>, + ), ] .into_iter() .collect(); @@ -240,6 +256,10 @@ fn parse_expression(obj: &JsonValue) -> Option { )) } Value::Object(constant) if constant.contains_key("Constant") => parse_constant(constant), + Value::Object(constant) if constant.contains_key("ConstantInt") => parse_constant(constant), + Value::Object(constant) if constant.contains_key("ConstantBool") => { + parse_constant(constant) + } otherwise => panic!("Unhandled Expression {:#?}", otherwise), } } @@ -282,24 +302,46 @@ fn parse_vec_op( let (key, value) = vec_op.into_iter().next()?; let constructor = vec_operators.get(key.as_str())?; - let args_parsed: Vec> = value["AbstractLiteral"]["AbsLitMatrix"][1] - .as_array()? - .iter() - .map(parse_expression) - .collect(); + parser_debug!("Trying to parse vec_op: {key} ..."); + + let mut args_parsed: Option>> = None; + if let Some(abs_lit_matrix) = value.pointer("/AbstractLiteral/AbsLitMatrix/1") { + parser_trace!("... containing a matrix of literals"); + args_parsed = abs_lit_matrix.as_array().map(|x| { + x.iter() + .map(parse_expression) + .collect::>>() + }); + } + // the input of this expression is constant - e.g. or([]), or([false]), min([2]), etc. + else if let Some(const_abs_lit_matrix) = + value.pointer("/Constant/ConstantAbstract/AbsLitMatrix/1") + { + parser_trace!("... containing a matrix of constants"); + args_parsed = const_abs_lit_matrix.as_array().map(|x| { + x.iter() + .map(parse_expression) + .collect::>>() + }); + } + + let args_parsed = args_parsed?; let number_of_args = args_parsed.len(); + parser_debug!("... with {number_of_args} args {args_parsed:#?}"); + let valid_args: Vec = args_parsed.into_iter().flatten().collect(); if number_of_args != valid_args.len() { None } else { + parser_debug!("... success!"); Some(constructor(Metadata::new(), valid_args)) } } fn parse_constant(constant: &serde_json::Map) -> Option { - match &constant["Constant"] { - Value::Object(int) if int.contains_key("ConstantInt") => { + match &constant.get("Constant") { + Some(Value::Object(int)) if int.contains_key("ConstantInt") => { let int_32: i32 = match int["ConstantInt"].as_array()?[1].as_i64()?.try_into() { Ok(x) => x, Err(_) => { @@ -313,6 +355,35 @@ fn parse_constant(constant: &serde_json::Map) -> Option { + let b: bool = b["ConstantBool"].as_bool().unwrap(); + Some(Expression::Constant(Metadata::new(), Constant::Bool(b))) + } + + // sometimes (e.g. constant matrices) we can have a ConstantInt / Constant bool that is + // not wrapped in Constant + None => { + let int_expr = constant["ConstantInt"] + .as_array() + .and_then(|x| x[1].as_i64()) + .and_then(|x| x.try_into().ok()) + .map(|x| Expression::Constant(Metadata::new(), Constant::Int(x))); + + if let e @ Some(_) = int_expr { + return e; + } + + let bool_expr = constant["ConstantBool"] + .as_bool() + .map(|x| Expression::Constant(Metadata::new(), Constant::Bool(x))); + + if let e @ Some(_) = bool_expr { + return e; + } + + panic!("Unhandled parse_constant {:#?}", constant); + } otherwise => panic!("Unhandled parse_constant {:#?}", otherwise), } } diff --git a/crates/conjure_core/src/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 eb38852ad4..e2662b971e 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -10,7 +10,7 @@ use uniplate::Uniplate; /* This file contains basic rules for simplifying expressions */ /*****************************************************************************/ -register_rule_set!("Base", 150, ()); +register_rule_set!("Base", 100, ()); /** * Remove nothing's from expressions: @@ -21,7 +21,7 @@ register_rule_set!("Base", 150, ()); * ... * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8800))] fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult { fn remove_nothings(exprs: Vec) -> Result, ApplicationError> { let mut changed = false; @@ -77,59 +77,33 @@ fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult { } } -/** - * Remove empty expressions: - * ```text - * [] = Nothing - * ``` - */ -#[register_rule(("Base", 100))] -fn empty_to_nothing(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Expr::Nothing | Expr::Reference(_, _) | Expr::Constant(_, _) => { - Err(ApplicationError::RuleNotApplicable) - } - _ => { - if expr.children().is_empty() { - Ok(Reduction::pure(Expr::Nothing)) - } else { - Err(ApplicationError::RuleNotApplicable) - } - } +/// Remove empty expressions: +/// ```text +/// or([]) ~> false +/// X([]) ~> Nothing +/// ``` +#[register_rule(("Base", 8800))] +fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult { + use Expr::*; + + // excluded expressions + if matches!( + expr, + Nothing | Reference(_, _) | Constant(_, _) | WatchedLiteral(_, _, _) + ) { + return Err(ApplicationError::RuleNotApplicable); } -} -/** - * 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), + if !expr.children().is_empty() { + return Err(ApplicationError::RuleNotApplicable); } + + let new_expr = match expr { + Or(_, _) => Constant(Metadata::new(), Const::Bool(false)), + _ => Nothing, + }; + + Ok(Reduction::pure(new_expr)) } /** @@ -138,7 +112,7 @@ fn sum_constants(expr: &Expr, _: &Model) -> ApplicationResult { * 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())), @@ -152,7 +126,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) => { @@ -188,7 +162,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) => { @@ -221,7 +195,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) => { @@ -257,7 +231,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() { @@ -274,7 +248,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) => { @@ -293,7 +267,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) => { @@ -307,6 +281,7 @@ fn remove_trivial_or(expr: &Expr, _: &Model) -> ApplicationResult { } /** +<<<<<<< HEAD * Remove constant bools from or expressions * ```text * or([true, a]) = true @@ -409,12 +384,12 @@ fn evaluate_constant_not(expr: &Expr, _: &Model) -> ApplicationResult { } /** - * Turn a Min into a new variable and post a top level constraint to ensure the new variable is the minimum. + * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum. * ```text * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 2000))] fn min_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult { match expr { Expr::Min(metadata, exprs) => { @@ -503,7 +478,7 @@ fn max_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult { * or(and(a, b), c) = and(or(a, c), or(b, c)) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8400))] fn distribute_or_over_and(expr: &Expr, _: &Model) -> ApplicationResult { fn find_and(exprs: &[Expr]) -> Option { // ToDo: may be better to move this to some kind of utils module? @@ -553,7 +528,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() { @@ -584,7 +559,7 @@ fn distribute_not_over_and(expr: &Expr, _: &Model) -> ApplicationResult { * not(or(a, b)) = and(not a, not b) * ``` */ -#[register_rule(("Base", 100))] +#[register_rule(("Base", 8400))] fn distribute_not_over_or(expr: &Expr, _: &Model) -> ApplicationResult { match expr { Expr::Not(_, contents) => match contents.as_ref() { diff --git a/crates/conjure_core/src/rules/bubble.rs b/crates/conjure_core/src/rules/bubble.rs index d94a6b0483..f9b17c0edc 100644 --- a/crates/conjure_core/src/rules/bubble.rs +++ b/crates/conjure_core/src/rules/bubble.rs @@ -6,7 +6,7 @@ use conjure_core::rule_engine::{ use conjure_core::Model; use uniplate::Uniplate; -register_rule_set!("Bubble", 254, ("Base")); +register_rule_set!("Bubble", 100, ("Base")); // Bubble reduction rules @@ -15,7 +15,7 @@ register_rule_set!("Bubble", 254, ("Base")); e.g. (a / b = c) @ (b != 0) => (a / b = c) & (b != 0) */ -#[register_rule(("Bubble", 100))] +#[register_rule(("Bubble", 8900))] fn expand_bubble(expr: &Expression, _: &Model) -> ApplicationResult { match expr { Expression::Bubble(_, a, b) if a.return_type() == Some(ReturnType::Bool) => { @@ -33,7 +33,7 @@ fn expand_bubble(expr: &Expression, _: &Model) -> ApplicationResult { E.g. ((a / b) @ (b != 0)) = c => (a / b = c) @ (b != 0) */ -#[register_rule(("Bubble", 100))] +#[register_rule(("Bubble", 8900))] fn bubble_up(expr: &Expression, _: &Model) -> ApplicationResult { let mut sub = expr.children(); let mut bubbled_conditions = vec![]; @@ -66,7 +66,7 @@ fn bubble_up(expr: &Expression, _: &Model) -> ApplicationResult { E.g. a / b => (a / b) @ (b != 0) */ -#[register_rule(("Bubble", 100))] +#[register_rule(("Bubble", 6000))] fn div_to_bubble(expr: &Expression, _: &Model) -> ApplicationResult { if let Expression::UnsafeDiv(_, a, b) = expr { return Ok(Reduction::pure(Expression::Bubble( diff --git a/crates/conjure_core/src/rules/constant.rs b/crates/conjure_core/src/rules/constant.rs index aacbe10bb7..d072cb3b29 100644 --- a/crates/conjure_core/src/rules/constant.rs +++ b/crates/conjure_core/src/rules/constant.rs @@ -5,9 +5,9 @@ use conjure_core::rule_engine::{ }; use conjure_core::Model; -register_rule_set!("Constant", 255, ()); +register_rule_set!("Constant", 100, ()); -#[register_rule(("Constant", 255))] +#[register_rule(("Constant", 9001))] fn apply_eval_constant(expr: &Expr, _: &Model) -> ApplicationResult { if let Expr::Constant(_, _) = expr { return Err(ApplicationError::RuleNotApplicable); diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index 1e265be0bf..5320499c2f 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -2,14 +2,16 @@ /* Rules for translating to Minion-supported constraints */ /************************************************************************/ -use crate::ast::{Constant as Const, DecisionVariable, Expression as Expr, SymbolTable}; +use crate::ast::{Constant as Const, DecisionVariable, Domain, Expression as Expr, SymbolTable}; use crate::metadata::Metadata; use crate::rule_engine::{ register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction, }; + use crate::solver::SolverFamily; use crate::Model; use uniplate::Uniplate; +use ApplicationError::RuleNotApplicable; register_rule_set!("Minion", 100, ("Base"), (SolverFamily::Minion)); @@ -64,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) => { @@ -85,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) => { @@ -106,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) => { @@ -145,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( @@ -166,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( @@ -186,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( @@ -206,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( @@ -226,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( @@ -258,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 { @@ -305,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) => { @@ -344,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() { @@ -365,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() { @@ -385,3 +387,116 @@ fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult { _ => Err(ApplicationError::RuleNotApplicable), } } + +/// Flattening rule that converts boolean variables to watched-literal constraints. +/// +/// For some boolean variable x: +/// ```text +/// and([x,...]) ~> and([w-literal(x,1),..]) +/// or([x,...]) ~> or([w-literal(x,1),..]) +/// not(x) ~> w-literal(x,0) +/// ``` +/// +/// ## Rationale +/// +/// Minion's watched-and and watched-or constraints only takes other constraints as arguments. +/// +/// This restates boolean variables as the equivalent constraint "SAT if x is true". +/// +#[register_rule(("Minion", 4100))] +fn boolean_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult { + use Domain::BoolDomain; + use Expr::*; + match expr { + Or(m, vec) => { + let mut changed = false; + let mut new_vec = Vec::new(); + for expr in vec { + new_vec.push(match expr { + Reference(m, name) + if mdl + .get_domain(name) + .is_some_and(|x| matches!(x, BoolDomain)) => + { + changed = true; + WatchedLiteral(m.clone_dirty(), name.clone(), Const::Bool(true)) + } + e => e.clone(), + }); + } + + if !changed { + return Err(RuleNotApplicable); + } + + Ok(Reduction::pure(Or(m.clone_dirty(), new_vec))) + } + And(m, vec) => { + let mut changed = false; + let mut new_vec = Vec::new(); + for expr in vec { + new_vec.push(match expr { + Reference(m, name) + if mdl + .get_domain(name) + .is_some_and(|x| matches!(x, BoolDomain)) => + { + changed = true; + WatchedLiteral(m.clone_dirty(), name.clone(), Const::Bool(true)) + } + e => e.clone(), + }); + } + + if !changed { + return Err(RuleNotApplicable); + } + + Ok(Reduction::pure(And(m.clone_dirty(), new_vec))) + } + + Not(m, expr) => { + if let Reference(_, name) = (**expr).clone() { + if mdl + .get_domain(&name) + .is_some_and(|x| matches!(x, BoolDomain)) + { + return Ok(Reduction::pure(WatchedLiteral( + m.clone_dirty(), + name.clone(), + Const::Bool(false), + ))); + } + } + Err(RuleNotApplicable) + } + _ => Err(RuleNotApplicable), + } +} + +/// Flattening rule for not(X) in Minion, where X is a constraint. +/// +/// ```text +/// not(X) ~> reify(X,0) +/// ``` +/// +/// This rule has lower priority than boolean_literal_to_wliteral so that we can assume that the +/// nested expressions are constraints not variables. + +#[register_rule(("Minion", 4090))] +fn not_constraint_to_reify(expr: &Expr, _: &Model) -> ApplicationResult { + use Expr::*; + if !matches!(expr, Not(_,c) if !matches!(**c, Reference(_,_)|Constant(_,_))) { + return Err(RuleNotApplicable); + } + + let Not(m, e) = expr else { + unreachable!(); + }; + + Ok(Reduction::pure(Reify( + m.clone(), + e.clone(), + Box::new(Constant(Metadata::new(), Const::Bool(false))), + ))) +} diff --git a/crates/conjure_core/src/rules/mod.rs b/crates/conjure_core/src/rules/mod.rs index e65f659901..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; @@ -5,3 +11,4 @@ mod bubble; mod cnf; mod constant; mod minion; +mod partial_eval; diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs new file mode 100644 index 0000000000..208013ce60 --- /dev/null +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -0,0 +1,280 @@ +use std::collections::HashSet; + +use conjure_macros::register_rule; + +use crate::ast::{Constant as Const, Expression as Expr}; +use crate::rule_engine::{ApplicationResult, Reduction}; +use crate::Model; + +#[register_rule(("Base",9000))] +fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { + use conjure_core::rule_engine::ApplicationError::RuleNotApplicable; + use Expr::*; + + // NOTE: If nothing changes, we must return RuleNotApplicable, or the rewriter will try this + // rule infinitely! + // This is why we always check whether we found a constant or not. + match expr.clone() { + Nothing => Err(RuleNotApplicable), + Bubble(_, _, _) => Err(RuleNotApplicable), + Constant(_, _) => Err(RuleNotApplicable), + Reference(_, _) => Err(RuleNotApplicable), + Sum(m, vec) => { + let mut acc = 0; + let mut n_consts = 0; + let mut new_vec: Vec = Vec::new(); + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + acc += x; + n_consts += 1; + } else { + new_vec.push(expr); + } + } + if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Sum(m, new_vec))) + } + } + Min(m, vec) => { + let mut acc: Option = None; + let mut n_consts = 0; + let mut new_vec: Vec = Vec::new(); + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc = match acc { + Some(i) => { + if i > x { + Some(x) + } else { + Some(i) + } + } + None => Some(x), + }; + } else { + new_vec.push(expr); + } + } + + if let Some(i) = acc { + new_vec.push(Constant(Default::default(), Const::Int(i))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Min(m, new_vec))) + } + } + Max(m, vec) => { + let mut acc: Option = None; + let mut n_consts = 0; + let mut new_vec: Vec = Vec::new(); + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc = match acc { + Some(i) => { + if i < x { + Some(x) + } else { + Some(i) + } + } + None => Some(x), + }; + } else { + new_vec.push(expr); + } + } + + if let Some(i) = acc { + new_vec.push(Constant(Default::default(), Const::Int(i))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Max(m, new_vec))) + } + } + Not(_, _) => Err(RuleNotApplicable), + Or(m, vec) => { + let mut new_vec: Vec = Vec::new(); + let mut has_const: bool = false; + for expr in vec { + if let Constant(_, Const::Bool(x)) = expr { + has_const = true; + if x { + return Ok(Reduction::pure(Constant( + Default::default(), + Const::Bool(true), + ))); + } + } else { + new_vec.push(expr); + } + } + + if !has_const { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(Or(m, new_vec))) + } + } + And(m, vec) => { + let mut new_vec: Vec = Vec::new(); + let mut has_const: bool = false; + for expr in vec { + if let Constant(_, Const::Bool(x)) = expr { + has_const = true; + if !x { + return Ok(Reduction::pure(Constant( + Default::default(), + Const::Bool(false), + ))); + } + } else { + new_vec.push(expr); + } + } + + if !has_const { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(And(m, new_vec))) + } + } + Eq(_, _, _) => Err(RuleNotApplicable), + Neq(_, _, _) => Err(RuleNotApplicable), + Geq(_, _, _) => Err(RuleNotApplicable), + Leq(_, _, _) => Err(RuleNotApplicable), + Gt(_, _, _) => Err(RuleNotApplicable), + Lt(_, _, _) => Err(RuleNotApplicable), + SafeDiv(_, _, _) => Err(RuleNotApplicable), + UnsafeDiv(_, _, _) => Err(RuleNotApplicable), + SumEq(m, vec, eq) => { + let mut acc = 0; + let mut new_vec: Vec = Vec::new(); + let mut n_consts = 0; + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc += x; + } else { + new_vec.push(expr); + } + } + + if let Constant(_, Const::Int(x)) = *eq { + if acc != 0 { + // when rhs is a constant, move lhs constants to rhs + return Ok(Reduction::pure(SumEq( + m, + new_vec, + Box::new(Constant(Default::default(), Const::Int(x - acc))), + ))); + } + } else if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(SumEq(m, new_vec, eq))) + } + } + SumGeq(m, vec, geq) => { + let mut acc = 0; + let mut new_vec: Vec = Vec::new(); + let mut n_consts = 0; + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc += x; + } else { + new_vec.push(expr); + } + } + + if let Constant(_, Const::Int(x)) = *geq { + if acc != 0 { + // when rhs is a constant, move lhs constants to rhs + return Ok(Reduction::pure(SumGeq( + m, + new_vec, + Box::new(Constant(Default::default(), Const::Int(x - acc))), + ))); + } + } else if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(SumGeq(m, new_vec, geq))) + } + } + SumLeq(m, vec, leq) => { + let mut acc = 0; + let mut new_vec: Vec = Vec::new(); + let mut n_consts = 0; + for expr in vec { + if let Constant(_, Const::Int(x)) = expr { + n_consts += 1; + acc += x; + } else { + new_vec.push(expr); + } + } + + if let Constant(_, Const::Int(x)) = *leq { + // when rhs is a constant, move lhs constants to rhs + if acc != 0 { + return Ok(Reduction::pure(SumLeq( + m, + new_vec, + Box::new(Constant(Default::default(), Const::Int(x - acc))), + ))); + } + } else if acc != 0 { + new_vec.push(Constant(Default::default(), Const::Int(acc))); + } + + if n_consts <= 1 { + Err(RuleNotApplicable) + } else { + Ok(Reduction::pure(SumLeq(m, new_vec, leq))) + } + } + DivEq(_, _, _, _) => Err(RuleNotApplicable), + Ineq(_, _, _, _) => Err(RuleNotApplicable), + AllDiff(m, vec) => { + let mut consts: HashSet = HashSet::new(); + + // check for duplicate constant values which would fail the constraint + for expr in &vec { + if let Constant(_, Const::Int(x)) = expr { + if !consts.insert(*x) { + return Ok(Reduction::pure(Constant(m, Const::Bool(false)))); + } + } + } + + // nothing has changed + Err(RuleNotApplicable) + } + + WatchedLiteral(_, _, _) => Err(RuleNotApplicable), + Reify(_, _, _) => Err(RuleNotApplicable), + } +} diff --git a/crates/conjure_core/src/rules/rule_semantics.md b/crates/conjure_core/src/rules/rule_semantics.md new file mode 100644 index 0000000000..abd0cd5e6d --- /dev/null +++ b/crates/conjure_core/src/rules/rule_semantics.md @@ -0,0 +1,16 @@ +## Priorities + +Rule are applied in priority order (highest number first). + +Rule priority levels are currently the following: + +| Priority level | Usage | +| --- | ----- | +| **9001** | **Total evaluation** | +| **9000** | **Partial evaluation** | +| 8800 | Trivial simplifications: removing nesting, removing empty / unit constraints | +| 8400 | Transformation into canonical forms: (distributivity, associativity, commutativity, etc.) | +| **8000** | **Simplifications** | +| **6000** | **Modelling enhancing reformulations** | +| **4000** | **Solver Specific** | +| **2000** | **Non solver specific, non enhancing reformulations** (e.g. restate a constraint using simpler constraints when needed for solver compatability) | diff --git a/crates/conjure_core/src/solver/adaptors/minion.rs b/crates/conjure_core/src/solver/adaptors/minion.rs index 2362976aeb..26b337161e 100644 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ b/crates/conjure_core/src/solver/adaptors/minion.rs @@ -248,7 +248,28 @@ fn parse_exprs( minion_model: &mut MinionModel, ) -> Result<(), SolverError> { for expr in conjure_model.get_constraints_vec().iter() { - parse_expr(expr.to_owned(), minion_model)?; + // TODO: top level false / trues should not go to the solver to begin with + // ... but changing this at this stage would require rewriting the tester + use crate::metadata::Metadata; + use conjure_ast::Constant; + use conjure_ast::Expression as Expr; + + match expr { + // top level false + Expr::Constant(_, Constant::Bool(false)) => { + minion_model.constraints.push(minion_ast::Constraint::False); + return Ok(()); + } + // top level true + Expr::Constant(_, Constant::Bool(true)) => { + minion_model.constraints.push(minion_ast::Constraint::True); + return Ok(()); + } + + _ => { + parse_expr(expr.to_owned(), minion_model)?; + } + } } Ok(()) } @@ -288,9 +309,26 @@ 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)?)) } + + conjure_ast::Expression::WatchedLiteral(_metadata, name, k) => { + Ok(minion_ast::Constraint::WLiteral( + minion_ast::Var::NameRef(_name_to_string(name)), + minion_ast::Constant::Integer(read_const_1(k)?), + )) + } + conjure_ast::Expression::Reify(_metadata, e, v) => Ok(minion_ast::Constraint::Reify( + Box::new(read_expr(*e)?), + read_var(*v)?, + )), x => Err(ModelFeatureNotSupported(format!("{:?}", x))), } } @@ -329,7 +367,19 @@ fn _read_ref(e: conjure_ast::Expression) -> Result { fn read_const(e: conjure_ast::Expression) -> Result { match e { - conjure_ast::Expression::Constant(_, conjure_ast::Constant::Int(n)) => Ok(n), + conjure_ast::Expression::Constant(_, x) => Ok(read_const_1(x)?), + x => Err(ModelInvalid(format!( + "expected a constant, but got `{0:?}`", + x + ))), + } +} + +fn read_const_1(k: conjure_ast::Constant) -> Result { + match k { + conjure_ast::Constant::Int(n) => Ok(n), + conjure_ast::Constant::Bool(true) => Ok(1), + conjure_ast::Constant::Bool(false) => Ok(0), x => Err(ModelInvalid(format!( "expected a constant, but got `{0:?}`", x diff --git a/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::>(); diff --git a/solvers/minion/src/ast.rs b/solvers/minion/src/ast.rs index 44bba6e441..09f6c299f4 100644 --- a/solvers/minion/src/ast.rs +++ b/solvers/minion/src/ast.rs @@ -111,6 +111,8 @@ pub enum Constraint { WatchLess(Var, Var), WatchNeq(Var, Var), Ineq(Var, Var, Constant), + False, + True, } /// Representation of a Minion Variable. diff --git a/solvers/minion/src/run.rs b/solvers/minion/src/run.rs index e31114c809..8c01aaae89 100644 --- a/solvers/minion/src/run.rs +++ b/solvers/minion/src/run.rs @@ -372,6 +372,8 @@ unsafe fn get_constraint_type(constraint: &Constraint) -> Result Ok(ffi::ConstraintType_CT_GACEQ), Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS), Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ), + Constraint::True => Ok(ffi::ConstraintType_CT_TRUE), + Constraint::False => Ok(ffi::ConstraintType_CT_FALSE), #[allow(unreachable_patterns)] x => Err(MinionError::NotImplemented(format!( @@ -562,7 +564,11 @@ unsafe fn constraint_add_args( //Constraint::WatchElementOne(_, _, _) => todo!(), //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(), //Constraint::WatchElementUndefZero(_, _, _) => todo!(), - //Constraint::WLiteral(_, _) => todo!(), + Constraint::WLiteral(a, b) => { + read_var(i, r_constr, a)?; + read_constant(r_constr, b)?; + Ok(()) + } //Constraint::WNotLiteral(_, _) => todo!(), //Constraint::WInIntervalSet(_, _) => todo!(), //Constraint::WInRange(_, _) => todo!(), @@ -588,6 +594,9 @@ unsafe fn constraint_add_args( read_var(i, r_constr, b)?; Ok(()) } + + Constraint::True => Ok(()), + Constraint::False => Ok(()), #[allow(unreachable_patterns)] x => Err(MinionError::NotImplemented(format!("{:?}", x))), }