docs/notebooks/recordDomains.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "<a href=\"https://colab.research.google.com/github/conjure-cp/conjure/blob/main/docs/notebooks/recordDomains.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "zN7EuFmUa_8o"
      },
      "source": [
        "## Records"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 1,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 150
        },
        "id": "nBQDiwTSbPNq",
        "outputId": "1a867a29-11bd-4568-874a-a907419d15a7"
      },
      "outputs": [
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "Installing Conjure version v2.5.1 and Conjure Notebook version v0.0.10...\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"
        },
        {
          "data": {
            "text/markdown": [
              "Conjure extension is loaded - run `%conjure_help`"
            ],
            "text/plain": [
              "<IPython.core.display.Markdown object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        }
      ],
      "source": [
        "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.10/scripts/install-colab.sh)\n",
        "%load_ext conjure"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "KjakQ_XYbD5v"
      },
      "source": [
        "Basically, a list of key domain pairs. So can be defined as below, using name: domain pairs."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 2,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 317
        },
        "id": "aWIQxcWnbXcg",
        "outputId": "eef701bd-858a-411a-ddef-bdc85a2ae95b"
      },
      "outputs": [
        {
          "data": {
            "text/markdown": [
              "```json\n",
              "{}\n",
              "```"
            ],
            "text/plain": [
              "<IPython.core.display.Markdown object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/markdown": [
              "| Statistic | Value |\n",
              "|:-|-:|\n",
              "| SolverTotalTime | 0.000 |\n",
              "| SavileRowClauseOut | 0 |\n",
              "| SavileRowTotalTime | 0.142 |\n",
              "| SolverFailures | 0 |\n",
              "| SolverSatisfiable | 1 |\n",
              "| SavileRowTimeOut | 0 |\n",
              "| SolverTimeOut | 0 |\n",
              "| SolverNodes | 1 |\n"
            ],
            "text/plain": [
              "<IPython.core.display.Markdown object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        }
      ],
      "source": [
        "%%conjure\n",
        "letting s be record{}\n",
        "letting t be domain record{A : int(0..1), B : int(0..2)}\n",
        "\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "quTfnycvbo2_"
      },
      "source": [
        "Domains stored by record can be accessed using their label."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 3,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 427
        },
        "id": "AsWfFUUemjc5",
        "outputId": "257a9dab-aba0-4585-80cd-2d60f34b6f98"
      },
      "outputs": [
        {
          "data": {
            "text/markdown": [
              "## Solution 1"
            ],
            "text/plain": [
              "<IPython.core.display.Markdown object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/markdown": [
              "```json\n",
              "[{\"x\": {\"A\": 0, \"B\": 1}}, {\"x\": {\"A\": 1, \"B\": 1}}]\n",
              "```"
            ],
            "text/plain": [
              "<IPython.core.display.Markdown object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/markdown": [
              "| Statistic | Value |\n",
              "|:-|-:|\n",
              "| SolverTotalTime | 0.000307 |\n",
              "| SavileRowClauseOut | 0 |\n",
              "| SolverSolveTime | 6.1e-05 |\n",
              "| SavileRowTotalTime | 0.072 |\n",
              "| SolverSatisfiable | 1 |\n",
              "| SavileRowTimeOut | 0 |\n",
              "| SolverNodes | 3 |\n",
              "| SolverTimeOut | 0 |\n",
              "| SolverSolutionsFound | 2 |\n",
              "| SolverSetupTime | 5.2e-05 |\n"
            ],
            "text/plain": [
              "<IPython.core.display.Markdown object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        }
      ],
      "source": [
        "%%conjure+ --solver=minion --number-of-solutions=all\n",
        "find x:t such that x[B] = 1"
      ]
    }
  ],
  "metadata": {
    "colab": {
      "provenance": []
    },
    "kernelspec": {
      "display_name": "Python 3",
      "name": "python3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 0
}