{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "cbf02367",
   "metadata": {},
   "source": [
    "# Constraint *AllEqual*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e0b77149",
   "metadata": {},
   "source": [
    "The constraint *AllEqual* enforces that the elements (typically, variables) from a specified list take the same value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4b649543",
   "metadata": {},
   "source": [
    "It is mainly introduced for its ease of use."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b5961963",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *AllEqual*. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "95224efb",
   "metadata": {},
   "source": [
    "## Case 1: *AllEqual* on Variables"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0b21fb9f",
   "metadata": {},
   "source": [
    "The first case is when all variables from a specified list must take the same value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b242f2d9",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "82783b72",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e67fc220",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 4 variables, each one with  {0,1,2}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "1f46b595",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7d490510",
   "metadata": {},
   "source": [
    "We can display (the structure of) the array as well as the domain of the first variable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "eb99b6ed",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3]]\n",
      "Domain of any variable:  0..2\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3a7fe491",
   "metadata": {},
   "source": [
    "We simply post a single constraint *AllEqual* on $x$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "ccc41093",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    AllEqual(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c559d1d8",
   "metadata": {},
   "source": [
    "By calling the function solve(), we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also print the values assigned to the variables in the found solution; we can call the function *values()* that collects the values assigned (in the last found solution) to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "e95346c8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e14fd25c",
   "metadata": {},
   "source": [
    "We can enumerate all solutions (supports) for this contraint by calling *solve()* with the named parameter *sols*. Note how the named parameter *sol* of *values()* is used to indicate the index of a solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "fb1e918c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 0]\n",
      "Solution 2: [1, 1, 1, 1]\n",
      "Solution 3: [2, 2, 2, 2]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "81a3e2a1",
   "metadata": {},
   "source": [
    "## Case 2: *AllEqual* on Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1f4e5115",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "6585e153",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bfe38c48",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "bbce7470",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "372771ce",
   "metadata": {},
   "source": [
    "We post a single constraint *AllEqual* on expressions involving the variables of $x$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "87045735",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    AllEqual(abs(x[0]-x[1]), abs(x[1]-x[2]), abs(x[2]-x[3]))\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1d7f0b25",
   "metadata": {},
   "source": [
    "Interestingly, we can display the internal representation of the posted constraint; although a little bit technical, we can see that the information is correctly recorded. Note that dist(a,b) is equivalent to abs(a-b)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "c647094c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allEqual(list:[dist(x[0],x[1]), dist(x[1],x[2]), dist(x[2],x[3])])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4dce9734",
   "metadata": {},
   "source": [
    "We can run the solver"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "879c20b1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "raw",
   "id": "9ade0afd",
   "metadata": {},
   "source": [
    "By enumerating the solutions, one can observe that the three expressions are always all equal."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "8053207d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 0]\n",
      "Solution 2: [0, 1, 0, 1]\n",
      "Solution 3: [0, 1, 2, 1]\n",
      "Solution 4: [0, 2, 0, 2]\n",
      "Solution 5: [2, 0, 2, 0]\n",
      "Solution 6: [2, 2, 2, 2]\n",
      "Solution 7: [1, 1, 1, 1]\n",
      "Solution 8: [2, 1, 0, 1]\n",
      "Solution 9: [2, 1, 2, 1]\n",
      "Solution 10: [1, 0, 1, 0]\n",
      "Solution 11: [1, 2, 1, 0]\n",
      "Solution 12: [1, 2, 1, 2]\n",
      "Solution 13: [1, 0, 1, 2]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}