From f2214d2a41357bc4962f1e369b4a8eae1b7f5c98 Mon Sep 17 00:00:00 2001 From: Chris Jefferson Date: Sat, 25 Feb 2023 11:45:40 +0800 Subject: [PATCH 1/3] Read solutions in the same order as conjure outputs them --- conjure/conjurehelper.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/conjure/conjurehelper.py b/conjure/conjurehelper.py index 03b8f04..dec251d 100644 --- a/conjure/conjurehelper.py +++ b/conjure/conjurehelper.py @@ -43,7 +43,7 @@ def read_solution_json_file(self) -> dict: solutions = [] try: if os.path.isdir('./conjure-output'): - files = os.listdir('./conjure-output') + files = sorted(os.listdir('./conjure-output')) for f in files: if f.endswith('.json'): with open('./conjure-output/' + f) as file: From cb466107137f3a273b25c2c6ca7712fb6d945635 Mon Sep 17 00:00:00 2001 From: Chris Jefferson Date: Thu, 23 Feb 2023 19:35:53 +0800 Subject: [PATCH 2/3] Handle solution counts differently * 0 solutions does not throw an exception * 'conjure_solutions' is always defined and always a list --- conjure/conjurehelper.py | 11 +- conjure/conjuremagics.py | 23 +++- test/numsols.ipynb | 243 +++++++++++++++++++++++++++++++++++++++ test/numsols.md | 125 ++++++++++++++++++++ 4 files changed, 388 insertions(+), 14 deletions(-) create mode 100644 test/numsols.ipynb create mode 100644 test/numsols.md diff --git a/conjure/conjurehelper.py b/conjure/conjurehelper.py index dec251d..0d09cda 100644 --- a/conjure/conjurehelper.py +++ b/conjure/conjurehelper.py @@ -2,6 +2,7 @@ import datetime import json from subprocess import Popen, PIPE +import uuid class ConjureHelper: @@ -39,7 +40,6 @@ def create_params_file(self, params={}) -> str: return self.create_temp_file("param.json", tempstr) def read_solution_json_file(self) -> dict: - solution_nums = 0 solutions = [] try: if os.path.isdir('./conjure-output'): @@ -48,15 +48,10 @@ def read_solution_json_file(self) -> dict: if f.endswith('.json'): with open('./conjure-output/' + f) as file: solutions.append(json.loads(file.read())) - solution_nums += 1 except: raise Exception('Error while reading json solution file(s).') - if solution_nums == 0: - raise Exception('No solution found for this Essence model.') - elif solution_nums == 1: - return solutions[0] - else: - return {"conjure_solutions": solutions} + + return {"conjure_solutions": solutions} def clean_tmp_files(self) -> None: # remove conjure-output-folder diff --git a/conjure/conjuremagics.py b/conjure/conjuremagics.py index 75dee2e..fbfa42b 100644 --- a/conjure/conjuremagics.py +++ b/conjure/conjuremagics.py @@ -66,15 +66,26 @@ def conjure(self, args, code): # assign results to notebook environment for key, value in resultdict.items(): self.shell.user_ns[key] = value + if len(resultdict['conjure_solutions']) == 1: + # assign results of single solution to notebook environment + for key, value in resultdict['conjure_solutions'][0].items(): + self.shell.user_ns[key] = value + if self.print_output == 'Yes': - return resultdict + if len(resultdict['conjure_solutions']) == 0: + return "No solution" + if len(resultdict['conjure_solutions']) == 1: + return resultdict['conjure_solutions'][0] + else: + return resultdict['conjure_solutions'] else: - # found multiple solutions - if len(resultdict.items()) == 1 and "conjure_solutions" in resultdict.keys(): - print("Done. Found %d solutions." % len(resultdict["conjure_solutions"])) + print("Done. Found %d solution(s)." % len(resultdict["conjure_solutions"])) + if len(resultdict['conjure_solutions']) == 1: + print("Variables have been assigned their value in the solution") + print("The solution is also stored in Python variable: conjure_solutions") + elif len(resultdict['conjure_solutions'] > 1): print("Solutions are stored in Python variable: conjure_solutions") - else: - print("Done.") + @line_magic def conjure_settings(self, line): diff --git a/test/numsols.ipynb b/test/numsols.ipynb new file mode 100644 index 0000000..4a8dc79 --- /dev/null +++ b/test/numsols.ipynb @@ -0,0 +1,243 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Conjure extension is loaded.\n", + "For usage help run: %conjure_help\n" + ] + } + ], + "source": [ + "%load_ext conjure\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "w = 7" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "'No solution'" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "%%conjure --number-of-solutions all --solver minion\n", + "\n", + "given w: int\n", + "find x : int(0..9)\n", + "such that\n", + " w = x /\\ (w != x)" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "\"x\" in locals()" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Conjure model cleared\n" + ] + } + ], + "source": [ + "%conjure_clear" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "[{'x': 8},\n", + " {'x': 2},\n", + " {'x': 0},\n", + " {'x': 3},\n", + " {'x': 5},\n", + " {'x': 6},\n", + " {'x': 9},\n", + " {'x': 4},\n", + " {'x': 1}]" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "%%conjure --number-of-solutions all --solver minion\n", + "\n", + "$ -O0 -S0 is to ensure solutions come out in lex order\n", + "given w: int\n", + "find x : int(0..9)\n", + "such that\n", + " w != x" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "\"x\" in locals()" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Conjure model cleared\n" + ] + } + ], + "source": [ + "%conjure_clear" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{'x': 1, 'y': 7}" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "%%conjure --number-of-solutions all --solver minion\n", + "given w: int\n", + "find x : int(0..9)\n", + "find y: int(5..12)\n", + "such that\n", + " x*y=w" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "True\n" + ] + } + ], + "source": [ + "print(\"x\" in locals())" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "env", + "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.10.6" + }, + "orig_nbformat": 4, + "vscode": { + "interpreter": { + "hash": "815559390840ce9b0b7cd48dd8184ccd76ec01fca5bb757616f04d8a9e4f3706" + } + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/test/numsols.md b/test/numsols.md new file mode 100644 index 0000000..eb61767 --- /dev/null +++ b/test/numsols.md @@ -0,0 +1,125 @@ +```python +%load_ext conjure + +``` + + + + + + Conjure extension is loaded. + For usage help run: %conjure_help + + + +```python +w = 7 +``` + + +```python +%%conjure --number-of-solutions all --solver minion + +given w: int +find x : int(0..9) +such that + w = x /\ (w != x) +``` + + + + + 'No solution' + + + + +```python +"x" in locals() +``` + + + + + False + + + + +```python +%conjure_clear +``` + + Conjure model cleared + + + +```python +%%conjure --number-of-solutions all --solver minion + +$ -O0 -S0 is to ensure solutions come out in lex order +given w: int +find x : int(0..9) +such that + w != x +``` + + + + + [{'x': 0}, + {'x': 1}, + {'x': 2}, + {'x': 3}, + {'x': 4}, + {'x': 5}, + {'x': 6}, + {'x': 8}, + {'x': 9}] + + + + +```python +"x" in locals() +``` + + + + + False + + + + +```python +%conjure_clear +``` + + Conjure model cleared + + + +```python +%%conjure --number-of-solutions all --solver minion +given w: int +find x : int(0..9) +find y: int(5..12) +such that + x*y=w +``` + + + + + {'x': 1, 'y': 7} + + + + +```python +print("x" in locals()) +``` + + True + From d4a0547ca9d5678d8d7262120f92049592c251e8 Mon Sep 17 00:00:00 2001 From: Chris Jefferson Date: Sat, 25 Feb 2023 11:46:02 +0800 Subject: [PATCH 3/3] Allow running a single test --- test/run_tests.sh | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/test/run_tests.sh b/test/run_tests.sh index e612a36..798a7bf 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -2,8 +2,16 @@ set -eux -for f in *.ipynb; do - jupyter nbconvert --to markdown --execute $f -done +if [ $# -eq 0 ]; then + for f in *.ipynb; do + jupyter nbconvert --to markdown --execute $f + done +else + for f in "$@" + do + jupyter nbconvert --to markdown --execute $f + done +fi + git diff --exit-code .