diff --git a/tests/custom/issues/395/1.essence b/tests/custom/issues/395/1.essence index 489f47d1d4..1f8365f887 100644 --- a/tests/custom/issues/395/1.essence +++ b/tests/custom/issues/395/1.essence @@ -1,5 +1,5 @@ given m : int(1..) find Cs : sequence (size m) of int(0..m) -find Cz : sequence (size m) of int(0..m) such that - Cz subsequence Cs + exists Cz : sequence (size m) of int(0..m) . + Cz subsequence Cs diff --git a/tests/custom/issues/395/run.sh b/tests/custom/issues/395/run.sh index db2d708e52..a5f0edf666 100755 --- a/tests/custom/issues/395/run.sh +++ b/tests/custom/issues/395/run.sh @@ -4,7 +4,7 @@ conjure modelling 1.essence ; head -n30 conjure-output/model000001.eprime conjure modelling 2.essence ; head -n30 conjure-output/model000001.eprime conjure modelling 3.essence ; head -n30 conjure-output/model000001.eprime -conjure solve 1.essence m_is_3.param ; cat *.solution ; rm -f *.solution +# conjure solve 1.essence m_is_3.param ; cat *.solution ; rm -f *.solution # conjure solve 2.essence m_is_3.param ; cat *.solution ; rm -f *.solution conjure solve 3.essence m_is_3.param ; cat *.solution ; rm -f *.solution diff --git a/tests/custom/issues/395/stdout.expected b/tests/custom/issues/395/stdout.expected index f869c73339..915250d68f 100644 --- a/tests/custom/issues/395/stdout.expected +++ b/tests/custom/issues/395/stdout.expected @@ -3,31 +3,31 @@ language ESSENCE' 1.0 given m: int(1..) find Cs_ExplicitBounded_Length: int(m) find Cs_ExplicitBounded_Values: matrix indexed by [int(1..m)] of int(0..m) -find Cz_ExplicitBounded_Length: int(m) -find Cz_ExplicitBounded_Values: matrix indexed by [int(1..m)] of int(0..m) -find conjure_aux1_ExplicitBounded_Length: int(m) -find conjure_aux1_ExplicitBounded_Values: matrix indexed by [int(1..m)] of int(1..m) -branching on - [Cs_ExplicitBounded_Length, Cs_ExplicitBounded_Values, Cz_ExplicitBounded_Length, Cz_ExplicitBounded_Values] +find conjure_aux1_ExplicitBounded_Length: + matrix indexed by [int(m), matrix indexed by [int(1..m)] of int(0..m)] of int(m) +find conjure_aux1_ExplicitBounded_Values: + matrix indexed by [int(m), matrix indexed by [int(1..m)] of int(0..m), int(1..m)] of int(1..m) +branching on [Cs_ExplicitBounded_Length, Cs_ExplicitBounded_Values] such that - and([and([conjure_aux1_ExplicitBounded_Values[q3 - 1] < conjure_aux1_ExplicitBounded_Values[q3], q3 - 1 <= m, - q3 <= m; - int(1..3)]) - | q3 : int(2..m), q3 <= m]), - and([and([Cz_ExplicitBounded_Values[q5] = Cs_ExplicitBounded_Values[conjure_aux1_ExplicitBounded_Values[q5]], - q5 <= m, conjure_aux1_ExplicitBounded_Values[q5] <= m /\ q5 <= m; - int(1..3)]) - | q5 : int(1..m), q5 <= m]) + and([and([conjure_aux1_ExplicitBounded_Values[q3 - 1] < conjure_aux1_ExplicitBounded_Values[q3] /\ q3 <= m /\ + q3 - 1 <= m + | q3 : int(2..m), q3 <= m]) + | Cz_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]), + and([true | Cz_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]), + or([and([Cz_ExplicitBounded_Values[q5] = Cs_ExplicitBounded_Values[conjure_aux1_ExplicitBounded_Values[q5]] /\ + q5 <= m + /\ (conjure_aux1_ExplicitBounded_Values[q5] <= m /\ q5 <= m) + | q5 : int(1..m), q5 <= m]) + | Cz_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]) $ Conjure's -$ {"finds": [{"Name": "Cs"}, {"Name": "Cz"}], +$ {"finds": [{"Name": "Cs"}], $ "givens": [{"Name": "m"}], $ "enumGivens": [], $ "enumLettings": [], $ "lettings": [], $ "unnameds": [], $ "strategyQ": {"PickFirst": []}, -$ "strategyA": {"Auto": {"Interactive": []}}, language ESSENCE' 1.0 given m: int(1..) @@ -88,21 +88,12 @@ $ "lettings": [], $ "unnameds": [], $ "strategyQ": {"PickFirst": []}, $ "strategyA": {"Auto": {"Interactive": []}}, -Generating models for 1.essence +Generating models for 3.essence Generated models: model000001.eprime Saved under: conjure-output Savile Row: model000001.eprime m_is_3.param Running minion for domain filtering. Running solver: minion -Copying solution to: 1-m_is_3.solution -language Essence 1.3 - -letting Cs be sequence(0, 0, 0) -letting Cz be sequence(0, 0, 0) -Using cached models. -Savile Row: model000001.eprime m_is_3.param -Running minion for domain filtering. -Running solver: minion Copying solution to: 3-m_is_3.solution language Essence 1.3