-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
a6d00e0
commit 7f89369
Showing
5 changed files
with
110 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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": []}}, |