-
Notifications
You must be signed in to change notification settings - Fork 20
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
documentation bits for "letting domain" and --> (#609)
* 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
- Loading branch information
1 parent
2b810bb
commit 2ae9cd7
Showing
4 changed files
with
1,105 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,30 @@ | ||
# letting domain | ||
|
||
This is how you define a domain (an abstract collection of objects with the same type). Domain attributes add further specialise the domain. | ||
For more information about domains and using them in effectively in Esscence programs see [here]( | ||
https://modref.github.io/papers/ModRef2021_ReformulatingEssenceRobustness.pdf). | ||
|
||
This is used like : | ||
```essence | ||
letting x be domain int(1..10) | ||
``` | ||
Types of domains: | ||
|
||
[boolean](https://github.com/conjure-cp/conjure/blob/main/docs/bits/type/L_bool.md) | ||
[integer](...) | ||
[enumerated](...) | ||
[unnamed](...) | ||
[tuple](...) | ||
[record](...) | ||
[variant](...) | ||
[matrix](...) | ||
[set](...) | ||
[multi-set](...) | ||
[function](https://github.com/conjure-cp/conjure/blob/main/docs/bits/type/function.md) | ||
[sequence](...) | ||
[relation](...) | ||
[partition](...) | ||
|
||
|
||
For more information about different domain types see [here](https://conjure.readthedocs.io/en/latest/essence.html). | ||
To see how to define these types as domains see [here](https://github.com/conjure-cp/conjure/blob/main/docs/notebooks/letting_domain.ipynb). |
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,10 @@ | ||
# --> (long arrow) | ||
|
||
The ```-->``` is used to define [function domains](https://github.com/conjure-cp/conjure/blob/main/docs/bits/type/function.md). | ||
Like: | ||
```essence | ||
letting letters be new type enum {A, B, C} | ||
find f: function letters --> int (1..3) | ||
``` | ||
|
||
This is further demonstrated [here](https://github.com/conjure-cp/conjure/blob/main/docs/notebooks/functionDemonstration.ipynb). |
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,220 @@ | ||
{ | ||
"cells": [ | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": {}, | ||
"source": [ | ||
"<a href=\"https://colab.research.google.com/github/conjure-cp/conjure/blob/main/docs/notebooks/addition_and_subtraction_examples.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>" | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": {}, | ||
"source": [ | ||
"## Addition and Subtraction" | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": 1, | ||
"metadata": { | ||
"colab": { | ||
"base_uri": "https://localhost:8080/", | ||
"height": 138 | ||
}, | ||
"id": "LXXtCG_TAc82", | ||
"outputId": "7bcad187-8e0b-41df-a33b-775268c81aa8" | ||
}, | ||
"outputs": [ | ||
{ | ||
"name": "stdout", | ||
"output_type": "stream", | ||
"text": [ | ||
"Installing Conjure version v2.5.0 and Conjure Notebook version v0.0.8...\n", | ||
"Downloading...\n", | ||
"Conjure: The Automated Constraint Modelling Tool\n", | ||
"Release version 2.5.0\n", | ||
"Repository version 41536c055 (2023-05-18 14:03:02 +0100)\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.8/scripts/install-colab.sh)\n", | ||
"%load_ext conjure" | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": { | ||
"id": "bh5XxFmsIksp" | ||
}, | ||
"source": [ | ||
"The + operator works exactly as you'd expect. Although, this only works for integer domains." | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": { | ||
"id": "f5KPXa-vgU8p" | ||
}, | ||
"source": [ | ||
"For example, the cell below finds all the pairs of numbers between -10 and 10 that sum to 5" | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": 2, | ||
"metadata": { | ||
"colab": { | ||
"base_uri": "https://localhost:8080/", | ||
"height": 54 | ||
}, | ||
"id": "Nz4eS1PDfaLm", | ||
"outputId": "48b4ca56-cc2f-4537-a84e-2ebd57532d29" | ||
}, | ||
"outputs": [ | ||
{ | ||
"data": { | ||
"text/markdown": [ | ||
"```json\n", | ||
"{\"conjure_solutions\": [{\"x\": -5, \"y\": 10}, {\"x\": -4, \"y\": 9}, {\"x\": -3, \"y\": 8}, {\"x\": -2, \"y\": 7}, {\"x\": -1, \"y\": 6}, {\"x\": 0, \"y\": 5}, {\"x\": 1, \"y\": 4}, {\"x\": 2, \"y\": 3}, {\"x\": 3, \"y\": 2}, {\"x\": 4, \"y\": 1}, {\"x\": 5, \"y\": 0}, {\"x\": 6, \"y\": -1}, {\"x\": 7, \"y\": -2}, {\"x\": 8, \"y\": -3}, {\"x\": 9, \"y\": -4}, {\"x\": 10, \"y\": -5}]}\n", | ||
"```" | ||
], | ||
"text/plain": [ | ||
"<IPython.core.display.Markdown object>" | ||
] | ||
}, | ||
"metadata": {}, | ||
"output_type": "display_data" | ||
} | ||
], | ||
"source": [ | ||
"%%conjure --number-of-solutions=all\n", | ||
"find x, y: int(-10..10) such that x + y = 5" | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": { | ||
"id": "5zc4fmBOI5sE" | ||
}, | ||
"source": [ | ||
"Similarly, subtraction works as you would expect for integers." | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": { | ||
"id": "nUbpKg1IJE2l" | ||
}, | ||
"source": [ | ||
"For example, the cell below finds all the pairs of numbers between -10 and 10 that subtract to 5" | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": 3, | ||
"metadata": { | ||
"colab": { | ||
"base_uri": "https://localhost:8080/", | ||
"height": 54 | ||
}, | ||
"id": "HBPe3V4wJMEL", | ||
"outputId": "e43a7556-250d-4616-95bc-83c107113cc2" | ||
}, | ||
"outputs": [ | ||
{ | ||
"data": { | ||
"text/markdown": [ | ||
"```json\n", | ||
"{\"conjure_solutions\": [{\"x\": -5, \"y\": -10}, {\"x\": -4, \"y\": -9}, {\"x\": -3, \"y\": -8}, {\"x\": -2, \"y\": -7}, {\"x\": -1, \"y\": -6}, {\"x\": 0, \"y\": -5}, {\"x\": 1, \"y\": -4}, {\"x\": 2, \"y\": -3}, {\"x\": 3, \"y\": -2}, {\"x\": 4, \"y\": -1}, {\"x\": 5, \"y\": 0}, {\"x\": 6, \"y\": 1}, {\"x\": 7, \"y\": 2}, {\"x\": 8, \"y\": 3}, {\"x\": 9, \"y\": 4}, {\"x\": 10, \"y\": 5}]}\n", | ||
"```" | ||
], | ||
"text/plain": [ | ||
"<IPython.core.display.Markdown object>" | ||
] | ||
}, | ||
"metadata": {}, | ||
"output_type": "display_data" | ||
} | ||
], | ||
"source": [ | ||
"%%conjure --number-of-solutions=all\n", | ||
"find x, y: int(-10..10) such that x - y = 5" | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": { | ||
"id": "3-bZgsPaOB0l" | ||
}, | ||
"source": [ | ||
"The minus operator can also negate values." | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": 4, | ||
"metadata": { | ||
"colab": { | ||
"base_uri": "https://localhost:8080/", | ||
"height": 54 | ||
}, | ||
"id": "1cgUQNRVOFJq", | ||
"outputId": "48dd5c96-ed6e-4aad-8425-d2e1dd381047" | ||
}, | ||
"outputs": [ | ||
{ | ||
"data": { | ||
"text/markdown": [ | ||
"```json\n", | ||
"{\"conjure_solutions\": [{\"x\": -5, \"y\": 5}, {\"x\": -4, \"y\": 4}, {\"x\": -3, \"y\": 3}, {\"x\": -2, \"y\": 2}, {\"x\": -1, \"y\": 1}, {\"x\": 0, \"y\": 0}, {\"x\": 1, \"y\": -1}, {\"x\": 2, \"y\": -2}, {\"x\": 3, \"y\": -3}, {\"x\": 4, \"y\": -4}, {\"x\": 5, \"y\": -5}]}\n", | ||
"```" | ||
], | ||
"text/plain": [ | ||
"<IPython.core.display.Markdown object>" | ||
] | ||
}, | ||
"metadata": {}, | ||
"output_type": "display_data" | ||
} | ||
], | ||
"source": [ | ||
"%%conjure --number-of-solutions=all\n", | ||
"find x, y: int(-5..5) such that x = -y" | ||
] | ||
} | ||
], | ||
"metadata": { | ||
"colab": { | ||
"provenance": [] | ||
}, | ||
"kernelspec": { | ||
"display_name": "Python 3", | ||
"name": "python3" | ||
}, | ||
"language_info": { | ||
"name": "python" | ||
} | ||
}, | ||
"nbformat": 4, | ||
"nbformat_minor": 0 | ||
} |
Oops, something went wrong.