Skip to content

Commit

Permalink
Matrix domains (#612)
Browse files Browse the repository at this point in the history 
* write start of L_Plus.md

* Plus and Minus docs and its notebook

* wrote doc pages for all the operators.

* fix to meet agreed format

* Created using Colaboratory

* add multiplicationDemonstration.ipynb

* add absoluteValues.ipynb

* add factorial.ipynb

* add toInt_demonstration.ipynb

* fixed absoluteValues.ipynb

* added notebook links

* fixed L_Minus.md typo

* add long_arrow.md

* improved these notebooks with hz66-404 suggestions

* fixed typo

* add letting_domain file

* added letting_domain notebook

* completed letting_domain

* added notebook link to md page

* added matrix.md

* add matrix notebook
  • Loading branch information
@N-J-Martin
N-J-Martin committed Nov 15, 2023
1 parent 53464a7 commit 591458b
Show file tree
Hide file tree
Showing 3 changed files with 368 additions and 1 deletion.
2 changes: 1 addition & 1 deletion docs/bits/keyword/letting_domain.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Types of domains:
[tuple](...)
[record](...)
[variant](...)
[matrix](...)
[matrix](https://github.com/conjure-cp/conjure/blob/main/docs/bits/type/matrix.md)
[set](...)
[multi-set](...)
[function](https://github.com/conjure-cp/conjure/blob/main/docs/bits/type/function.md)
Expand Down
17 changes: 17 additions & 0 deletions docs/bits/type/matrix.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# matrix

Takes a list of (integer, boolean or enumerated) domains for its indices and a domain for the entries.

Defined by
``` matrix indexed by [COMMA SEPARATED DOMAIN LIST] of [DOMAIN]```
as demonstrated [here](https://github.com/conjure-cp/conjure/blob/main/docs/notebooks/letting_domain.ipynb).

or by explicity defining values in square brackets like
``` letting M be [0,1]```
The domain used to index the elements may be specifed too, such that.
```[0,1]``` is the same as ```[0,1; int(1..2)]``` but different from ```[0,1; int(0..1)]```

They are not ordered, but can be compared using equality operators.
Two matrices are only equal if their indices are the same.

Read more about matrix domains [here](https://conjure.readthedocs.io/en/latest/essence.html#types).
350 changes: 350 additions & 0 deletions docs/notebooks/matrix.ipynb
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,350 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<a href=\"https://colab.research.google.com/github/conjure-cp/conjure/blob/main/docs/notebooks/matrix.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "zOKoIulU1Doz"
},
"source": [
"## Matrix Domains"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 156
},
"id": "TgBvtR2h1SHE",
"outputId": "b108e1e6-5992-4828-96ef-0dfd292f0333"
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Installing Conjure version v2.5.1 and Conjure Notebook version v0.0.9...\n",
"Conjure is already installed.\n",
"Conjure notebook is already installed.\n",
"Conjure: The Automated Constraint Modelling Tool\n",
"Release version 2.5.1\n",
"Repository version a9cbc2e (2023-11-07 23:44:00 +0000)\n"
]
},
{
"data": {
"application/javascript": "\"use strict\";\n\nCodeMirror.defineMode(\"text/conjure\", function (config) {\n\n var isOperatorChar = /[+\\-*=<>%^\\/]/;\n\n var keywords = {\n \"forall\": true,\n \"allDifferent\": true,\n \"allDiff\": true,\n \"alldifferent_except\": true,\n \"dim\": true,\n \"toSet\": true,\n \"toMSet\": true,\n \"toRelation\": true,\n \"maximising\": true,\n \"minimising\": true,\n \"forAll\": true,\n \"exists\": true,\n \"toInt\": true,\n \"sum\": true,\n \"be\": true,\n \"bijective\": true,\n \"bool\": true,\n \"by\": true,\n \"complete\": true,\n \"defined\": true,\n \"domain\": true,\n \"in\": true,\n \"or\": true,\n \"and\": true,\n \"false\": true,\n \"find\": true,\n \"from\": true,\n \"function\": true,\n \"given\": true,\n \"image\": true,\n \"indexed\": true,\n \"injective\": true,\n \"int\": true,\n \"intersect\": true,\n \"freq\": true,\n \"lambda\": true,\n \"language\": true,\n \"letting\": true,\n \"matrix\": true,\n \"maxNumParts\": true,\n \"maxOccur\": true,\n \"maxPartSize\": true,\n \"maxSize\": true,\n \"minNumParts\": true,\n \"minOccur\": true,\n \"minPartSize\": true,\n \"minSize\": true,\n \"mset\": true,\n \"numParts\": true,\n \"of\": true,\n \"partial\": true,\n \"partition\": true,\n \"partSize\": true,\n \"preImage\": true,\n \"quantifier\": true,\n \"range\": true,\n \"regular\": true,\n \"relation\": true,\n \"representation\": true,\n \"set\": true,\n \"size\": true,\n \"subset\": true,\n \"subsetEq\": true,\n \"such\": true,\n \"supset\": true,\n \"supsetEq\": true,\n \"surjective\": true,\n \"that\": true,\n \"together\": true,\n \"enum\": true,\n \"total\": true,\n \"true\": true,\n \"new\": true,\n \"type\": true,\n \"tuple\": true,\n \"union\": true,\n \"where\": true,\n \"branching\": true,\n \"on\": true\n }; \n var punc = \":;,.(){}[]\";\n\n function tokenBase(stream, state) {\n var ch = stream.next();\n if (ch == '\"') {\n state.tokenize.push(tokenString);\n return tokenString(stream, state);\n }\n if (/[\\d\\.]/.test(ch)) {\n if (ch == \".\") {\n stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n } else if (ch == \"0\") {\n stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n } else {\n stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n }\n return \"number\";\n }\n if (ch == \"/\") {\n if (stream.eat(\"*\")) {\n state.tokenize.push(tokenComment);\n return tokenComment(stream, state);\n }\n }\n if (ch == \"$\") {\n stream.skipToEnd();\n return \"comment\";\n }\n if (isOperatorChar.test(ch)) {\n stream.eatWhile(isOperatorChar);\n return \"operator\";\n }\n if (punc.indexOf(ch) > -1) {\n return \"punctuation\";\n }\n stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n var cur = stream.current();\n \n if (keywords.propertyIsEnumerable(cur)) {\n return \"keyword\";\n }\n return \"variable\";\n }\n\n function tokenComment(stream, state) {\n var maybeEnd = false, ch;\n while (ch = stream.next()) {\n if (ch == \"/\" && maybeEnd) {\n state.tokenize.pop();\n break;\n }\n maybeEnd = (ch == \"*\");\n }\n return \"comment\";\n }\n\n function tokenUntilClosingParen() {\n var depth = 0;\n return function (stream, state, prev) {\n var inner = tokenBase(stream, state, prev);\n console.log(\"untilClosing\", inner, stream.current());\n if (inner == \"punctuation\") {\n if (stream.current() == \"(\") {\n ++depth;\n } else if (stream.current() == \")\") {\n if (depth == 0) {\n stream.backUp(1)\n state.tokenize.pop()\n return state.tokenize[state.tokenize.length - 1](stream, state)\n } else {\n --depth;\n }\n }\n }\n return inner;\n }\n }\n\n function tokenString(stream, state) {\n var escaped = false, next, end = false;\n while ((next = stream.next()) != null) {\n if (next == '(' && escaped) {\n state.tokenize.push(tokenUntilClosingParen());\n return \"string\";\n }\n if (next == '\"' && !escaped) { end = true; break; }\n escaped = !escaped && next == \"\\\\\";\n }\n if (end || !escaped)\n state.tokenize.pop();\n return \"string\";\n }\n\n return {\n startState: function (basecolumn) {\n return {\n tokenize: []\n };\n },\n\n token: function (stream, state) {\n if (stream.eatSpace()) return null;\n var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n console.log(\"token\", style);\n return style;\n },\n\n blockCommentStart: \"/*\",\n blockCommentEnd: \"*/\",\n lineComment: \"$\"\n };\n});\n\n\nCodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n\nrequire(['notebook/js/codecell'], function (codecell) {\n codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n Jupyter.notebook.get_cells().map(function (cell) {\n if (cell.cell_type == 'code') { cell.auto_highlight(); }\n });\n });\n});\n\n",
"text/plain": [
"<IPython.core.display.Javascript object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Conjure extension is loaded.\n",
"For usage help run: %conjure_help\n"
]
}
],
"source": [
"!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.9/scripts/install-colab.sh)\n",
"%load_ext conjure"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "nullPyun2_XH"
},
"source": [
"A matrix domain can be defined using letting notation. Entries can be of any domain, but can only be indexed by"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "G4tJgPv33OG2"
},
"source": [
"integer domains:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 34
},
"id": "8fvCAXoS1kwe",
"outputId": "8cfac03e-5706-456b-be5f-374e9459e817"
},
"outputs": [
{
"data": {
"text/markdown": [
"```json\n",
"{}\n",
"```"
],
"text/plain": [
"<IPython.core.display.Markdown object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"%%conjure\n",
"letting x be domain matrix indexed by [int] of int"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "VxftYeLD3QGj"
},
"source": [
"boolean domains:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 34
},
"id": "RCMWODKO2N59",
"outputId": "95a48db1-3424-42da-a180-97fd2d045d2e"
},
"outputs": [
{
"data": {
"text/markdown": [
"```json\n",
"{}\n",
"```"
],
"text/plain": [
"<IPython.core.display.Markdown object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"%%conjure\n",
"letting x be domain matrix indexed by [bool] of int"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "-HuukCTg3Swr"
},
"source": [
"enumerated domains:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 34
},
"id": "IzkO-M172Zll",
"outputId": "ff6a6ca8-c158-45b5-a24b-847c9c9aba2d"
},
"outputs": [
{
"data": {
"text/markdown": [
"```json\n",
"{}\n",
"```"
],
"text/plain": [
"<IPython.core.display.Markdown object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"%%conjure\n",
"letting y be new type enum {a, b, c}\n",
"letting x be domain matrix indexed by [y] of int"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "EdAM73Gk3Z0s"
},
"source": [
"Matrices can also be defined explicitly:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 34
},
"id": "soVvma8w3cHW",
"outputId": "bbce58da-9e91-4654-d57f-8799618ed4ed"
},
"outputs": [
{
"data": {
"text/markdown": [
"```json\n",
"{}\n",
"```"
],
"text/plain": [
"<IPython.core.display.Markdown object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"%%conjure\n",
"letting x be [0,1]"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "r1jxu3SG3hd7"
},
"source": [
"You can also specify the index domains."
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "1wiyLMe1Ns2M"
},
"source": [
"Note, however that ```[0,1]``` is the same as ```[0,1; int(1..2)]```,"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 34
},
"id": "wZWm3QpR3sfu",
"outputId": "fd6d5ab1-ccbf-449e-81d1-51584b3390ca"
},
"outputs": [
{
"data": {
"text/markdown": [
"```json\n",
"{\"z\": true}\n",
"```"
],
"text/plain": [
"<IPython.core.display.Markdown object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"%%conjure+ --solver=minion --number-of-solutions=all\n",
"letting y be [0,1; int(1..2)]\n",
"find z: bool such that z = (x = y)\n"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "MNqARB9vN4L1"
},
"source": [
"but not the same as ```[0,1; int(0..1)]```"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {
"colab": {
"base_uri": "https://localhost:8080/",
"height": 34
},
"id": "acUJyKwI48F1",
"outputId": "8c4922ae-40b7-4314-b622-ebd4c3de8ffc"
},
"outputs": [
{
"data": {
"text/markdown": [
"```json\n",
"{\"z\": false}\n",
"```"
],
"text/plain": [
"<IPython.core.display.Markdown object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"%%conjure --solver=minion --number-of-solutions=all\n",
"letting x be [0,1]\n",
"letting y be [0,1; int(0..1)]\n",
"find z:bool such that z = (x = y)\n"
]
}
],
"metadata": {
"colab": {
"provenance": []
},
"kernelspec": {
"display_name": "Python 3",
"name": "python3"
},
"language_info": {
"name": "python"
}
},
"nbformat": 4,
"nbformat_minor": 0
}

0 comments on commit 591458b

Please sign in to comment.