Skip to content

Commit

Permalink
Fix copy/paste error in the regression test for #395
Browse files Browse the repository at this point in the history
  • Loading branch information
ozgurakgun committed Jun 29, 2019
1 parent 16c3e4b commit d8d81ee
Show file tree
Hide file tree
Showing 3 changed files with 20 additions and 29 deletions.
4 changes: 2 additions & 2 deletions tests/custom/issues/395/1.essence
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/custom/issues/395/run.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
43 changes: 17 additions & 26 deletions tests/custom/issues/395/stdout.expected
Original file line number Diff line number Diff line change
Expand Up @@ -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..)
Expand Down Expand Up @@ -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

Expand Down

0 comments on commit d8d81ee

Please sign in to comment.