Skip to content

Commit

Permalink
Merge pull request Z3Prover#6 from PKHG/master
Browse files Browse the repository at this point in the history 
How to use the code
  • Loading branch information
@NikolajBjorner
NikolajBjorner authored Jun 10, 2019
2 parents 70b3c8b + bc862fc commit 9438d84
Showing 1 changed file with 266 additions and 0 deletions.
266 changes: 266 additions & 0 deletions HowToUseCode.ipynb
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,266 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# www \n",
"https://github.com/Z3Prover/doc\n",
"\n",
"After downloading (see <font color=\"green\">Clone or download</font>)\n",
"\n",
"Open a jupyter-notebook at the directory code and see how to work\n",
"easily from here by **New Python3**"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"\u001b[1m\u001b[32mREADME.md\u001b[m\u001b[m \u001b[1m\u001b[34mimages\u001b[m\u001b[m \u001b[1m\u001b[32mprogrammingz3.mdk\u001b[m\u001b[m \u001b[1m\u001b[34msave\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[34mcode\u001b[m\u001b[m \u001b[1m\u001b[32mllncs.cls\u001b[m\u001b[m \u001b[1m\u001b[32mrefs.bib\u001b[m\u001b[m\r\n"
]
}
],
"source": [
"!ls .."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"/Users/peterkhgragert/IpythonNotebooks/z3-master/doc-master/programmingz3/code\r\n"
]
}
],
"source": [
"!pwd"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"\u001b[1m\u001b[32marrays.py\u001b[m\u001b[m \u001b[1m\u001b[32mmbqi.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mbmc.py\u001b[m\u001b[m \u001b[1m\u001b[32mmemset.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mbv1.py\u001b[m\u001b[m \u001b[1m\u001b[32mmondec.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mbv2.py\u001b[m\u001b[m \u001b[1m\u001b[32mmss.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mcard.py\u001b[m\u001b[m \u001b[1m\u001b[32mpareto.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mcdclT.py\u001b[m\u001b[m \u001b[1m\u001b[32mpb.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mcdclTdual.py\u001b[m\u001b[m \u001b[1m\u001b[32mpy2smtlib.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mconsequences.py\u001b[m\u001b[m \u001b[1m\u001b[32mqfdt.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mcores.py\u001b[m\u001b[m \u001b[1m\u001b[32mqffd.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mdt.py\u001b[m\u001b[m \u001b[1m\u001b[32mqflra.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mematching.py\u001b[m\u001b[m \u001b[1m\u001b[32mquantifiers.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mequality_as_second_order.py\u001b[m\u001b[m \u001b[1m\u001b[32mscopes.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32meuf.py\u001b[m\u001b[m \u001b[1m\u001b[32mscopes2.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32meuf_fg.py\u001b[m\u001b[m \u001b[1m\u001b[32mscopes3.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mexpr_access.py\u001b[m\u001b[m \u001b[1m\u001b[32mseq1.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mfp.py\u001b[m\u001b[m \u001b[1m\u001b[32mseq2.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mhorn.py\u001b[m\u001b[m \u001b[1m\u001b[32msmt101.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32minterp.py\u001b[m\u001b[m \u001b[1m\u001b[32msorts_are_nonempty.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mlia.py\u001b[m\u001b[m \u001b[1m\u001b[32mspecial_relations.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mmarco.py\u001b[m\u001b[m \u001b[1m\u001b[32mterms_and_formulas.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mmaxbin.py\u001b[m\u001b[m \u001b[1m\u001b[32mtieshirt.py\u001b[m\u001b[m\r\n",
"\u001b[1m\u001b[32mmaxres.py\u001b[m\u001b[m \u001b[1m\u001b[32mufbv.py\u001b[m\u001b[m\r\n"
]
}
],
"source": [
"!ls *.py"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"from z3 import *\r\n",
"Z = IntSort()\r\n",
"A = Array('A', Z, Z)\r\n",
"x, y = Ints('x y')\r\n",
"solve(A[x] == x, Store(A, x, y) == A)\r\n"
]
}
],
"source": [
"!cat arrays.py"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[A = Store(K(Int, 0), 1, 1), y = 1, x = 1]\n"
]
}
],
"source": [
"from arrays import *"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"from z3 import *\r\n",
"index = 0\r\n",
"def fresh(round, s):\r\n",
" global index\r\n",
" index += 1\r\n",
" return Const(\"!f%d_%d\" % (round, index), s)\r\n",
"\r\n",
"def zipp(xs, ys):\r\n",
" return [p for p in zip(xs, ys)]\r\n",
"\r\n",
"def bmc(init, trans, goal, fvs, xs, xns):\r\n",
" s = Solver()\r\n",
" s.add(init)\r\n",
" count = 0\r\n",
" while True:\r\n",
" print(\"iteration \", count)\r\n",
" count += 1\r\n",
" p = fresh(count, BoolSort())\r\n",
" s.add(Implies(p, goal))\r\n",
" if sat == s.check(p):\r\n",
" print (s.model())\r\n",
" return\r\n",
" s.add(trans)\r\n",
" ys = [fresh(count, x.sort()) for x in xs]\r\n",
" nfvs = [fresh(count, x.sort()) for x in fvs]\r\n",
" trans = substitute(trans, \r\n",
" zipp(xns + xs + fvs, ys + xns + nfvs))\r\n",
" goal = substitute(goal, zipp(xs, xns))\r\n",
" xs, xns, fvs = xns, ys, nfvs\r\n",
"\r\n",
"\r\n",
"x0, x1 = Consts('x0 x1', BitVecSort(4))\r\n",
"bmc(x0 == 0, x1 == x0 + 3, x0 == 10, [], [x0], [x1])\r\n"
]
}
],
"source": [
"!cat bmc.py"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"iteration 0\n",
"iteration 1\n",
"iteration 2\n",
"iteration 3\n",
"iteration 4\n",
"iteration 5\n",
"iteration 6\n",
"iteration 7\n",
"iteration 8\n",
"iteration 9\n",
"iteration 10\n",
"iteration 11\n",
"iteration 12\n",
"iteration 13\n",
"iteration 14\n",
"[!f14_27 = False,\n",
" !f3_5 = False,\n",
" !f7_13 = False,\n",
" !f5_10 = 2,\n",
" !f11_22 = 4,\n",
" !f10_19 = False,\n",
" !f12_23 = False,\n",
" !f9_18 = 14,\n",
" !f4_7 = False,\n",
" !f8_15 = False,\n",
" !f6_12 = 5,\n",
" !f11_21 = False,\n",
" !f6_11 = False,\n",
" !f3_6 = 12,\n",
" !f12_24 = 7,\n",
" !f13_26 = 10,\n",
" !f13_25 = False,\n",
" !f9_17 = False,\n",
" x1 = 3,\n",
" !f8_16 = 11,\n",
" !f10_20 = 1,\n",
" !f5_9 = False,\n",
" !f2_4 = 9,\n",
" !f15_29 = True,\n",
" !f4_8 = 15,\n",
" !f7_14 = 8,\n",
" !f1_1 = False,\n",
" !f2_3 = False,\n",
" !f1_2 = 6,\n",
" x0 = 0]\n"
]
}
],
"source": [
"from bmc import*"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"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.3"
}
},
"nbformat": 4,
"nbformat_minor": 2
}

0 comments on commit 9438d84

Please sign in to comment.