This repository has been archived by the owner on Apr 30, 2019. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
precompile examples rather than loading them from server every time
- Loading branch information
1 parent
617888f
commit e50e2c4
Showing
31 changed files
with
481 additions
and
99 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 |
---|---|---|
|
@@ -17,3 +17,4 @@ src/main/resources/build.properties | |
config.groovy | ||
.cache | ||
.groovy/ | ||
src/main/webapp/examples.js |
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
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,17 @@ | ||
/* Translation of example from page 82 of Abrial's B-Book */ | ||
p = {3|->5, 3|->9, 6|->3, 9|->2} & | ||
q = {2|->7, 3|->4, 5|->1, 9|->5} & | ||
u = {1,2,3} & | ||
s = {4,7,3} & | ||
t = {4,8,1} & | ||
|
||
/* and now some assertions about the above: */ | ||
p~ = {5|->3, 9|->3, 3|->6, 2|->9} & | ||
dom(p) = {3,6,9} & | ||
ran(p) = {5,9,3,2} & | ||
(p;q) = {3|->1, 3|->5, 6|->4, 9|->7} & | ||
id(u) = {1|->1, 2|->2, 3|->3} & | ||
s <|p = {3|->5, 3|->9} & | ||
p |> t = {} & | ||
s <<| p = {6|->3, 9|->2} & | ||
p |>> t = {3|->5, 3|->9, 6|->3, 9|->2} |
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,26 @@ | ||
/* Translation of example from page 83 of Abrial's B-Book */ | ||
p = {3|->5, 3|->9, 6|->3, 9|->2} & | ||
w = {1, 2, 3} & | ||
p[w] = {5,9} & | ||
q = {2|->7, 3|->4, 5|->1, 9|->5} & | ||
q <+ p = {3|->5, 3|->9, 6|->3, 9|->2, 2|->7, 5|->1} & | ||
f = {8|->10, 7|->11, 2|->11, 6|->12} & | ||
g = {1|->20, 7|->20, 2|->21, 1|->22} & | ||
f >< g = {(7|->(11|->20)), (2|->(11|->21))} & | ||
s = {1,4} & | ||
t = {2,3} & | ||
prj1(s,t) = {((1|->2)|->1),((1|->3)|->1),((4|->2)|->4),((4|->3)|->4)} & | ||
prj2(s,t) = {((1|->2)|->2),((1|->3)|->3),((4|->2)|->2),((4|->3)|->3)} & | ||
h = {1|->11, 4|->12} & | ||
k = {2|->21, 7|->22} & | ||
(h||k) = { (1,2) |-> (11,21), (1,7) |-> (11,22), | ||
(4,2) |-> (12,21), (4,7) |-> (12,22) } | ||
& | ||
/* and now some assertions about the above : */ | ||
p[w] = {5,9} & | ||
q <+ p = {(3|->5),(3|->9),(6|->3),(9|->2),(2|->7),(5|->1)} & | ||
f >< g = {(7|->(11|->20)), (2|->(11|->21))} & | ||
prj1(s,t) = {((1|->2)|->1),((1|->3)|->1),((4|->2)|->4),((4|->3)|->4)} & | ||
prj2(s,t) = {((1|->2)|->2),((1|->3)|->3),((4|->2)|->2),((4|->3)|->3)} & | ||
(h||k) = { (1,2) |-> (11,21), (1,7) |-> (11,22), | ||
(4,2) |-> (12,21), (4,7) |-> (12,22) } |
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,7 @@ | ||
n=7 & length = 25 & | ||
a:1..n --> 0..length & | ||
!i.(i:2..n => a(i-1) < a(i)) & | ||
!(i1,j1,i2,j2).(( i1>0 & i2>0 & j1<=n & j2 <= n & | ||
i1<j1 & i2<j2 & (i1,j1) /= (i2,j2) & | ||
i1<=i2 & (i1=i2 => j1<j2) | ||
) => (a(j1)-a(i1) /= a(j2)-a(i2))) |
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,8 @@ | ||
/* Colouring a graph with 40 vertexes and 200 edges */ | ||
Vertexes = 1..40 & | ||
maxnocol : 1..6 & /* possible number of colours */ | ||
colour: Vertexes --> 1..maxnocol & | ||
!(x,y).(x|->y : Edges => colour(x) /= colour(y)) & /* neighbours have different colour */ | ||
colour(1) = 1 /* fix the colour of vertex 1 */ | ||
& | ||
Edges = {13|->3, 26|->14, 19|->24, 2|->13, 1|->18, 10|->20, 15|->8, 9|->8, 4|->19, 7|->3, 23|->27, 9|->7, 23|->2, 29|->17, 35|->14, 8|->1, 27|->2, 9|->36, 34|->26, 7|->26, 34|->23, 14|->20, 39|->3, 7|->31, 5|->21, 23|->11, 35|->30, 6|->11, 9|->28, 18|->30, 19|->33, 25|->28, 39|->4, 2|->19, 9|->24, 8|->26, 10|->6, 22|->25, 32|->25, 23|->40, 30|->17, 2|->4, 5|->24, 27|->36, 20|->38, 31|->38, 35|->9, 19|->5, 8|->16, 18|->15, 35|->4, 19|->21, 15|->37, 34|->24, 6|->8, 8|->36, 2|->1, 23|->13, 13|->35, 36|->25, 26|->20, 32|->36, 24|->2, 9|->17, 38|->27, 18|->38, 36|->20, 34|->32, 8|->5, 5|->1, 28|->7, 33|->8, 5|->22, 31|->9, 30|->40, 26|->33, 32|->1, 6|->19, 14|->5, 8|->18, 40|->22, 4|->5, 5|->13, 34|->40, 12|->15, 25|->14, 3|->35, 10|->23, 18|->26, 31|->15, 13|->38, 13|->18, 20|->22, 18|->9, 11|->13, 40|->25, 40|->5, 28|->20, 37|->28, 3|->26, 38|->4, 3|->12, 5|->6, 30|->26, 32|->26, 7|->17, 31|->32, 22|->37, 38|->26, 3|->23, 34|->3, 6|->35, 34|->30, 23|->4, 23|->15, 10|->17, 12|->37, 40|->37, 28|->34, 38|->5, 16|->29, 5|->25, 21|->30, 37|->39, 32|->7, 7|->13, 15|->20, 39|->13, 26|->36, 18|->12, 4|->6, 21|->39, 21|->7, 29|->36, 11|->21, 20|->11, 22|->36, 24|->23, 38|->24, 4|->10, 20|->23, 38|->36, 16|->23, 12|->30, 17|->6, 29|->10, 10|->31, 7|->37, 40|->19, 27|->18, 12|->16, 6|->7, 8|->30, 25|->27, 38|->21, 27|->31, 4|->31, 5|->9, 23|->29, 35|->8, 11|->27, 17|->21, 26|->37, 3|->6, 5|->27, 9|->6, 26|->27, 5|->12, 14|->30, 35|->29, 10|->11, 38|->8, 36|->28, 1|->14, 31|->37, 13|->34, 26|->2, 12|->7, 34|->5, 3|->19, 15|->16, 20|->39, 19|->10, 12|->23, 6|->30, 11|->2, 25|->34, 24|->10, 40|->38, 24|->13, 35|->37, 37|->2, 33|->2, 31|->22, 15|->11, 22|->29, 9|->34, 34|->8, 17|->12, 1|->29} |
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,7 @@ | ||
n=9 & | ||
graph1 = {1|->3,2|->3, 3|->6, 4|->6,5|->6, 8|->9,9|->8, 6 |-> 6, 7|->7} & | ||
graph2 = {2|->5,3|->5, 4|->5, 6|->4,7|->4, 1|->9,9|->1, 5 |-> 5, 8|->8} & | ||
|
||
/* now try and find an isomporphism p : */ | ||
p: 1..n >->> 1..n & | ||
!i.(i:1..n => p[graph1[{i}]] = graph2[p[{i}]]) |
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,13 @@ | ||
/* | ||
Find a different digit (between 0 and 9) for each capital letter in the following equation: | ||
K I S S * K I S S = P A S S I O N | ||
(Found at http://www.cse.unsw.edu.au/~cs4418/2010/Lectures/ ) | ||
*/ | ||
K : 1..9 & P : 1..9 & | ||
I : 0..9 & S : 0..9 & A : 0..9 & | ||
O : 0..9 & N : 0..9 & | ||
|
||
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) | ||
= 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & | ||
|
||
card({K, I, S, P, A, O, N}) = 7 |
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,12 @@ | ||
/* A Puzzle from Smullyan: | ||
Knights: always tell the truth | ||
Knaves: always lie | ||
|
||
1: A says: “B is a knave or C is a knave” | ||
2: B says “A is a knight” | ||
|
||
What are A & B & C? | ||
Note: A,B,C are equal to TRUE if they are a Knight */ | ||
|
||
(A=TRUE <=> (B=FALSE or C=FALSE)) & | ||
(B=TRUE <=> A=TRUE) |
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,13 @@ | ||
/* A Puzzle from Smullyan: | ||
Knights: always tell the truth | ||
Knaves: always lie | ||
|
||
1: A says: “B is a knave or C is a knave” | ||
2: B says “A is a knight” | ||
|
||
What are A & B & C? | ||
Note: A,B,C are equal to TRUE if they are a Knight */ | ||
|
||
/* this computes the set of all models: */ | ||
{A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) & | ||
(B=TRUE <=> A=TRUE) } |
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,9 @@ | ||
/* define an infinite function cube and | ||
map it over a list using relational composition (;) | ||
and compute its image over the set 1..10 */ | ||
|
||
cube = %x.(x:INTEGER|x*x*x) & | ||
([1,2,3,4,5] ; cube) = list & | ||
cube[1..10] = image & | ||
|
||
cube(y) = 15625 /* and take the cubic root of a number */ |
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 @@ | ||
n = 8 & | ||
queens : 1..n >-> 1..n /* for each column the row in which the queen is in */ | ||
& | ||
!(q1,q2).(q1:1..n & q2:2..n & q2>q1 | ||
=> queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2)) |
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 @@ | ||
/* Find values for n which the n-Queens puzzle has 92 solutions */ | ||
card({queens| queens : 1..n >-> 1..n & | ||
!(q1,q2).(q1:1..n & q2:2..n & q2>q1 | ||
=> queens(q1)+(q2-q1) /= queens(q2) & | ||
queens(q1)+(q1-q2) /= queens(q2))}) = 92 & n:1..50 |
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,29 @@ | ||
ID={"A","B","C","D","E","F","G","H"} & | ||
next: ID <-> ID & | ||
number: ID --> 1..8 & | ||
!(x,y).(x|->y:next => (number(x)-number(y) >1 or number(y)-number(x) > 1)) & | ||
next = { "A"|->"B", "A"|->"C", "A"|->"D", "A"|->"E", | ||
"B"|->"D", "B"|->"E", "B"|->"F", | ||
"C"|->"D", "C"|->"G", | ||
"D"|->"E", "D"|->"G", "D"|->"H", | ||
"E"|->"F", "E"|->"G", "E"|->"H", | ||
"F"|->"H", | ||
"G"|->"H" } | ||
/* | ||
Assign the numbers 1..8 to vertices A..H in the graph below such that the values of connected vertices differ by more than one: | ||
|
||
A----B | ||
/|\ /|\ | ||
/ | \/ | \ | ||
/ | /\ | \ | ||
/ |/ \| \ | ||
C----D----E----F | ||
\ |\ /| / | ||
\ | \/ | / | ||
\ | /\ | / | ||
\|/ \|/ | ||
G----H | ||
|
||
From : http://www.g12.csse.unimelb.edu.au/wiki/doku.php?id=contrib:no_neighbours:wiki | ||
|
||
*/ |
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,4 @@ | ||
parity = %x.(x:NATURAL|x mod 2) & | ||
parity[1..10] = res & | ||
mapresult = ( [2,3,5,7] ; parity) | ||
|
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,13 @@ | ||
|
||
x >= 0 & x <= 100 & | ||
y >= 0 & y <= 100 & | ||
x * y - 37 * y + 71 * x - 2627 = 0 | ||
|
||
/* | ||
Source: http://pexforfun.com:80/default.aspx?language=CSharp&sample=NonLinearArithmetic | ||
// What values of x and y solve this equation? Ask Pex to find out! | ||
if (x >= 0 && x <= 100 && | ||
y >= 0 && y <= 100 && | ||
x * y - 37 * y + 71 * x - 2627 == 0) | ||
Console.WriteLine("equation solved"); | ||
*/ |
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,92 @@ | ||
/* a small SAT problem with 20 variables and 91 clauses */ | ||
( x10=FALSE or x16=FALSE or x5=TRUE ) & | ||
( x16=TRUE or x6=FALSE or x5=TRUE ) & | ||
( x17=FALSE or x14=FALSE or x18=FALSE ) & | ||
( x10=FALSE or x15=FALSE or x19=TRUE ) & | ||
( x1=FALSE or x9=FALSE or x18=FALSE ) & | ||
( x3=TRUE or x7=TRUE or x6=FALSE ) & | ||
( x13=FALSE or x1=TRUE or x6=TRUE ) & | ||
( x2=FALSE or x16=FALSE or x20=FALSE ) & | ||
( x7=TRUE or x8=TRUE or x18=TRUE ) & | ||
( x7=FALSE or x10=TRUE or x20=FALSE ) & | ||
( x2=TRUE or x14=FALSE or x17=FALSE ) & | ||
( x2=TRUE or x1=TRUE or x19=TRUE ) & | ||
( x7=TRUE or x20=FALSE or x1=FALSE ) & | ||
( x11=FALSE or x1=TRUE or x17=FALSE ) & | ||
( x3=TRUE or x12=FALSE or x19=TRUE ) & | ||
( x3=FALSE or x13=FALSE or x6=TRUE ) & | ||
( x13=FALSE or x3=TRUE or x12=FALSE ) & | ||
( x5=TRUE or x7=FALSE or x12=FALSE ) & | ||
( x20=TRUE or x8=TRUE or x16=FALSE ) & | ||
( x13=FALSE or x6=FALSE or x19=TRUE ) & | ||
( x5=FALSE or x1=TRUE or x14=TRUE ) & | ||
( x9=TRUE or x5=FALSE or x18=TRUE ) & | ||
( x12=FALSE or x17=FALSE or x1=FALSE ) & | ||
( x20=FALSE or x16=FALSE or x19=TRUE ) & | ||
( x12=TRUE or x10=TRUE or x11=FALSE ) & | ||
( x6=TRUE or x7=FALSE or x2=FALSE ) & | ||
( x13=TRUE or x10=FALSE or x17=TRUE ) & | ||
( x20=FALSE or x8=TRUE or x16=FALSE ) & | ||
( x10=FALSE or x1=FALSE or x8=FALSE ) & | ||
( x7=FALSE or x3=FALSE or x19=TRUE ) & | ||
( x19=TRUE or x1=FALSE or x6=FALSE ) & | ||
( x19=TRUE or x2=FALSE or x13=TRUE ) & | ||
( x2=FALSE or x20=TRUE or x9=FALSE ) & | ||
( x8=FALSE or x20=FALSE or x16=TRUE ) & | ||
( x13=FALSE or x1=FALSE or x11=TRUE ) & | ||
( x15=TRUE or x12=FALSE or x6=FALSE ) & | ||
( x17=FALSE or x19=FALSE or x9=TRUE ) & | ||
( x19=TRUE or x18=FALSE or x16=TRUE ) & | ||
( x7=TRUE or x8=FALSE or x19=FALSE ) & | ||
( x3=FALSE or x7=FALSE or x1=FALSE ) & | ||
( x7=TRUE or x17=FALSE or x16=FALSE ) & | ||
( x2=FALSE or x14=FALSE or x1=TRUE ) & | ||
( x18=FALSE or x10=FALSE or x8=FALSE ) & | ||
( x16=FALSE or x5=TRUE or x8=TRUE ) & | ||
( x4=TRUE or x8=TRUE or x10=TRUE ) & | ||
( x20=FALSE or x11=FALSE or x19=FALSE ) & | ||
( x8=TRUE or x16=FALSE or x6=FALSE ) & | ||
( x18=TRUE or x12=TRUE or x8=TRUE ) & | ||
( x5=FALSE or x20=FALSE or x10=FALSE ) & | ||
( x16=TRUE or x17=TRUE or x3=TRUE ) & | ||
( x7=TRUE or x1=FALSE or x17=FALSE ) & | ||
( x17=TRUE or x4=FALSE or x7=TRUE ) & | ||
( x20=TRUE or x9=FALSE or x13=FALSE ) & | ||
( x13=TRUE or x18=TRUE or x16=TRUE ) & | ||
( x16=FALSE or x6=FALSE or x5=TRUE ) & | ||
( x5=TRUE or x17=TRUE or x7=TRUE ) & | ||
( x12=FALSE or x17=FALSE or x6=FALSE ) & | ||
( x20=FALSE or x19=TRUE or x5=FALSE ) & | ||
( x9=TRUE or x19=FALSE or x16=TRUE ) & | ||
( x13=FALSE or x16=FALSE or x11=TRUE ) & | ||
( x4=FALSE or x19=FALSE or x18=FALSE ) & | ||
( x13=FALSE or x10=TRUE or x15=FALSE ) & | ||
( x16=TRUE or x7=FALSE or x14=FALSE ) & | ||
( x19=FALSE or x7=FALSE or x18=FALSE ) & | ||
( x20=FALSE or x5=TRUE or x13=TRUE ) & | ||
( x12=TRUE or x6=FALSE or x4=TRUE ) & | ||
( x7=TRUE or x9=TRUE or x13=FALSE ) & | ||
( x16=TRUE or x3=TRUE or x7=TRUE ) & | ||
( x9=TRUE or x1=FALSE or x12=TRUE ) & | ||
( x3=FALSE or x14=TRUE or x7=TRUE ) & | ||
( x1=TRUE or x15=TRUE or x14=TRUE ) & | ||
( x8=FALSE or x11=FALSE or x18=TRUE ) & | ||
( x19=TRUE or x9=FALSE or x7=TRUE ) & | ||
( x10=FALSE or x6=TRUE or x2=TRUE ) & | ||
( x14=TRUE or x18=TRUE or x11=FALSE ) & | ||
( x9=FALSE or x16=FALSE or x14=TRUE ) & | ||
( x1=TRUE or x11=TRUE or x20=FALSE ) & | ||
( x11=TRUE or x12=TRUE or x4=FALSE ) & | ||
( x13=TRUE or x11=FALSE or x14=FALSE ) & | ||
( x17=TRUE or x12=FALSE or x9=TRUE ) & | ||
( x14=TRUE or x9=TRUE or x1=TRUE ) & | ||
( x8=TRUE or x19=TRUE or x4=TRUE ) & | ||
( x6=TRUE or x13=FALSE or x20=FALSE ) & | ||
( x2=FALSE or x13=FALSE or x11=TRUE ) & | ||
( x14=TRUE or x13=FALSE or x17=TRUE ) & | ||
( x9=TRUE or x11=FALSE or x18=TRUE ) & | ||
( x13=FALSE or x6=FALSE or x5=TRUE ) & | ||
( x5=TRUE or x19=TRUE or x18=FALSE ) & | ||
( x4=FALSE or x10=TRUE or x11=TRUE ) & | ||
( x18=FALSE or x19=FALSE or x20=FALSE ) & | ||
( x3=TRUE or x9=FALSE or x8=TRUE ) |
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,9 @@ | ||
S : 1..9 & E : 0..9 & N : 0..9 & | ||
D : 0..9 & M : 1..9 & O : 0..9 & | ||
R : 0..9 & Y : 0..9 & | ||
S >0 & M >0 & | ||
card({S,E,N,D, M,O,R, Y}) = 8 & | ||
S*1000 + E*100 + N*10 + D + | ||
M*1000 + O*100 + R*10 + E = | ||
M*10000 + O*1000 + N*100 + E*10 + Y | ||
|
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,3 @@ | ||
sqrt>0 & sqrt*sqrt <= i & (sqrt+1)*(sqrt+1)>i | ||
/* specify the integer square root of i */ | ||
& i = 10000000 |
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,14 @@ | ||
coins = {16,17,23,24,39,40} & /* number of coins in each bag */ | ||
stolen : coins --> NATURAL & /* number of bags of each type stolen */ | ||
SIGMA(x).(x:coins|stolen(x)*x)=100 | ||
|
||
/* | ||
$ From Katta G. Murty: "Optimization Models for Decision Making", page 340 | ||
$ http://ioe.engin.umich.edu/people/fac/books/murty/opti_model/junior-7.pdf | ||
$ | ||
$ Example 7.8.1 | ||
$ A bank van had several bags of coins, each containing either | ||
$ 16, 17, 23, 24, 39, or 40 coins. While the van was parked on the | ||
$ street, thieves stole some bags. A total of 100 coins were lost. | ||
$ It is required to find how many bags were stolen. | ||
*/ |
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,26 @@ | ||
DOM = 1..9 & | ||
SUBSQ = { {1,2,3}, {4,5,6}, {7,8,9} } & | ||
Board : DOM --> (DOM --> DOM) & | ||
!y.(y:DOM => !(x1,x2).(x1:DOM & x1<x2 & x2:DOM => (Board(x1)(y) /= Board(x2)(y) & | ||
Board(y)(x1) /= Board(y)(x2)))) & | ||
!(s1,s2).(s1:SUBSQ & s2:SUBSQ => | ||
!(x1,y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & (x1=x2 => y1>y2) & | ||
y1:s2 & y2:s2 & (x1,y1) /= (x2,y2)) | ||
=> | ||
Board(x1)(y1) /= Board(x2)(y2) | ||
)) | ||
|
||
& /* PUZZLE CONSTRAINTS : */ | ||
|
||
Board(1)(1)=7 & Board(1)(2)=8 & Board(1)(3)=1 & Board(1)(4)=6 & Board(1)(6)=2 | ||
& Board(1)(7)=9 & Board(1)(9) = 5 & | ||
Board(2)(1)=9 & Board(2)(3)=2 & Board(2)(4)=7 & Board(2)(5)=1 & | ||
Board(3)(3)=6 & Board(3)(4)=8 & Board(3)(8)=1 & Board(3)(9)=2 & | ||
|
||
Board(4)(1)=2 & Board(4)(4)=3 & Board(4)(7)=8 & Board(4)(8)=5 & Board(4)(9)=1 & | ||
Board(5)(2)=7 & Board(5)(3)=3 & Board(5)(4)=5 & Board(5)(9)=4 & | ||
Board(6)(3)=8 & Board(6)(6)=9 & Board(6)(7)=3 & Board(6)(8)=6 & | ||
|
||
Board(7)(1)=1 & Board(7)(2)=9 & Board(7)(6)=7 & Board(7)(8)=8 & | ||
Board(8)(1)=8 & Board(8)(2)=6 & Board(8)(3)=7 & Board(8)(6)=3 & Board(8)(7)=4 & Board(8)(9)=9 & | ||
Board(9)(3)=5 & Board(9)(7)=1 |
Oops, something went wrong.