From a9a673bb8a9532c41f7b24d497dd37fcb28e098c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Nov 2012 17:53:43 -0800 Subject: [PATCH] New API website Signed-off-by: Leonardo de Moura --- doc/footer.html | 4 - doc/header.html | 23 - doc/mk_api_doc.py | 8 +- doc/website.dox | 1 + doc/z3.css | 934 -------------------------------------- doc/z3.png | Bin 8130 -> 0 bytes doc/{z3.dox => z3api.dox} | 33 +- src/api/c++/z3++.h | 8 +- 8 files changed, 28 insertions(+), 983 deletions(-) delete mode 100644 doc/footer.html delete mode 100644 doc/header.html delete mode 100644 doc/z3.css delete mode 100644 doc/z3.png rename doc/{z3.dox => z3api.dox} (99%) diff --git a/doc/footer.html b/doc/footer.html deleted file mode 100644 index 724bd6e7c..000000000 --- a/doc/footer.html +++ /dev/null @@ -1,4 +0,0 @@ - - - diff --git a/doc/header.html b/doc/header.html deleted file mode 100644 index 071e30b91..000000000 --- a/doc/header.html +++ /dev/null @@ -1,23 +0,0 @@ - - - - - - - - Z3: Theorem Prover - - - - - - - - - - -
Z3 - -
- diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index cb90748ff..6f0b88960 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -26,17 +26,15 @@ try: print "Removed annotations from z3_api.h." DEVNULL = open(os.devnull, 'wb') try: - subprocess.call(['doxygen', 'z3.dox'], stdout=DEVNULL, stderr=DEVNULL) + if subprocess.call(['doxygen', 'z3api.dox'], stdout=DEVNULL, stderr=DEVNULL) != 0: + print "ERROR: doxygen returned nonzero return code" + exit(1) except: print "ERROR: failed to execute 'doxygen', make sure doxygen (http://www.doxygen.org) is available in your system." exit(1) print "Generated C and .NET API documentation." os.remove('z3_api.h') print "Removed temporary file z3_api.h." - shutil.copy('z3.css', 'api/html/z3.css') - print "Copied z3.css." - shutil.copy('z3.png', 'api/html/z3.png') - print "Copied z3.png." sys.path.append('../src/api/python') pydoc.writedoc('z3') shutil.move('z3.html', 'api/html/z3.html') diff --git a/doc/website.dox b/doc/website.dox index 91034aafa..685bc0af1 100644 --- a/doc/website.dox +++ b/doc/website.dox @@ -11,6 +11,7 @@ This website hosts the automatically generated documentation for the Z3 APIs. - \ref capi + - \ref cppapi - .NET API - Python API - Try Z3 online at RiSE4Fun using Python or SMT 2.0. diff --git a/doc/z3.css b/doc/z3.css deleted file mode 100644 index c642d7794..000000000 --- a/doc/z3.css +++ /dev/null @@ -1,934 +0,0 @@ - -/* Section Start for new text handling */ -.PSubText -{ - FONT-SIZE: 8pt; - COLOR: #555555; -} -.LeftJustifyBullet -{ - FONT-SIZE: 10pt; - margin-left:-24px; -} -/* Section End for new text handling */ - -/* Section Start for text handling based on Rob Gruen's layout for the Download Details page */ -A:hover -{ - TEXT-DECORATION: underline -} -A -{ - TEXT-DECORATION: none; - COLOR: #333399; -} -LI -{ - FONT-SIZE: 10pt; - COLOR: #555555; - margin-bottom:10px; - margin-left: -3px; -} -LI LI -{ - FONT-SIZE: 10pt; - COLOR: #555555; - margin-bottom:10px; - margin-left: -3px; -} -BODY -{ - margin-right: 20px; - margin-left: 20px; - COLOR: #555555; - FONT-FAMILY: Verdana, Arial, Helvetica, sans-serif; - FONT-SIZE: 10pt; -} -P -{ - FONT-SIZE: 10pt; - COLOR: #555555; -} -.Z3Title -{ - FONT-SIZE: 18pt; - COLOR: #1A41A8; - margin-bottom:-10px; -} -.PageTitle -{ - FONT-SIZE: 12pt; - COLOR: #333333; - margin-bottom:-10px; -} -.BlobTitle -{ - FONT-SIZE: 12pt; - COLOR: #333333; - LINE-HEIGHT: 100%; - margin-bottom:-10px; -} -.Heading1 -{ - FONT-SIZE: 10pt; - COLOR: #2A51B8; - margin-bottom:-10px; - -} -.Heading2 -{ - FONT-WEIGHT: bold; - FONT-SIZE: 10pt; - COLOR: #555555; - margin-bottom:-10px; -} -.Heading3 -{ - FONT-SIZE: 10pt; - COLOR: #2A51B8; - margin-bottom:-10px; -} -.title -{ - font-size: 18pt; - color: #1A41A8; - margin-bottom:-10px; - line-height: 35pt -} -.quote -{ - FONT-FAMILY: Georgia, Times, Times New Roman, serif; - FONT-STYLE: italic; - FONT-SIZE: 20pt; - COLOR: #2A51B8; -} -.attribution -{ - FONT-SIZE: 8pt; - COLOR: #555555; -} -.quickinfo -{ - FONT-WEIGHT: bold; - FONT-SIZE: 13pt; - MARGIN-LEFT: 12px; - COLOR: #2A51B8; -} -.quickinfo_header -{ - font-weight: bold; - color: #555555; - margin-left: 25px; -} -hr -{ - width: 100%; - margin-top: 10px; - margin-bottom: 10px; - color: #cccccc; -} - -.RHPSectionHeader -{ - font-size: 10pt; - margin-left: 20px; - color: #2A51B8; - display: block; -} -.RHPNav -{ - FONT-SIZE: 10pt; - MARGIN-TOP: 6px; - COLOR: #333333; -} -.author -{ - FONT-SIZE: 8pt; - COLOR: #555555; -} -.lastupdated -{ - FONT-SIZE: 8pt; - COLOR: #555555; -} -/* Section End for text handling based on Rob Gruen's layout for the Download Details page */ - -/* Section Start for text handling based on rmcstyle.css */ -.title_2ndLvl -{ - font-family: tahoma; - font-size: 120%; - color: #FFFFFF; - padding-left: 5px; -} -.VR -{ - background-color: #cccccc; - width: 1px; - margin-top: -24; -} -.link1 -{ - font-size:70%; - font-family: verdana; -} -.link2 -{ - font-size: 70%; - font-family:Verdana; - font-style:italic; -} -.link3 -{ - font-style: italic; - font-family: Verdana; - color: #000000; - font-weight: bold; -} -.link4 -{ - font: italic 70% Verdana; - color: #000000; - text-decoration: none; -} -.link5 -{ - font: 70% Verdana; - color: #003399; - text-decoration: none; -} -.link6 -{ - font: 70% verdana; - color: #003399; -} -.ReadMore -{ - text-decoration:none; -} -/* .text1 -{ - font: 70% Verdana; -} */ -.text2 -{ - padding-bottom: 10px; - font: 70% Verdana; -} -.text3 -{ - font-size: 120%; - font-family:Verdana; - color: #000000; -} -.text3_w_padding -{ - font: 120% Verdana; - color: #000000; - padding-left:20px; -} -.text4 -{ - font-weight: bold; - font-size: 70%; - font-family: Verdana; - color: #000000; -} -.text5 -{ - padding-left: 5px; - font-weight: bold; - font-size: 70%; - font-family: Verdana; - color: #ffffff; -} -.text6 -{ - font: 70%; - font-family: verdana; -} -.newsTitle -{ - font-family: tahoma; - font-size: 120%; - color: #CCCCCC; -} -.areaTitle -{ - font-family: tahoma; - font-size: 120%; - color: #FFFFFF; -} -.newsContentTitle -{ - font-family: tahoma; - font-size: 120%; - color: #FFFFFF; -} -.areaContentTitle -{ - font-family: verdana; - font-size: 140%; - color: #000000; -} -.areaContentTitle_w_pad -{ - font-family: verdana; - font-size: 140%; - color: #000000; - padding-left: 20px; - padding-top: 20px; -} -.newsArchiveTitle -{ - font-family: verdana; - font-size: 150%; - color: #000000; -} -.FeatureStoryTitle -{ - font-family: verdana; - font-size: 18 pt; - COLOR: #2A51B8; - margin-bottom:-15px; -} -.FeatureStoryDate -{ - font-family: Verdana; - font-size: 8 pt; - color: #555555; - -} -.FeatureStoryByLine -{ - font-family: verdana; - font-size: 10 pt; - color: #555555; - margin-bottom:-15px; - font-weight: bold; -} -.SideBarLink -{ - font-family: verdana; - font-size: 80%; - color: #000000; -} -.newsArchiveSubTitle -{ - font-family: verdana; - font-size: 118%; - color: #666666; -} -.newsArchiveYear -{ - font: bold 80% Verdana; - color: #000000; - border-bottom: #cccccc 1px solid; - border-top: #cccccc 1px solid; -} -.newsHeadlineTitle -{ - font-family: verdana; - font-size: 140%; - color: #000000; -} -.newsPublicationDate -{ - font-family: Verdana; - font-size: 60%; - color: #000000; - font-weight: bold; -} -.newsPublicationSource -{ - font-family: Verdana; - font-size: 60%; - color: #000000; - font-weight: bold; -} - - -h1 {font-size: 16pt; color: #2A51B8; margin: 30px 0px; font-weight: normal;} - -.anchor { color: #2A51B8; } - -h2 {font-size: 14pt; color: #2A51B8; margin: 10px 0px; font-weight: normal;} - -h3 {font-size: 12pt; color: #2A51B8; margin: 10px 0px; font-weight: normal;} - -h4 -{ - color: #808080; - font-family: Tahoma; - font-size: 90%; - margin-bottom: -10px -} - -.TitleHeader {font-family: tahoma; font-weight: bold; font-size: 110%; color: #000000;} - -P P -{ - font-size: 100%; -} -.groupheading -{ - padding-left: 20px; - padding-top: 40px; - padding-bottom: 10px; - font-size: 1.4em; - color: #0065CF; - font-family:verdana; -} -.GroupTitle -{ - padding-left: 20px; - padding-top: 20px; - padding-bottom: 10px; - font-size: 1.4em; - color: #0065CF; -} -LI LI -{ - font-size: 100%; -} -LI A -{ - font-size: 100%; -} -/* Section End for text handling based on rmcstyle.css */ - -/* Section Start for text handling based on new_style.css */ -.O -{ - color:white; - font-size:149%; -} -ul -{ - color: #808080; - list-style-type:square -} - - -/* Section End for text handling based on new_style.css */ - -/* Section Start for page layout based on Rob Gruen's downloads Page */ -.bodymargin -{ - margin-left: 20px; - position: relative; -} -/* Section Start for page layout based on Rob Gruen's downloads Page */ - -/* Section Start for page layout based on Rob Gruen's downloads Page */ -.quickinfo_tbl -{ - color: #555555; - BORDER-RIGHT: black 1px solid; - BORDER-TOP: black 1px solid; - BORDER-LEFT: black 1px solid; - WIDTH: 560px; - BORDER-BOTTOM: black 1px solid; - HEIGHT: 164px; -} -/* Section Start for page layout based on Rob Gruen's downloads Page */ - -/* Section Start for page layout based on rmcstyle.css */ -.linkbox -{ - margin-left: 20px; - margin-right: 30px; - margin-bottom: 20px; - padding-bottom: 10px; - width: 175px; - float: right; - background: #ffffff; - border-bottom: #CCCCCC 1px solid; -} -.outlineDivTitle -{ - border-top: #CCCCCC 1px solid; - background-color: #FFFFFF; - color: #CCCCCC; - padding-left: 15px; - padding-bottom: 12px; - padding-top: 12px; - font: bold 70% Verdana; - color: #2A51B8; -} -.outlineDiv -{ - padding-left: 20px; - background-image: URL(/images/orangesquare.gif); - background-repeat: no-repeat; - background-position: 6 8; - font: 70% verdana; - color: #555555; - line-height: 200%; -} -/* Section End for page layout based on rmcstyle.css */ - -/* Section Start for page layout based on new_style.css */ -.QL_border -{ - border-right: #555555 1px solid; - background: #ffffff; - border-left: #555555 1px solid; - border-bottom: #555555 1px solid; -} - -/* Section End for page layout based on new_style.css */ - - -/* Begin Versal-specific styles */ - - -.imageAlignLeft -{ - background-color: #ffffff; - margin: 0px 10px 10px 10px; - color: #666666; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 70%; - font-weight:normal; - text-align: left; -} -.imageAlignRight -{ - background-color: #ffffff; - margin: 0px 10px 10px 10px; - color: #666666; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 70%; - font-weight:normal; - text-align: left; -} -.imageFloatLeft -{ - float: left; - background-color: #ffffff; - margin: 0px 10px 10px 0px; - color: #666666; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 70%; - font-weight:normal; - text-align: left; -} -.imageFloatRight -{ - float: right; - background-color: #ffffff; - margin: 0px 10px 10px 10px; - color: #666666; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 70%; - font-weight:normal; - text-align: left; -} -.imageCaptionText -{ - color:#666666; - font-family:Verdana, Arial, Helvetica, sans-serif; - font-size:xx-small; - font-weight:normal; -} -.tableBorder -{ - border-top: solid 1px #C0C0C0; - border-left: solid 1px #C0C0C0; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - margin-top: 1em; -} -.tableNoBorder -{ - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - margin-top: 1em; -} -.tableBorderLabel -{ - border-top: solid 1px #C0C0C0; - border-left: solid 1px #C0C0C0; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - font-weight: bold; - background: #999999; - color: #FFFFFF; -} -.tableNoBorderLabel -{ - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - font-weight: bold; - background: #999999; - color: #FFFFFF; -} -.tableBorderHeader -{ - background: #CCCCCC; - color: #000000; -} -.tableBorderHeader td -{ - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - font-weight: bold; - border-top: solid 1px #CCCCCC; - border-left: solid 1px #CCCCCC; -} -.tableNoBorderHeader -{ - background: #CCCCCC; - color: #000000; -} -.tableNoBorderHeader td -{ - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - font-weight: bold; -} -.tableBorderSection -{ - background: #DDDDDD; -} -.tableBorderSection td -{ - border-top: solid 1px #CCCCCC; - border-left: solid 1px #CCCCCC; - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - font-weight: bold; -} -.tableNoBorderSection -{ - background: #DDDDDD; -} -.tableNoBorderSection td -{ - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 100%; - font-weight: bold; -} -.tableBorderRecord td -{ - border-bottom: solid 1px #CCCCCC; - border-right: solid 1px #CCCCCC; -} -.tableBorderRecord td td -{ - border-width: 0px; -} -.tableNoBorderRecord td -{ -} -.tableNoBorderRecord td td -{ -} -.tableFootnotes -{ - margin-top: 7px; - margin-left: 5px; -} -.dataTableBottomMargin -{ - height: 1px; - overflow: hidden; - margin-bottom: 18px; -} - -.footnote -{ - font: 70% Arial; - position: relative; - top: -0.2em; -} - -.footnoteText -{ - font-family: Verdana, Arial, Helvetica, sans-serif; - font-size: 65%; -} - -.footnotes -{ - margin-top: 11px; - margin-bottom: 36px; -} - -pre.codeSample -{ - background: #DDDDDD; - font-family: Lucida Console, Courier New; - font-size: 70%; - padding: 10px 15px 10px 25px; - margin-bottom: 1em; -} - -span.codeSample -{ - font-family: Lucida Console, Courier New; -} - -/* End Versal-specific styles */ - -/* Section Start for MNP styles */ - -.mnpSearchButton {width:22px;} - - -table.centered-small { - background-color: #eef3f5; - border: 1px solid; - border-color: #dedeee; - width: 100%; - border-style: solid; border-width: thin; - font-size: 10pt; text-decoration: none; -} -table.centered-small a:link { text-decoration: none; } -table.centered-small a:visited { text-decoration: none; } -table.centered-small a:active { text-decoration: none; } - -address { font-size: 10pt; font-family: Verdana, Arial, Helvetica, sans-serif; } - -.fragment { - font-family: monospace, fixed; - font-size: 10ptr; -} -PRE.fragment { - border: 1px solid #CCCCCC; - background-color: #f5f5f5; - margin-top: 4px; - margin-bottom: 4px; - margin-left: 2px; - margin-right: 8px; - padding-left: 6px; - padding-right: 6px; - padding-top: 4px; - padding-bottom: 4px; -} - - -/* Style for detailed member documentation */ -.memtemplate { - font-size: 80%; - color: #606060; - font-weight: normal; -} -.memnav { - background-color: #e8eef2; - border: 1px solid #84b0c7; - text-align: center; - margin: 2px; - margin-right: 15px; - padding: 2px; -} -.memitem { - padding: 4px; - background-color: #eef3f5; - border-width: 1px; - border-style: solid; - border-color: #dedeee; - -moz-border-radius: 8px 8px 8px 8px; -} -.memname { - white-space: nowrap; - font-weight: normal; - font-size: 10pt; -} -.memdoc{ - padding-left: 10px; -} -.memproto { - background-color: #d5e1e8; - width: 100%; - border-width: 1px; - border-style: solid; - border-color: #84b0c7; - font-weight: bold; - -moz-border-radius: 8px 8px 8px 8px; -} -.paramkey { - text-align: right; -} -.paramtype { - white-space: nowrap; -} -.paramname { - color: #602020; - font-style: italic; - white-space: nowrap; -} -DIV.ah { background-color: black; font-weight: bold; color: #ffffff; margin-bottom: 3px; margin-top: 3px } - -DIV.groupHeader { - margin-left: 16px; - margin-top: 12px; - margin-bottom: 6px; - font-weight: bold; -} -DIV.groupText { margin-left: 16px; font-style: italic; font-size: 90% } -TD.indexkey { - background-color: #e8eef2; - font-weight: bold; - padding-right : 10px; - padding-top : 2px; - padding-left : 10px; - padding-bottom : 2px; - margin-left : 0px; - margin-right : 0px; - margin-top : 2px; - margin-bottom : 2px; - border: 1px solid #CCCCCC; -} -TD.indexvalue { - background-color: #e8eef2; - font-style: italic; - padding-right : 10px; - padding-top : 2px; - padding-left : 10px; - padding-bottom : 2px; - margin-left : 0px; - margin-right : 0px; - margin-top : 2px; - margin-bottom : 2px; - border: 1px solid #CCCCCC; -} -TR.memlist { - background-color: #f0f0f0; -} -P.formulaDsp { text-align: center; } -IMG.formulaDsp { } -IMG.formulaInl { vertical-align: middle; } -SPAN.keyword { color: #008000 } -SPAN.keywordtype { color: #604020 } -SPAN.keywordflow { color: #e08000 } -SPAN.comment { color: #800000 } -SPAN.preprocessor { color: #806020 } -SPAN.stringliteral { color: #002080 } -SPAN.charliteral { color: #008080 } - - -.mdescLeft { - padding: 0px 8px 4px 8px; - font-size: 80%; - font-style: italic; - background-color: #FAFAFA; - border-top: 1px none #E0E0E0; - border-right: 1px none #E0E0E0; - border-bottom: 1px none #E0E0E0; - border-left: 1px none #E0E0E0; - margin: 0px; -} -.mdescRight { - padding: 0px 8px 4px 8px; - font-size: 80%; - font-style: italic; - background-color: #FAFAFA; - border-top: 1px none #E0E0E0; - border-right: 1px none #E0E0E0; - border-bottom: 1px none #E0E0E0; - border-left: 1px none #E0E0E0; - margin: 0px; -} -.memItemLeft { - padding: 1px 0px 0px 8px; - margin: 4px; - border-top-width: 1px; - border-right-width: 1px; - border-bottom-width: 1px; - border-left-width: 1px; - border-top-color: #E0E0E0; - border-right-color: #E0E0E0; - border-bottom-color: #E0E0E0; - border-left-color: #E0E0E0; - border-top-style: solid; - border-right-style: none; - border-bottom-style: none; - border-left-style: none; - background-color: #FAFAFA; - font-size: 80%; -} -.memItemRight { - padding: 1px 8px 0px 8px; - margin: 4px; - border-top-width: 1px; - border-right-width: 1px; - border-bottom-width: 1px; - border-left-width: 1px; - border-top-color: #E0E0E0; - border-right-color: #E0E0E0; - border-bottom-color: #E0E0E0; - border-left-color: #E0E0E0; - border-top-style: solid; - border-right-style: none; - border-bottom-style: none; - border-left-style: none; - background-color: #FAFAFA; - font-size: 80%; -} -.memTemplItemLeft { - padding: 1px 0px 0px 8px; - margin: 4px; - border-top-width: 1px; - border-right-width: 1px; - border-bottom-width: 1px; - border-left-width: 1px; - border-top-color: #E0E0E0; - border-right-color: #E0E0E0; - border-bottom-color: #E0E0E0; - border-left-color: #E0E0E0; - border-top-style: none; - border-right-style: none; - border-bottom-style: none; - border-left-style: none; - background-color: #FAFAFA; - font-size: 80%; -} -.memTemplItemRight { - padding: 1px 8px 0px 8px; - margin: 4px; - border-top-width: 1px; - border-right-width: 1px; - border-bottom-width: 1px; - border-left-width: 1px; - border-top-color: #E0E0E0; - border-right-color: #E0E0E0; - border-bottom-color: #E0E0E0; - border-left-color: #E0E0E0; - border-top-style: none; - border-right-style: none; - border-bottom-style: none; - border-left-style: none; - background-color: #FAFAFA; - font-size: 80%; -} -.memTemplParams { - padding: 1px 0px 0px 8px; - margin: 4px; - border-top-width: 1px; - border-right-width: 1px; - border-bottom-width: 1px; - border-left-width: 1px; - border-top-color: #E0E0E0; - border-right-color: #E0E0E0; - border-bottom-color: #E0E0E0; - border-left-color: #E0E0E0; - border-top-style: solid; - border-right-style: none; - border-bottom-style: none; - border-left-style: none; - color: #606060; - background-color: #FAFAFA; - font-size: 80%; -} - -dl { font-size: 10pt; } -td { font-size: 10pt; } -th { font-weight: normal; } - -#nav {font-family: Verdana, Arial, sans-serif; margin:0 0 0 10px;border-bottom:3px solid #DDE4EC; height:35px; min-width:500px;} -#nav ul { list-style: none; margin-top:15px; padding: 0; font-size:150%; float:left; } -#nav ul li, div.sitemenu ul li a, div.sitemenu ul li a:visited {color: #4E688E;display: block;padding: 0 5px;text-decoration: none;white-space: nowrap;float:left;} -#nav ul li a:hover {color: #000;text-decoration: none;} -#nav ul li a:active {color: #cfdbe6;text-decoration: none;} diff --git a/doc/z3.png b/doc/z3.png deleted file mode 100644 index 4aa69df7237cb04f3d8e3a86101313e8b1d78442..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 8130 zcmV;zA3flSP)Px#1ZP1_K>z@;j|==^1poj532;bRa{vGi!vFvd!vV){sAK>DA6H34K~#8N<(vta zRMnNo->ZG=y_=@H*%cIQKx7vb6hETq;5Le)aa=M+aE%#_QPGS>jm8}##vL64E<_!p zh@;U-f*KTzyF_+@?xwqG8hWehuB!Q+dtMb~cd>M9=9}-EM}4o~d-dMC_x|tyocllL z-oj2Mlh*%_Egp~4ST?uY?Q*%kmqy!J;j6B$_W68v#zuLWr%=hw=#~**38g_Jabgd^>>g((G zR*LPlBIT}nz9y}c`*z7 zJRT1`xB4AvC1O@G0Z&qU`qG?QTuJYRNODC!&MteC97giThPrZ(?Dg0sd;M^XWx2do zbB(oq%_Wyya_Oa)_U_#~Cnu*9sd>TEPd|OmIp^4Aquc|hy7K#4p+a}0)Qa?S2lJ_v zZFNv{TRzeR%)_?$7^87&x0_SkOQYOarO-wSa5YKbB|_cAt9csV}_nf;yZ|U6=*F^0MAl)iu_f zkFAb2;obk{W|$#;=8ae@eq(+3(D~<|KW*By$&)Ad>C>kxd?QDW_~esMBNzSI7(iU; zE6+<;q>c^QTP{x8R zmet;rhA*pQWR1wqXT%AK~tc#yh2P$;fk=#poWPGn(}coh@?LT zO7lX2*lpR(+XnvA)!~Xm8X6jIz4cc1%E9dHYi?o0VC>7%;XOdhJYpa-6tiKO701ee zOiYGK3tlue?zZ?Up$O7!tG$IMyUAxqN_h6yu z1{X%~9X7Gbv|$RNTtYF!GE+(B>3J9cJZ|>p*x)Fj$j9(hdM<^pKASLrax=#^e$c>Y9EU=<@}|sbQ6Bvud`C9zsBuLpQMVn2R2|K?WA~u8!sbho453a2j=WbBGdAp6Hg761$s>zJ2?4hL7+Fd$Iia)_^0erW&iG)#`{^u_i0lEY65H zWPdjbcU%6P;JL3`@hDsqh=oO{D$@yeBGna&qx71HTiGW(MFXquJv_0i=AL`*88&Pf z@a5*_W|n-@O*h?mP zqg%dw`AaXo#8>^NT{vLsxuCDzhJz4Mt&b>z1~~J)+Lj$I=(XhPBV$bs1R<12av_WH zlDhcoU;oPZqD%w}b>6%tJqTu|TRLG))ft#Bzx;B+ZuVkVL0>x_HFeOA)vCyWgP>GZ zBPzM*4Hq?k{#xxHuIH4O0L_RIBgTvw11_BkTDfv1k-*liTe+?y3`GY50i+@u$LV25 zT_=IOrXI*Aopzddu}Rl0^I?+)CsQTpX1s{h6@mzM!aMUV?GF`{Jo}T$(dHe`KmUA5 zNy)fz2sFGFvw@UxLBS@uroc9VZPP*4UU~;l`2UJznA%T%P6bDCX zmI(#4QI2?w05U`U?fWpq5JHPz$%N;v*KsUf;BSZnd zbeC&wm4lil0YS`*=G<_@4R_yt_dzHAtm4pPd?M0}2|Jc+yq>`mDXOp2$0@R39VJAg=|rZ$kSjn=6X9jF#nr!hR6KlQTUgdfLtR7t-X(dJOk@p6fj zkTX_e_~;4cv~Kud^WsZ5oi}e@ad9!PV%#|R;DfQ;PRd!cSXxO6&6I~-E7qx=oGx0l zX!h*c2hF&&&zKYZ48({OXOo(kLBn`Esl4M2CGtro7G5zGuZP>kSCGiaB3!5_-B?sq z1V7m`y1d3PD5|rkV(k?>$MUP(Jq9W9*Cj4Yfrx zCcGXuR%|qi$URYfMz#1nwhwTLg59p5-@onal{|IOK?lKNjV80}zWwRIu3b85(j?;0 zK%Wt%r`{W_T_-X)CF@1U8aXOrRpL-5{M3L6)n>KSuYdF`-g((&myukda%t?ch8$YD zGA6Sod%`aB<^>BDpxykD{63Wv5$6)#YJ4X70^8>WIG`kPpnBT|L=JLtb3cCb8QwEx z$`neW&%}>)MWJU`X3d)Q?z``L^UM4H>yoy*^%BW~i{vmQ%#`39-H%jO^$+9Fr6!Q_ z(e+kx_57KXOYRdj0FT(y$z5%BFLh&7lT{lq1*x!5ay(5k|V(#3z+%tAfGJ`0c9yuE7c>Q$H_W=rpC-LlVhbQeJq!YB-vFEsS} zmCf~4@i-P?NaKwCDM^(fTpV%0xa141x@B@Q(Lq|24S8|MA&21d3JMDLzjq-%oyP!B zP*B*ffB#-3C82N#c1ELZ4GlZCZrM^@Q{C2PQX!TV&hK^d4U1aZI@+3d<)CwdArWFJ ziDyPz;k5C3I`UdYW&Q8GVA777O*j^&MDS5KK5F*!#M{Hc5S|=i=JchgS=G$i^C|JveX0 z(*HmJ+;-b-WLy|?F%F#XcZF}^!iD71Y1qi?-)n7)(V>#@h6ctb?UwRRPCTsxplbm5(EEuK%g=xvlH zBd`&R|bfn4mFnPbwZtiF-R(*n8E3 z=QOTgg)k-p!*fxskt0XyoJM!YF0nXI;FLT5xNF;Hf54CDuoCDvqs*y;s9^GmNLLqO z03RH#h-y=gF%#7*yKR>1K7Syup!l(WzwndgOL@;T&pd;1phM8`xIY}Uyu8QoA^Ld{ zuNZaZEAc>KTXUnR5Yg5~0~^dzsHJtEqmYAzWuGp*vgVUFn8v;T{`+fdYjG&>4(zB_ zcd+`r7q$Fo&#{1nV zGc;5x`NL2fDJ)&RuBGw*YM;(}ul>s5Q&`!29dIo&%fX^EY_(K7I zIOq=reL>7O;0^k{0l$}_*2hPNT83B1h*EL+_1Nu-gu}f`dpA^XxZ~mz?z;RWu$ww{ z>WeSFNF~vsgpb$?Ag1lFC+s6mV$k6gl|Q^IJa}r;_N@#R#uTtRW2mX5g+oBcawRGX z=9a8``^m5Va3A+D1&%o|!w>Hm%hGXvcby5V4CsJCqmG(z=Fi>982WzqXrRoK*h{D< zA+0l>8ap*SH@uUBU?gYd+pqlRlXo@N*H8zLBIxGL#K_2a#x!ge5KZeGvDp*$DRx6o zyCHw*wAO~LK9}wH!8_4MD&-`V#b}VI{pkdZI{q5>>JaGm_ilD{88FHB zs&!s>l7yt+>yjAOnW-`{Bb|u@HbIXjy91$MYwZTb?&h0s*3<~R!$8t*xVtu+zQ3xf zO863r5WT=JVo{A!sQ{LtajUQl(!oTBjCdQ5kkLdM>I#$b=+NOK&z$q~pU;1O?#+)) znsFwtefHUBso_^&eWk^98fm)$A2dOlmL76M<*b`_Z220K4Eac_!Fhuh6_sF{fYD5^ z$XtP$({kH^V8Cu~edAZNDE_Leu2N}2SjG#xnnMpjRO8Jr?!|CHP?cYhUr<;mpQ56I zqC!b|;5h=mtp!xfcCo5(Qs) z;e{->XlZGIcSL603TgKO>zp}r9(w4ZNi)yGPbAt~k)P3)W|Dg-THuQ06%-Vg7L``? z88Bo><)QGtt+k~++Lo@crc2WUh%s*oUJ{9pSTxF@`1;GwKJ~z@RN#XTKA_qJyy<9i zzu-Ie*khM1Tb5rw_?UUGR&V$c2IE;J#b#2nni*5gY4p109p#h}*&hloykvYL-f_w) zr<{KJ>F^icbvLBlJ0&MhocR9x@9!sV%LfcO`RqBku@ya&j#=FHge9)D3MS>Hli?Sq$cBd zFcynJc9a$dj#gzAB~pp&!Enw)FZ?$-OcoYtYQqURbYKy6t(25JH2yA`?8rum@q;-a!NurY@Pird8?5naomj#VS__T3IQ8BjSb6 zyzx;ajKs!_OxSC}H;sQaZZyXNBC3{2l^I7KhDv?;<(COOB;6v7-gC@LF(fZ3=B)WE zYip}JVr`_DF;gd*$u3BjIYXqS$oyX-!7K;2K}POjA_WvCOqu>~H{OvO2{E%o#i6T_GHKKda%Qpt zCDg05*T^CLw{F?QLK3u!HS~9d;O#dp!%w_KCG7nZ=sS)^!~tUvbe)qs9Rd z8j|Se;v>)hS6OK>p|_EWDaU90ph*Hco{>L=1^HKBdHLfHKS*-u#1l`%1xdm=Yt0y> z6}z+Ue6yvct-ZAgl1GAmtd`(G1-;R9dLW5e`IroCNom<17v2JPC_BbMI~(h3Tbg!Zy#W?-_{cmHGP_I)n!WiD zLHpf7^qHL;KXxpSeDlpW_zL=f<1Fyu7mhjR7`~fz^NX>#i)qaqunXh!B(9YhTlP*a zI~8&h{YWrWRNQODt53ZDicG{j_0&`N3lg7n6w?>qyUlhB->x^;)ye|qpx@Wt*1~j^ zUr`eT$vAjW7Un}x;0bs<0YW;rJ$Uc|Jfhg)1jLzkdM^#8wOl;;>PJ11qL!U?IiUdF zAt=~oK;}e|W^zClGKpYDt$z95(q&JGMA8fo2BIM?L*aL9?f3gQb!%yDE$`De684i2 zq!oT3lT;0Rz%o#}$;5C)G4-&rC=`@d=p1R56;?z)`m2PQSKOE1Z`iK7DzMAT2`hFI z?r4l{!tC@6o`gqkJ2x-4dhMsr-E{?z|Ms`P#ft+OB9jp#GsE*8Q8@YJlM%^ZeDTG1 ze2-4#|I2w7wlp>3ltQQpqEEsPC7>XvPx8gy0tYHTKFBm)oD}YfOEc#F zs_fti4b|UZu=#lrA{_}EP0T2Zgrc{5kjtQu|oLmAk zQru=?iV91llgJkPvJZ^P^ zZo zr(xE{ten*)NTix5oghEXy1aQ8&)%|W9Rh$_LSY?tbiqyEK7CgI{qHS1>caugz_DXS zj~OjXe%!8&>(*@Cux{dsi7J$j?EzA8g#&*;g!Sr$=dJ{BQ~sGw_)wq z{rmMJg6z~iT@g%o%&JwZI6msAqc9qJQS)pL``&*0ZNk#A$Ng~lQU45l`FXiCFBQO= zK*nSr4QeJ6>BNa9@GzW5lJ00|XlmLe?R4^#+L>kYI!(WUZ24KNFe zis#Hee#iE@C!Tl$_OUQhliLa(CW4{dwcv@e($XP=2jd)CTbi3&nxk#4tbqhd`aleY zzOs_!OE^WW`h9+maU0w~@%UwkgOcaX>7P7wGS#khM)ngjGb%C?GT}?~DOq0ieXLSH z?zrP7op?dz5hv#51k(vyNyBPvYnqny$x!>oWd+t|vKQNGWf0dOiUSh>Q zMngu2Ef#BQ2dB0ui!<9}Fua@WT(u*W*<)T!guABSCU-0=DHh4j~P31#PFh` zLW8{N7*arHA%l1!6Q60*G=P%|r?!+g>V~gYZZ27}gi#TDr&ekcj%+5S!wLBSS*;~< z5shLJ*|N9@p=WC{mQ`Rn(P#E@o4J#3CF(G`$rUhnn)}T~)V$AjrUyk^rBmc0O?__3 z^qPW9gd_(RRKmIF?5);2y{Rm1Y^ZnH{Qk%ivBt+IRZ@k4IWyEK(R4W-GK~)4Kvz!o zAlXB9fI`nZ?>t>9M--4=>iTW?_yHN=i^yYI1t@ZWAR^#XXyl3kR}SRVfN0Q^8$>^w zSyTxXfy_j526U<|-x|0{#Yu8p9wE}?S@wdRl*JdOMyjH^<`?uwdCg5bbq-HZGos8) ze(#QXGfCGCj%B-*3AXj?*CSy0X)FiKRci3A_d4*I^)<}4gjn>VlwlczbgT(50**XZ zQJ#SpQq!=>x$aMWi%d7902h&?L_8j^NO^N75jbJF0H^Vgd_1rqaH73UI7Kp<7c0JHpzBG zC>e4h0?qYyhL2%OOePqj0R+bK39-U~BvpWP0U{?H2+A>^h@W3fXdWRF4zfIsnAoIb zg1HV*)PQQV z^hSI@HU*7>W(E$0FLPtoiJ3{#Ya~u+Cl&`H{Oqb{-HA!ET8yBAJ!R1`pbYL*fUnSZ zds%<8yPf!B93&HZI&x`MGC|2a-BU%o<+(fEte~@}_81X48?2Z%WV&jlAq-;9lY2CU zqd#_`>AX(dRC=9uIuU{C8^GwF^!u}e*uAl#dS?* zrb(TyNhZg&fzS