Skip to content

Commit

Permalink
Merge pull request #24 from ChrisJefferson/numsols
Browse files Browse the repository at this point in the history 
Handle solution counts differently
  • Loading branch information
@ozgurakgun
ozgurakgun authored Mar 2, 2023
2 parents 768eb8e + d4a0547 commit fc85e06
Show file tree
Hide file tree
Showing 5 changed files with 400 additions and 18 deletions.
13 changes: 4 additions & 9 deletions conjure/conjurehelper.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
import datetime
import json
from subprocess import Popen, PIPE
import uuid


class ConjureHelper:
Expand Down Expand Up @@ -39,24 +40,18 @@ 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'):
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:
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
Expand Down
23 changes: 17 additions & 6 deletions conjure/conjuremagics.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand Down
243 changes: 243 additions & 0 deletions test/numsols.ipynb
View file
Original file line number Diff line number Diff line change
@@ -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": [
"<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": [
"%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
}
Loading

0 comments on commit fc85e06

Please sign in to comment.