diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index f8ad604c7a..3792071605 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -328,9 +328,6 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model) Max(_, ref vec) => assert_constants_leq_one(&node, vec), Or(_, ref vec) => assert_constants_leq_one(&node, vec), And(_, ref vec) => assert_constants_leq_one(&node, vec), - SumEq(_, ref vec, _) => assert_constants_leq_one(&node, vec), - SumGeq(_, ref vec, _) => assert_constants_leq_one(&node, vec), - SumLeq(_, ref vec, _) => assert_constants_leq_one(&node, vec), _ => (), }; } 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 dbea6278f0..ad7c6c5ec1 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 @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json index 5dc46d1208..bbd1bf6638 100644 --- a/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json @@ -1,49 +1,23 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] } 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 a7ab120847..587b1d1ae5 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 @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null 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 f5ed3671a5..0892efedaf 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 @@ -79,7 +79,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/div/05/div-05.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/05/div-05.expected-rewrite.serialised.json index e482b2d1bf..fba38b5af9 100644 --- a/conjure_oxide/tests/integration/basic/div/05/div-05.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/05/div-05.expected-rewrite.serialised.json @@ -79,7 +79,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/div/06/div-06.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/06/div-06.expected-rewrite.serialised.json index f5ed3671a5..0892efedaf 100644 --- a/conjure_oxide/tests/integration/basic/div/06/div-06.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/div/06/div-06.expected-rewrite.serialised.json @@ -79,7 +79,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt index 73c7e9b48a..5c663c67b8 100644 --- a/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt @@ -1,15 +1,15 @@ -(Max([2, a]) <= 2), - ~~> leq_to_ineq ([("Minion", 4100)]) -Ineq(Max([2, a]), 2, 0) - --- - Max([2, a]), ~~> max_to_var ([("Base", 100)]) __0 -- +(__0 <= 2), + ~~> leq_to_ineq ([("Minion", 4100)]) +Ineq(__0, 2, 0) + +-- + (__0 >= 2), ~~> geq_to_ineq ([("Minion", 4100)]) Ineq(2, __0, 0) diff --git a/conjure_oxide/tests/integration/basic/max/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/max/02/input.expected-rewrite.serialised.json index 93b0417741..351503a241 100644 --- a/conjure_oxide/tests/integration/basic/max/02/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/max/02/input.expected-rewrite.serialised.json @@ -1,143 +1,65 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt index 9affa1b16c..eb3271e88b 100644 --- a/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt @@ -1,15 +1,15 @@ -(Min([a, b]) >= 3), - ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(3, Min([a, b]), 0) - --- - Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 -- +(__0 >= 3), + ~~> geq_to_ineq ([("Minion", 4100)]) +Ineq(3, __0, 0) + +-- + (__0 <= a), ~~> leq_to_ineq ([("Minion", 4100)]) Ineq(__0, a, 0) diff --git a/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json index 0225666984..d6e4635e69 100644 --- a/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json @@ -1,143 +1,65 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 3 - } - } - ] + "Literal": { + "Int": 3 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt index 332b8191e6..5cec6e6d2e 100644 --- a/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt @@ -1,15 +1,15 @@ -(Min([a, b]) <= 2), - ~~> leq_to_ineq ([("Minion", 4100)]) -Ineq(Min([a, b]), 2, 0) - --- - Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 -- +(__0 <= 2), + ~~> leq_to_ineq ([("Minion", 4100)]) +Ineq(__0, 2, 0) + +-- + (__0 <= a), ~~> leq_to_ineq ([("Minion", 4100)]) Ineq(__0, a, 0) diff --git a/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json index e77b9d714c..fa42a8a4b9 100644 --- a/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json @@ -1,143 +1,65 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt index 332b8191e6..5cec6e6d2e 100644 --- a/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt @@ -1,15 +1,15 @@ -(Min([a, b]) <= 2), - ~~> leq_to_ineq ([("Minion", 4100)]) -Ineq(Min([a, b]), 2, 0) - --- - Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 -- +(__0 <= 2), + ~~> leq_to_ineq ([("Minion", 4100)]) +Ineq(__0, 2, 0) + +-- + (__0 <= a), ~~> leq_to_ineq ([("Minion", 4100)]) Ineq(__0, a, 0) diff --git a/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json index e9dc13d490..27a6093ecb 100644 --- a/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json @@ -1,143 +1,65 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt index 9affa1b16c..eb3271e88b 100644 --- a/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt @@ -1,15 +1,15 @@ -(Min([a, b]) >= 3), - ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(3, Min([a, b]), 0) - --- - Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 -- +(__0 >= 3), + ~~> geq_to_ineq ([("Minion", 4100)]) +Ineq(3, __0, 0) + +-- + (__0 <= a), ~~> leq_to_ineq ([("Minion", 4100)]) Ineq(__0, a, 0) diff --git a/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json index 80d90314f0..0141cc5cdc 100644 --- a/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json @@ -1,143 +1,65 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 3 - } - } - ] + "Literal": { + "Int": 3 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt index 332b8191e6..5cec6e6d2e 100644 --- a/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt @@ -1,15 +1,15 @@ -(Min([a, b]) <= 2), - ~~> leq_to_ineq ([("Minion", 4100)]) -Ineq(Min([a, b]), 2, 0) - --- - Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 -- +(__0 <= 2), + ~~> leq_to_ineq ([("Minion", 4100)]) +Ineq(__0, 2, 0) + +-- + (__0 <= a), ~~> leq_to_ineq ([("Minion", 4100)]) Ineq(__0, a, 0) diff --git a/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json index 8f940f6694..b37d7147c7 100644 --- a/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json @@ -1,143 +1,65 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/basic/mod/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/01/input.expected-rewrite.serialised.json index 98ace3e5ec..3bbbc2e7c4 100644 --- a/conjure_oxide/tests/integration/basic/mod/01/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/mod/01/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/mod/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/02/input.expected-rewrite.serialised.json index 8a89848227..0a64b17310 100644 --- a/conjure_oxide/tests/integration/basic/mod/02/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/mod/02/input.expected-rewrite.serialised.json @@ -1,49 +1,23 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Literal": { + "Int": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] } diff --git a/conjure_oxide/tests/integration/basic/mod/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/03/input.expected-rewrite.serialised.json index 95e268fec3..e820be38f8 100644 --- a/conjure_oxide/tests/integration/basic/mod/03/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/mod/03/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/mod/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/04/input.expected-rewrite.serialised.json index f79086352f..b3d0ee42d2 100644 --- a/conjure_oxide/tests/integration/basic/mod/04/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/mod/04/input.expected-rewrite.serialised.json @@ -79,7 +79,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/mod/05/mod-05.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/05/mod-05.expected-rewrite.serialised.json index 0f7a4c1e46..0988118d51 100644 --- a/conjure_oxide/tests/integration/basic/mod/05/mod-05.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/mod/05/mod-05.expected-rewrite.serialised.json @@ -79,7 +79,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/mod/06/mod-06.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/06/mod-06.expected-rewrite.serialised.json index f79086352f..b3d0ee42d2 100644 --- a/conjure_oxide/tests/integration/basic/mod/06/mod-06.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/mod/06/mod-06.expected-rewrite.serialised.json @@ -79,7 +79,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/neg/01-negeq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/neg/01-negeq/input.expected-rewrite.serialised.json index e796e5c8e3..d6ed1dcc13 100644 --- a/conjure_oxide/tests/integration/basic/neg/01-negeq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/neg/01-negeq/input.expected-rewrite.serialised.json @@ -1,7 +1,7 @@ { "constraints": [ { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input.expected-rewrite.serialised.json index 73276e42c3..3a49f71f85 100644 --- a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -68,7 +68,7 @@ ] }, { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input.expected-rewrite.serialised.json index 3298a2bdc4..8506deaba4 100644 --- a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null @@ -63,7 +63,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input.expected-rewrite.serialised.json index 26dac9b466..43d13551fe 100644 --- a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -102,7 +102,7 @@ ] }, { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null @@ -120,7 +120,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt index 96326a5823..e3ac1726ee 100644 --- a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt @@ -1,24 +1,6 @@ -(x = Sum([-(y), z])), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) -SumEq([-(y), z], x) - --- - -SumEq([-(y), z], x), - ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([-(y), z], x), SumLeq([-(y), z], x)]) - --- - -SumGeq([-(y), z], x), - ~~> flatten_vecop ([("Minion", 4400)]) -SumGeq([__0, z], x) - --- - -SumLeq([-(y), z], x), +Sum([-(y), z]), ~~> flatten_vecop ([("Minion", 4400)]) -SumLeq([__1, z], x) +Sum([__0, z]) -- @@ -28,9 +10,15 @@ MinusEq(__0,y) -- -__1 =aux -(y), - ~~> introduce_minuseq_from_aux_decl ([("Minion", 4400)]) -MinusEq(__1,y) +(x = Sum([__0, z])), + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) +SumEq([__0, z], x) + +-- + +SumEq([__0, z], x), + ~~> sumeq_to_minion ([("Minion", 4400)]) +And([SumLeq([__0, z], x), SumGeq([__0, z], x)]) -- diff --git a/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-minion.solutions.json index 0dca40956c..af9e005879 100644 --- a/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-minion.solutions.json @@ -1,21 +1,18 @@ [ { "__0": 0, - "__1": 0, "x": 1, "y": 0, "z": 1 }, { "__0": 1, - "__1": 1, "x": 1, "y": -1, "z": 0 }, { "__0": 1, - "__1": 1, "x": 2, "y": -1, "z": 1 diff --git a/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-rewrite.serialised.json index f2ddc68ebb..f485e10d58 100644 --- a/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/neg/05-sum/input.expected-rewrite.serialised.json @@ -8,100 +8,52 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "z" - } - } - ] + "Reference": { + "UserName": "z" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 1 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "z" - } - } - ] + "Reference": { + "UserName": "z" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } } ] } @@ -109,7 +61,7 @@ ] }, { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null @@ -125,27 +77,9 @@ } } ] - }, - { - "MinusEq": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 1 - } - }, - { - "Reference": { - "UserName": "y" - } - } - ] } ], - "next_var": 2, + "next_var": 1, "variables": [ [ { @@ -164,23 +98,6 @@ } } ], - [ - { - "MachineName": 1 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - -1, - 1 - ] - } - ] - } - } - ], [ { "UserName": "x" diff --git a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt index 00d85b8783..77b24b2a2f 100644 --- a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt @@ -46,27 +46,9 @@ a -- -(x = Sum([-(y), -(z), -1, a, b])), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) -SumEq([-(y), -(z), -1, a, b], x) - --- - -SumEq([-(y), -(z), -1, a, b], x), - ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([-(y), -(z), -1, a, b], x), SumLeq([-(y), -(z), -1, a, b], x)]) - --- - -SumGeq([-(y), -(z), -1, a, b], x), +Sum([-(y), -(z), -1, a, b]), ~~> flatten_vecop ([("Minion", 4400)]) -SumGeq([__0, __1, -1, a, b], x) - --- - -SumLeq([-(y), -(z), -1, a, b], x), - ~~> flatten_vecop ([("Minion", 4400)]) -SumLeq([__2, __3, -1, a, b], x) +Sum([__0, __1, -1, a, b]) -- @@ -82,15 +64,15 @@ MinusEq(__1,z) -- -__2 =aux -(y), - ~~> introduce_minuseq_from_aux_decl ([("Minion", 4400)]) -MinusEq(__2,y) +(x = Sum([__0, __1, -1, a, b])), + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) +SumEq([__0, __1, -1, a, b], x) -- -__3 =aux -(z), - ~~> introduce_minuseq_from_aux_decl ([("Minion", 4400)]) -MinusEq(__3,z) +SumEq([__0, __1, -1, a, b], x), + ~~> sumeq_to_minion ([("Minion", 4400)]) +And([SumLeq([__0, __1, -1, a, b], x), SumGeq([__0, __1, -1, a, b], x)]) -- diff --git a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-minion.solutions.json index 6a3fc7a371..28e94dffc5 100644 --- a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-minion.solutions.json @@ -2,8 +2,6 @@ { "__0": -1, "__1": 1, - "__2": -1, - "__3": 1, "a": 1, "b": 1, "x": 1, @@ -13,8 +11,6 @@ { "__0": 0, "__1": 0, - "__2": 0, - "__3": 0, "a": 1, "b": 1, "x": 1, @@ -24,8 +20,6 @@ { "__0": 0, "__1": 1, - "__2": 0, - "__3": 1, "a": 0, "b": 1, "x": 1, @@ -35,8 +29,6 @@ { "__0": 0, "__1": 1, - "__2": 0, - "__3": 1, "a": 1, "b": 0, "x": 1, @@ -46,8 +38,6 @@ { "__0": 0, "__1": 1, - "__2": 0, - "__3": 1, "a": 1, "b": 1, "x": 2, @@ -57,8 +47,6 @@ { "__0": 1, "__1": -1, - "__2": 1, - "__3": -1, "a": 1, "b": 1, "x": 1, @@ -68,8 +56,6 @@ { "__0": 1, "__1": 0, - "__2": 1, - "__3": 0, "a": 0, "b": 1, "x": 1, @@ -79,8 +65,6 @@ { "__0": 1, "__1": 0, - "__2": 1, - "__3": 0, "a": 1, "b": 0, "x": 1, @@ -90,8 +74,6 @@ { "__0": 1, "__1": 0, - "__2": 1, - "__3": 0, "a": 1, "b": 1, "x": 2, @@ -101,8 +83,6 @@ { "__0": 1, "__1": 1, - "__2": 1, - "__3": 1, "a": -1, "b": 1, "x": 1, @@ -112,8 +92,6 @@ { "__0": 1, "__1": 1, - "__2": 1, - "__3": 1, "a": 0, "b": 0, "x": 1, @@ -123,8 +101,6 @@ { "__0": 1, "__1": 1, - "__2": 1, - "__3": 1, "a": 0, "b": 1, "x": 2, @@ -134,8 +110,6 @@ { "__0": 1, "__1": 1, - "__2": 1, - "__3": 1, "a": 1, "b": -1, "x": 1, @@ -145,8 +119,6 @@ { "__0": 1, "__1": 1, - "__2": 1, - "__3": 1, "a": 1, "b": 0, "x": 2, @@ -156,8 +128,6 @@ { "__0": 1, "__1": 1, - "__2": 1, - "__3": 1, "a": 1, "b": 1, "x": 3, diff --git a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-rewrite.serialised.json index 1aa86460d4..92a464ff14 100644 --- a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input.expected-rewrite.serialised.json @@ -8,178 +8,82 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 1 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": -1 - } - } - ] + "Literal": { + "Int": -1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 2 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 3 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": -1 - } - } - ] + "Literal": { + "Int": -1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } } ] } @@ -187,7 +91,7 @@ ] }, { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null @@ -205,7 +109,7 @@ ] }, { - "MinusEq": [ + "FlatMinusEq": [ { "clean": false, "etype": null @@ -221,45 +125,9 @@ } } ] - }, - { - "MinusEq": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 2 - } - }, - { - "Reference": { - "UserName": "y" - } - } - ] - }, - { - "MinusEq": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 3 - } - }, - { - "Reference": { - "UserName": "z" - } - } - ] } ], - "next_var": 4, + "next_var": 2, "variables": [ [ { @@ -295,40 +163,6 @@ } } ], - [ - { - "MachineName": 2 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - -1, - 1 - ] - } - ] - } - } - ], - [ - { - "MachineName": 3 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - -1, - 1 - ] - } - ] - } - } - ], [ { "UserName": "a" diff --git a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt index ef08e33a42..c92fa6de9e 100644 --- a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt @@ -5,14 +5,14 @@ Sum([a, b, c, d, e]) -- (Sum([a, b, c, d, e]) = 5), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) SumEq([a, b, c, d, e], 5) -- SumEq([a, b, c, d, e], 5), ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([a, b, c, d, e], 5), SumLeq([a, b, c, d, e], 5)]) +And([SumLeq([a, b, c, d, e], 5), SumGeq([a, b, c, d, e], 5)]) -- diff --git a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input.expected-rewrite.serialised.json index b28b6a32d9..2acd01c2f1 100644 --- a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input.expected-rewrite.serialised.json @@ -8,178 +8,82 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Reference": { + "UserName": "c" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "d" - } - } - ] + "Reference": { + "UserName": "d" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "e" - } - } - ] + "Reference": { + "UserName": "e" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 5 - } - } - ] + "Literal": { + "Int": 5 + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Reference": { + "UserName": "c" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "d" - } - } - ] + "Reference": { + "UserName": "d" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "e" - } - } - ] + "Reference": { + "UserName": "e" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 5 - } - } - ] + "Literal": { + "Int": 5 + } } ] } diff --git a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt index 1684fb9c25..eb7cc185b6 100644 --- a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt @@ -34,21 +34,21 @@ SafeDiv(__0, a) -- +(SafeDiv(__0, a) = 3), + ~~> introduce_diveq ([("Minion", 4200)]) +DivEq(__0, a, 3) + +-- + __0 =aux Sum([x, y, z]), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) SumEq([x, y, z], __0) -- SumEq([x, y, z], __0), ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([x, y, z], __0), SumLeq([x, y, z], __0)]) - --- - -(SafeDiv(__0, a) = 3), - ~~> introduce_diveq ([("Minion", 4200)]) -DivEq(__0, a, 3) +And([SumLeq([x, y, z], __0), SumGeq([x, y, z], __0)]) -- diff --git a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input.expected-rewrite.serialised.json index e29aace62e..dd819e33b9 100644 --- a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -75,126 +75,62 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "z" - } - } - ] + "Reference": { + "UserName": "z" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "z" - } - } - ] + "Reference": { + "UserName": "z" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } } ] } diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt index 5dd2dee0e2..01e4228bf5 100644 --- a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt @@ -1,18 +1,12 @@ -(Sum([Min([a, b]), 6]) <= 10), - ~~> sum_leq_to_sumleq ([("Minion", 4400)]) -SumLeq([Min([a, b]), 6], 10) - --- - -SumLeq([Min([a, b]), 6], 10), - ~~> partial_evaluator ([("Base", 9000)]) -SumLeq([Min([a, b])], 4) +Sum([Min([a, b]), 6]), + ~~> flatten_vecop ([("Minion", 4400)]) +Sum([__0, 6]) -- -SumLeq([Min([a, b])], 4), - ~~> flatten_vecop ([("Minion", 4400)]) -SumLeq([__0], 4) +(Sum([__0, 6]) <= 10), + ~~> introduce_sumleq ([("Minion", 4400)]) +SumLeq([__0, 6], 10) -- 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 index 56b8659f3b..5ae3a29d9d 100644 --- 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 @@ -1,38 +1,27 @@ { "constraints": [ { - "SumLeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } + }, + { + "Literal": { + "Int": 6 + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 4 - } - } - ] + "Literal": { + "Int": 10 + } } ] }, @@ -61,96 +50,44 @@ ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 1 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 1 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, diff --git a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt index 96aba4c949..9e11c7dabf 100644 --- a/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/bugs/yb33-min-of-constants-parses-as-nothing/input-expected-rule-trace-human.txt @@ -5,14 +5,8 @@ Min([5, 7]), -- (Sum([5, c]) <= 10), - ~~> sum_leq_to_sumleq ([("Minion", 4400)]) + ~~> introduce_sumleq ([("Minion", 4400)]) SumLeq([5, c], 10) -- -SumLeq([5, c], 10), - ~~> partial_evaluator ([("Base", 9000)]) -SumLeq([c], 5) - --- - 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 index 38bea76acf..9d07a984e1 100644 --- 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 @@ -1,38 +1,27 @@ { "constraints": [ { - "SumLeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Literal": { + "Int": 5 + } + }, + { + "Reference": { + "UserName": "c" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 5 - } - } - ] + "Literal": { + "Int": 10 + } } ] } 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 index 11221dfde0..d4566c95c4 100644 --- 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 @@ -51,7 +51,7 @@ }, [ { - "WatchedLiteral": [ + "FlatWatchedLiteral": [ { "clean": false, "etype": null @@ -88,7 +88,7 @@ }, [ { - "WatchedLiteral": [ + "FlatWatchedLiteral": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt index 4a0645daec..d27d475e77 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt @@ -11,7 +11,7 @@ Sum([x, y, 35]) -- (Sum([x, y, 35]) = 100), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) SumEq([x, y, 35], 100) -- @@ -24,7 +24,7 @@ SumEq([x, y], 65) SumEq([x, y], 65), ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([x, y], 65), SumLeq([x, y], 65)]) +And([SumLeq([x, y], 65), SumGeq([x, y], 65)]) -- 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 index 3e9d911a71..5773a11a65 100644 --- 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 @@ -8,100 +8,52 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 65 - } - } - ] + "Literal": { + "Int": 65 + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 65 - } - } - ] + "Literal": { + "Int": 65 + } } ] } diff --git a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt index 4a0645daec..d27d475e77 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt @@ -11,7 +11,7 @@ Sum([x, y, 35]) -- (Sum([x, y, 35]) = 100), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) SumEq([x, y, 35], 100) -- @@ -24,7 +24,7 @@ SumEq([x, y], 65) SumEq([x, y], 65), ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([x, y], 65), SumLeq([x, y], 65)]) +And([SumLeq([x, y], 65), SumGeq([x, y], 65)]) -- 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 index 3e9d911a71..5773a11a65 100644 --- 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 @@ -8,100 +8,52 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 65 - } - } - ] + "Literal": { + "Int": 65 + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 65 - } - } - ] + "Literal": { + "Int": 65 + } } ] } diff --git a/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt index 7f7bb34698..99ee85110c 100644 --- a/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt @@ -5,14 +5,14 @@ Sum([a, b, c]) -- (Sum([a, b, c]) = 4), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) SumEq([a, b, c], 4) -- SumEq([a, b, c], 4), ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([a, b, c], 4), SumLeq([a, b, c], 4)]) +And([SumLeq([a, b, c], 4), SumGeq([a, b, c], 4)]) -- diff --git a/conjure_oxide/tests/integration/eprime-minion/xyz/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/xyz/input.expected-rewrite.serialised.json index 3237a7cc60..d18b9969af 100644 --- a/conjure_oxide/tests/integration/eprime-minion/xyz/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/eprime-minion/xyz/input.expected-rewrite.serialised.json @@ -8,126 +8,62 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Reference": { + "UserName": "c" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 4 - } - } - ] + "Literal": { + "Int": 4 + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Reference": { + "UserName": "c" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 4 - } - } - ] + "Literal": { + "Int": 4 + } } ] } @@ -135,49 +71,23 @@ ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] } diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt index 5ac55d4f0a..38b2cc8ca4 100644 --- a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt @@ -1,84 +1,60 @@ -(x = Sum([Max([a, b]), 1])), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) -SumEq([Max([a, b]), 1], x) - --- - -SumEq([Max([a, b]), 1], x), - ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([Max([a, b]), 1], x), SumLeq([Max([a, b]), 1], x)]) - --- - -SumGeq([Max([a, b]), 1], x), +Sum([Max([a, b]), 1]), ~~> flatten_vecop ([("Minion", 4400)]) -SumGeq([__0, 1], x) +Sum([__0, 1]) -- -SumLeq([Max([a, b]), 1], x), - ~~> flatten_vecop ([("Minion", 4400)]) -SumLeq([__1, 1], x) +(x = Sum([__0, 1])), + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) +SumEq([__0, 1], x) -- -(Max([a, b]) >= 2), - ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(2, Max([a, b]), 0) +SumEq([__0, 1], x), + ~~> sumeq_to_minion ([("Minion", 4400)]) +And([SumLeq([__0, 1], x), SumGeq([__0, 1], x)]) -- Max([a, b]), ~~> max_to_var ([("Base", 100)]) -__2 +__1 -- -(__2 >= a), +(__1 >= 2), ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(a, __2, 0) +Ineq(2, __1, 0) -- -(__2 >= b), +(__1 >= a), ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(b, __2, 0) +Ineq(a, __1, 0) -- -Max([a, b]), - ~~> max_to_var ([("Base", 100)]) -__3 - --- - -(__3 >= a), - ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(a, __3, 0) - --- - -(__3 >= b), +(__1 >= b), ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(b, __3, 0) +Ineq(b, __1, 0) -- Max([a, b]), ~~> max_to_var ([("Base", 100)]) -__4 +__2 -- -(__4 >= a), +(__2 >= a), ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(a, __4, 0) +Ineq(a, __2, 0) -- -(__4 >= b), +(__2 >= b), ~~> geq_to_ineq ([("Minion", 4100)]) -Ineq(b, __4, 0) +Ineq(b, __2, 0) -- diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/experiment/works/max2/input.expected-minion.solutions.json index 8db64f8337..44088d458d 100644 --- a/conjure_oxide/tests/integration/experiment/works/max2/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/experiment/works/max2/input.expected-minion.solutions.json @@ -3,8 +3,6 @@ "__0": 2, "__1": 2, "__2": 2, - "__3": 2, - "__4": 2, "a": 1, "b": 2, "x": 3 @@ -13,8 +11,6 @@ "__0": 2, "__1": 2, "__2": 2, - "__3": 2, - "__4": 2, "a": 2, "b": 1, "x": 3 @@ -23,8 +19,6 @@ "__0": 2, "__1": 2, "__2": 2, - "__3": 2, - "__4": 2, "a": 2, "b": 2, "x": 3 @@ -33,8 +27,6 @@ "__0": 3, "__1": 3, "__2": 3, - "__3": 3, - "__4": 3, "a": 1, "b": 3, "x": 4 @@ -43,8 +35,6 @@ "__0": 3, "__1": 3, "__2": 3, - "__3": 3, - "__4": 3, "a": 2, "b": 3, "x": 4 @@ -53,8 +43,6 @@ "__0": 3, "__1": 3, "__2": 3, - "__3": 3, - "__4": 3, "a": 3, "b": 1, "x": 4 @@ -63,8 +51,6 @@ "__0": 3, "__1": 3, "__2": 3, - "__3": 3, - "__4": 3, "a": 3, "b": 2, "x": 4 @@ -73,8 +59,6 @@ "__0": 3, "__1": 3, "__2": 3, - "__3": 3, - "__4": 3, "a": 3, "b": 3, "x": 4 diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/experiment/works/max2/input.expected-rewrite.serialised.json index 4c928d0dce..e17be392ab 100644 --- a/conjure_oxide/tests/integration/experiment/works/max2/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/experiment/works/max2/input.expected-rewrite.serialised.json @@ -1,49 +1,23 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Literal": { + "Int": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 2 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, @@ -55,100 +29,52 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 0 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 1 - } - } - ] + "Literal": { + "Int": 1 + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 1 - } - } - ] + "Reference": { + "MachineName": 0 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 1 - } - } - ] + "Literal": { + "Int": 1 + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } } ] } @@ -164,64 +90,6 @@ { "MachineName": 0 }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 3 - } - } - ] - } - ] - }, - { - "AuxDeclaration": [ - { - "clean": false, - "etype": null - }, - { - "MachineName": 1 - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 4 - } - } - ] - } - ] - }, - { - "Ineq": [ - { - "clean": false, - "etype": null - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] - }, { "Atomic": [ { @@ -234,238 +102,48 @@ } } ] - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 2 - } - } - ] - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] - } - ] - }, - { - "Or": [ - { - "clean": false, - "etype": null - }, - [ - { - "Eq": [ - { - "clean": false, - "etype": null - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 2 - } - } - ] - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] - } - ] - }, - { - "Eq": [ - { - "clean": false, - "etype": null - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 2 - } - } - ] - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] - } - ] + "Reference": { + "UserName": "a" } - ] - ] - }, - { - "Ineq": [ - { - "clean": false, - "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] - }, - { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 3 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 3 - } - } - ] + "Reference": { + "MachineName": 1 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, @@ -490,7 +168,7 @@ }, { "Reference": { - "MachineName": 3 + "MachineName": 1 } } ] @@ -524,7 +202,7 @@ }, { "Reference": { - "MachineName": 3 + "MachineName": 1 } } ] @@ -548,96 +226,44 @@ ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 4 - } - } - ] + "Reference": { + "MachineName": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "MachineName": 4 - } - } - ] + "Reference": { + "MachineName": 2 + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] }, @@ -662,7 +288,7 @@ }, { "Reference": { - "MachineName": 4 + "MachineName": 2 } } ] @@ -696,7 +322,7 @@ }, { "Reference": { - "MachineName": 4 + "MachineName": 2 } } ] @@ -720,7 +346,7 @@ ] } ], - "next_var": 5, + "next_var": 3, "variables": [ [ { @@ -773,40 +399,6 @@ } } ], - [ - { - "MachineName": 3 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - 1, - 4 - ] - } - ] - } - } - ], - [ - { - "MachineName": 4 - }, - { - "domain": { - "IntDomain": [ - { - "Bounded": [ - 1, - 4 - ] - } - ] - } - } - ], [ { "UserName": "a" diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input.expected-rewrite.serialised.json index 9b840a803e..9664db4a0d 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-01-simple/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input.expected-rewrite.serialised.json index 91e44b0900..a72a7575e9 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-02-zero/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input.expected-rewrite.serialised.json index 1636b27b6f..4998a3c04b 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -102,7 +102,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -125,7 +125,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input.expected-rewrite.serialised.json index 904f86c7fc..251115e0ca 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input.expected-rewrite.serialised.json @@ -113,7 +113,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -136,7 +136,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -159,7 +159,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json index eb0821f912..d93f0af439 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json @@ -42,7 +42,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -102,7 +102,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null @@ -125,7 +125,7 @@ ] }, { - "DivEqUndefZero": [ + "MinionDivEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input.expected-rewrite.serialised.json index fecf724409..5650386144 100644 --- a/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/ineq-01-strict-less-than/input.expected-rewrite.serialised.json @@ -1,49 +1,23 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": -1 - } - } - ] + "Int": -1 } ] } diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input.expected-rewrite.serialised.json index 874065f009..933fc69ad8 100644 --- a/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/ineq-02-leq/input.expected-rewrite.serialised.json @@ -1,49 +1,23 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] } diff --git a/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input.expected-rewrite.serialised.json index ef446e0678..3836f933ed 100644 --- a/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/ineq-03-leq-plus-k/input.expected-rewrite.serialised.json @@ -1,49 +1,23 @@ { "constraints": [ { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 2 - } - } - ] + "Int": 2 } ] } diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input.expected-rewrite.serialised.json index 86cf8cb468..65e299c221 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-01-simple/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input.expected-rewrite.serialised.json index ba53a7e43d..cca840e642 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-02-zero/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input.expected-rewrite.serialised.json index f7232f0905..b7f61b28e4 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input.expected-rewrite.serialised.json @@ -8,7 +8,7 @@ }, [ { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null @@ -102,7 +102,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null @@ -125,7 +125,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input.expected-rewrite.serialised.json index 48057ea075..228671e132 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input.expected-rewrite.serialised.json @@ -113,7 +113,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null @@ -136,7 +136,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null @@ -159,7 +159,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json index d2a9469135..868a063103 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json @@ -42,7 +42,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null @@ -102,7 +102,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null @@ -125,7 +125,7 @@ ] }, { - "ModuloEqUndefZero": [ + "MinionModuloEqUndefZero": [ { "clean": false, "etype": null diff --git a/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt index d0c72dd8db..ab58bbf1cf 100644 --- a/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/sumgeq/input-expected-rule-trace-human.txt @@ -1,5 +1,5 @@ (Sum([x, y]) >= z), - ~~> flatten_sum_geq ([("Minion", 4400)]) + ~~> introduce_sumgeq ([("Minion", 4400)]) SumGeq([x, y], z) -- diff --git a/conjure_oxide/tests/integration/minion_constraints/sumgeq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/sumgeq/input.expected-rewrite.serialised.json index 8fffb50488..7a9d716a6a 100644 --- a/conjure_oxide/tests/integration/minion_constraints/sumgeq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/sumgeq/input.expected-rewrite.serialised.json @@ -1,51 +1,27 @@ { "constraints": [ { - "SumGeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "z" - } - } - ] + "Reference": { + "UserName": "z" + } } ] } diff --git a/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt index 8577cf5c5f..c00324929d 100644 --- a/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/sumleq/input-expected-rule-trace-human.txt @@ -1,5 +1,5 @@ (Sum([x, y]) <= z), - ~~> sum_leq_to_sumleq ([("Minion", 4400)]) + ~~> introduce_sumleq ([("Minion", 4400)]) SumLeq([x, y], z) -- diff --git a/conjure_oxide/tests/integration/minion_constraints/sumleq/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/minion_constraints/sumleq/input.expected-rewrite.serialised.json index cd8bef5024..55e31b0d5a 100644 --- a/conjure_oxide/tests/integration/minion_constraints/sumleq/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/minion_constraints/sumleq/input.expected-rewrite.serialised.json @@ -1,51 +1,27 @@ { "constraints": [ { - "SumLeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "x" - } - } - ] + "Reference": { + "UserName": "x" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "y" - } - } - ] + "Reference": { + "UserName": "y" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "z" - } - } - ] + "Reference": { + "UserName": "z" + } } ] } diff --git a/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt index 7f7bb34698..99ee85110c 100644 --- a/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt @@ -5,14 +5,14 @@ Sum([a, b, c]) -- (Sum([a, b, c]) = 4), - ~~> sum_eq_to_sumeq ([("Minion", 4400)]) + ~~> sum_eq_to_sumeq ([("Minion", 4200)]) SumEq([a, b, c], 4) -- SumEq([a, b, c], 4), ~~> sumeq_to_minion ([("Minion", 4400)]) -And([SumGeq([a, b, c], 4), SumLeq([a, b, c], 4)]) +And([SumLeq([a, b, c], 4), SumGeq([a, b, c], 4)]) -- diff --git a/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json index 3237a7cc60..d18b9969af 100644 --- a/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/integration/xyz/input.expected-rewrite.serialised.json @@ -8,126 +8,62 @@ }, [ { - "SumGeq": [ + "FlatSumLeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Reference": { + "UserName": "c" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 4 - } - } - ] + "Literal": { + "Int": 4 + } } ] }, { - "SumLeq": [ + "FlatSumGeq": [ { "clean": false, "etype": null }, [ { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "c" - } - } - ] + "Reference": { + "UserName": "c" + } } ], { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 4 - } - } - ] + "Literal": { + "Int": 4 + } } ] } @@ -135,49 +71,23 @@ ] }, { - "Ineq": [ + "FlatIneq": [ { "clean": false, "etype": null }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "b" - } - } - ] + "Reference": { + "UserName": "b" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Reference": { - "UserName": "a" - } - } - ] + "Reference": { + "UserName": "a" + } }, { - "Atomic": [ - { - "clean": false, - "etype": null - }, - { - "Literal": { - "Int": 0 - } - } - ] + "Int": 0 } ] } diff --git a/conjure_oxide/tests/rewrite_tests.rs b/conjure_oxide/tests/rewrite_tests.rs index ac85555470..62bceb51c2 100644 --- a/conjure_oxide/tests/rewrite_tests.rs +++ b/conjure_oxide/tests/rewrite_tests.rs @@ -178,7 +178,7 @@ fn rule_sum_constants() { #[test] fn rule_sum_geq() { - let flatten_sum_geq = get_rule_by_name("flatten_sum_geq").unwrap(); + let introduce_sumgeq = get_rule_by_name("introduce_sumgeq").unwrap(); let mut expr = Expression::Geq( Metadata::new(), @@ -195,23 +195,20 @@ fn rule_sum_geq() { )), ); - expr = flatten_sum_geq + expr = introduce_sumgeq .apply(&expr, &Model::new_empty(Default::default())) .unwrap() .new_expression; assert_eq!( expr, - Expression::SumGeq( + Expression::FlatSumGeq( Metadata::new(), vec![ - Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))), - Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))), + Atom::Literal(Literal::Int(1)), + Atom::Literal(Literal::Int(2)), ], - Box::new(Expression::Atomic( - Metadata::new(), - Atom::Literal(Literal::Int(3)) - )) + Atom::Literal(Literal::Int(3)) ) ); } @@ -229,7 +226,7 @@ fn reduce_solve_xyz() { let sum_constants = get_rule_by_name("partial_evaluator").unwrap(); let unwrap_sum = get_rule_by_name("remove_unit_vector_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(); + let introduce_sumleq = get_rule_by_name("introduce_sumleq").unwrap(); // 2 + 3 - 1 let mut expr1 = Expression::Sum( @@ -276,32 +273,20 @@ fn reduce_solve_xyz() { )), Box::new(expr1), ); - expr1 = sum_leq_to_sumleq + expr1 = introduce_sumleq .apply(&expr1, &Model::new_empty(Default::default())) .unwrap() .new_expression; assert_eq!( expr1, - Expression::SumLeq( + Expression::FlatSumLeq( Metadata::new(), vec![ - Expression::Atomic( - Metadata::new(), - Atom::Reference(Name::UserName(String::from("a"))) - ), - Expression::Atomic( - Metadata::new(), - Atom::Reference(Name::UserName(String::from("b"))) - ), - Expression::Atomic( - Metadata::new(), - Atom::Reference(Name::UserName(String::from("c"))) - ), + Atom::Reference(Name::UserName(String::from("a"))), + Atom::Reference(Name::UserName(String::from("b"))), + Atom::Reference(Name::UserName(String::from("c"))), ], - Box::new(Expression::Atomic( - Metadata::new(), - Atom::Literal(Literal::Int(4)) - )) + Atom::Literal(Literal::Int(4)) ) ); @@ -323,20 +308,11 @@ fn reduce_solve_xyz() { .new_expression; assert_eq!( expr2, - Expression::Ineq( + Expression::FlatIneq( Metadata::new(), - Box::new(Expression::Atomic( - Metadata::new(), - Atom::Reference(Name::UserName(String::from("a"))) - )), - Box::new(Expression::Atomic( - Metadata::new(), - Atom::Reference(Name::UserName(String::from("b"))) - )), - Box::new(Expression::Atomic( - Metadata::new(), - Atom::Literal(Literal::Int(-1)) - )) + Atom::Reference(Name::UserName(String::from("a"))), + Atom::Reference(Name::UserName(String::from("b"))), + Literal::Int(-1), ) ); diff --git a/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index 3e328b8fff..abdab0bc8d 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -8,6 +8,7 @@ use uniplate::derive::Uniplate; use uniplate::{Biplate, Uniplate as _}; use crate::ast::literals::Literal; +use crate::ast::pretty::pretty_vec; use crate::ast::symbol_table::{Name, SymbolTable}; use crate::ast::Atom; use crate::ast::ReturnType; @@ -34,15 +35,9 @@ pub enum Expression { Atomic(Metadata, Atom), - #[compatible(Minion, JsonInput)] + #[compatible(JsonInput)] Sum(Metadata, Vec), - // /// Division after preventing division by zero, usually with a top-level constraint - // #[compatible(Minion)] - // SafeDiv(Metadata, Box, Box), - // /// Division with a possibly undefined value (division by 0) - // #[compatible(Minion, JsonInput)] - // Div(Metadata, Box, Box), #[compatible(JsonInput)] Min(Metadata, Vec), @@ -94,11 +89,15 @@ pub enum Expression { #[compatible(JsonInput)] Neg(Metadata, Box), + #[compatible(JsonInput)] + AllDiff(Metadata, Vec), + /// Binary subtraction operator /// - /// This mainly exists for ease of parsing, and is immediately normalised to `Sum([a,-b])`. + /// This is a parser-level construct, and is immediately normalised to `Sum([a,-b])`. #[compatible(JsonInput)] Minus(Metadata, Box, Box), + /* Flattened SumEq. * * Note: this is an intermediary step that's used in the process of converting from conjure model to minion. @@ -108,53 +107,97 @@ pub enum Expression { */ SumEq(Metadata, Vec, Box), - // Flattened Constraints + /// Ensures that sum(vec) >= x. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#sumgeq) #[compatible(Minion)] - SumGeq(Metadata, Vec, Box), + FlatSumGeq(Metadata, Vec, Atom), + /// Ensures that sum(vec) <= x. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#sumleq) #[compatible(Minion)] - SumLeq(Metadata, Vec, Box), + FlatSumLeq(Metadata, Vec, Atom), - /// `a / b = c` + /// `ineq(x,y,k)` ensures that x <= y + k. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#ineq) #[compatible(Minion)] - DivEqUndefZero(Metadata, Atom, Atom, Atom), + FlatIneq(Metadata, Atom, Atom, Literal), - /// `a % b = c` + /// `w-literal(x,k)` ensures that x == k, where x is a variable and k a constant. + /// + /// Low-level Minion constraint. + /// + /// 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 also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#minuseq) + /// + `rules::minion::boolean_literal_to_wliteral`. #[compatible(Minion)] - ModuloEqUndefZero(Metadata, Atom, Atom, Atom), + FlatWatchedLiteral(Metadata, Name, Literal), + /// Ensures that x =-y, where x and y are atoms. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#minuseq) #[compatible(Minion)] - Ineq(Metadata, Box, Box, Box), + FlatMinusEq(Metadata, Atom, Atom), + /// Ensures that floor(x/y)=z. Always true when y=0. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#div_undefzero) #[compatible(Minion)] - AllDiff(Metadata, Vec), + MinionDivEqUndefZero(Metadata, Atom, Atom, Atom), - /// w-literal(x,k) is SAT iff x == k, where x is a variable and k a constant. + /// Ensures that x%y=z. Always true when y=0. /// - /// 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`. + /// Low-level Minion constraint. /// + /// # See also /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#mod_undefzero) #[compatible(Minion)] - WatchedLiteral(Metadata, Name, Literal), + MinionModuloEqUndefZero(Metadata, Atom, Atom, Atom), + /// `reify(constraint,r)` ensures that r=1 iff `constraint` is satisfied, where r is a 0/1 + /// variable. + /// + /// Low-level Minion constraint. + /// + /// # See also + /// + /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#reify) #[compatible(Minion)] - Reify(Metadata, Box, Box), + MinionReify(Metadata, Box, Atom), /// Declaration of an auxiliary variable. /// /// As with Savile Row, we semantically distinguish this from `Eq`. #[compatible(Minion)] AuxDeclaration(Metadata, Name, Box), - - /// `x =-y`, where x and y are atoms. - /// - /// Low-level Minion constraint. - #[compatible(Minion)] - MinusEq(Metadata, Atom, Atom), } fn expr_vec_to_domain_i32( @@ -265,14 +308,14 @@ impl Expression { Expression::Gt(_, _, _) => Some(Domain::BoolDomain), Expression::Lt(_, _, _) => Some(Domain::BoolDomain), Expression::SumEq(_, _, _) => Some(Domain::BoolDomain), - Expression::SumGeq(_, _, _) => Some(Domain::BoolDomain), - Expression::SumLeq(_, _, _) => Some(Domain::BoolDomain), - Expression::DivEqUndefZero(_, _, _, _) => Some(Domain::BoolDomain), - Expression::ModuloEqUndefZero(_, _, _, _) => Some(Domain::BoolDomain), - Expression::Ineq(_, _, _, _) => Some(Domain::BoolDomain), + Expression::FlatSumGeq(_, _, _) => Some(Domain::BoolDomain), + Expression::FlatSumLeq(_, _, _) => Some(Domain::BoolDomain), + Expression::MinionDivEqUndefZero(_, _, _, _) => Some(Domain::BoolDomain), + Expression::MinionModuloEqUndefZero(_, _, _, _) => Some(Domain::BoolDomain), + Expression::FlatIneq(_, _, _, _) => Some(Domain::BoolDomain), Expression::AllDiff(_, _) => Some(Domain::BoolDomain), - Expression::WatchedLiteral(_, _, _) => Some(Domain::BoolDomain), - Expression::Reify(_, _, _) => Some(Domain::BoolDomain), + Expression::FlatWatchedLiteral(_, _, _) => Some(Domain::BoolDomain), + Expression::MinionReify(_, _, _) => Some(Domain::BoolDomain), Expression::Neg(_, x) => { let Some(Domain::IntDomain(mut ranges)) = x.domain_of(vars) else { return None; @@ -291,7 +334,7 @@ impl Expression { .domain_of(vars)? .apply_i32(|x, y| Some(x - y), &b.domain_of(vars)?), - Expression::MinusEq(_, _, _) => Some(Domain::BoolDomain), + Expression::FlatMinusEq(_, _, _) => Some(Domain::BoolDomain), // #[allow(unreachable_patterns)] // _ => bug!("Cannot calculate domain of {:?}", self), }; @@ -353,21 +396,21 @@ impl Expression { Expression::SafeDiv(_, _, _) => Some(ReturnType::Int), Expression::UnsafeDiv(_, _, _) => Some(ReturnType::Int), Expression::SumEq(_, _, _) => Some(ReturnType::Bool), - Expression::SumGeq(_, _, _) => Some(ReturnType::Bool), - Expression::SumLeq(_, _, _) => Some(ReturnType::Bool), - Expression::DivEqUndefZero(_, _, _, _) => Some(ReturnType::Bool), - Expression::Ineq(_, _, _, _) => Some(ReturnType::Bool), + Expression::FlatSumGeq(_, _, _) => Some(ReturnType::Bool), + Expression::FlatSumLeq(_, _, _) => Some(ReturnType::Bool), + Expression::MinionDivEqUndefZero(_, _, _, _) => Some(ReturnType::Bool), + Expression::FlatIneq(_, _, _, _) => Some(ReturnType::Bool), Expression::AllDiff(_, _) => Some(ReturnType::Bool), Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool? - Expression::WatchedLiteral(_, _, _) => Some(ReturnType::Bool), - Expression::Reify(_, _, _) => Some(ReturnType::Bool), + Expression::FlatWatchedLiteral(_, _, _) => Some(ReturnType::Bool), + Expression::MinionReify(_, _, _) => Some(ReturnType::Bool), Expression::AuxDeclaration(_, _, _) => Some(ReturnType::Bool), Expression::UnsafeMod(_, _, _) => Some(ReturnType::Int), Expression::SafeMod(_, _, _) => Some(ReturnType::Int), - Expression::ModuloEqUndefZero(_, _, _, _) => Some(ReturnType::Bool), + Expression::MinionModuloEqUndefZero(_, _, _, _) => Some(ReturnType::Bool), Expression::Neg(_, _) => Some(ReturnType::Int), Expression::Minus(_, _, _) => Some(ReturnType::Int), - Expression::MinusEq(_, _, _) => Some(ReturnType::Bool), + Expression::FlatMinusEq(_, _, _) => Some(ReturnType::Bool), } } @@ -391,25 +434,6 @@ impl Expression { } } -fn display_expressions(expressions: &[Expression]) -> String { - // if expressions.len() <= 3 { - format!( - "[{}]", - expressions - .iter() - .map(|e| e.to_string()) - .collect::>() - .join(", ") - ) - // } else { - // format!( - // "[{}..{}]", - // expressions[0], - // expressions[expressions.len() - 1] - // ) - // } -} - impl From for Expression { fn from(i: i32) -> Self { Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(i))) @@ -433,22 +457,22 @@ impl Display for Expression { match &self { Expression::Atomic(_, atom) => atom.fmt(f), Expression::Sum(_, expressions) => { - write!(f, "Sum({})", display_expressions(expressions)) + write!(f, "Sum({})", pretty_vec(expressions)) } Expression::Min(_, expressions) => { - write!(f, "Min({})", display_expressions(expressions)) + write!(f, "Min({})", pretty_vec(expressions)) } Expression::Max(_, expressions) => { - write!(f, "Max({})", display_expressions(expressions)) + write!(f, "Max({})", pretty_vec(expressions)) } Expression::Not(_, expr_box) => { write!(f, "Not({})", expr_box.clone()) } Expression::Or(_, expressions) => { - write!(f, "Or({})", display_expressions(expressions)) + write!(f, "Or({})", pretty_vec(expressions)) } Expression::And(_, expressions) => { - write!(f, "And({})", display_expressions(expressions)) + write!(f, "And({})", pretty_vec(expressions)) } Expression::Eq(_, box1, box2) => { write!(f, "({} = {})", box1.clone(), box2.clone()) @@ -472,17 +496,17 @@ impl Display for Expression { write!( f, "SumEq({}, {})", - display_expressions(expressions), + pretty_vec(expressions), expr_box.clone() ) } - Expression::SumGeq(_, box1, box2) => { - write!(f, "SumGeq({}, {})", display_expressions(box1), box2.clone()) + Expression::FlatSumGeq(_, box1, box2) => { + write!(f, "SumGeq({}, {})", pretty_vec(box1), box2.clone()) } - Expression::SumLeq(_, box1, box2) => { - write!(f, "SumLeq({}, {})", display_expressions(box1), box2.clone()) + Expression::FlatSumLeq(_, box1, box2) => { + write!(f, "SumLeq({}, {})", pretty_vec(box1), box2.clone()) } - Expression::Ineq(_, box1, box2, box3) => write!( + Expression::FlatIneq(_, box1, box2, box3) => write!( f, "Ineq({}, {}, {})", box1.clone(), @@ -490,7 +514,7 @@ impl Display for Expression { box3.clone() ), Expression::AllDiff(_, expressions) => { - write!(f, "AllDiff({})", display_expressions(expressions)) + write!(f, "AllDiff({})", pretty_vec(expressions)) } Expression::Bubble(_, box1, box2) => { write!(f, "{{{} @ {}}}", box1.clone(), box2.clone()) @@ -501,7 +525,7 @@ impl Display for Expression { Expression::UnsafeDiv(_, box1, box2) => { write!(f, "UnsafeDiv({}, {})", box1.clone(), box2.clone()) } - Expression::DivEqUndefZero(_, box1, box2, box3) => { + Expression::MinionDivEqUndefZero(_, box1, box2, box3) => { write!( f, "DivEq({}, {}, {})", @@ -510,7 +534,7 @@ impl Display for Expression { box3.clone() ) } - Expression::ModuloEqUndefZero(_, box1, box2, box3) => { + Expression::MinionModuloEqUndefZero(_, box1, box2, box3) => { write!( f, "ModEq({}, {}, {})", @@ -520,10 +544,10 @@ impl Display for Expression { ) } - Expression::WatchedLiteral(_, x, l) => { + Expression::FlatWatchedLiteral(_, x, l) => { write!(f, "WatchedLiteral({},{})", x, l) } - Expression::Reify(_, box1, box2) => { + Expression::MinionReify(_, box1, box2) => { write!(f, "Reify({}, {})", box1.clone(), box2.clone()) } Expression::AuxDeclaration(_, n, e) => { @@ -541,7 +565,7 @@ impl Display for Expression { Expression::Minus(_, a, b) => { write!(f, "({} - {})", a.clone(), b.clone()) } - Expression::MinusEq(_, a, b) => { + Expression::FlatMinusEq(_, a, b) => { write!(f, "MinusEq({},{})", a.clone(), b.clone()) } } diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs index 5c3d2de9ab..9dfb16d59d 100644 --- a/crates/conjure_core/src/rules/base.rs +++ b/crates/conjure_core/src/rules/base.rs @@ -28,10 +28,14 @@ fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult { if matches!( expr, Atomic(_, _) - | WatchedLiteral(_, _, _) - | DivEqUndefZero(_, _, _, _) - | ModuloEqUndefZero(_, _, _, _) - | MinusEq(_, _, _) + | FlatIneq(_, _, _, _) + | FlatMinusEq(_, _, _) + | FlatSumGeq(_, _, _) + | FlatSumLeq(_, _, _) + | FlatWatchedLiteral(_, _, _) + | MinionDivEqUndefZero(_, _, _, _) + | MinionModuloEqUndefZero(_, _, _, _) + | MinionReify(_, _, _) ) { return Err(ApplicationError::RuleNotApplicable); } diff --git a/crates/conjure_core/src/rules/constant_eval.rs b/crates/conjure_core/src/rules/constant_eval.rs index 27423eef47..4e759d8fc5 100644 --- a/crates/conjure_core/src/rules/constant_eval.rs +++ b/crates/conjure_core/src/rules/constant_eval.rs @@ -43,15 +43,31 @@ pub fn eval_constant(expr: &Expr) -> Option { Expr::Sum(_, exprs) => vec_op::(|e| e.iter().sum(), exprs).map(Lit::Int), - Expr::Ineq(_, a, b, c) => { - tern_op::(|a, b, c| a <= (b + c), a, b, c).map(Lit::Bool) + Expr::FlatIneq(_, a, b, c) => { + let a: i32 = a.try_into().ok()?; + let b: i32 = b.try_into().ok()?; + let c: i32 = c.try_into().ok()?; + + Some(Lit::Bool(a <= b + c)) } - Expr::SumGeq(_, exprs, a) => { - flat_op::(|e, a| e.iter().sum::() >= a, exprs, a).map(Lit::Bool) + Expr::FlatSumGeq(_, exprs, a) => { + let sum = exprs.iter().try_fold(0, |acc, atom: &Atom| { + let n: i32 = atom.try_into().ok()?; + let acc = acc + n; + Some(acc) + })?; + + Some(Lit::Bool(sum >= a.try_into().ok()?)) } - Expr::SumLeq(_, exprs, a) => { - flat_op::(|e, a| e.iter().sum::() <= a, exprs, a).map(Lit::Bool) + Expr::FlatSumLeq(_, exprs, a) => { + let sum = exprs.iter().try_fold(0, |acc, atom: &Atom| { + let n: i32 = atom.try_into().ok()?; + let acc = acc + n; + Some(acc) + })?; + + Some(Lit::Bool(sum >= a.try_into().ok()?)) } Expr::Min(_, exprs) => { opt_vec_op::(|e| e.iter().min().copied(), exprs).map(Lit::Int) @@ -72,7 +88,7 @@ pub fn eval_constant(expr: &Expr) -> Option { bin_op::(|a, b| a - b * (a as f32 / b as f32).floor() as i32, a, b) .map(Lit::Int) } - Expr::DivEqUndefZero(_, a, b, c) => { + Expr::MinionDivEqUndefZero(_, a, b, c) => { // div always rounds down let a: i32 = a.try_into().ok()?; let b: i32 = b.try_into().ok()?; @@ -89,11 +105,18 @@ pub fn eval_constant(expr: &Expr) -> Option { } Expr::Bubble(_, a, b) => bin_op::(|a, b| a && b, a, b).map(Lit::Bool), - Expr::Reify(_, a, b) => bin_op::(|a, b| a == b, a, b).map(Lit::Bool), + Expr::MinionReify(_, a, b) => { + let result = eval_constant(a)?; + + let result: bool = result.try_into().ok()?; + let b: bool = b.try_into().ok()?; + + Some(Lit::Bool(b == result)) + } Expr::SumEq(_, exprs, a) => { flat_op::(|e, a| e.iter().sum::() == a, exprs, a).map(Lit::Bool) } - Expr::ModuloEqUndefZero(_, a, b, c) => { + Expr::MinionModuloEqUndefZero(_, a, b, c) => { // From Savile Row. Same semantics as division. // // a - (b * floor(a/b)) @@ -126,7 +149,7 @@ pub fn eval_constant(expr: &Expr) -> Option { } Some(Lit::Bool(true)) } - Expr::WatchedLiteral(_, _, _) => None, + Expr::FlatWatchedLiteral(_, _, _) => None, Expr::AuxDeclaration(_, _, _) => None, Expr::Neg(_, a) => { let a: &Atom = a.try_into().ok()?; @@ -142,7 +165,7 @@ pub fn eval_constant(expr: &Expr) -> Option { Some(Lit::Int(a - b)) } - Expr::MinusEq(_, a, b) => { + Expr::FlatMinusEq(_, a, b) => { let a: i32 = a.try_into().ok()?; let b: i32 = b.try_into().ok()?; Some(Lit::Bool(a == -b)) @@ -170,6 +193,7 @@ where Some(f(a, b)) } +#[allow(dead_code)] fn tern_op(f: fn(T, T, T) -> A, a: &Expr, b: &Expr, c: &Expr) -> Option where T: TryFrom, diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index 15e8e7068e..229fd47fa4 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -2,13 +2,9 @@ /* Rules for translating to Minion-supported constraints */ /************************************************************************/ -use crate::ast::{ - Atom::{self, *}, - Domain, - Expression::{self as Expr, *}, - Literal::*, -}; -use std::borrow::Borrow; +use std::borrow::Borrow as _; + +use crate::ast::{Atom, Domain, Expression as Expr, Literal as Lit}; use crate::ast::Name; use crate::metadata::Metadata; @@ -22,7 +18,7 @@ use crate::Model; use uniplate::Uniplate; use ApplicationError::RuleNotApplicable; -use super::utils::{is_flat, to_aux_var}; +use super::utils::{expressions_to_atoms, is_flat, to_aux_var}; register_rule_set!("Minion", 100, ("Base"), (SolverFamily::Minion)); @@ -70,7 +66,7 @@ fn introduce_diveq(expr: &Expr, _: &Model) -> ApplicationResult { let a: &Atom = (&children[0]).try_into().or(Err(RuleNotApplicable))?; let b: &Atom = (&children[1]).try_into().or(Err(RuleNotApplicable))?; - Ok(Reduction::pure(DivEqUndefZero( + Ok(Reduction::pure(Expr::MinionDivEqUndefZero( meta.clone_dirty(), a.clone(), b.clone(), @@ -121,7 +117,7 @@ fn introduce_modeq(expr: &Expr, _: &Model) -> ApplicationResult { let a: &Atom = (&children[0]).try_into().or(Err(RuleNotApplicable))?; let b: &Atom = (&children[1]).try_into().or(Err(RuleNotApplicable))?; - Ok(Reduction::pure(ModuloEqUndefZero( + Ok(Reduction::pure(Expr::MinionModuloEqUndefZero( meta.clone_dirty(), a.clone(), b.clone(), @@ -138,13 +134,13 @@ fn introduce_modeq(expr: &Expr, _: &Model) -> ApplicationResult { /// ``` #[register_rule(("Minion", 4400))] fn introduce_minuseq_from_eq(expr: &Expr, _: &Model) -> ApplicationResult { - let Eq(_, a, b) = expr else { + let Expr::Eq(_, a, b) = expr else { return Err(RuleNotApplicable); }; fn try_get_atoms(a: &Expr, b: &Expr) -> Option<(Atom, Atom)> { let a: &Atom = a.try_into().ok()?; - let Neg(_, b) = b else { + let Expr::Neg(_, b) = b else { return None; }; @@ -161,7 +157,7 @@ fn introduce_minuseq_from_eq(expr: &Expr, _: &Model) -> ApplicationResult { return Err(RuleNotApplicable); }; - Ok(Reduction::pure(MinusEq(Metadata::new(), x, y))) + Ok(Reduction::pure(Expr::FlatMinusEq(Metadata::new(), x, y))) } /// Introduces a Minion `MinusEq` constraint from `x =aux -y`, where x and y are atoms. @@ -175,13 +171,13 @@ fn introduce_minuseq_from_eq(expr: &Expr, _: &Model) -> ApplicationResult { fn introduce_minuseq_from_aux_decl(expr: &Expr, _: &Model) -> ApplicationResult { // a =aux -b // - let AuxDeclaration(_, a, b) = expr else { + let Expr::AuxDeclaration(_, a, b) = expr else { return Err(RuleNotApplicable); }; let a = Atom::Reference(a.clone()); - let Neg(_, b) = (**b).clone() else { + let Expr::Neg(_, b) = (**b).clone() else { return Err(RuleNotApplicable); }; @@ -189,7 +185,7 @@ fn introduce_minuseq_from_aux_decl(expr: &Expr, _: &Model) -> ApplicationResult return Err(RuleNotApplicable); }; - Ok(Reduction::pure(MinusEq(Metadata::new(), a, b))) + Ok(Reduction::pure(Expr::FlatMinusEq(Metadata::new(), a, b))) } #[register_rule(("Minion", 4400))] @@ -229,7 +225,7 @@ fn flatten_binop(expr: &Expr, model: &Model) -> ApplicationResult { fn flatten_vecop(expr: &Expr, model: &Model) -> ApplicationResult { if !matches!( expr, - Expr::Sum(_, _) | Expr::SumGeq(_, _, _) | Expr::SumLeq(_, _, _) + Expr::Sum(_, _) | Expr::FlatSumGeq(_, _, _) | Expr::FlatSumLeq(_, _, _) ) { return Err(RuleNotApplicable); } @@ -290,15 +286,6 @@ fn flatten_eq(expr: &Expr, model: &Model) -> ApplicationResult { Ok(Reduction::new(expr, new_tops, model.variables)) } -fn is_nested_sum(exprs: &Vec) -> bool { - for e in exprs { - if let Sum(_, _) = e { - return true; - } - } - false -} - /// Flattens `a=-e`, where e is a non-atomic expression. /// /// ```text @@ -313,11 +300,11 @@ fn flatten_minuseq(expr: &Expr, m: &Model) -> ApplicationResult { // parses arguments a = -e, where a is an atom and e is a non-atomic expression // (when e is an atom, flattening is done, so introduce_minus_eq should be applied instead) fn try_get_args(name: &Expr, negated_expr: &Expr) -> Option<(Name, Expr)> { - let Atomic(_, Atom::Reference(name)) = name else { + let Expr::Atomic(_, Atom::Reference(name)) = name else { return None; }; - let Neg(_, e) = negated_expr else { + let Expr::Neg(_, e) = negated_expr else { return None; }; @@ -326,12 +313,12 @@ fn flatten_minuseq(expr: &Expr, m: &Model) -> ApplicationResult { let (name, e) = match expr { // parse arguments symmetrically - Eq(_, a, b) => try_get_args(a.borrow(), b.borrow()) + Expr::Eq(_, a, b) => try_get_args(a.borrow(), b.borrow()) .or_else(|| try_get_args(b.borrow(), a.borrow())) .ok_or(RuleNotApplicable), - AuxDeclaration(_, name, e) => match e.borrow() { - Neg(_, e) => Some((name.clone(), (*e.clone()))), + Expr::AuxDeclaration(_, name, e) => match e.borrow() { + Expr::Neg(_, e) => Some((name.clone(), (*e.clone()))), _ => None, } .ok_or(RuleNotApplicable), @@ -341,7 +328,7 @@ fn flatten_minuseq(expr: &Expr, m: &Model) -> ApplicationResult { let aux_var_out = to_aux_var(&e, m).ok_or(RuleNotApplicable)?; - let new_expr = MinusEq( + let new_expr = Expr::FlatMinusEq( Metadata::new(), Atom::Reference(name), aux_var_out.as_atom(), @@ -354,94 +341,70 @@ fn flatten_minuseq(expr: &Expr, m: &Model) -> ApplicationResult { )) } -/** - * Helper function to get the vector of expressions from a sum (or error if it's a nested sum - we need to flatten it first) - */ -fn sum_to_vector(expr: &Expr) -> Result, ApplicationError> { - match expr { - Sum(_, exprs) => { - if is_nested_sum(exprs) { - Err(RuleNotApplicable) - } else { - Ok(exprs.clone()) - } - } - _ => Err(RuleNotApplicable), - } -} +// TODO: normalise equalities such that atoms are always on the LHS. +// i.e. always have a = sum(x,y,z), not sum(x,y,z) = a -// /** -// * Convert an Eq to a conjunction of Geq and Leq: -// * ```text -// * a = b => a >= b && a <= b -// * ``` -// */ -// #[register_rule(("Minion", 100))] -// fn eq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult { -// match expr { -// Expr::Eq(metadata, a, b) => Ok(Reduction::pure(Expr::And( -// metadata.clone_dirty(), -// vec![ -// Expr::Geq(metadata.clone_dirty(), a.clone(), b.clone()), -// Expr::Leq(metadata.clone_dirty(), a.clone(), b.clone()), -// ], -// ))), -// _ => Err(ApplicationError::RuleNotApplicable), -// } -// } - -/** - * Convert a Geq to a SumGeq if the left hand side is a sum: - * ```text - * sum([a, b, c]) >= d => sum_geq([a, b, c], d) - * ``` - */ +/// Converts a Geq to a SumGeq if the left hand side is a sum +/// +/// ```text +/// sum([a, b, c]) >= d ~> sumgeq([a, b, c], d) +/// ``` #[register_rule(("Minion", 4400))] -fn flatten_sum_geq(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Geq(metadata, a, b) => { - let exprs = sum_to_vector(a)?; - Ok(Reduction::pure(SumGeq( - metadata.clone_dirty(), - exprs, - b.clone(), - ))) - } - _ => Err(RuleNotApplicable), - } +fn introduce_sumgeq(expr: &Expr, _: &Model) -> ApplicationResult { + let Expr::Geq(meta, e1, e2) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Expr::Sum(_, es) = *e1 else { + return Err(RuleNotApplicable); + }; + + let Some(atoms) = expressions_to_atoms(&es) else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, rhs) = *e2 else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::FlatSumGeq(meta, atoms, rhs))) } -/** - * Convert a Leq to a SumLeq if the left hand side is a sum: - * ```text - * sum([a, b, c]) <= d => sum_leq([a, b, c], d) - * ``` - */ +/// Converts a Leq to a SumLeq if the left hand side is a sum +/// +/// ```text +/// sum([a, b, c]) >= d ~> sumgeq([a, b, c], d) +/// ``` #[register_rule(("Minion", 4400))] -fn sum_leq_to_sumleq(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Leq(metadata, a, b) => { - let exprs = sum_to_vector(a)?; - Ok(Reduction::pure(SumLeq( - metadata.clone_dirty(), - exprs, - b.clone(), - ))) - } - _ => Err(RuleNotApplicable), - } +fn introduce_sumleq(expr: &Expr, _: &Model) -> ApplicationResult { + let Expr::Leq(meta, e1, e2) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Expr::Sum(_, es) = *e1 else { + return Err(RuleNotApplicable); + }; + + let Some(atoms) = expressions_to_atoms(&es) else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, rhs) = *e2 else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::FlatSumLeq(meta, atoms, rhs))) } -/** - * Convert a 'Eq(Sum([...]))' to a SumEq - * ```text - * eq(sum([a, b]), c) => sumeq([a, b], c) - * ``` -*/ -#[register_rule(("Minion", 4400))] +/// Converts a 'Eq(Sum([...]))' to a SumEq +/// ```text +/// eq(sum([a, b]), c) => sumeq([a, b], c) +/// ``` + +#[register_rule(("Minion", 4200))] fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { fn try_get_args(sum_expr: &Expr, value: &Expr) -> Option<(Vec, Expr)> { - let Sum(_, xs) = sum_expr else { + let Expr::Sum(_, xs) = sum_expr else { return None; }; @@ -449,17 +412,17 @@ fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { } let (xs, value) = match expr { - Eq(_, a, b) => { + Expr::Eq(_, a, b) => { // get arguments symmetrically try_get_args(a, b) .or_else(|| try_get_args(b, a)) .ok_or(RuleNotApplicable) } - AuxDeclaration(_, name, e) => { + Expr::AuxDeclaration(_, name, e) => { let value = Atom::Reference(name.clone()).into(); let xs = match *e.clone() { - Sum(_, xs) => Ok(xs), + Expr::Sum(_, xs) => Ok(xs), _ => Err(RuleNotApplicable), }?; @@ -469,164 +432,187 @@ fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { _ => Err(RuleNotApplicable), }?; - Ok(Reduction::pure(SumEq(Metadata::new(), xs, Box::new(value)))) + Ok(Reduction::pure(Expr::SumEq( + Metadata::new(), + xs, + Box::new(value), + ))) } -/** - * Convert a `SumEq` to an `And(SumGeq, SumLeq)` - * This is a workaround for Minion not having support for a flat "equals" operation on sums - * ```text - * sumeq([a, b], c) -> watched_and({ - * sumleq([a, b], c), - * sumgeq([a, b], c) - * }) - * ``` - * I. e. - * ```text - * ((a + b) >= c) && ((a + b) <= c) - * a + b = c - * ``` - */ +/// Converts a `SumEq` to an `And(SumGeq, SumLeq)` +/// +/// This is a workaround for Minion not having support for a flat "equals" operation on sums +/// +/// ```text +/// sumeq([a, b], c) -> watched_and({ +/// sumleq([a, b], c), +/// sumgeq([a, b], c) +/// }) +/// ``` #[register_rule(("Minion", 4400))] fn sumeq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - SumEq(_metadata, exprs, eq_to) => Ok(Reduction::pure(And( - Metadata::new(), - vec![ - SumGeq(Metadata::new(), exprs.clone(), Box::from(*eq_to.clone())), - SumLeq(Metadata::new(), exprs.clone(), Box::from(*eq_to.clone())), - ], - ))), - _ => Err(RuleNotApplicable), - } + let Expr::SumEq(_, exprs, eq_to) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Some(atoms) = expressions_to_atoms(&exprs) else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, eq_to_atom) = *eq_to else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::And( + Metadata::new(), + vec![ + Expr::FlatSumLeq(Metadata::new(), atoms.clone(), eq_to_atom.clone()), + Expr::FlatSumGeq(Metadata::new(), atoms, eq_to_atom), + ], + ))) } /** -* Convert a Lt to an Ineq: +* Convert a Lt to an Ineq * ```text -* a < b ~> a <= b -1 ~> ineq(a,b,-1) +* x < y ~> x <= y -1 ~> ineq(x,y,-1) * ``` */ #[register_rule(("Minion", 4100))] fn lt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Lt(metadata, a, b) => Ok(Reduction::pure(Ineq( - metadata.clone_dirty(), - a.clone(), - b.clone(), - Box::new(Atomic(Metadata::new(), Literal(Int(-1)))), - ))), - _ => Err(RuleNotApplicable), - } + let Expr::Lt(meta, e1, e2) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, x) = *e1 else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, y) = *e2 else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::FlatIneq( + meta.clone_dirty(), + x, + y, + Lit::Int(-1), + ))) } -/** -* Convert a Gt to an Ineq: -* -* ```text -* a > b ~> b <= a -1 ~> ineq(b,a,-1) -* ``` -*/ +/// Converts a Gt to an Ineq +/// +/// ```text +/// x > y ~> y <= x -1 ~> ineq(y,x,-1) +/// ``` #[register_rule(("Minion", 4100))] fn gt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Gt(metadata, a, b) => Ok(Reduction::pure(Ineq( - metadata.clone_dirty(), - b.clone(), - a.clone(), - Box::new(Atomic(Metadata::new(), Literal(Int(-1)))), - ))), - _ => Err(RuleNotApplicable), - } + let Expr::Gt(meta, e1, e2) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, x) = *e1 else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, y) = *e2 else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::FlatIneq( + meta.clone_dirty(), + y, + x, + Lit::Int(-1), + ))) } -/** -* Convert a Geq to an Ineq: -* -* ```text -* a >= b ~> b <= a + 0 ~> ineq(b,a,0) -* ``` -*/ +/// Converts a Geq to an Ineq +/// +/// ```text +/// x >= y ~> y <= x + 0 ~> ineq(y,x,0) +/// ``` #[register_rule(("Minion", 4100))] fn geq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Geq(metadata, a, b) => Ok(Reduction::pure(Ineq( - metadata.clone_dirty(), - b.clone(), - a.clone(), - Box::new(Atomic(Metadata::new(), Literal(Int(0)))), - ))), - _ => Err(RuleNotApplicable), - } + let Expr::Geq(meta, e1, e2) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, x) = *e1 else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, y) = *e2 else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::FlatIneq( + meta.clone_dirty(), + y, + x, + Lit::Int(0), + ))) } -/** -* Convert a Leq to an Ineq: -* -* ```text -* a <= b ~> a <= b + 0 ~> ineq(a,b,0) -* ``` -*/ +/// Converts a Leq to an Ineq +/// +/// ```text +/// x <= y ~> x <= y + 0 ~> ineq(x,y,0) +/// ``` #[register_rule(("Minion", 4100))] fn leq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { - match expr { - Leq(metadata, a, b) => Ok(Reduction::pure(Ineq( - metadata.clone_dirty(), - a.clone(), - b.clone(), - Box::new(Atomic(Metadata::new(), Literal(Int(0)))), - ))), - _ => Err(RuleNotApplicable), - } + let Expr::Leq(meta, e1, e2) = expr.clone() else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, x) = *e1 else { + return Err(RuleNotApplicable); + }; + + let Expr::Atomic(_, y) = *e2 else { + return Err(RuleNotApplicable); + }; + + Ok(Reduction::pure(Expr::FlatIneq( + meta.clone_dirty(), + x, + y, + Lit::Int(0), + ))) } +// TODO: add this rule for geq + /// ```text /// x <= y + k ~> ineq(x,y,k) /// ``` - #[register_rule(("Minion",4400))] fn x_leq_y_plus_k_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { - let Leq(_, x, b) = expr else { + let Expr::Leq(meta, e1, e2) = expr.clone() else { return Err(RuleNotApplicable); }; - let x @ Atomic(_, Reference(_)) = *x.to_owned() else { + let Expr::Atomic(_, x) = *e1 else { return Err(RuleNotApplicable); }; - let Sum(_, c) = *b.to_owned() else { + let Expr::Sum(_, sum_exprs) = *e2 else { return Err(RuleNotApplicable); }; - let [ref y @ Atomic(_, Reference(_)), ref k @ Atomic(_, Literal(_))] = c[..] else { + let [Expr::Atomic(_, y), Expr::Atomic(_, Atom::Literal(k))] = sum_exprs.as_slice() else { return Err(RuleNotApplicable); }; - Ok(Reduction::pure(Ineq( - expr.get_meta().clone_dirty(), - Box::new(x), - Box::new(y.clone()), - Box::new(k.clone()), + Ok(Reduction::pure(Expr::FlatIneq( + meta.clone_dirty(), + x, + y.clone(), + k.clone(), ))) } -// #[register_rule(("Minion", 99))] -// fn eq_to_leq_geq(expr: &Expr, _: &Model) -> ApplicationResult { -// match expr { -// Eq(metadata, a, b) => { -// return Ok(Reduction::pure(Expr::And( -// metadata.clone(), -// vec![ -// Expr::Leq(metadata.clone(), a.clone(), b.clone()), -// Expr::Geq(metadata.clone(), a.clone(), b.clone()), -// ], -// ))); -// } -// _ => Err(RuleNotApplicable), -// } -// } - /// Flattening rule for not(bool_lit) /// /// For some boolean variable x: @@ -647,16 +633,16 @@ fn x_leq_y_plus_k_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult { fn not_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult { use Domain::BoolDomain; match expr { - Not(m, expr) => { - if let Atomic(_, Reference(name)) = (**expr).clone() { + Expr::Not(m, expr) => { + if let Expr::Atomic(_, Atom::Reference(name)) = (**expr).clone() { if mdl .get_domain(&name) .is_some_and(|x| matches!(x, BoolDomain)) { - return Ok(Reduction::pure(WatchedLiteral( + return Ok(Reduction::pure(Expr::FlatWatchedLiteral( m.clone_dirty(), name.clone(), - Bool(false), + Lit::Bool(false), ))); } } @@ -677,11 +663,11 @@ fn not_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult { #[register_rule(("Minion", 4090))] fn not_constraint_to_reify(expr: &Expr, _: &Model) -> ApplicationResult { - if !matches!(expr, Not(_,c) if !matches!(**c, Atomic(_,_))) { + if !matches!(expr, Expr::Not(_,c) if !matches!(**c, Expr::Atomic(_,_))) { return Err(RuleNotApplicable); } - let Not(m, e) = expr else { + let Expr::Not(m, e) = expr else { unreachable!(); }; @@ -691,9 +677,9 @@ fn not_constraint_to_reify(expr: &Expr, _: &Model) -> ApplicationResult { } }; - Ok(Reduction::pure(Reify( + Ok(Reduction::pure(Expr::MinionReify( m.clone(), e.clone(), - Box::new(Atomic(Metadata::new(), Literal(Bool(false)))), + Atom::Literal(Lit::Bool(false)), ))) } diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs index fb7ba33676..9e5ab7b80a 100644 --- a/crates/conjure_core/src/rules/partial_eval.rs +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -194,78 +194,6 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { 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 Expr::Atomic(_, Atom::Literal(Int(x))) = expr { - n_consts += 1; - acc += x; - } else { - new_vec.push(expr); - } - } - - if let Expr::Atomic(_, Atom::Literal(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(Expr::Atomic( - Default::default(), - Atom::Literal(Int(x - acc)), - )), - ))); - } - } else if acc != 0 { - new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(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 Expr::Atomic(_, Atom::Literal(Int(x))) = expr { - n_consts += 1; - acc += x; - } else { - new_vec.push(expr); - } - } - - if let Expr::Atomic(_, Atom::Literal(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(Expr::Atomic( - Default::default(), - Atom::Literal(Int(x - acc)), - )), - ))); - } - } else if acc != 0 { - new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Int(acc)))); - } - - if n_consts <= 1 { - Err(RuleNotApplicable) - } else { - Ok(Reduction::pure(SumLeq(m, new_vec, leq))) - } - } - DivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable), - Ineq(_, _, _, _) => Err(RuleNotApplicable), AllDiff(m, vec) => { let mut consts: HashSet = HashSet::new(); @@ -282,13 +210,20 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { Err(RuleNotApplicable) } Neg(_, _) => Err(RuleNotApplicable), - WatchedLiteral(_, _, _) => Err(RuleNotApplicable), - Reify(_, _, _) => Err(RuleNotApplicable), AuxDeclaration(_, _, _) => Err(RuleNotApplicable), UnsafeMod(_, _, _) => Err(RuleNotApplicable), SafeMod(_, _, _) => Err(RuleNotApplicable), - ModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable), Minus(_, _, _) => Err(RuleNotApplicable), - MinusEq(_, _, _) => Err(RuleNotApplicable), + + // As these are in a low level solver form, I'm assuming that these have already been + // simplified and partially evaluated. + FlatIneq(_, _, _, _) => Err(RuleNotApplicable), + FlatMinusEq(_, _, _) => Err(RuleNotApplicable), + FlatSumLeq(_, _, _) => Err(RuleNotApplicable), + FlatSumGeq(_, _, _) => Err(RuleNotApplicable), + FlatWatchedLiteral(_, _, _) => Err(RuleNotApplicable), + MinionDivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable), + MinionModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable), + MinionReify(_, _, _) => Err(RuleNotApplicable), } } diff --git a/crates/conjure_core/src/rules/utils.rs b/crates/conjure_core/src/rules/utils.rs index d70808469c..773d78e3a4 100644 --- a/crates/conjure_core/src/rules/utils.rs +++ b/crates/conjure_core/src/rules/utils.rs @@ -36,6 +36,23 @@ pub fn is_all_constant(expression: &Expr) -> bool { true } +/// Converts a vector of expressions to a vector of atoms. +/// +/// # Returns +/// +/// `Some(Vec)` if the vectors direct children expressions are all atomic, otherwise `None`. +pub fn expressions_to_atoms(exprs: &Vec) -> Option> { + let mut atoms: Vec = vec![]; + for expr in exprs { + let Expr::Atomic(_, atom) = expr else { + return None; + }; + atoms.push(atom.clone()); + } + + Some(atoms) +} + /// Creates a new auxiliary variable using the given expression. /// /// # Returns diff --git a/crates/conjure_core/src/solver/adaptors/minion.rs b/crates/conjure_core/src/solver/adaptors/minion.rs deleted file mode 100644 index 6488b239d0..0000000000 --- a/crates/conjure_core/src/solver/adaptors/minion.rs +++ /dev/null @@ -1,430 +0,0 @@ -use std::collections::HashMap; -use std::sync::{Mutex, OnceLock}; - -use regex::Regex; - -use minion_ast::Model as MinionModel; -use minion_rs::ast as minion_ast; -use minion_rs::error::MinionError; -use minion_rs::{get_from_table, run_minion}; - -use crate::ast as conjure_ast; -use crate::solver::SolverCallback; -use crate::solver::SolverFamily; -use crate::solver::SolverMutCallback; -use crate::stats::SolverStats; -use crate::Model as ConjureModel; - -use super::super::model_modifier::NotModifiable; -use super::super::private; -use super::super::SearchComplete::*; -use super::super::SearchIncomplete::*; -use super::super::SearchStatus::*; -use super::super::SolveSuccess; -use super::super::SolverAdaptor; -use super::super::SolverError; -use super::super::SolverError::*; - -/// A [SolverAdaptor] for interacting with Minion. -/// -/// This adaptor uses the `minion_rs` crate to talk to Minion over FFI. -pub struct Minion { - __non_constructable: private::Internal, - model: Option, -} - -static MINION_LOCK: Mutex<()> = Mutex::new(()); -static USER_CALLBACK: OnceLock> = OnceLock::new(); -static ANY_SOLUTIONS: Mutex = Mutex::new(false); -static USER_TERMINATED: Mutex = Mutex::new(false); - -#[allow(clippy::unwrap_used)] -fn minion_rs_callback(solutions: HashMap) -> bool { - *(ANY_SOLUTIONS.lock().unwrap()) = true; - let callback = USER_CALLBACK - .get_or_init(|| Mutex::new(Box::new(|x| true))) - .lock() - .unwrap(); - - let mut conjure_solutions: HashMap = HashMap::new(); - for (minion_name, minion_const) in solutions.into_iter() { - let conjure_const = match minion_const { - minion_ast::Constant::Bool(x) => conjure_ast::Literal::Bool(x), - minion_ast::Constant::Integer(x) => conjure_ast::Literal::Int(x), - _ => todo!(), - }; - - let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap(); - let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) { - conjure_ast::Name::MachineName(caps[1].parse::().unwrap()) - } else { - conjure_ast::Name::UserName(minion_name) - }; - - conjure_solutions.insert(conjure_name, conjure_const); - } - - let continue_search = (**callback)(conjure_solutions); - if !continue_search { - *(USER_TERMINATED.lock().unwrap()) = true; - } - - continue_search -} - -impl private::Sealed for Minion {} - -impl Minion { - pub fn new() -> Minion { - Minion { - __non_constructable: private::Internal, - model: None, - } - } -} - -impl Default for Minion { - fn default() -> Self { - Minion::new() - } -} - -impl SolverAdaptor for Minion { - #[allow(clippy::unwrap_used)] - fn solve( - &mut self, - callback: SolverCallback, - _: private::Internal, - ) -> Result { - // our minion callback is global state, so single threading the adaptor as a whole is - // probably a good move... - #[allow(clippy::unwrap_used)] - let mut minion_lock = MINION_LOCK.lock().unwrap(); - - #[allow(clippy::unwrap_used)] - let mut user_callback = USER_CALLBACK - .get_or_init(|| Mutex::new(Box::new(|x| true))) - .lock() - .unwrap(); - *user_callback = callback; - drop(user_callback); // release mutex. REQUIRED so that run_minion can use the - // user callback and not deadlock. - - run_minion( - self.model.clone().expect("STATE MACHINE ERR"), - minion_rs_callback, - ) - .map_err(|err| match err { - MinionError::RuntimeError(x) => Runtime(format!("{:#?}", x)), - MinionError::Other(x) => Runtime(format!("{:#?}", x)), - MinionError::NotImplemented(x) => RuntimeNotImplemented(x), - x => Runtime(format!("unknown minion_rs error: {:#?}", x)), - })?; - - let mut status = Complete(HasSolutions); - if *(USER_TERMINATED.lock()).unwrap() { - status = Incomplete(UserTerminated); - } else if *(ANY_SOLUTIONS.lock()).unwrap() { - status = Complete(NoSolutions); - } - Ok(SolveSuccess { - stats: get_solver_stats(), - status, - }) - } - - fn solve_mut( - &mut self, - callback: SolverMutCallback, - _: private::Internal, - ) -> Result { - Err(OpNotImplemented("solve_mut".into())) - } - - fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> { - let mut minion_model = MinionModel::new(); - parse_vars(&model, &mut minion_model)?; - parse_exprs(&model, &mut minion_model)?; - self.model = Some(minion_model); - Ok(()) - } - - fn get_family(&self) -> SolverFamily { - SolverFamily::Minion - } - - fn get_name(&self) -> Option { - Some("Minion".to_owned()) - } -} - -fn parse_vars( - conjure_model: &ConjureModel, - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - // TODO (niklasdewally): remove unused vars? - // TODO (niklasdewally): ensure all vars references are used. - - for (name, variable) in conjure_model.variables.iter() { - parse_var(name, variable, minion_model)?; - } - Ok(()) -} - -fn parse_var( - name: &conjure_ast::Name, - var: &conjure_ast::DecisionVariable, - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - match &var.domain { - conjure_ast::Domain::IntDomain(ranges) => _parse_intdomain_var(name, ranges, minion_model), - conjure_ast::Domain::BoolDomain => _parse_booldomain_var(name, minion_model), - x => Err(ModelFeatureNotSupported(format!("{:?}", x))), - } -} - -fn _parse_intdomain_var( - name: &conjure_ast::Name, - ranges: &[conjure_ast::Range], - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - let str_name = _name_to_string(name.to_owned()); - - if ranges.len() != 1 { - return Err(ModelFeatureNotImplemented(format!( - "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.", - str_name, - ranges.len() - ))); - } - - let range = ranges.first().ok_or(ModelInvalid(format!( - "variable {:?} has no range", - str_name - )))?; - - let (low, high) = match range { - conjure_ast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())), - conjure_ast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())), - #[allow(unreachable_patterns)] - x => Err(ModelFeatureNotSupported(format!("{:?}", x))), - }?; - - _try_add_var( - str_name.to_owned(), - minion_ast::VarDomain::Bound(low, high), - minion_model, - ) -} - -fn _parse_booldomain_var( - name: &conjure_ast::Name, - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - let str_name = _name_to_string(name.to_owned()); - _try_add_var( - str_name.to_owned(), - minion_ast::VarDomain::Bool, - minion_model, - ) -} - -fn _try_add_var( - name: minion_ast::VarName, - domain: minion_ast::VarDomain, - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - minion_model - .named_variables - .add_var(name.clone(), domain) - .ok_or(ModelInvalid(format!( - "variable {:?} is defined twice", - name - ))) -} - -fn parse_exprs( - conjure_model: &ConjureModel, - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - for expr in conjure_model.get_constraints_vec().iter() { - // 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::Atom; - use conjure_ast::Expression as Expr; - use conjure_ast::Literal::*; - - match expr { - // top level false - Expr::Atomic(_, Atom::Literal(Bool(false))) => { - minion_model.constraints.push(minion_ast::Constraint::False); - } - // top level true - Expr::Atomic(_, Atom::Literal(Bool(true))) => { - minion_model.constraints.push(minion_ast::Constraint::True); - } - - _ => { - parse_expr(expr.to_owned(), minion_model)?; - } - } - } - Ok(()) -} - -fn parse_expr( - expr: conjure_ast::Expression, - minion_model: &mut MinionModel, -) -> Result<(), SolverError> { - minion_model.constraints.push(read_expr(expr)?); - Ok(()) -} - -fn read_expr(expr: conjure_ast::Expression) -> Result { - match expr { - conjure_ast::Expression::Atomic(_metadata, reff) => Ok(minion_ast::Constraint::WLiteral( - read_var(reff.into())?, - minion_ast::Constant::Integer(1), - )), - conjure_ast::Expression::SumLeq(_metadata, lhs, rhs) => Ok(minion_ast::Constraint::SumLeq( - read_vars(lhs)?, - read_var(*rhs)?, - )), - conjure_ast::Expression::SumGeq(_metadata, lhs, rhs) => Ok(minion_ast::Constraint::SumGeq( - read_vars(lhs)?, - read_var(*rhs)?, - )), - conjure_ast::Expression::Ineq(_metadata, a, b, c) => Ok(minion_ast::Constraint::Ineq( - read_var(*a)?, - read_var(*b)?, - minion_ast::Constant::Integer(read_const(*c)?), - )), - conjure_ast::Expression::Neq(_metadata, a, b) => { - Ok(minion_ast::Constraint::DisEq(read_var(*a)?, read_var(*b)?)) - } - conjure_ast::Expression::DivEqUndefZero(_metadata, a, b, c) => { - Ok(minion_ast::Constraint::DivUndefZero( - (read_var(a.into())?, read_var(b.into())?), - read_var(c.into())?, - )) - } - conjure_ast::Expression::ModuloEqUndefZero(_metadata, a, b, c) => { - Ok(minion_ast::Constraint::ModuloUndefZero( - (read_var(a.into())?, read_var(b.into())?), - read_var(c.into())?, - )) - } - conjure_ast::Expression::Or(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedOr( - exprs - .iter() - .map(|x| read_expr(x.to_owned())) - .collect::, SolverError>>()?, - )), - conjure_ast::Expression::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)?, - )), - - conjure_ast::Expression::AuxDeclaration(_metadata, name, expr) => { - Ok(minion_ast::Constraint::Eq( - read_var(conjure_ast::Expression::Atomic( - _metadata, - conjure_ast::Atom::Reference(name), - ))?, - read_var(*expr)?, - )) - } - - conjure_ast::Expression::MinusEq(_metadata, a, b) => Ok(minion_ast::Constraint::MinusEq( - read_var(conjure_ast::Expression::Atomic(_metadata.clone(), a))?, - read_var(conjure_ast::Expression::Atomic(_metadata, b))?, - )), - x => Err(ModelFeatureNotSupported(format!("{:?}", x))), - } -} -fn read_vars(exprs: Vec) -> Result, SolverError> { - let mut minion_vars: Vec = vec![]; - for expr in exprs { - let minion_var = read_var(expr)?; - minion_vars.push(minion_var); - } - Ok(minion_vars) -} - -fn read_var(e: conjure_ast::Expression) -> Result { - // a minion var is either a reference or a "var as const" - match _read_ref(e.clone()) { - Ok(name) => Ok(minion_ast::Var::NameRef(name)), - Err(_) => match read_const(e) { - Ok(n) => Ok(minion_ast::Var::ConstantAsVar(n)), - Err(x) => Err(x), - }, - } -} - -fn _read_ref(e: conjure_ast::Expression) -> Result { - let name = match e { - conjure_ast::Expression::Atomic(_metadata, conjure_ast::Atom::Reference(n)) => Ok(n), - x => Err(ModelInvalid(format!( - "expected a reference, but got `{0:?}`", - x - ))), - }?; - - let str_name = _name_to_string(name); - Ok(str_name) -} - -fn read_const(e: conjure_ast::Expression) -> Result { - match e { - conjure_ast::Expression::Atomic(_, conjure_ast::Atom::Literal(x)) => Ok(read_const_1(x)?), - x => Err(ModelInvalid(format!( - "expected a constant, but got `{0:?}`", - x - ))), - } -} - -fn read_const_1(k: conjure_ast::Literal) -> Result { - match k { - conjure_ast::Literal::Int(n) => Ok(n), - conjure_ast::Literal::Bool(true) => Ok(1), - conjure_ast::Literal::Bool(false) => Ok(0), - x => Err(ModelInvalid(format!( - "expected a constant, but got `{0:?}`", - x - ))), - } -} - -fn _name_to_string(name: conjure_ast::Name) -> String { - match name { - conjure_ast::Name::UserName(x) => x, - conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x), - } -} - -#[allow(clippy::unwrap_used)] -fn get_solver_stats() -> SolverStats { - SolverStats { - nodes: get_from_table("Nodes".into()).map(|x| x.parse::().unwrap()), - ..Default::default() - } -} diff --git a/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs b/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs new file mode 100644 index 0000000000..d39c1d9320 --- /dev/null +++ b/crates/conjure_core/src/solver/adaptors/minion/adaptor.rs @@ -0,0 +1,165 @@ +use regex::Regex; +use std::collections::HashMap; +use std::sync::{Mutex, OnceLock}; + +use minion_ast::Model as MinionModel; +use minion_rs::ast as minion_ast; +use minion_rs::error::MinionError; +use minion_rs::{get_from_table, run_minion}; + +use crate::ast as conjure_ast; +use crate::solver::SolverCallback; +use crate::solver::SolverFamily; +use crate::solver::SolverMutCallback; +use crate::stats::SolverStats; +use crate::Model as ConjureModel; + +use crate::solver::model_modifier::NotModifiable; +use crate::solver::private; +use crate::solver::SearchComplete::*; +use crate::solver::SearchIncomplete::*; +use crate::solver::SearchStatus::*; +use crate::solver::SolveSuccess; +use crate::solver::SolverAdaptor; +use crate::solver::SolverError; +use crate::solver::SolverError::*; + +use super::parse_model::model_to_minion; + +/// A [SolverAdaptor] for interacting with Minion. +/// +/// This adaptor uses the `minion_rs` crate to talk to Minion over FFI. +pub struct Minion { + __non_constructable: private::Internal, + model: Option, +} + +static MINION_LOCK: Mutex<()> = Mutex::new(()); +static USER_CALLBACK: OnceLock> = OnceLock::new(); +static ANY_SOLUTIONS: Mutex = Mutex::new(false); +static USER_TERMINATED: Mutex = Mutex::new(false); + +#[allow(clippy::unwrap_used)] +fn minion_rs_callback(solutions: HashMap) -> bool { + *(ANY_SOLUTIONS.lock().unwrap()) = true; + let callback = USER_CALLBACK + .get_or_init(|| Mutex::new(Box::new(|x| true))) + .lock() + .unwrap(); + + let mut conjure_solutions: HashMap = HashMap::new(); + for (minion_name, minion_const) in solutions.into_iter() { + let conjure_const = match minion_const { + minion_ast::Constant::Bool(x) => conjure_ast::Literal::Bool(x), + minion_ast::Constant::Integer(x) => conjure_ast::Literal::Int(x), + _ => todo!(), + }; + + let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap(); + let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) { + conjure_ast::Name::MachineName(caps[1].parse::().unwrap()) + } else { + conjure_ast::Name::UserName(minion_name) + }; + + conjure_solutions.insert(conjure_name, conjure_const); + } + + let continue_search = (**callback)(conjure_solutions); + if !continue_search { + *(USER_TERMINATED.lock().unwrap()) = true; + } + + continue_search +} + +impl private::Sealed for Minion {} + +impl Minion { + pub fn new() -> Minion { + Minion { + __non_constructable: private::Internal, + model: None, + } + } +} + +impl Default for Minion { + fn default() -> Self { + Minion::new() + } +} + +impl SolverAdaptor for Minion { + #[allow(clippy::unwrap_used)] + fn solve( + &mut self, + callback: SolverCallback, + _: private::Internal, + ) -> Result { + // our minion callback is global state, so single threading the adaptor as a whole is + // probably a good move... + #[allow(clippy::unwrap_used)] + let mut minion_lock = MINION_LOCK.lock().unwrap(); + + #[allow(clippy::unwrap_used)] + let mut user_callback = USER_CALLBACK + .get_or_init(|| Mutex::new(Box::new(|x| true))) + .lock() + .unwrap(); + *user_callback = callback; + drop(user_callback); // release mutex. REQUIRED so that run_minion can use the + // user callback and not deadlock. + + run_minion( + self.model.clone().expect("STATE MACHINE ERR"), + minion_rs_callback, + ) + .map_err(|err| match err { + MinionError::RuntimeError(x) => Runtime(format!("{:#?}", x)), + MinionError::Other(x) => Runtime(format!("{:#?}", x)), + MinionError::NotImplemented(x) => RuntimeNotImplemented(x), + x => Runtime(format!("unknown minion_rs error: {:#?}", x)), + })?; + + let mut status = Complete(HasSolutions); + if *(USER_TERMINATED.lock()).unwrap() { + status = Incomplete(UserTerminated); + } else if *(ANY_SOLUTIONS.lock()).unwrap() { + status = Complete(NoSolutions); + } + Ok(SolveSuccess { + stats: get_solver_stats(), + status, + }) + } + + fn solve_mut( + &mut self, + callback: SolverMutCallback, + _: private::Internal, + ) -> Result { + Err(OpNotImplemented("solve_mut".into())) + } + + fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> { + self.model = Some(model_to_minion(model)?); + Ok(()) + } + + fn get_family(&self) -> SolverFamily { + SolverFamily::Minion + } + + fn get_name(&self) -> Option { + Some("Minion".to_owned()) + } +} + +#[allow(clippy::unwrap_used)] +fn get_solver_stats() -> SolverStats { + SolverStats { + nodes: get_from_table("Nodes".into()).map(|x| x.parse::().unwrap()), + ..Default::default() + } +} diff --git a/crates/conjure_core/src/solver/adaptors/minion/mod.rs b/crates/conjure_core/src/solver/adaptors/minion/mod.rs new file mode 100644 index 0000000000..fbb5a9fa51 --- /dev/null +++ b/crates/conjure_core/src/solver/adaptors/minion/mod.rs @@ -0,0 +1,5 @@ +/// Minion solver adaptor +mod adaptor; +mod parse_model; + +pub use adaptor::Minion; diff --git a/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs b/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs new file mode 100644 index 0000000000..58065ef2f8 --- /dev/null +++ b/crates/conjure_core/src/solver/adaptors/minion/parse_model.rs @@ -0,0 +1,271 @@ +//! Parse / `load_model` step of running Minion. + +use minion_ast::Model as MinionModel; +use minion_rs::ast as minion_ast; +use minion_rs::error::MinionError; +use minion_rs::{get_from_table, run_minion}; + +use crate::ast as conjure_ast; +use crate::solver::SolverError::*; +use crate::solver::SolverFamily; +use crate::solver::SolverMutCallback; +use crate::solver::{SolverCallback, SolverError}; +use crate::stats::SolverStats; +use crate::Model as ConjureModel; + +/// Converts a conjure-oxide model to a `minion_rs` model. +pub fn model_to_minion(model: ConjureModel) -> Result { + let mut minion_model = MinionModel::new(); + load_symbol_table(&model, &mut minion_model)?; + load_constraints(&model, &mut minion_model)?; + Ok(minion_model) +} + +/// Loads the symbol table into `minion_model`. +fn load_symbol_table( + conjure_model: &ConjureModel, + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + for (name, variable) in conjure_model.variables.iter() { + load_var(name, variable, minion_model)?; + } + Ok(()) +} + +/// Loads a single variable into `minion_model` +fn load_var( + name: &conjure_ast::Name, + var: &conjure_ast::DecisionVariable, + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + match &var.domain { + conjure_ast::Domain::IntDomain(ranges) => load_intdomain_var(name, ranges, minion_model), + conjure_ast::Domain::BoolDomain => load_booldomain_var(name, minion_model), + x => Err(ModelFeatureNotSupported(format!("{:?}", x))), + } +} + +/// Loads a variable with domain IntDomain into `minion_model` +fn load_intdomain_var( + name: &conjure_ast::Name, + ranges: &[conjure_ast::Range], + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + let str_name = name_to_string(name.to_owned()); + + if ranges.len() != 1 { + return Err(ModelFeatureNotImplemented(format!( + "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.", + str_name, + ranges.len() + ))); + } + + let range = ranges.first().ok_or(ModelInvalid(format!( + "variable {:?} has no range", + str_name + )))?; + + let (low, high) = match range { + conjure_ast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())), + conjure_ast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())), + #[allow(unreachable_patterns)] + x => Err(ModelFeatureNotSupported(format!("{:?}", x))), + }?; + + _try_add_var( + str_name.to_owned(), + minion_ast::VarDomain::Bound(low, high), + minion_model, + ) +} + +/// Loads a variable with domain BoolDomain into `minion_model` +fn load_booldomain_var( + name: &conjure_ast::Name, + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + let str_name = name_to_string(name.to_owned()); + _try_add_var( + str_name.to_owned(), + minion_ast::VarDomain::Bool, + minion_model, + ) +} + +fn _try_add_var( + name: minion_ast::VarName, + domain: minion_ast::VarDomain, + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + minion_model + .named_variables + .add_var(name.clone(), domain) + .ok_or(ModelInvalid(format!( + "variable {:?} is defined twice", + name + ))) +} + +fn name_to_string(name: conjure_ast::Name) -> String { + match name { + conjure_ast::Name::UserName(x) => x, + conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x), + } +} + +/// Loads the constraints into `minion_model`. +fn load_constraints( + conjure_model: &ConjureModel, + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + for expr in conjure_model.get_constraints_vec().iter() { + // 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::Atom; + use conjure_ast::Expression as Expr; + use conjure_ast::Literal::*; + + match expr { + // top level false + Expr::Atomic(_, Atom::Literal(Bool(false))) => { + minion_model.constraints.push(minion_ast::Constraint::False); + } + // top level true + Expr::Atomic(_, Atom::Literal(Bool(true))) => { + minion_model.constraints.push(minion_ast::Constraint::True); + } + + _ => { + load_expr(expr.to_owned(), minion_model)?; + } + } + } + Ok(()) +} + +/// Adds `expr` to `minion_model` +fn load_expr( + expr: conjure_ast::Expression, + minion_model: &mut MinionModel, +) -> Result<(), SolverError> { + minion_model.constraints.push(parse_expr(expr)?); + Ok(()) +} + +/// Parses a Conjure Oxide expression into a `minion_rs` constraint. +fn parse_expr(expr: conjure_ast::Expression) -> Result { + match expr { + conjure_ast::Expression::Atomic(_metadata, atom) => Ok(minion_ast::Constraint::WLiteral( + parse_atom(atom)?, + minion_ast::Constant::Integer(1), + )), + conjure_ast::Expression::FlatSumLeq(_metadata, lhs, rhs) => Ok( + minion_ast::Constraint::SumLeq(parse_atoms(lhs)?, parse_atom(rhs)?), + ), + conjure_ast::Expression::FlatSumGeq(_metadata, lhs, rhs) => Ok( + minion_ast::Constraint::SumGeq(parse_atoms(lhs)?, parse_atom(rhs)?), + ), + conjure_ast::Expression::FlatIneq(_metadata, a, b, c) => Ok(minion_ast::Constraint::Ineq( + parse_atom(a)?, + parse_atom(b)?, + parse_literal(c)?, + )), + conjure_ast::Expression::Neq(_metadata, a, b) => Ok(minion_ast::Constraint::DisEq( + parse_atomic_expr(*a)?, + parse_atomic_expr(*b)?, + )), + conjure_ast::Expression::MinionDivEqUndefZero(_metadata, a, b, c) => Ok( + minion_ast::Constraint::DivUndefZero((parse_atom(a)?, parse_atom(b)?), parse_atom(c)?), + ), + conjure_ast::Expression::MinionModuloEqUndefZero(_metadata, a, b, c) => { + Ok(minion_ast::Constraint::ModuloUndefZero( + (parse_atom(a)?, parse_atom(b)?), + parse_atom(c)?, + )) + } + conjure_ast::Expression::Or(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedOr( + exprs + .iter() + .map(|x| parse_expr(x.to_owned())) + .collect::, SolverError>>()?, + )), + conjure_ast::Expression::And(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedAnd( + exprs + .iter() + .map(|x| parse_expr(x.to_owned())) + .collect::, SolverError>>()?, + )), + conjure_ast::Expression::Eq(_metadata, a, b) => Ok(minion_ast::Constraint::Eq( + parse_atomic_expr(*a)?, + parse_atomic_expr(*b)?, + )), + + conjure_ast::Expression::FlatWatchedLiteral(_metadata, name, k) => Ok( + minion_ast::Constraint::WLiteral(parse_name(name)?, parse_literal(k)?), + ), + conjure_ast::Expression::MinionReify(_metadata, e, v) => Ok(minion_ast::Constraint::Reify( + Box::new(parse_expr(*e)?), + parse_atom(v)?, + )), + + conjure_ast::Expression::AuxDeclaration(_metadata, name, expr) => Ok( + minion_ast::Constraint::Eq(parse_name(name)?, parse_atomic_expr(*expr)?), + ), + + conjure_ast::Expression::FlatMinusEq(_metadata, a, b) => Ok( + minion_ast::Constraint::MinusEq(parse_atom(a)?, parse_atom(b)?), + ), + x => Err(ModelFeatureNotSupported(format!("{:?}", x))), + } +} + +fn parse_atomic_expr(expr: conjure_ast::Expression) -> Result { + let conjure_ast::Expression::Atomic(_, atom) = expr else { + return Err(ModelInvalid(format!( + "expected atomic expression, got {:?}", + expr + ))); + }; + + parse_atom(atom) +} + +fn parse_atoms(exprs: Vec) -> Result, SolverError> { + let mut minion_vars: Vec = vec![]; + for expr in exprs { + let minion_var = parse_atom(expr)?; + minion_vars.push(minion_var); + } + Ok(minion_vars) +} + +fn parse_atom(atom: conjure_ast::Atom) -> Result { + match atom { + conjure_ast::Atom::Literal(l) => { + Ok(minion_ast::Var::ConstantAsVar(parse_literal_as_int(l)?)) + } + conjure_ast::Atom::Reference(name) => Ok(parse_name(name))?, + } +} + +fn parse_literal_as_int(k: conjure_ast::Literal) -> Result { + match k { + conjure_ast::Literal::Int(n) => Ok(n), + conjure_ast::Literal::Bool(true) => Ok(1), + conjure_ast::Literal::Bool(false) => Ok(0), + x => Err(ModelInvalid(format!( + "expected a literal but got `{0:?}`", + x + ))), + } +} + +fn parse_literal(k: conjure_ast::Literal) -> Result { + Ok(minion_ast::Constant::Integer(parse_literal_as_int(k)?)) +} + +fn parse_name(name: conjure_ast::Name) -> Result { + Ok(minion_ast::Var::NameRef(name_to_string(name))) +} diff --git a/crates/conjure_core/src/solver/adaptors/mod.rs b/crates/conjure_core/src/solver/adaptors/mod.rs index 9311122ddf..e842edbaf0 100644 --- a/crates/conjure_core/src/solver/adaptors/mod.rs +++ b/crates/conjure_core/src/solver/adaptors/mod.rs @@ -1,11 +1,11 @@ //! Solver adaptors. +mod kissat; +mod minion; +mod sat_common; + #[doc(inline)] pub use kissat::Kissat; + #[doc(inline)] pub use minion::Minion; - -mod sat_common; - -mod kissat; -mod minion;