diff --git a/tests/custom/issues/395/1.essence b/tests/custom/issues/395/1.essence new file mode 100644 index 0000000000..489f47d1d4 --- /dev/null +++ b/tests/custom/issues/395/1.essence @@ -0,0 +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 diff --git a/tests/custom/issues/395/2.essence b/tests/custom/issues/395/2.essence new file mode 100644 index 0000000000..5bb92517ff --- /dev/null +++ b/tests/custom/issues/395/2.essence @@ -0,0 +1,5 @@ +given m : int(1..) +find Cz : sequence (size m) of int(0..m) +such that + exists Cs : sequence (size m) of int(0..m) . + Cz subsequence Cs diff --git a/tests/custom/issues/395/3.essence b/tests/custom/issues/395/3.essence new file mode 100644 index 0000000000..489f47d1d4 --- /dev/null +++ b/tests/custom/issues/395/3.essence @@ -0,0 +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 diff --git a/tests/custom/issues/395/run.sh b/tests/custom/issues/395/run.sh new file mode 100755 index 0000000000..d8ed8277eb --- /dev/null +++ b/tests/custom/issues/395/run.sh @@ -0,0 +1,5 @@ +rm -rf conjure-output +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 +rm -rf conjure-output diff --git a/tests/custom/issues/395/stdout.expected b/tests/custom/issues/395/stdout.expected new file mode 100644 index 0000000000..15590b4673 --- /dev/null +++ b/tests/custom/issues/395/stdout.expected @@ -0,0 +1,90 @@ +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] +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]) + +$ Conjure's +$ {"finds": [{"Name": "Cs"}, {"Name": "Cz"}], +$ "givens": [{"Name": "m"}], +$ "enumGivens": [], +$ "enumLettings": [], +$ "lettings": [], +$ "unnameds": [], +$ "strategyQ": {"PickFirst": []}, +$ "strategyA": {"Auto": {"Interactive": []}}, +language ESSENCE' 1.0 + +given m: int(1..) +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: + 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 [Cz_ExplicitBounded_Length, Cz_ExplicitBounded_Values] +such that + and([and([and([conjure_aux1_ExplicitBounded_Values[m, Cs_ExplicitBounded_Values, q3 - 1] < + conjure_aux1_ExplicitBounded_Values[m, Cs_ExplicitBounded_Values, q3], + q3 - 1 <= m, q3 <= m; + int(1..3)]) + | q3 : int(2..m), q3 <= m]) + | Cs_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]), + and([true | Cs_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]) + | Cs_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]) + +$ Conjure's +$ {"finds": [{"Name": "Cz"}], +$ "givens": [{"Name": "m"}], +$ "enumGivens": [], +$ "enumLettings": [], +$ "lettings": [], +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] +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]) + +$ Conjure's +$ {"finds": [{"Name": "Cs"}, {"Name": "Cz"}], +$ "givens": [{"Name": "m"}], +$ "enumGivens": [], +$ "enumLettings": [], +$ "lettings": [], +$ "unnameds": [], +$ "strategyQ": {"PickFirst": []}, +$ "strategyA": {"Auto": {"Interactive": []}},