CLI: add option to decompress hanab.live JSON links

This allows easy conversion of shortened JSON links
to the full-fledged JSON game format, which can be
used with other programs

.gitignore

@@ -4,6 +4,7 @@ hanab.live
 venv/
 # pycache dir
 __pycache__
+test.py
 
 
 # a few output files

LICENSE

@@ -0,0 +1,674 @@
+                    GNU GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The GNU General Public License is a free, copyleft license for
+software and other kinds of works.
+
+  The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works.  By contrast,
+the GNU General Public License is intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.  We, the Free Software Foundation, use the
+GNU General Public License for most of our software; it applies also to
+any other work released this way by its authors.  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+  To protect your rights, we need to prevent others from denying you
+these rights or asking you to surrender the rights.  Therefore, you have
+certain responsibilities if you distribute copies of the software, or if
+you modify it: responsibilities to respect the freedom of others.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must pass on to the recipients the same
+freedoms that you received.  You must make sure that they, too, receive
+or can get the source code.  And you must show them these terms so they
+know their rights.
+
+  Developers that use the GNU GPL protect your rights with two steps:
+(1) assert copyright on the software, and (2) offer you this License
+giving you legal permission to copy, distribute and/or modify it.
+
+  For the developers' and authors' protection, the GPL clearly explains
+that there is no warranty for this free software.  For both users' and
+authors' sake, the GPL requires that modified versions be marked as
+changed, so that their problems will not be attributed erroneously to
+authors of previous versions.
+
+  Some devices are designed to deny users access to install or run
+modified versions of the software inside them, although the manufacturer
+can do so.  This is fundamentally incompatible with the aim of
+protecting users' freedom to change the software.  The systematic
+pattern of such abuse occurs in the area of products for individuals to
+use, which is precisely where it is most unacceptable.  Therefore, we
+have designed this version of the GPL to prohibit the practice for those
+products.  If such problems arise substantially in other domains, we
+stand ready to extend this provision to those domains in future versions
+of the GPL, as needed to protect the freedom of users.
+
+  Finally, every program is threatened constantly by software patents.
+States should not allow patents to restrict development and use of
+software on general-purpose computers, but in those that do, we wish to
+avoid the special danger that patents applied to a free program could
+make it effectively proprietary.  To prevent this, the GPL assures that
+patents cannot be used to render the program non-free.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                       TERMS AND CONDITIONS
+
+  0. Definitions.
+
+  "This License" refers to version 3 of the GNU General Public License.
+
+  "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+  "The Program" refers to any copyrightable work licensed under this
+License.  Each licensee is addressed as "you".  "Licensees" and
+"recipients" may be individuals or organizations.
+
+  To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy.  The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+  A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+  To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy.  Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+  To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies.  Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+  An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License.  If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+  1. Source Code.
+
+  The "source code" for a work means the preferred form of the work
+for making modifications to it.  "Object code" means any non-source
+form of a work.
+
+  A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+  The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form.  A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+  The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities.  However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work.  For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+  The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+  The Corresponding Source for a work in source code form is that
+same work.
+
+  2. Basic Permissions.
+
+  All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met.  This License explicitly affirms your unlimited
+permission to run the unmodified Program.  The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work.  This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+  You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force.  You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright.  Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+  Conveying under any other circumstances is permitted solely under
+the conditions stated below.  Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+  3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+  No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+  When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+  4. Conveying Verbatim Copies.
+
+  You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+  You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+  5. Conveying Modified Source Versions.
+
+  You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+    a) The work must carry prominent notices stating that you modified
+    it, and giving a relevant date.
+
+    b) The work must carry prominent notices stating that it is
+    released under this License and any conditions added under section
+    7.  This requirement modifies the requirement in section 4 to
+    "keep intact all notices".
+
+    c) You must license the entire work, as a whole, under this
+    License to anyone who comes into possession of a copy.  This
+    License will therefore apply, along with any applicable section 7
+    additional terms, to the whole of the work, and all its parts,
+    regardless of how they are packaged.  This License gives no
+    permission to license the work in any other way, but it does not
+    invalidate such permission if you have separately received it.
+
+    d) If the work has interactive user interfaces, each must display
+    Appropriate Legal Notices; however, if the Program has interactive
+    interfaces that do not display Appropriate Legal Notices, your
+    work need not make them do so.
+
+  A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit.  Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+  6. Conveying Non-Source Forms.
+
+  You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+    a) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by the
+    Corresponding Source fixed on a durable physical medium
+    customarily used for software interchange.
+
+    b) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by a
+    written offer, valid for at least three years and valid for as
+    long as you offer spare parts or customer support for that product
+    model, to give anyone who possesses the object code either (1) a
+    copy of the Corresponding Source for all the software in the
+    product that is covered by this License, on a durable physical
+    medium customarily used for software interchange, for a price no
+    more than your reasonable cost of physically performing this
+    conveying of source, or (2) access to copy the
+    Corresponding Source from a network server at no charge.
+
+    c) Convey individual copies of the object code with a copy of the
+    written offer to provide the Corresponding Source.  This
+    alternative is allowed only occasionally and noncommercially, and
+    only if you received the object code with such an offer, in accord
+    with subsection 6b.
+
+    d) Convey the object code by offering access from a designated
+    place (gratis or for a charge), and offer equivalent access to the
+    Corresponding Source in the same way through the same place at no
+    further charge.  You need not require recipients to copy the
+    Corresponding Source along with the object code.  If the place to
+    copy the object code is a network server, the Corresponding Source
+    may be on a different server (operated by you or a third party)
+    that supports equivalent copying facilities, provided you maintain
+    clear directions next to the object code saying where to find the
+    Corresponding Source.  Regardless of what server hosts the
+    Corresponding Source, you remain obligated to ensure that it is
+    available for as long as needed to satisfy these requirements.
+
+    e) Convey the object code using peer-to-peer transmission, provided
+    you inform other peers where the object code and Corresponding
+    Source of the work are being offered to the general public at no
+    charge under subsection 6d.
+
+  A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+  A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling.  In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage.  For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product.  A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+  "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source.  The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+  If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information.  But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+  The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed.  Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+  Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+  7. Additional Terms.
+
+  "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law.  If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+  When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it.  (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.)  You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+  Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+    a) Disclaiming warranty or limiting liability differently from the
+    terms of sections 15 and 16 of this License; or
+
+    b) Requiring preservation of specified reasonable legal notices or
+    author attributions in that material or in the Appropriate Legal
+    Notices displayed by works containing it; or
+
+    c) Prohibiting misrepresentation of the origin of that material, or
+    requiring that modified versions of such material be marked in
+    reasonable ways as different from the original version; or
+
+    d) Limiting the use for publicity purposes of names of licensors or
+    authors of the material; or
+
+    e) Declining to grant rights under trademark law for use of some
+    trade names, trademarks, or service marks; or
+
+    f) Requiring indemnification of licensors and authors of that
+    material by anyone who conveys the material (or modified versions of
+    it) with contractual assumptions of liability to the recipient, for
+    any liability that these contractual assumptions directly impose on
+    those licensors and authors.
+
+  All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10.  If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term.  If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+  If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+  Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+  8. Termination.
+
+  You may not propagate or modify a covered work except as expressly
+provided under this License.  Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+  However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+  Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+  Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License.  If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+  9. Acceptance Not Required for Having Copies.
+
+  You are not required to accept this License in order to receive or
+run a copy of the Program.  Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance.  However,
+nothing other than this License grants you permission to propagate or
+modify any covered work.  These actions infringe copyright if you do
+not accept this License.  Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+  10. Automatic Licensing of Downstream Recipients.
+
+  Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License.  You are not responsible
+for enforcing compliance by third parties with this License.
+
+  An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations.  If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+  You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License.  For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+  11. Patents.
+
+  A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based.  The
+work thus licensed is called the contributor's "contributor version".
+
+  A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version.  For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+  Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+  In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement).  To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+  If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients.  "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+
+  If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+  A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License.  You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+  Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+  12. No Surrender of Others' Freedom.
+
+  If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all.  For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+  13. Use with the GNU Affero General Public License.
+
+  Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU Affero General Public License into a single
+combined work, and to convey the resulting work.  The terms of this
+License will continue to apply to the part which is the covered work,
+but the special requirements of the GNU Affero General Public License,
+section 13, concerning interaction through a network will apply to the
+combination as such.
+
+  14. Revised Versions of this License.
+
+  The Free Software Foundation may publish revised and/or new versions of
+the GNU General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+  Each version is given a distinguishing version number.  If the
+Program specifies that a certain numbered version of the GNU General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation.  If the Program does not specify a version number of the
+GNU General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+  If the Program specifies that a proxy can decide which future
+versions of the GNU General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+  Later license versions may give you additional or different
+permissions.  However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+  15. Disclaimer of Warranty.
+
+  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. Limitation of Liability.
+
+  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+  17. Interpretation of Sections 15 and 16.
+
+  If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+                     END OF TERMS AND CONDITIONS
+
+            How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    Hanabi
+    Copyright (C) 2023  Maximilian Keßler
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+Also add information on how to contact you by electronic and paper mail.
+
+  If the program does terminal interaction, make it output a short
+notice like this when it starts in an interactive mode:
+
+    <program>  Copyright (C) 2023  Maximilian Keßler
+    This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, your program's commands
+might be different; for a GUI interface, you would use an "about box".
+
+  You should also get your employer (if you work as a programmer) or school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.
+For more information on this, and how to apply and follow the GNU GPL, see
+<https://www.gnu.org/licenses/>.
+
+  The GNU General Public License does not permit incorporating your program
+into proprietary programs.  If your program is a subroutine library, you
+may consider it more useful to permit linking proprietary applications with
+the library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.  But first, please read
+<https://www.gnu.org/licenses/why-not-lgpl.html>.

README.md

@@ -1,10 +1,9 @@
 # Hanabi-Suite
 
-Disclaimer: This repository is still not in a good cleaned up code style, mainly due to me lacking time to clean stuff up properly
+Disclaimer: This repository is still not in a good cleaned up code style, mainly due to me lacking time to clean stuff up properly.
-Do not expect everything to work, do not expect everything to be well-documented
+Do not expect everything to work, do not expect everything to be well-documented.
 However, I try to improve this from now on so that eventually, reasonable interfaces will exist so that this becomes actually more usable than now
 
-Generally speaking, stuff that is already in a proper package/subfolder should be alright and I plan to keep it clean (also with a clean git history)
 
 ## What is this?
 
@@ -38,5 +37,48 @@ Apart from the obvious use-cases for some features, I want to explore boundaries
 - Analyse every seed on hanab.live for feasibility
 
 
+## Installation
+
+### Python
+The hanabi folder is a working python package that you should be able to import if it's in your python path.
+You will need to install the `requirements.txt` as usual, I recommend setting up a `venv`:
+```
+python -m venv venv
+source venv/bin/activate
+pip install -r requirements.txt
+```
+
+### SAT-solver
+After installing python, you should have installed `pysmt` with it, an interface to use SAT-solvers with python.
+We still need a solver, for this, run
+```
+$ pysmt-install --help
+// Pick a solver, e.g. z3 works
+$ pysmt-install --z3
+```
+
+### PostgreSQL
+You need to install PostgreSQL on your system, for installation instructions refer to your distribution.
+Create a new database and user, for example:
+```
+$ sudo -iu postgres
+$ psql
+# CREATE USER hanabi WITH PASSWORD 'Insert password here';
+# CREATE DATABASE "hanab-live" with owner "hanabi";
+```
+Put the connection parameters in a config file (for the format, see `example_config.yaml`).
+This should be located at your system default for the application `hanabi-suite`,
+on POSIX systems this should be `~/.config/hanabi-suite/config.yaml`.
+
+
 ## Usage of stuff that already works:
-Use the `hanabi_suite.py` CLI interface to download games and analyze them
+Use the `hanabi_suite.py` CLI interface to download games and analyze them.
+An initial setup might look like this:
+
+```
+hanabi_cli.py gen-config                    // Generates configuration file for DB connection parameters and prints its location
+<Edit your configuration file>
+hanabi_cli.py init                          // Initializes database tables
+hanabi_cli.py download --var 0              // Donwloads information on all 'No Variant' games
+hanabi_cli.py analyze --download <game id>  // Downloads and analyzes game from hanab.live
+```

cheating_strategy

@@ -1,54 +0,0 @@
-card types:
-trash, playable, useful (dispensable), critical
-
-
-pace          := #(cards left in deck) + #players - #(cards left to play)
-modified_pace := pace - #(players without useful cards)
-endgame       := #(cards left to play) - #(cards left in deck)   = #players - pace
-  -> endgame >= 0    iff   pace <= #players
-in_endgame    := endgame >= 0
-
-discard_badness(card) :=
-  1               if trash
-  8 - #players    if card useful but duplicate visible         # TODO: should probably account for rank of card as well, currently, lowest one is chosen
-  80 - 10*rank    if card is not critical but currently unique # this ensures we prefer to discard higher ranked cards
-  600 - 100*rank  if only criticals in hand                    # essentially not relevant, since we are currently only optimizing for full score 
-  
- 
-Algorithm: 
-
-if (have playable card):
-  if (in endgame) and not (in extraround):
-    stall in the following situations:
-      - we have exactly one useful card, it is a 5, and a copy of each useful card is visible
-      - we have exactly one useful card, it is a 4, the player with the matching 5 has another critical card to play
-      - we have exactly one useful card (todo: maybe use critical here?), the deck has size 1, someone else has 2 crits
-      - we have exactly one playable card, it is a 4, and a further useful card, but the playable is redistributable in the following sense:
-          the other playing only has this one useful card, and the player holding the matching 5 sits after the to-be-redistributed player
-      - sth else that seems messy and is currently not understood, ignored for now
-  TODO: maybe introduce some midgame stalls here, since we know the deck?
-  play a card, matching the first of the following criteria. if several cards match, recurse with this set of cards
-    - if in extraround, play crit
-    - if in second last round and we have 2 crits, play crit
-    - play card with lowest rank
-    - play a critical card
-    - play unique card, i.e. not visible
-    - lowest suit index (for determinancy)
-
-if 8 hints:
-  give a hint
-
-if 0 hints:
-  discard card with lowest badness
-
-stall in the following situations:
-  - #(cards in deck) == 2 and (card of rank 3 or lower is missing) and we have the connecting card
-  - #clues >= 8 - #(useful cards in hand), there are useful cards in the deck and either:
-    - the next player has no useful cards at all
-    - we have two more crits than the next player and they have trash
-  - we are in endgame and the deck only contains one card
-  - it is possible that no-one discards in the following round and we are not waiting for a card whose rank is smaller than pace   // TODO: this feels like a weird condition
-
-discard if (discard badness) + #hints < 10
-
-stall if someone has a better discard

compress.py

@@ -1,250 +0,0 @@
-#! /bin/python3
-import json
-import sys
-import more_itertools
-
-from enum import Enum
-from termcolor import colored
-from typing import List, Optional, Union
-
-from variants import variant_id, variant_name
-from hanabi import DeckCard, ActionType, Action, GameState, HanabiInstance
-from hanab_live import HanabLiveGameState, HanabLiveInstance
-
-
-# use same BASE62 as on hanab.live to encode decks
-BASE62 = "abcdefghijklmnopqrstuvwxyz0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ";
-
-
-# Helper method, iterate over chunks of length n in a string
-def chunks(s: str, n: int):
-    for i in range(0, len(s), n):
-        yield s[i:i+n]
-
-
-# exception thrown by decompression methods if parsing fails
-class InvalidFormatError(ValueError):
-        pass
-
-
-def compress_actions(actions: List[Action], game_id=None) -> str:
-    minType = 0
-    maxType = 0
-    if len(actions) != 0:
-        minType = min(map(lambda a: a.type.value, actions))
-        maxType = max(map(lambda a: a.type.value, actions))
-    typeRange = maxType - minType + 1
-
-    def compress_action(action):
-        ## We encode action values with +1 to differentiate 
-        # null (encoded 0) and 0 (encoded 1)
-        value = 0 if action.value is None else action.value + 1
-        if action.type == ActionType.VoteTerminate:
-            # This is currently a hack, the actual format has a 10 here
-            # but we cannot encode this
-            value = 0
-        try:
-            a = BASE62[typeRange * value + (action.type.value - minType)]
-            b = BASE62[action.target]
-        except IndexError as e:
-            raise ValueError("Encoding action failed, value too large, found {}".format(value)) from e
-        return a + b
-
-    return "{}{}{}".format(
-            minType,
-            maxType,
-            ''.join(map(compress_action, actions))
-    )
-
-
-def decompress_actions(actions_str: str) -> List[Action]:
-    if not len(actions_str) >= 2:
-        raise InvalidFormatError("min/max range not specified, found: {}".format(actions_str))
-    try:
-        minType = int(actions_str[0])
-        maxType = int(actions_str[1])
-    except ValueError as e:
-        raise InvalidFormatError(
-                "min/max range of actions not specified, expected two integers, found {}".format(actions_str[:2])
-        ) from e
-    if not minType <= maxType:
-        raise InvalidFormatError("min/max range illegal, found [{},{}]".format(minType, maxType))
-    typeRange = maxType - minType + 1
-
-    if not len(actions_str) % 2 == 0:
-        raise InvalidFormatError("Invalid action string length: Expected even number of characters")
-
-    for (index, char) in enumerate(actions_str[2:]):
-        if not char in BASE62:
-            raise InvalidFormatError(
-                    "Invalid character at index {}: Found {}, expected one of {}".format(
-                        index, char, BASE62
-                        )
-            )
-
-    def decompress_action(index, action):
-        try:
-            action_type_value = (BASE62.index(action[0]) % typeRange) + minType
-            action_type = ActionType(action_type_value)
-        except ValueError as e:
-            raise InvalidFormatError(
-                    "Invalid action type at action {}: Found {}, expected one of {}".format(
-                        index, action_type_value,
-                        [action_type.value for action_type in ActionType]
-                        )
-            ) from e
-        ## We encode values with +1 to differentiate null (encoded 0) and 0 (encoded 1)
-        value = BASE62.index(action[0]) // typeRange - 1
-        if value == -1:
-            value = None
-        if action_type in [ActionType.Play, ActionType.Discard]:
-            if value is not None:
-                raise InvalidFormatError(
-                        "Invalid action value: Action at action index {} is Play/Discard, expected value None, found: {}".format(index, value)
-                )
-        target = BASE62.index(action[1])
-        return Action(action_type, target, value)
-
-    return [decompress_action(idx, a) for (idx, a) in enumerate(chunks(actions_str[2:], 2))]
-
-
-def compress_deck(deck: List[DeckCard]) -> str:
-    assert(len(deck) != 0)
-    minRank = min(map(lambda c: c.rank, deck))
-    maxRank = max(map(lambda c: c.rank, deck))
-    rankRange = maxRank - minRank + 1
-
-    def compress_card(card):
-        try:
-            return BASE62[rankRange * card.suitIndex + (card.rank - minRank)]
-        except IndexError as e:
-            raise InvalidFormatError(
-                    "Could not compress card, suit or rank too large. Found: {}".format(card)
-            ) from e
-    return "{}{}{}".format(
-            minRank,
-            maxRank,
-            ''.join(map(compress_card, deck))
-    )
-
-
-def decompress_deck(deck_str: str) -> List[DeckCard]:
-    if len(deck_str) < 2:
-        raise InvalidFormatError("min/max rank range not specified, found: {}".format(deck_str))
-    try:
-        minRank = int(deck_str[0])
-        maxRank = int(deck_str[1])
-    except ValueError as e:
-        raise InvalidFormatError(
-                "min/max rank range not specified, expected two integers, found {}".format(deck_str[:2])
-        ) from e
-    if not maxRank >= minRank:
-        raise InvalidFormatError(
-                "Invalid rank range, found [{},{}]".format(minRank, maxRank)
-        )
-    rankRange = maxRank - minRank + 1
-
-    for (index, char) in enumerate(deck_str[2:]):
-        if not char in BASE62:
-            raise InvalidFormatError(
-                    "Invalid character at index {}: Found {}, expected one of {}".format(
-                        index, char, BASE62
-                        )
-            )
-
-    def decompress_card(card_char):
-        index = BASE62.index(card_char)
-        suitIndex = index // rankRange
-        rank = index % rankRange + minRank
-        return DeckCard(suitIndex, rank)
-
-    return [decompress_card(c) for c in deck_str[2:]]
-
-
-# compresses a standard GameState object into hanab.live format
-# which can be used in json replay links
-# The GameState object has to be standard / fitting hanab.live variants,
-# otherwise compression is not possible
-def compress_game_state(state: Union[GameState, HanabLiveGameState]) -> str:
-    var_id = -1
-    if isinstance(state, HanabLiveGameState):
-        var_id = state.instance.variant_id
-    else:
-        assert isinstance(state, GameState)
-        var_id = HanabLiveInstance.select_standard_variant_id(state.instance)
-    out = "{}{},{},{}".format(
-            state.instance.num_players,
-            compress_deck(state.instance.deck),
-            compress_actions(state.actions),
-            var_id
-            )
-    with_dashes = ''.join(more_itertools.intersperse("-", out, 20))
-    return with_dashes
-
-
-def decompress_game_state(game_str: str) -> GameState:
-    game_str = game_str.replace("-", "")
-    parts = game_str.split(",")
-    if not len(parts) == 3:
-        raise InvalidFormatError(
-                "Expected 3 comma-separated parts of game, found {}".format(
-                    len(parts)
-                )
-        )
-    [players_deck, actions, variant_id] = parts
-    if len(players_deck) == 0:
-        raise InvalidFormatError("Expected nonempty first part")
-    try:
-        num_players = int(players_deck[0])
-    except ValueError as e:
-        raise InvalidFormatError(
-            "Expected number of players, found: {}".format(players_deck[0])
-        ) from e
-
-    try:
-        deck = decompress_deck(players_deck[1:])
-    except InvalidFormatError as e:
-        raise InvalidFormatError("Error while parsing deck") from e
-
-    try:
-        actions = decompress_actions(actions)
-    except InvalidFormatError as e:
-        raise InvalidFormatError("Error while parsing actions") from e
-
-    try:
-        variant_id = int(variant_id)
-    except ValueError:
-        raise ValueError("Expected variant id, found: {}".format(variant_id))
-
-    instance = HanabiInstance(deck, num_players)
-    game = GameState(instance)
-    
-    # TODO: game is not in consistent state
-    game.actions = actions
-    return game
-
-
-def link(game_state: GameState) -> str:
-    compressed = compress_game_state(game_state)
-    return "https://hanab.live/shared-replay-json/{}".format(compressed)
-
-
-# add link method to GameState class
-GameState.link = link
-
-
-
-if __name__ == "__main__":
-    for arg in sys.argv[1:]:
-        deck = decompress_deck(arg)
-        c = compress_deck(deck)
-        assert(c == arg)
-        print(deck)
-        
-        inst = HanabiInstance(deck, 5, variant_id = 32)
-        game = GameState(inst)
-        game.play(1)
-        game.play(5)
-        game.clue()
-        print(game.link())
-

database/__init__.py

@@ -1 +0,0 @@
-from .database import cur, conn

database/database.py

@@ -1,79 +0,0 @@
-import psycopg2
-from typing import Optional, Dict
-
-# global connection
-conn = psycopg2.connect("dbname=hanab-live-2 user=postgres")
-
-# cursor
-cur = conn.cursor()
-
-
-# init_database_tables()
-# populate_static_tables()
-
-
-class Game():
-    def __init__(self, info=None):
-        self.id = -1
-        self.num_players = -1
-        self.score = -1
-        self.seed = ""
-        self.variant_id = -1
-        self.deck_plays = None
-        self.one_extra_card = None
-        self.one_less_card = None
-        self.all_or_nothing = None
-        self.num_turns = None
-        if type(info) == dict:
-            self.__dict__.update(info)
-
-    @staticmethod
-    def from_tuple(t):
-        g = Game()
-        g.id = t[0]
-        g.num_players = t[1]
-        g.score = t[2]
-        g.seed = t[3]
-        g.variant_id = t[4]
-        g.deck_plays = t[5]
-        g.one_extra_card = t[6]
-        g.one_less_card = t[7]
-        g.all_or_nothing = t[8]
-        g.num_turns = t[9]
-        return g
-
-    def __eq__(self, other):
-        return self.__dict__ == other.__dict__
-
-
-def load(game_id: int) -> Optional[Game]:
-    cur.execute("SELECT * from games WHERE id = {};".format(game_id))
-    a = cur.fetchone()
-    if a is None:
-        return None
-    else:
-        return Game.from_tuple(a)
-
-
-def store(game: Game):
-    stored = load(game.id)
-    if stored is None:
-        #        print("inserting game with id {} into DB".format(game.id))
-        cur.execute(
-            "INSERT INTO games"
-            "(id, num_players, score, seed, variant_id)"
-            "VALUES"
-            "(%s, %s, %s, %s, %s);",
-            (game.id, game.num_players, game.score, game.seed, game.variant_id)
-        )
-        print("Inserted game with id {}".format(game.id))
-    else:
-        pass
-#        if not stored == game:
-#            print("Already stored game with id {}, aborting".format(game.id))
-#            print("Stored game is: {}".format(stored.__dict__))
-#            print("New game is:    {}".format(game.__dict__))
-
-
-def commit():
-    conn.commit()

database/games_seeds_schema.sql

@@ -1,30 +0,0 @@
-DROP TABLE IF EXISTS seeds CASCADE;
-CREATE TABLE seeds (
-    seed                    TEXT        NOT NULL PRIMARY KEY,
-    num_players             SMALLINT    NOT NULL,
-    variant_id              SMALLINT    NOT NULL,
-    deck                    VARCHAR(62) NOT NULL,
-    feasible                BOOLEAN     DEFAULT NULL,
-    max_score_theoretical   SMALLINT
-);
-CREATE INDEX seeds_variant_idx ON seeds (variant_id);
-
-
-DROP TABLE IF EXISTS games CASCADE;
-CREATE TABLE games (
-    id              INT      PRIMARY KEY,
-    seed            TEXT     NOT NULL REFERENCES seeds,
-    num_players     SMALLINT NOT NULL,
-    starting_player SMALLINT NOT NULL DEFAULT 0,
-    score           SMALLINT NOT NULL,
-    variant_id      SMALLINT NOT NULL,
-    deck_plays      BOOLEAN,
-    one_extra_card  BOOLEAN,
-    one_less_card   BOOLEAN,
-    all_or_nothing  BOOLEAN,
-    num_turns       SMALLINT,
-    actions         TEXT
-);
-CREATE INDEX games_seed_score_idx ON games (seed, score);
-CREATE INDEX games_var_seed_idx ON games (variant_id, seed);
-CREATE INDEX games_player_idx ON games (num_players);

deck_analyzer.py

@@ -1,220 +0,0 @@
-from compress import DeckCard
-from typing import List
-from enum import Enum
-
-from database import conn
-from hanabi import HanabiInstance, pp_deck
-from compress import decompress_deck
-import constants
-
-
-class InfeasibilityType(Enum):
-    OutOfPace = 0           # idx denotes index of last card drawn before being forced to reduce pace, value denotes how bad pace is
-    OutOfHandSize = 1       # idx denotes index of last card drawn before being forced to discard a crit
-    NotTrivial = 2
-    CritAtBottom = 3
-
-
-class InfeasibilityReason():
-    def __init__(self, infeasibility_type, idx, value=None):
-        self.type = infeasibility_type
-        self.index = idx
-        self.value = value
-
-    def __repr__(self):
-        match self.type:
-            case InfeasibilityType.OutOfPace:
-                return "Deck runs out of pace ({}) after drawing card {}".format(self.value, self.index)
-            case InfeasibilityType.OutOfHandSize:
-                return "Deck runs out of hand size after drawing card {}".format(self.index)
-            case InfeasibilityType.CritAtBottom:
-                return "Deck has crit non-5 at bottom (index {})".format(self.index)
-
-
-def analyze_suit(occurrences):
-    # denotes the indexes of copies we can use wlog
-    picks = {
-            1: 0,
-            **{ r: None for r in range(2, 5) },
-            5: 0
-    }
-
-    # denotes the intervals when cards will be played wlog
-    play_times = {
-            1: [occurrences[1][0]],
-            **{ r: None for _ in range(instance.num_suits)
-                for r in range(2,6)
-              }
-    }
-
-    print("occurrences are: {}".format(occurrences))
-
-    for rank in range(2, 6):
-
-        # general analysis
-        earliest_play = max(min(play_times[rank - 1]), min(occurrences[rank]))
-        latest_play = max( *play_times[rank - 1], *occurrences[rank])
-        play_times[rank] = [earliest_play, latest_play]
-
-        # check a few extra cases regarding the picks when the rank is not 5
-        if rank != 5:
-            # check if we can just play the first copy
-            if max(play_times[rank - 1]) < min(occurrences[rank]):
-                picks[rank] = 0
-                play_times[rank] = [min(occurrences[rank])]
-                continue
-
-
-            # check if the second copy is not worse than the first when it comes,
-            # because we either have to wait for smaller cards anyway
-            # or the next card is not there anyway
-            if max(occurrences[rank]) < max(earliest_play,  min(occurrences[rank + 1])):
-                picks[rank] = 1
-
-
-    return picks, play_times
-
-
-
-def analyze_card_usage(instance: HanabiInstance):
-    storage_size = instance.num_players * instance.hand_size
-    for suit in range(instance.num_suits):
-        print("analysing suit {}: {}".format(
-            suit,
-            pp_deck((c for c in instance.deck if c.suitIndex == suit))
-            )
-        )
-
-        occurrences = {
-                rank: [max(0, i - storage_size + 1) for (i, card) in enumerate(instance.deck) if card == DeckCard(suit, rank)]
-                for rank in range(1,6)
-        }
-
-        picks, play_times = analyze_suit(occurrences)
-
-        print("did analysis:")
-        print("play times: ", play_times)
-        print("picks: ", picks)
-        print()
-
-
-
-def analyze(instance: HanabiInstance, find_non_trivial=False) -> InfeasibilityReason | None:
-
-    if instance.deck[-1].rank != 5 and instance.deck[-1].suitIndex + instance.num_dark_suits >= instance.num_suits:
-        return InfeasibilityReason(InfeasibilityType.CritAtBottom, instance.deck_size - 1)
-
-    # we will sweep through the deck and pretend that we instantly play all cards
-    # as soon as we have them (and recurse this)
-    # this allows us to detect standard pace issue arguments
-
-    stacks = [0] * instance.num_suits
-    stored_cards = set()
-    stored_crits = set()
-
-    min_forced_pace = 100
-    worst_index = 0
-
-    ret = None
-
-    for (i, card) in enumerate(instance.deck):
-        if card.rank == stacks[card.suitIndex] + 1:
-            # card is playable
-            stacks[card.suitIndex] += 1
-            # check for further playables that we stored
-            for check_rank in range(card.rank + 1, 6):
-                check_card = DeckCard(card.suitIndex, check_rank)
-                if check_card in stored_cards:
-                    stacks[card.suitIndex] += 1
-                    stored_cards.remove(check_card)
-                    if check_card in stored_crits:
-                        stored_crits.remove(check_card)
-                else:
-                    break
-        elif card.rank <= stacks[card.suitIndex]:
-            pass # card is trash
-        elif card.rank > stacks[card.suitIndex] + 1:
-            # need to store card
-            if card in stored_cards or card.rank == 5:
-                stored_crits.add(card)
-            stored_cards.add(card)
-        
-        ## check for out of handsize:
-        if len(stored_crits) == instance.num_players * instance.hand_size:
-            return InfeasibilityReason(InfeasibilityType.OutOfHandSize, i)
-
-        if find_non_trivial and len(stored_cards) == instance.num_players * instance.hand_size:
-            ret =  InfeasibilityReason(InfeasibilityType.NotTrivial, i)
-
-        # the last - 1 is there because we have to discard 'next', causing a further draw
-        max_remaining_plays = (instance.deck_size - i - 1) + instance.num_players - 1
-
-        needed_plays = 5 * instance.num_suits - sum(stacks)
-        missing =  max_remaining_plays - needed_plays
-        if missing < min_forced_pace:
-#            print("update to {}: {}".format(i, missing))
-            min_forced_pace = missing
-            worst_index = i
-
-    # check that we correctly walked through the deck
-    assert(len(stored_cards) == 0)
-    assert(len(stored_crits) == 0)
-    assert(sum(stacks) == 5 * instance.num_suits)
-
-    if min_forced_pace < 0: 
-        return InfeasibilityReason(InfeasibilityType.OutOfPace, worst_index, min_forced_pace)
-    elif ret is not None:
-        return ret
-    else:
-        return None
-
-
-def run_on_database():
-    cur = conn.cursor()
-    cur2 = conn.cursor()
-    for num_p in range(2, 6):
-        cur.execute("SELECT seed, num_players, deck from seeds where variant_id = 0 and num_players = (%s) order by seed asc", (num_p,))
-        res = cur.fetchall()
-        hand = 0
-        pace = 0
-        non_trivial = 0
-        d = None
-        print("Checking {} {}-player seeds from database".format(len(res), num_p))
-        for (seed, num_players, deck) in res:
-            deck = decompress_deck(deck)
-            a = analyze(HanabiInstance(deck, num_players), True)
-            if type(a) == InfeasibilityReason:
-                if a.type == InfeasibilityType.OutOfHandSize:
-    #                print("Seed {} infeasible: {}\n{}".format(seed, a, deck))
-                    hand += 1
-                elif a.type == InfeasibilityType.OutOfPace:
-                    pace += 1
-                elif a.type == InfeasibilityType.NotTrivial:
-                    non_trivial += 1
-                    d = seed, deck
-
-        print("Found {} seeds running out of hand size, {} running out of pace and {} that are not trivial".format(hand, pace, non_trivial))
-        if d is not None:
-            print("example non-trivial deck (seed {}): [{}]"
-                  .format(
-                      d[0],
-                      ", ".join(c.colorize() for c in d[1])
-                      )
-                  )
-        print()
-#        if p < 0:
-#            print("seed {} ({} players) runs out of pace ({}) after drawing {}: {}:\n{}".format(seed, num_players, p, i, deck[i], deck))
-#            cur.execute("UPDATE seeds SET feasible = f WHERE seed = (%s)", seed)
-
-if __name__ == "__main__":
-#    print(deck)
-#    a = analyze(deck, 4)
-#    print(a)
-#    run_on_database()
-    deck_str = "15bcfwnqsdmbnfuvhskrgfixwckklojxgemrhpqppuaaiyadultv"
-    deck_str = "15misofrmvvuxujkphaqpcflegysdwqaakcilbxtuhwfrbgdnpkn"
-    deck_str = "15wqpvhdkufjcrewyxulvarhgolkixmfgmndbpstqbupcanfisak"
-    deck = decompress_deck(deck_str)
-    print(pp_deck(deck))
-    instance = HanabiInstance(deck, 2)
-    analyze_card_usage(instance)

download_data.py

@@ -1,190 +0,0 @@
-import alive_progress
-from typing import Dict, Optional
-
-import psycopg2.errors
-
-from site_api import get, api, replay
-from database.database import Game, store, load, commit, conn, cur
-from compress import compress_deck, compress_actions, DeckCard, Action, InvalidFormatError
-from variants import variant_id, variant_name
-from hanab_live import HanabLiveInstance, HanabLiveGameState
-
-from log_setup import logger
-
-
-#
-def detailed_export_game(game_id: int, score: Optional[int] = None, var_id: Optional[int] = None,
-                         seed_exists: bool = False) -> None:
-    """
-    Downloads full details of game, inserts seed and game into DB
-    If seed is already present, it is left as is
-    If game is already present, game details will be updated
-
-    :param game_id:
-    :param score: If given, this will be inserted as score of the game. If not given, score is calculated
-    :param var_id If given, this will be inserted as variant id of the game. If not given, this is looked up
-    :param seed_exists: If specified and true, assumes that the seed is already present in database.
-        If this is not the case, call will raise a DB insertion error
-    """
-    logger.debug("Importing game {}".format(game_id))
-
-    assert_msg = "Invalid response format from hanab.live while exporting game id {}".format(game_id)
-
-    game_json = get("export/{}".format(game_id))
-    assert game_json.get('id') == game_id, assert_msg
-
-    players = game_json.get('players', [])
-    num_players = len(players)
-    seed = game_json.get('seed', None)
-    options = game_json.get('options', {})
-    var_id = var_id or variant_id(options.get('variant', 'No Variant'))
-    deck_plays = options.get('deckPlays', False)
-    one_extra_card = options.get('oneExtraCard', False)
-    one_less_card = options.get('oneLessCard', False)
-    all_or_nothing = options.get('allOrNothing', False)
-    starting_player = options.get('startingPlayer', 0)
-    actions = [Action.from_json(action) for action in game_json.get('actions', [])]
-    deck = [DeckCard.from_json(card) for card in game_json.get('deck', None)]
-
-    assert players != [], assert_msg
-    assert seed is not None, assert_msg
-
-    if score is None:
-        # need to play through the game once to find out its score
-        game = HanabLiveGameState(
-            HanabLiveInstance(
-                deck, num_players, var_id,
-                deck_plays=deck_plays,
-                one_less_card=one_less_card,
-                one_extra_card=one_extra_card,
-                all_or_nothing=all_or_nothing
-            ),
-            starting_player
-        )
-        print(game.instance.hand_size, game.instance.num_players)
-        for action in actions:
-            game.make_action(action)
-        score = game.score
-
-    try:
-        compressed_deck = compress_deck(deck)
-    except InvalidFormatError:
-        logger.error("Failed to compress deck while exporting game {}: {}".format(game_id, deck))
-        raise
-    try:
-        compressed_actions = compress_actions(actions)
-    except InvalidFormatError:
-        logger.error("Failed to compress actions while exporting game {}".format(game_id))
-        raise
-
-    if not seed_exists:
-        cur.execute(
-            "INSERT INTO seeds (seed, num_players, variant_id, deck)"
-            "VALUES (%s, %s, %s, %s)"
-            "ON CONFLICT (seed) DO NOTHING",
-            (seed, num_players, var_id, compressed_deck)
-        )
-        logger.debug("New seed {} imported.".format(seed))
-
-    cur.execute(
-        "INSERT INTO games ("
-        "id, num_players, starting_player, score, seed, variant_id, deck_plays, one_extra_card, one_less_card,"
-        "all_or_nothing, actions"
-        ")"
-        "VALUES (%s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s)"
-        "ON CONFLICT (id) DO UPDATE SET ("
-        "deck_plays, one_extra_card, one_less_card, all_or_nothing, actions"
-        ") = ("
-        "EXCLUDED.deck_plays, EXCLUDED.one_extra_card, EXCLUDED.one_less_card, EXCLUDED.all_or_nothing,"
-        "EXCLUDED.actions"
-        ")",
-        (
-            game_id, num_players, starting_player, score, seed, var_id, deck_plays, one_extra_card, one_less_card,
-            all_or_nothing, compressed_actions
-        )
-    )
-    logger.debug("Imported game {}".format(game_id))
-
-
-def process_game_row(game: Dict, var_id):
-    game_id = game.get('id', None)
-    seed = game.get('seed', None)
-    num_players = game.get('num_players', None)
-    score = game.get('score', None)
-
-    if any(v is None for v in [game_id, seed, num_players, score]):
-        raise ValueError("Unknown response format on hanab.live")
-
-    cur.execute("SAVEPOINT seed_insert")
-    try:
-        cur.execute(
-            "INSERT INTO games (id, seed, num_players, score, variant_id)"
-            "VALUES"
-            "(%s, %s ,%s ,%s ,%s)"
-            "ON CONFLICT (id) DO NOTHING",
-            (game_id, seed, num_players, score, var_id)
-        )
-    except psycopg2.errors.ForeignKeyViolation:
-        cur.execute("ROLLBACK TO seed_insert")
-        detailed_export_game(game_id, score, var_id)
-    cur.execute("RELEASE seed_insert")
-    logger.debug("Imported game {}".format(game_id))
-
-
-def download_games(var_id):
-    name = variant_name(var_id)
-    page_size = 100
-    if name is None:
-        raise ValueError("{} is not a known variant_id.".format(var_id))
-
-    url = "variants/{}".format(var_id)
-    r = api(url, refresh=True)
-    if not r:
-        raise RuntimeError("Failed to download request from hanab.live")
-
-    num_entries = r.get('total_rows', None)
-    if num_entries is None:
-        raise ValueError("Unknown response format on hanab.live")
-
-    cur.execute(
-        "SELECT COUNT(*) FROM games WHERE variant_id = %s AND id <= "
-        "(SELECT COALESCE (last_game_id, 0) FROM variant_game_downloads WHERE variant_id = %s)",
-        (var_id, var_id)
-    )
-    num_already_downloaded_games = cur.fetchone()[0]
-    assert num_already_downloaded_games <= num_entries, "Database inconsistent, too many games present."
-    next_page = num_already_downloaded_games // page_size
-    last_page = (num_entries - 1) // page_size
-
-    if num_already_downloaded_games == num_entries:
-        logger.info("Already downloaded all games ({} many) for variant {} [{}]".format(num_entries, var_id, name))
-        return
-    logger.info(
-        "Downloading remaining {} (total {}) entries for variant {} [{}]".format(
-            num_entries - num_already_downloaded_games, num_entries, var_id, name
-        )
-    )
-
-    with alive_progress.alive_bar(
-            total=num_entries - num_already_downloaded_games,
-            title='Downloading games for variant id {} [{}]'.format(var_id, name),
-            enrich_print=False
-    ) as bar:
-        for page in range(next_page, last_page + 1):
-            r = api(url + "?col[0]=0&page={}".format(page), refresh=page == last_page)
-            rows = r.get('rows', [])
-            if page == next_page:
-                rows = rows[num_already_downloaded_games % 100:]
-            if not (page == last_page or len(rows) == page_size):
-                logger.warn('WARN: received unexpected row count ({}) on page {}'.format(len(rows), page))
-            for row in rows:
-                process_game_row(row, var_id)
-                bar()
-            cur.execute(
-                "INSERT INTO variant_game_downloads (variant_id, last_game_id) VALUES"
-                "(%s, %s)"
-                "ON CONFLICT (variant_id) DO UPDATE SET last_game_id = EXCLUDED.last_game_id",
-                (var_id, r['rows'][-1]['id'])
-            )
-            conn.commit()
-

example_config.yaml

@@ -0,0 +1,3 @@
+dbname: hanab-live
+dbuser: hanabi
+dbpass: null

hanab_live.py

@@ -1,81 +0,0 @@
-from typing import List, Optional
-
-import hanabi
-import constants
-from variants import Variant
-
-
-class HanabLiveInstance(hanabi.HanabiInstance):
-    def __init__(
-            self,
-            deck: List[hanabi.DeckCard],
-            num_players: int,
-            variant_id: int,
-            one_extra_card: bool = False,
-            one_less_card: bool = False,
-            *args, **kwargs
-    ):
-        assert 2 <= num_players <= 6
-        hand_size = constants.HAND_SIZES[num_players]
-        if one_less_card:
-            hand_size -= 1
-        if one_extra_card:
-            hand_size += 1
-
-        super().__init__(deck, num_players, hand_size=hand_size, *args, **kwargs)
-        self.variant_id = variant_id
-        self.variant = Variant.from_db(self.variant_id)
-
-    @staticmethod
-    def select_standard_variant_id(instance: hanabi.HanabiInstance):
-        err_msg = "Hanabi instance not supported by hanab.live, cannot convert to HanabLiveInstance: "
-        assert 3 <= instance.num_suits <= 6, \
-            err_msg + "Illegal number of suits ({}) found, must be in range [3,6]".format(instance.num_suits)
-        assert 0 <= instance.num_dark_suits <= 2, \
-            err_msg + "Illegal number of dark suits ({}) found, must be in range [0,2]".format(instance.num_dark_suits)
-        assert 4 <= instance.num_suits - instance.num_dark_suits, \
-            err_msg + "Illegal ratio of dark suits to suits, can have at most {} dark suits with {} total suits".format(
-                max(instance.num_suits - 4, 0), instance.num_suits
-            )
-        return constants.VARIANT_IDS_STANDARD_DISTRIBUTIONS[instance.num_suits][instance.num_dark_suits]
-
-
-class HanabLiveGameState(hanabi.GameState):
-    def __init__(self, instance: HanabLiveInstance, starting_player: int = 0):
-        super().__init__(instance, starting_player)
-        self.instance: HanabLiveInstance = instance
-
-    def make_action(self, action):
-        match action.type:
-            case hanabi.ActionType.ColorClue | hanabi.ActionType.RankClue:
-                assert(self.clues > 0)
-                self.actions.append(action)
-                self.clues -= self.instance.clue_increment
-                self._make_turn()
-                # TODO: could check that the clue specified is in fact legal
-            case hanabi.ActionType.Play:
-                self.play(action.target)
-            case hanabi.ActionType.Discard:
-                self.discard(action.target)
-            case hanabi.ActionType.EndGame | hanabi.ActionType.VoteTerminate:
-                self.over = True
-
-    def _waste_clue(self) -> hanabi.Action:
-        for player in range(self.turn + 1, self.turn + self.num_players):
-            for card in self.hands[player % self.num_players]:
-                for rank in self.instance.variant.ranks:
-                    if self.instance.variant.rank_touches(card, rank):
-                        return hanabi.Action(
-                            hanabi.ActionType.RankClue,
-                            player % self.num_players,
-                            rank
-                        )
-                for color in range(self.instance.variant.num_colors):
-                    if self.instance.variant.color_touches(card, color):
-                        return hanabi.Action(
-                            hanabi.ActionType.ColorClue,
-                            player % self.num_players,
-                            color
-                        )
-        raise RuntimeError("Current game state did not permit any legal clue."
-                           "This case is incredibly rare and currently not handled.")

hanabi_cli.py

@@ -0,0 +1,10 @@
+#! /usr//bin/env python3
+
+"""
+Short executable file to start the command-line-interface for the hanabi package.
+Note this is not part of the package itself
+"""
+
+from hanabi import cli
+
+cli.hanabi_cli()

hanabi_suite.py

@@ -1,81 +0,0 @@
-#! /usr/bin/python3
-
-import argparse
-import logging
-
-import verboselogs
-
-from check_game import check_game
-from download_data import detailed_export_game
-from compress import link
-from log_setup import logger, logger_manager
-
-"""
-init db + populate tables
-download games of variant
-download single game
-analyze single game
-"""
-
-
-def add_init_subparser(subparsers):
-    parser = subparsers.add_parser(
-        'init',
-        help='Init database tables, retrieve variant and suit information from hanab.live'
-    )
-
-
-def add_download_subparser(subparsers):
-    parser = subparsers.add_parser('download', help='Download games from hanab.live')
-    group = parser.add_mutually_exclusive_group(required=True)
-    group.add_argument('--var', '-v', type=int)
-    group.add_argument('--id', '-i', type=int)
-
-
-def add_analyze_subparser(subparsers):
-    parser = subparsers.add_parser('analyze', help='Analyze a game and find the last winning state')
-    parser.add_argument('game_id', type=int)
-    parser.add_argument('--download', '-d', help='Download game if not in database', action='store_true')
-
-
-def analyze_game(game_id: int, download: bool = False):
-    if download:
-        detailed_export_game(game_id)
-    logger.info('Analyzing game {}'.format(game_id))
-    turn, sol = check_game(game_id)
-    if turn == 0:
-        logger.info('Instance is unfeasible')
-    else:
-        logger.info('Game was first lost after {} turns.'.format(turn))
-        logger.info(
-            'A replay achieving perfect score from the previous turn onwards is: {}#{}'
-            .format(link(sol), turn)
-        )
-
-
-def main_parser() -> argparse.ArgumentParser:
-    parser = argparse.ArgumentParser(
-        prog='hanabi_suite',
-        description='High-level interface for analysis of hanabi instances.'
-    )
-    parser.add_argument('--verbose', '-v', help='Enable verbose logging to console', action='store_true')
-    subparsers = parser.add_subparsers(dest='command', required=True, help='select subcommand')
-
-    add_init_subparser(subparsers)
-    add_analyze_subparser(subparsers)
-    add_download_subparser(subparsers)
-
-    return parser
-
-
-if __name__ == "__main__":
-    args = main_parser().parse_args()
-    switcher = {
-        'analyze': analyze_game
-    }
-    if args.verbose:
-        logger_manager.set_console_level(verboselogs.VERBOSE)
-    method_args = dict(vars(args))
-    method_args.pop('command')
-    method_args.pop('verbose')
-    switcher[args.command](**method_args)

instance_finder.py

@@ -1,204 +0,0 @@
-from typing import Optional
-import pebble.concurrent
-import concurrent.futures
-
-import traceback
-
-from sat import solve_sat
-from database.database import conn, cur
-from download_data import detailed_export_game
-from alive_progress import alive_bar
-from compress import decompress_deck, link
-from hanabi import HanabiInstance
-from threading import Lock
-from time import perf_counter
-from greedy_solver import GameState, GreedyStrategy
-from log_setup import logger
-from deck_analyzer import analyze, InfeasibilityReason
-from variants import Variant
-
-MAX_PROCESSES = 6
-
-
-def update_seeds_db():
-    cur2 = conn.cursor()
-    with conn.cursor() as cur:
-        cur.execute("SELECT num_players, seed, variant_id from games;")
-        for (num_players, seed, variant_id) in cur:
-            cur2.execute("SELECT COUNT(*) from seeds WHERE seed = (%s);", (seed,))
-            if cur2.fetchone()[0] == 0:
-                print("new seed {}".format(seed))
-                cur2.execute("INSERT INTO seeds"
-                             "(seed, num_players, variant_id)"
-                             "VALUES"
-                             "(%s, %s, %s)",
-                             (seed, num_players, variant_id)
-                             )
-                conn.commit()
-            else:
-                print("seed {} already found in DB".format(seed))
-
-
-def get_decks_of_seeds():
-    cur2 = conn.cursor()
-    cur.execute("SELECT seed, variant_id FROM seeds WHERE deck is NULL")
-    for (seed, variant_id) in cur:
-        cur2.execute("SELECT id FROM games WHERE seed = (%s) LIMIT 1", (seed,))
-        (game_id,) = cur2.fetchone()
-        logger.verbose("Exporting game {} for seed {}.".format(game_id, seed))
-        detailed_export_game(game_id, var_id=variant_id, seed_exists=True)
-        conn.commit()
-
-
-def update_trivially_feasible_games(variant_id):
-    variant: Variant = Variant.from_db(variant_id)
-    cur.execute("SELECT seed FROM seeds WHERE variant_id = (%s) AND feasible is null", (variant_id,))
-    seeds = cur.fetchall()
-    print('Checking variant {} (id {}), found {} seeds to check...'.format(variant.name, variant_id, len(seeds)))
-
-    with alive_bar(total=len(seeds), title='{} ({})'.format(variant.name, variant_id)) as bar:
-        for (seed,) in seeds:
-            cur.execute("SELECT id, deck_plays, one_extra_card, one_less_card, all_or_nothing "
-                        "FROM games WHERE score = (%s) AND seed = (%s) ORDER BY id;",
-                        (variant.max_score, seed)
-                        )
-            res = cur.fetchall()
-            logger.debug("Checking seed {}: {:3} results".format(seed, len(res)))
-            for (game_id, a, b, c, d) in res:
-                if None in [a, b, c, d]:
-                    logger.debug('  Game {} not found in database, exporting...'.format(game_id))
-                    detailed_export_game(game_id, var_id=variant_id)
-                else:
-                    logger.debug('  Game {} already in database'.format(game_id, valid))
-                valid = not any([a, b, c, d])
-                if valid:
-                    logger.verbose('Seed {:10} (variant {}) found to be feasible via game {:6}'.format(seed, variant_id, game_id))
-                    cur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (True, seed))
-                    conn.commit()
-                    break
-                else:
-                    logger.verbose('  Cheaty game found')
-            bar()
-
-
-def get_decks_for_all_seeds():
-    cur = conn.cursor()
-    cur.execute("SELECT id "
-                "FROM games "
-                "  INNER JOIN seeds "
-                "  ON seeds.seed = games.seed"
-                "    WHERE"
-                "      seeds.deck is null"
-                "      AND"
-                "      games.id = ("
-                "         SELECT id FROM games WHERE games.seed = seeds.seed LIMIT 1"
-                "     )"
-                )
-    print("Exporting decks for all seeds")
-    res = cur.fetchall()
-    with alive_bar(len(res), title="Exporting decks") as bar:
-        for (game_id,) in res:
-            export_game(game_id)
-            bar()
-
-
-mutex = Lock()
-
-
-def solve_instance(instance: HanabiInstance):
-    # first, sanity check on running out of pace
-    result = analyze(instance)
-    if result is not None:
-        assert type(result) == InfeasibilityReason
-        logger.debug("found infeasible deck")
-        return False, None, None
-    for num_remaining_cards in [0, 20]:
-        #        logger.info("trying with {} remaining cards".format(num_remaining_cards))
-        game = GameState(instance)
-        strat = GreedyStrategy(game)
-
-        # make a number of greedy moves
-        while not game.is_over() and not game.is_known_lost():
-            if num_remaining_cards != 0 and game.progress == game.deck_size - num_remaining_cards:
-                break  # stop solution here
-            strat.make_move()
-
-        # check if we won already
-        if game.is_won():
-            #            print("won with greedy strat")
-            return True, game, num_remaining_cards
-
-        # now, apply sat solver
-        if not game.is_over():
-            logger.debug("continuing greedy sol with SAT")
-            solvable, sol = solve_sat(game)
-            if solvable is None:
-                return True, sol, num_remaining_cards
-        logger.debug(
-            "No success with {} remaining cards, reducing number of greedy moves, failed attempt was: {}".format(
-                num_remaining_cards, link(game)))
-    #    print("Aborting trying with greedy strat")
-    logger.debug("Starting full SAT solver")
-    game = GameState(instance)
-    a, b = solve_sat(game)
-    return a, b, instance.draw_pile_size
-
-
-@pebble.concurrent.process(timeout=150)
-def solve_seed_with_timeout(seed, num_players, deck_compressed, var_name: Optional[str] = None):
-    try:
-        logger.verbose("Starting to solve seed {}".format(seed))
-        deck = decompress_deck(deck_compressed)
-        t0 = perf_counter()
-        solvable, solution, num_remaining_cards = solve_instance(HanabiInstance(deck, num_players))
-        t1 = perf_counter()
-        logger.verbose("Solved instance {} in {} seconds: {}".format(seed, round(t1 - t0, 2), solvable))
-
-        mutex.acquire()
-        if solvable is not None:
-            cur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (solvable, seed))
-            conn.commit()
-        mutex.release()
-
-        if solvable == True:
-            logger.verbose("Success with {} cards left in draw by greedy solver on seed {}: {}\n".format(
-                num_remaining_cards, seed, link(solution))
-            )
-        elif solvable == False:
-            logger.debug("seed {} was not solvable".format(seed))
-            logger.debug('{}-player, seed {:10}, {}\n'.format(num_players, seed, var_name))
-        elif solvable is None:
-            logger.verbose("seed {} skipped".format(seed))
-        else:
-            raise Exception("Programming Error")
-
-    except Exception as e:
-        print("exception in subprocess:")
-        traceback.print_exc()
-
-
-def solve_seed(seed, num_players, deck_compressed, var_name: Optional[str] = None):
-    f = solve_seed_with_timeout(seed, num_players, deck_compressed, var_name)
-    try:
-        return f.result()
-    except TimeoutError:
-        logger.verbose("Solving on seed {} timed out".format(seed))
-        return
-
-
-def solve_unknown_seeds(variant_id, variant_name: Optional[str] = None):
-    cur.execute("SELECT seed, num_players, deck FROM seeds WHERE variant_id = (%s) AND feasible IS NULL", (variant_id,))
-    res = cur.fetchall()
-
-    #    for r in res:
-    #        solve_seed(r[0], r[1], r[2], variant_name)
-
-    with concurrent.futures.ProcessPoolExecutor(max_workers=MAX_PROCESSES) as executor:
-        fs = [executor.submit(solve_seed, r[0], r[1], r[2], variant_name) for r in res]
-        with alive_bar(len(res), title='Seed solving on {}'.format(variant_name)) as bar:
-            for f in concurrent.futures.as_completed(fs):
-                bar()
-
-
-update_trivially_feasible_games(0)
-solve_unknown_seeds(0, "No Variant")

old.py

@@ -1,63 +0,0 @@
-
-def print_suits_and_attrs():
-    with open("variants.json") as f:
-        variants = json.loads(f.read())
-    x = set()
-    c = []
-    for var in variants:
-        for k in var.keys():
-            x.add(k)
-        for s in var['suits']:
-            if s not in c:
-                c.append(s)
-    for y in x:
-        print(y)
-    print()
-
-    for s in c:
-        print(s)
-
-    attributes = {
-        "nativeColors": ["Red"],
-        "ranks": 1,  # 0: none, 1: default, 2: all
-        "colors": 1,  # 0: none, 1: default, 2: all, 3: prism
-        "dark": False,
-        "reversed": False,
-        "prism": False
-    }
-
-    d = OrderedDict((s, attributes) for s in c)
-
-    if not os.path.isfile("colors.json"):
-        with open("colors.json", "w") as f:
-            f.writelines(json.dumps(d, indent=4, sort_keys=False))
-
-    # need: suit name -> colors
-
-
-def create_suit_graph():
-    with open("variants.json") as f:
-        variants = json.loads(f.read())
-    G = nx.DiGraph()
-    for var in variants:
-        suits = var['suits']
-        for suit in suits:
-            if suit not in G.nodes:
-                G.add_node(suit)
-        for i in range(0, len(suits) - 1):
-            G.add_edge(suits[i], suits[i + 1], var=var['name'])
-
-    H = nx.DiGraph()
-    try:
-        while True:
-            cycle = nx.find_cycle(G)
-            #            J = nx.DiGraph()
-            #            J.add_edges_from(cycle)
-            #            nx.draw(J, with_labels=True)
-            H.add_edges_from(cycle)
-            G.remove_edges_from(cycle)
-    except nx.NetworkXNoCycle:
-        pass
-
-    nx.draw(H, with_labels=True, font_weight='bold')
-    plt.show()

pyproject.toml

@@ -0,0 +1,32 @@
+[project]
+name = "hanabi"
+version = "1.1.5"
+description = "Hanabi interface"
+readme = "README.md"
+license = { file = "LICENSE" }
+keywords = [ "hanabi" ]
+authors = [
+  { name = "Maximilian Keßler", email = "git@maximilian-kessler.de" }
+]
+dependencies = [
+  "requests",
+  "requests_cache",
+  "pysmt",
+  "termcolor",
+  "more_itertools",
+  "psycopg2",
+  "alive_progress",
+  "argparse",
+  "verboselogs",
+  "pebble",
+  "platformdirs",
+  "PyYAML",
+  "cython==0.29.36"
+]
+
+[project.urls]
+"Homepage" = "https://gitlab.com/kesslermaximilian/hanabi"
+
+[build-system]
+requires = ["setuptools>=43.0.0", "wheel"]
+build-backend = "setuptools.build_meta"

requirements.txt

@@ -8,3 +8,7 @@ alive_progress
 argparse
 verboselogs
 pebble
+platformdirs
+PyYAML
+cython==0.29.36
+unidecode

sat.py

@@ -1,389 +0,0 @@
-import copy
-from pysmt.shortcuts import Symbol, Bool, Not, Implies, Iff, And, Or, AtMostOne, ExactlyOne, get_model, get_atoms, get_formula_size, get_unsat_core, Equals, GE, NotEquals, Int
-from pysmt.typing import INT
-from pysmt.rewritings import conjunctive_partition
-import json
-from typing import List, Optional, Tuple
-from concurrent.futures import ProcessPoolExecutor
-
-from hanabi import DeckCard, Action, ActionType, GameState, HanabiInstance
-from compress import link, decompress_deck
-from greedy_solver import GreedyStrategy
-from constants import COLOR_INITIALS
-from log_setup import logger
-
-
-# literals to model game as sat instance to check for feasibility
-# variants 'throw it in a hole not handled', 'clue starved' and 'up or down' currently not handled
-class Literals():
-    # num_suits is total number of suits, i.e. also counts the dark suits
-    # default distribution among all suits is assumed
-    def __init__(self, instance: HanabiInstance):
-
-        # clues[m][i] == "after move m we have i clues", in clue starved, this counts half clues
-        self.clues = {
-                -1: Int(16 if instance.clue_starved else 8)  # we have 8 clues after turn
-                , **{
-                        m: Symbol('m{}clues'.format(m), INT)
-                        for m in range(instance.max_winning_moves)
-                    }
-                }
-
-        self.pace = {
-            -1: Int(instance.initial_pace)
-            , **{
-                m: Symbol('m{}pace'.format(m), INT)
-                for m in range(instance.max_winning_moves)
-            }
-        }
-
-        # strikes[m][i] == "after move m we have at least i strikes"
-        self.strikes = {
-                    -1: {i: Bool(i == 0) for i in range(0, instance.num_strikes + 1)}    # no strikes when we start
-                  , **{
-                          m: {
-                              0: Bool(True),
-                              **{ s: Symbol('m{}strikes{}'.format(m,s)) for s in range(1, instance.num_strikes) },
-                              instance.num_strikes: Bool(False)                              # never so many clues that we lose. Implicitly forbids striking out
-                             }
-                          for m in range(instance.max_winning_moves)
-                      }
-                  }
-
-        # extraturn[m] = "turn m is a move part of the extra round or a dummy turn"
-        self.extraround = {
-                     -1: Bool(False)
-                     , **{
-                             m: Bool(False) if m < instance.draw_pile_size else Symbol('m{}extra'.format(m))   # it takes at least as many turns as cards in the draw pile to start the extra round
-                             for m in range(0, instance.max_winning_moves)
-                         }
-                     }
-
-        # dummyturn[m] = "turn m is a dummy nurn and not actually part of the game"
-        self.dummyturn = {
-                    -1: Bool(False)
-                    , **{
-                            m: Bool(False) if m < instance.draw_pile_size + instance.num_players else Symbol('m{}dummy'.format(m))
-                            for m in range(0, instance.max_winning_moves)
-                        }
-                    }
-
-        # draw[m][i] == "at move m we play/discard deck[i]"
-        self.discard = {
-                    m: {i: Symbol('m{}discard{}'.format(m, i)) for i in range(instance.deck_size)}
-                    for m in range(instance.max_winning_moves)
-                  }
-
-        # draw[m][i] == "at move m we draw deck card i"
-        self.draw = {
-                -1: { i: Bool(i == instance.num_dealt_cards - 1) for i in range(instance.num_dealt_cards - 1, instance.deck_size) }
-                , **{
-                        m: {
-                            instance.num_dealt_cards - 1: Bool(False),
-                            **{i: Symbol('m{}draw{}'.format(m, i)) for i in range(instance.num_dealt_cards, instance.deck_size)}
-                            }
-                        for m in range(instance.max_winning_moves)
-                    }
-               }
-
-        # strike[m] = "at move m we get a strike"
-        self.strike = {
-                 -1: Bool(False)
-                 , **{
-                        m: Symbol('m{}newstrike'.format(m))
-                        for m in range(instance.max_winning_moves)
-                     }
-                 }
-
-        # progress[m][card = (suitIndex, rank)] == "after move m we have played in suitIndex up to rank"
-        self.progress = {
-                     -1: {(s, r): Bool(r == 0) for s in range(0, instance.num_suits) for r in range(0, 6)} # at start, have only played rank zero
-                   , **{
-                           m: {
-                               **{(s, 0): Bool(True) for s in range(0, instance.num_suits)},
-                               **{(s, r): Symbol('m{}progress{}{}'.format(m, s, r)) for s in range(0, instance.num_suits) for r in range(1, 6)}
-                              }
-                           for m in range(instance.max_winning_moves)
-                       }
-                   }
-
-        ## Utility variables
-
-        # discard_any[m] == "at move m we play/discard a card"
-        self.discard_any = { m: Symbol('m{}discard_any'.format(m)) for m in range(instance.max_winning_moves) }
-
-        # draw_any[m] == "at move m we draw a card"
-        self.draw_any = {m: Symbol('m{}draw_any'.format(m)) for m in range(instance.max_winning_moves)}
-
-        # play[m] == "at move m we play a card"
-        self.play = {m: Symbol('m{}play'.format(m)) for m in range(instance.max_winning_moves)}
-
-        # play5[m] == "at move m we play a 5"
-        self.play5 = {m: Symbol('m{}play5'.format(m)) for m in range(instance.max_winning_moves)}
-
-        # incr_clues[m] == "at move m we obtain a clue"
-        self.incr_clues = {m: Symbol('m{}c+'.format(m)) for m in range(instance.max_winning_moves)}
-
-
-def solve_sat(starting_state: GameState | HanabiInstance, min_pace: Optional[int] = 0) -> Tuple[bool, Optional[GameState]]:
-    if isinstance(starting_state, HanabiInstance):
-        instance = starting_state
-        game_state = GameState(instance)
-    elif isinstance(starting_state, GameState):
-        instance = starting_state.instance
-        game_state = starting_state
-    else:
-        raise ValueError("Bad argument type")
-
-    ls = Literals(instance)
-
-    ##### setup of initial game state
-
-    # properties used later to model valid moves
-
-    starting_hands = [[card.deck_index for card in hand] for hand in game_state.hands]
-    first_turn = len(game_state.actions)
-
-    if isinstance(starting_state, GameState):
-        # have to set additional variables
-
-        # set initial clues
-        for i in range(0, 10):
-            ls.clues[first_turn - 1] = Int(game_state.clues)
-
-        # set initial pace
-        ls.pace[first_turn - 1] = Int(game_state.pace)
-
-        # set initial strikes
-        for i in range(0, instance.num_strikes + 1):
-            ls.strikes[first_turn - 1][i] = Bool(i <= game_state.strikes)
-
-        # check if extraround has started (usually not)
-        ls.extraround[first_turn - 1] = Bool(game_state.remaining_extra_turns < game_state.num_players)
-        ls.dummyturn[first_turn -1] = Bool(False)
-
-        # set recent draws: important to model progress
-        # we just pretend that the last card drawn was in fact drawn last turn,
-        # regardless of when it was actually drawn
-        for neg_turn in range(1, min(9, first_turn + 2)):
-            for i in range(instance.num_players * instance.hand_size, instance.deck_size):
-                ls.draw[first_turn - neg_turn][i] = Bool(neg_turn == 1 and i == game_state.progress - 1)
-        # forbid re-drawing of the last card drawn
-        for m in range(first_turn, instance.max_winning_moves):
-            ls.draw[m][game_state.progress - 1] = Bool(False)
-
-
-        # model initial progress
-        for s in range(0, game_state.num_suits):
-            for r in range(0, 6):
-                ls.progress[first_turn - 1][s, r] = Bool(r <= game_state.stacks[s])
-
-    ### Now, model all valid moves
-
-    valid_move = lambda m: And(
-        # in dummy turns, nothing can be discarded
-        Implies(ls.dummyturn[m], Not(ls.discard_any[m])),
-
-        # definition of discard_any
-        Iff(ls.discard_any[m], Or(ls.discard[m][i] for i in range(instance.deck_size))),
-
-        # definition of draw_any
-        Iff(ls.draw_any[m], Or(ls.draw[m][i] for i in range(game_state.progress, instance.deck_size))),
-
-        # ls.draw implies ls.discard (and converse true before the ls.extraround)
-        Implies(ls.draw_any[m], ls.discard_any[m]),
-        Implies(ls.discard_any[m], Or(ls.extraround[m], ls.draw_any[m])),
-
-        # ls.play requires ls.discard
-        Implies(ls.play[m], ls.discard_any[m]),
-
-        # definition of ls.play5
-        Iff(ls.play5[m], And(ls.play[m], Or(ls.discard[m][i] for i in range(instance.deck_size) if instance.deck[i].rank == 5))),
-
-        # definition of ls.incr_clues
-        Iff(ls.incr_clues[m], And(ls.discard_any[m], NotEquals(ls.clues[m-1], Int(16 if instance.clue_starved else 8)), Implies(ls.play[m], ls.play5[m]))),
-
-        # change of ls.clues
-        Implies(And(Not(ls.discard_any[m]), Not(ls.dummyturn[m])),
-                Equals(ls.clues[m], ls.clues[m-1] - (2 if instance.clue_starved else 1))),
-        Implies(ls.incr_clues[m], Equals(ls.clues[m], ls.clues[m-1] + 1)),
-        Implies(And(Or(ls.discard_any[m], ls.dummyturn[m]), Not(ls.incr_clues[m])), Equals(ls.clues[m], ls.clues[m-1])),
-
-        # change of pace
-        Implies(And(ls.discard_any[m], Or(ls.strike[m], Not(ls.play[m]))), Equals(ls.pace[m], ls.pace[m-1] - 1)),
-        Implies(Or(Not(ls.discard_any[m]), And(Not(ls.strike[m]), ls.play[m])), Equals(ls.pace[m], ls.pace[m-1])),
-
-        # pace is nonnegative
-        GE(ls.pace[m], Int(min_pace)),
-
-        ## more than 8 clues not allowed, ls.discarding produces a strike
-        # Note that this means that we will never strike while not at 8 clues.
-        # It's easy to see that if there is any solution to the instance, then there is also one where we only strike at 8 clues
-        # (or not at all) -> Just strike later if neccessary
-        # So, we decrease the solution space with this formulation, but do not change whether it's empty or not
-        Iff(ls.strike[m], And(ls.discard_any[m], Not(ls.play[m]), Equals(ls.clues[m-1], Int(16 if instance.clue_starved else 8)))),
-
-        # change of strikes
-        *[Iff(ls.strikes[m][i], Or(ls.strikes[m-1][i], And(ls.strikes[m-1][i-1], ls.strike[m]))) for i in range(1, instance.num_strikes + 1)],
-
-        # less than 0 clues not allowed
-        Implies(Not(ls.discard_any[m]), Or(GE(ls.clues[m-1], Int(1)), ls.dummyturn[m])),
-
-        # we can only draw card i if the last ls.drawn card was i-1
-        *[Implies(ls.draw[m][i], Or(And(ls.draw[m0][i-1], *[Not(ls.draw_any[m1]) for m1 in range(m0+1, m)]) for m0 in range(max(first_turn - 1, m-9), m))) for i in range(game_state.progress, instance.deck_size)],
-
-        # we can only draw at most one card (NOTE: redundant, FIXME: avoid quadratic formula)
-        AtMostOne(ls.draw[m][i] for i in range(game_state.progress, instance.deck_size)),
-
-        # we can only discard a card if we drew it earlier...
-        *[Implies(ls.discard[m][i], Or(ls.draw[m0][i] for m0 in range(m-instance.num_players, first_turn - 1, -instance.num_players))) for i in range(game_state.progress, instance.deck_size)],
-
-        # ...or if it was part of the initial hand
-        *[Not(ls.discard[m][i]) for i in range(0, game_state.progress) if i not in starting_hands[m % instance.num_players] ],
-
-        # we can only discard a card if we did not discard it yet
-        *[Implies(ls.discard[m][i], And(Not(ls.discard[m0][i]) for m0 in range(m-instance.num_players, first_turn - 1, -instance.num_players))) for i in range(instance.deck_size)],
-
-        # we can only discard at most one card (FIXME: avoid quadratic formula)
-        AtMostOne(ls.discard[m][i] for i in range(instance.deck_size)),
-
-        # we can only play a card if it matches the progress
-        *[Implies(
-                    And(ls.discard[m][i], ls.play[m]),
-                    And(
-                        Not(ls.progress[m-1][instance.deck[i].suitIndex, instance.deck[i].rank]),
-                        ls.progress[m-1][instance.deck[i].suitIndex, instance.deck[i].rank-1 ]
-                       )
-                  )
-          for i in range(instance.deck_size)
-          ],
-
-        # change of progress
-        *[
-            Iff(
-                ls.progress[m][s, r],
-                Or(
-                    ls.progress[m-1][s, r],
-                    And(ls.play[m], Or(ls.discard[m][i]
-                        for i in range(0, instance.deck_size)
-                        if instance.deck[i] == DeckCard(s, r) ))
-                  )
-                )
-            for s in range(0, instance.num_suits)
-            for r in range(1, 6)
-         ],
-
-        # extra round bool
-        Iff(ls.extraround[m], Or(ls.extraround[m-1], ls.draw[m-1][instance.deck_size-1])),
-
-        # dummy turn bool
-        *[Iff(ls.dummyturn[m], Or(ls.dummyturn[m-1], ls.draw[m-1 - instance.num_players][instance.deck_size-1])) for i in range(0,1) if m >= instance.num_players]
-    )
-
-    win = And(
-        # maximum progress at each color
-        *[ls.progress[instance.max_winning_moves-1][s, 5] for s in range(0, instance.num_suits)],
-
-        # played every color/value combination (NOTE: redundant, but makes solving faster)
-        *[
-            Or(
-               And(ls.discard[m][i], ls.play[m])
-               for m in range(first_turn, instance.max_winning_moves)
-               for i in range(instance.deck_size)
-               if game_state.deck[i] == DeckCard(s, r)
-              )
-          for s in range(0, instance.num_suits)
-          for r in range(1, 6)
-          if r > game_state.stacks[s]
-          ]
-    )
-
-    constraints = And(*[valid_move(m) for m in range(first_turn, instance.max_winning_moves)], win)
-#    print('Solving instance with {} variables, {} nodes'.format(len(get_atoms(constraints)), get_formula_size(constraints)))
-
-    model = get_model(constraints)
-    if model:
-        log_model(model, game_state, ls)
-        solution = evaluate_model(model, copy.deepcopy(game_state), ls)
-        return True, solution
-    else:
-        #conj = list(conjunctive_partition(constraints))
-        #print('statements: {}'.format(len(conj)))
-        #ucore = get_unsat_core(conj)
-        #print('unsat core size: {}'.format(len(ucore)))
-        #for f in ucore:
-        #    print(f.serialize())
-        return False, None
-
-
-def log_model(model, cur_game_state, ls: Literals):
-    deck = cur_game_state.deck
-    first_turn = len(cur_game_state.actions)
-    if first_turn > 0:
-        logger.debug('[print_model] Note: Omitting first {} turns, since they were fixed already.'.format(first_turn))
-    for m in range(first_turn, cur_game_state.instance.max_winning_moves):
-        logger.debug('=== move {} ==='.format(m))
-        logger.debug('clues: {}'.format(model.get_py_value(ls.clues[m])))
-        logger.debug('strikes: ' + ''.join(str(i) for i in range(1, 3) if model.get_py_value(ls.strikes[m][i])))
-        logger.debug('draw: ' + ', '.join('{}: {}'.format(i, deck[i]) for i in range(cur_game_state.progress, cur_game_state.instance.deck_size) if model.get_py_value(ls.draw[m][i])))
-        logger.debug('discard: ' + ', '.join('{}: {}'.format(i, deck[i]) for i in range(cur_game_state.instance.deck_size) if model.get_py_value(ls.discard[m][i])))
-        logger.debug('pace: {}'.format(model.get_py_value(ls.pace[m])))
-        for s in range(0, cur_game_state.instance.num_suits):
-            logger.debug('progress {}: '.format(COLOR_INITIALS[s]) + ''.join(str(r) for r in range(1, 6) if model.get_py_value(ls.progress[m][s, r])))
-        flags = ['discard_any', 'draw_any', 'play', 'play5', 'incr_clues', 'strike', 'extraround', 'dummyturn']
-        logger.debug(', '.join(f for f in flags if model.get_py_value(getattr(ls, f)[m])))
-
-
-
-# given the initial game state and the model found by the SAT solver,
-# evaluates the model to produce a full game history
-def evaluate_model(model, cur_game_state: GameState, ls: Literals) -> GameState:
-    for m in range(len(cur_game_state.actions), cur_game_state.instance.max_winning_moves):
-        if model.get_py_value(ls.dummyturn[m]) or cur_game_state.is_over():
-            break
-        if model.get_py_value(ls.discard_any[m]):
-            card_idx = next(i for i in range(0, cur_game_state.instance.deck_size) if model.get_py_value(ls.discard[m][i]))
-            if model.get_py_value(ls.play[m]) or model.get_py_value(ls.strike[m]):
-                cur_game_state.play(card_idx)
-            else:
-                cur_game_state.discard(card_idx)
-        else:
-            cur_game_state.clue()
-
-    return cur_game_state
-
-
-
-def run_deck():
-    puzzle = True
-    if puzzle:
-        deck_str = 'p5 p3 b4 r5 y4 y4 y5 r4 b2 y2 y3 g5 g2 g3 g4 p4 r3 b2 b3 b3 p4 b1 p2 b1 b1 p2 p1 p1 g1 r4 g1 r1 r3 r1 g1 r1 p1 b4 p3 g2 g3 g4 b5 y1 y1 y1 r2 r2 y2 y3'
-
-        deck = [DeckCard(COLOR_INITIALS.index(c[0]), int(c[1])) for c in deck_str.split(" ")]
-        num_p = 5
-    else:
-        deck_str = "15gfvqluvuwaqnmrkpkaignlaxpjbmsprksfcddeybfixchuhtwo"
-        deck_str = "15diuknfwhqbplsrlkxjuvfbwyacoaxgtudcerskqfnhpgampmiv"
-        deck_str = "15jdxlpobvikrnhkslcuwggimtphafquqfvcwadampxkeyfrbnsu"
-        deck = decompress_deck(deck_str)
-        num_p = 6
-
-    print(deck)
-
-    gs = GameState(HanabiInstance(deck, num_p))
-    if puzzle:
-        gs.play(2)
-    else:
-        strat = GreedyStrategy(gs)
-        for _ in range(17):
-            strat.make_move()
-
-    solvable, sol = solve_sat(gs, 0)
-    if solvable:
-        print(sol)
-        print(link(sol))
-    else:
-        print('unsolvable')
-
-if __name__ == "__main__":
-    run_deck()

src/hanabi/cli.py

@@ -0,0 +1,193 @@
+import argparse
+import json
+from typing import Optional
+
+import verboselogs
+
+from hanabi import logger, logger_manager
+from hanabi.live import variants
+from hanabi.live import check_game
+from hanabi.live import download_data
+from hanabi.live import compress
+from hanabi.live import instance_finder
+from hanabi.database import init_database
+from hanabi.database import global_db_connection_manager
+
+"""
+Commands supported:
+
+init db + populate tables
+download games of variant
+download single game
+analyze single game
+
+"""
+
+
+def subcommand_analyze(game_id: int, download: bool = False):
+    if download:
+        download_data.detailed_export_game(game_id)
+    logger.info('Analyzing game {}'.format(game_id))
+    turn, sol = check_game.check_game(game_id)
+    if turn == 0:
+        logger.info('Instance is unfeasible')
+    else:
+        logger.info('Game was first lost after {} turns.'.format(turn))
+        logger.info(
+            'A replay achieving perfect score from the previous turn onwards is: {}#{}'
+            .format(compress.link(sol), turn)
+        )
+
+
+def subcommand_decompress(game_link: str):
+    parts = game_link.split('replay-json/')
+    game_str = parts[-1].rstrip('/')
+    game = compress.decompress_game_state(game_str)
+    print(json.dumps(game.to_json()))
+
+
+def subcommand_init(force: bool, populate: bool):
+    tables = init_database.get_existing_tables()
+    if len(tables) > 0 and not force:
+        logger.info(
+            'Database tables "{}" exist already, aborting. To force re-initialization, use the --force options'
+            .format(", ".join(tables))
+        )
+        return
+    if len(tables) > 0:
+        logger.info(
+            "WARNING: This will drop all existing tables from the database and re-initialize them."
+        )
+        response = input("Do you wish to continue? [y/N] ")
+        if response not in ["y", "Y", "yes"]:
+            return
+    init_database.init_database_tables()
+    logger.info("Successfully initialized database tables")
+    if populate:
+        init_database.populate_static_tables()
+        logger.info("Successfully populated tables with variants and suits from hanab.live")
+
+
+def subcommand_download(
+          game_id: Optional[int]
+        , variant_id: Optional[int]
+        , export_all: bool = False
+        , all_variants: bool = False
+):
+    if game_id is not None:
+        download_data.detailed_export_game(game_id)
+        logger.info("Successfully exported game {}".format(game_id))
+    if variant_id is not None:
+        download_data.download_games(variant_id, export_all)
+        logger.info("Successfully exported games for variant id {}".format(variant_id))
+    if all_variants:
+        for variant in variants.get_all_variant_ids():
+            download_data.download_games(variant, export_all)
+        logger.info("Successfully exported games for all variants")
+
+
+def subcommand_solve(var_id):
+    instance_finder.solve_unknown_seeds(var_id, '')
+
+
+
+def subcommand_gen_config():
+    global_db_connection_manager.create_config_file()
+
+
+def add_init_subparser(subparsers):
+    parser = subparsers.add_parser(
+        'init',
+        help='Init database tables, retrieve variant and suit information from hanab.live'
+    )
+    parser.add_argument('--force', '-f', help='Force initialization (Drops existing tables)', action='store_true')
+    parser.add_argument(
+        '--no-populate-tables', '-n',
+        help='Do not download variant and suit information from hanab.live',
+        action='store_false',
+        dest='populate'
+    )
+
+
+def add_download_subparser(subparsers):
+    parser = subparsers.add_parser('download', help='Download games from hanab.live')
+    group = parser.add_mutually_exclusive_group(required=True)
+    group.add_argument(
+        '--var', '--variant', '-v',
+        type=int,
+        dest='variant_id',
+        help='Download information on all games given variant id (but not necessarily export all of them)'
+    )
+    group.add_argument('--id', '-i', type=int, dest='game_id', help='Download single game given id')
+    group.add_argument(
+        '--all-variants', '-a',
+        action='store_true',
+        dest='all_variants',
+        help='Download information from games on all variants (but not necessarily export all of them)'
+    )
+    parser.add_argument(
+        '--export-all', '-e',
+        action='store_true',
+        dest='export_all',
+        help='Export all games specified in full detail (i.e. also actions and game options)'
+    )
+
+
+def add_analyze_subparser(subparsers):
+    parser = subparsers.add_parser('analyze', help='Analyze a game and find the last winning state')
+    parser.add_argument('game_id', type=int)
+    parser.add_argument('--download', '-d', help='Download game if not in database', action='store_true')
+
+
+def add_config_gen_subparser(subparsers):
+    parser = subparsers.add_parser('gen-config', help='Generate config file at default location')
+
+
+def add_solve_subparser(subparsers):
+    parser = subparsers.add_parser('solve', help='Seed solving')
+    parser.add_argument('--var_id', type=int, help='Variant id to solve instances from.', default=0)
+
+def add_decompress_subparser(subparsers):
+    parser = subparsers.add_parser('decompress', help='Decompress a hanab.live JSON-encoded replay link')
+    parser.add_argument('game_link', type=str)
+
+
+def main_parser() -> argparse.ArgumentParser:
+    parser = argparse.ArgumentParser(
+        prog='hanabi_suite',
+        description='High-level interface for analysis of hanabi instances.'
+    )
+    parser.add_argument('--verbose', '-v', help='Enable verbose logging to console', action='store_true')
+    subparsers = parser.add_subparsers(dest='command', required=True, help='select subcommand')
+
+    add_init_subparser(subparsers)
+    add_analyze_subparser(subparsers)
+    add_download_subparser(subparsers)
+    add_config_gen_subparser(subparsers)
+    add_solve_subparser(subparsers)
+    add_decompress_subparser(subparsers)
+
+    return parser
+
+
+def hanabi_cli():
+    args = main_parser().parse_args()
+    subcommand_func = {
+        'analyze': subcommand_analyze,
+        'init': subcommand_init,
+        'download': subcommand_download,
+        'gen-config': subcommand_gen_config,
+        'solve': subcommand_solve,
+        'decompress': subcommand_decompress
+    }[args.command]
+
+    if args.command != 'gen-config':
+        global_db_connection_manager.read_config()
+        global_db_connection_manager.connect()
+
+    if args.verbose:
+        logger_manager.set_console_level(verboselogs.VERBOSE)
+    del args.command
+    del args.verbose
+
+    subcommand_func(**vars(args))

src/hanabi/constants.py

@@ -1,5 +1,6 @@
 # constants.py
 
+APP_NAME = 'hanabi-suite'
 
 # some values shared by all (default) hanabi instances
 HAND_SIZES = {2: 5, 3: 5, 4: 4, 5: 4, 6: 3}
@@ -7,10 +8,14 @@ NUM_STRIKES = 3
 COLOR_INITIALS = 'rygbpt'
 PLAYER_NAMES = ["Alice", "Bob", "Cathy", "Donald", "Emily", "Frank"]
 
+# DB connection parameters
+DEFAULT_DB_NAME = 'hanab-live'
+DEFAULT_DB_USER = 'hanabi'
 
-#### hanab.live stuff
 
-# Id of no variant
+# hanab.live stuff
+
+# id of no variant
 NO_VARIANT_ID = 0
 
 # a map (num_suits, num_dark_suits) -> variant id of a variant on hanab.live fitting that distribution

src/hanabi/database/__init__.py

@@ -0,0 +1,6 @@
+from .database import DBConnectionManager
+
+global_db_connection_manager = DBConnectionManager()
+
+conn = global_db_connection_manager.lazy_conn
+cur = global_db_connection_manager.lazy_cur

src/hanabi/database/database.py

@@ -0,0 +1,95 @@
+from typing import Optional
+from pathlib import Path
+import yaml
+
+import psycopg2
+import platformdirs
+
+from hanabi import constants
+from hanabi import logger
+
+
+class LazyDBCursor:
+    def __init__(self):
+        self.__cur: Optional[psycopg2.cursor] = None
+
+    def __getattr__(self, item):
+        if self.__cur is None:
+            raise ValueError(
+                "DB cursor used in uninitialized state. Did you forget to initialize the DB connection?"
+            )
+        return getattr(self.__cur, item)
+
+    def set_cur(self, cur):
+        self.__cur = cur
+
+
+class LazyDBConnection:
+    def __init__(self):
+        self.__conn: Optional[psycopg2.connection] = None
+
+    def __getattr__(self, item):
+        if self.__conn is None:
+            raise ValueError(
+                "DB connection used in uninitialized state. Did you forget to initialize the DB connection?"
+            )
+        return getattr(self.__conn, item)
+
+    def set_conn(self, conn):
+        self.__conn = conn
+
+
+class DBConnectionManager:
+    def __init__(self):
+        self.lazy_conn: LazyDBConnection = LazyDBConnection()
+        self.lazy_cur: LazyDBCursor = LazyDBCursor()
+        self.config_file = Path(platformdirs.user_config_dir(constants.APP_NAME, ensure_exists=True)) / 'config.yaml'
+        self.db_name: str = constants.DEFAULT_DB_NAME
+        self.db_user: str = constants.DEFAULT_DB_USER
+        self.db_pass: Optional[str] = None
+
+    def read_config(self):
+        logger.debug("DB connection configuration read from {}".format(self.config_file))
+        if self.config_file.exists():
+            with open(self.config_file, "r") as f:
+                config = yaml.safe_load(f)
+            self.db_name = config.get('dbname', None)
+            self.db_user = config.get('dbuser', None)
+            self.db_pass = config.get('dbpass', None)
+            if self.db_name is None:
+                logger.verbose("Falling back to default database name {}".format(constants.DEFAULT_DB_NAME))
+                self.db_name = constants.DEFAULT_DB_NAME
+            if self.db_user is None:
+                logger.verbose("Falling back to default database user {}".format(constants.DEFAULT_DB_USER))
+                self.db_user = constants.DEFAULT_DB_USER
+        else:
+            logger.info(
+                "No configuration file for database connection found, falling back to default values "
+                "(dbname={}, dbuser={}).".format(
+                    constants.DEFAULT_DB_NAME, constants.DEFAULT_DB_USER
+                )
+            )
+            logger.info(
+                "Note: To turn off this message, create a config file at {}".format(self.config_file)
+            )
+
+    def create_config_file(self):
+        if self.config_file.exists():
+            raise FileExistsError("Configuration file already exists, not overriding.")
+        self.config_file.write_text(
+            "dbname: {}\n"
+            "dbuser: {}\n"
+            "dbpass: null".format(
+                constants.DEFAULT_DB_NAME,
+                constants.DEFAULT_DB_USER
+            )
+        )
+        logger.info("Initialised default config file {}".format(self.config_file))
+
+    def connect(self):
+        conn = psycopg2.connect("dbname='{}' user='{}' password='{}' host='localhost'".format(
+            self.db_name, self.db_user, self.db_pass)
+        )
+        cur = conn.cursor()
+        self.lazy_conn.set_conn(conn)
+        self.lazy_cur.set_cur(cur)

src/hanabi/database/games_db_interface.py

@@ -0,0 +1,129 @@
+from typing import List, Tuple
+
+import psycopg2.extras
+
+import hanabi.hanab_game
+import hanabi.live.hanab_live
+from hanabi import logger
+
+from hanabi.database import conn, cur
+
+
+def store_actions(game_id: int, actions: List[hanabi.hanab_game.Action]):
+    vals = []
+    for turn, action in enumerate(actions):
+        vals.append((game_id, turn, action.type.value, action.target, action.value or 0))
+
+    psycopg2.extras.execute_values(
+        cur,
+        "INSERT INTO game_actions (game_id, turn, type, target, value) "
+        "VALUES %s "
+        "ON CONFLICT (game_id, turn) "
+        "DO NOTHING",
+        vals
+    )
+    conn.commit()
+
+
+def store_deck_for_seed(seed: str, deck: List[hanabi.hanab_game.DeckCard]):
+    vals = []
+    for index, card in enumerate(deck):
+        vals.append((seed, index, card.suitIndex, card.rank))
+
+    psycopg2.extras.execute_values(
+        cur,
+        "INSERT INTO decks (seed, deck_index, suit_index, rank) "
+        "VALUES %s "
+        "ON CONFLICT (seed, deck_index) DO UPDATE SET "
+        "(suit_index, rank) = (excluded.suit_index, excluded.rank)",
+        vals
+    )
+    conn.commit()
+
+
+def load_actions(game_id: int) -> List[hanabi.hanab_game.Action]:
+    cur.execute("SELECT type, target, value FROM game_actions "
+                "WHERE game_id = %s "
+                "ORDER BY turn ASC",
+                (game_id,))
+    actions = []
+    for action_type, target, value in cur.fetchall():
+        actions.append(
+            hanabi.hanab_game.Action(hanabi.hanab_game.ActionType(action_type), target, value)
+        )
+    if len(actions) == 0:
+        err_msg = "Failed to load actions for game id {} from DB: No actions stored.".format(game_id)
+        logger.error(err_msg)
+        raise ValueError(err_msg)
+    return actions
+
+
+def load_deck(seed: str) -> List[hanabi.hanab_game.DeckCard]:
+    cur.execute("SELECT deck_index, suit_index, rank FROM decks "
+                "WHERE seed = %s "
+                "ORDER BY deck_index ASC",
+                (seed,)
+                )
+    deck = []
+    for index, (card_index, suit_index, rank) in enumerate(cur.fetchall()):
+        assert index == card_index
+        deck.append(
+            hanabi.hanab_game.DeckCard(suit_index, rank, card_index)
+        )
+    if len(deck) == 0:
+        err_msg = "Failed to load deck for seed {} from DB: No cards stored.".format(seed)
+        logger.error(err_msg)
+        raise ValueError(err_msg)
+    return deck
+
+
+def load_game_parts(game_id: int) -> Tuple[hanabi.live.hanab_live.HanabLiveInstance, List[hanabi.hanab_game.Action]]:
+    """
+    Loads information on game from database
+    @param game_id: ID of game
+    @return: Instance (i.e. deck + settings) of game, list of actions, variant name
+    """
+    cur.execute(
+        "SELECT "
+        "games.num_players, games.seed, games.one_extra_card, games.one_less_card, games.deck_plays, "
+        "games.all_or_nothing,"
+        "variants.clue_starved, variants.name, variants.id, variants.throw_it_in_a_hole "
+        "FROM games "
+        "INNER JOIN variants"
+        "  ON games.variant_id = variants.id "
+        "WHERE games.id = %s",
+        (game_id,)
+    )
+    res = cur.fetchone()
+    if res is None:
+        err_msg = "Failed to retrieve game details of game {}.".format(game_id)
+        logger.error(err_msg)
+        raise ValueError(err_msg)
+
+    # Unpack results now
+    (num_players, seed, one_extra_card, one_less_card, deck_plays, all_or_nothing, clue_starved, variant_name, variant_id, throw_it_in_a_hole) = res
+
+    actions = load_actions(game_id)
+    deck = load_deck(seed)
+
+    instance = hanabi.live.hanab_live.HanabLiveInstance(
+        deck=deck,
+        num_players=num_players,
+        variant_id=variant_id,
+        one_extra_card=one_extra_card,
+        one_less_card=one_less_card,
+        fives_give_clue=not throw_it_in_a_hole,
+        deck_plays=deck_plays,
+        all_or_nothing=all_or_nothing,
+        clue_starved=clue_starved
+    )
+    return instance, actions
+
+
+def load_game(game_id: int) -> hanabi.live.hanab_live.HanabLiveGameState:
+    instance, actions = load_game_parts(game_id)
+    game = hanabi.live.hanab_live.HanabLiveGameState(instance)
+    for action in actions:
+        game.make_action(action)
+    return game
+

src/hanabi/database/games_seeds_schema.sql

@@ -0,0 +1,154 @@
+DROP TABLE IF EXISTS users CASCADE;
+CREATE TABLE users (
+    id SERIAL PRIMARY KEY,
+    username TEXT NOT NULL UNIQUE,
+    normalized_username TEXT NOT NULL UNIQUE
+);
+
+
+DROP TABLE IF EXISTS seeds CASCADE;
+CREATE TABLE seeds (
+    seed                    TEXT        NOT NULL PRIMARY KEY,
+    num_players             SMALLINT    NOT NULL,
+    variant_id              SMALLINT    NOT NULL,
+    starting_player         SMALLINT    NOT NULL DEFAULT 0,
+    feasible                BOOLEAN     DEFAULT NULL,
+    max_score_theoretical   SMALLINT
+);
+CREATE INDEX seeds_variant_idx ON seeds (variant_id);
+
+
+DROP TABLE IF EXISTS decks CASCADE;
+CREATE TABLE decks (
+    seed TEXT REFERENCES seeds (seed),
+    /* Order of card in deck*/
+    deck_index SMALLINT NOT NULL,
+    /* Suit */
+    suit_index SMALLINT NOT NULL,
+    /* Rank */
+    rank SMALLINT NOT NULL,
+    PRIMARY KEY (seed, deck_index)
+);
+
+DROP TABLE IF EXISTS games CASCADE;
+CREATE TABLE games (
+    id                      INT      PRIMARY KEY,
+    num_players             SMALLINT NOT NULL,
+
+    starting_player         SMALLINT NOT NULL DEFAULT 0,
+
+    variant_id              SMALLINT NOT NULL,
+
+    timed                   BOOLEAN,
+    time_base               INTEGER,
+    time_per_turn           INTEGER,
+    speedrun                BOOLEAN,
+    card_cycle              BOOLEAN,
+    deck_plays              BOOLEAN,
+    empty_clues             BOOLEAN,
+    one_extra_card          BOOLEAN,
+    one_less_card           BOOLEAN,
+    all_or_nothing          BOOLEAN,
+    detrimental_characters  BOOLEAN,
+
+    seed                    TEXT     NOT NULL REFERENCES seeds,
+    score                   SMALLINT NOT NULL,
+    num_turns               SMALLINT
+);
+
+CREATE INDEX games_seed_score_idx ON games (seed, score);
+CREATE INDEX games_var_seed_idx ON games (variant_id, seed);
+CREATE INDEX games_player_idx ON games (num_players);
+
+
+
+DROP TABLE IF EXISTS game_participants CASCADE;
+CREATE TABLE game_participants (
+   id                    SERIAL    PRIMARY KEY,
+   game_id               INTEGER   NOT NULL,
+   user_id               INTEGER   NOT NULL,
+   seat                  SMALLINT  NOT NULL, /* Needed for the "GetNotes()" function */
+   FOREIGN KEY (game_id) REFERENCES games (id) ON DELETE CASCADE,
+   FOREIGN KEY (user_id) REFERENCES users (id) ON DELETE CASCADE,
+   CONSTRAINT game_participants_unique UNIQUE (game_id, user_id)
+);
+
+
+DROP FUNCTION IF EXISTS delete_game_of_deleted_participant;
+CREATE FUNCTION delete_game_of_deleted_participant() RETURNS TRIGGER AS $_$
+BEGIN
+    DELETE FROM games WHERE games.id = OLD.game_id;
+    RETURN OLD;
+END $_$ LANGUAGE 'plpgsql';
+
+CREATE TRIGGER delete_game_upon_participant_deletion
+    AFTER DELETE ON game_participants
+    FOR EACH ROW
+EXECUTE PROCEDURE delete_game_of_deleted_participant();
+
+
+DROP TABLE IF EXISTS game_participant_notes CASCADE;
+CREATE TABLE game_participant_notes (
+    game_participant_id  INTEGER   NOT NULL,
+    card_order           SMALLINT  NOT NULL, /* "order" is a reserved word in PostgreSQL. */
+    note                 TEXT      NOT NULL,
+    FOREIGN KEY (game_participant_id) REFERENCES game_participants (id) ON DELETE CASCADE,
+    PRIMARY KEY (game_participant_id, card_order)
+);
+
+
+DROP TABLE IF EXISTS game_actions CASCADE;
+CREATE TABLE game_actions (
+                              game_id  INTEGER   NOT NULL,
+                              turn     SMALLINT  NOT NULL,
+
+    /**
+     * Corresponds to the "DatabaseGameActionType" enum.
+     *
+     * - 0 - play
+     * - 1 - discard
+     * - 2 - color clue
+     * - 3 - rank clue
+     * - 4 - game over
+     */
+                              type     SMALLINT  NOT NULL,
+
+    /**
+     * - If a play or a discard, corresponds to the order of the the card that was played/discarded.
+     * - If a clue, corresponds to the index of the player that received the clue.
+     * - If a game over, corresponds to the index of the player that caused the game to end or -1 if
+     *   the game was terminated by the server.
+     */
+                              target   SMALLINT  NOT NULL,
+
+    /**
+     * - If a play or discard, then 0 (as NULL). It uses less database space and reduces code
+     *   complexity to use a value of 0 for NULL than to use a SQL NULL:
+     *   https://dev.mysql.com/doc/refman/8.0/en/data-size.html
+     * - If a color clue, then 0 if red, 1 if yellow, etc.
+     * - If a rank clue, then 1 if 1, 2 if 2, etc.
+     * - If a game over, then the value corresponds to the "endCondition" values in "constants.go".
+     */
+                              value    SMALLINT  NOT NULL,
+
+                              FOREIGN KEY (game_id) REFERENCES games (id) ON DELETE CASCADE,
+                              PRIMARY KEY (game_id, turn)
+);
+
+
+DROP TABLE IF EXISTS score_upper_bounds;
+CREATE TABLE score_upper_bounds (
+    seed              TEXT     NOT NULL REFERENCES seeds ON DELETE CASCADE,
+    score_upper_bound SMALLINT NOT NULL,
+    reason            SMALLINT NOT NULL,
+    UNIQUE (seed, reason)
+);
+
+DROP TABLE IF EXISTS score_lower_bounds;
+CREATE TABLE score_lower_bounds (
+  seed              TEXT NOT NULL REFERENCES seeds ON DELETE CASCADE,
+  score_lower_bound SMALLINT NOT NULL,
+  game_id           INT REFERENCES games ON DELETE CASCADE,
+  actions           TEXT,
+  CHECK (num_nonnulls(game_id, actions) = 1)
+);

src/hanabi/database/init_database.py

@@ -1,9 +1,31 @@
 import json
 import requests
 from pathlib import Path
-from log_setup import logger
 
-from .database import cur, conn
+import platformdirs
+
+from hanabi import logger
+from hanabi import constants
+from hanabi.database import cur, conn
+
+
+def get_existing_tables():
+    cur.execute(
+        "   SELECT tablename FROM pg_tables"
+        "   WHERE"
+        "       schemaname = 'public' AND "
+        "       tablename IN ("
+        "           'seeds',"
+        "           'games',"
+        "           'suits',"
+        "           'colors',"
+        "           'suit_colors',"
+        "           'variants',"
+        "           'variant_suits',"
+        "           'variant_game_downloads'"
+        "       )"
+    )
+    return [table for (table,) in cur.fetchall()]
 
 
 def init_database_tables():
@@ -170,15 +192,21 @@ def _populate_variants(variants):
 
 def _download_json_files():
     logger.verbose("Downloading JSON files for suits and variants from github...")
-    base_url = "https://raw.githubusercontent.com/Hanabi-Live/hanabi-live/main/packages/data/src/json"
+    base_url = "https://raw.githubusercontent.com/Hanabi-Live/hanabi-live/main/packages/game/src/json"
+    cache_dir = Path(platformdirs.user_cache_dir(constants.APP_NAME))
+    cache_dir.mkdir(parents=True, exist_ok=True)
     data = {}
     for name in ["suits", "variants"]:
-        filename = name + '.json'
+        file = (cache_dir / name).with_suffix(".json")
-        url = base_url + "/" + filename
+        if file.exists():
+            data[name] = json.loads(file.read_text())
+            continue
+        url = base_url + "/" + file.name
         response = requests.get(url)
         if not response.status_code == 200:
-            err_msg = "Could not download initialization file {} from github (tried url {})".format(filename, url)
+            err_msg = "Could not download initialization file {} from github (tried url {})".format(file.name, url)
             logger.error(err_msg)
             raise RuntimeError(err_msg)
+        file.write_text(response.text)
         data[name] = json.loads(response.text)
     return data['suits'], data['variants']

src/hanabi/database/variant_suits_schema.sql

@@ -1,6 +1,6 @@
 /* Database schema for the tables storing information on available hanab.live variants, suits and colors */
 
-/* Available suits. The associated id is arbitrary upon initial generation, but fixed for referentiability */
+/* Available suits. The associated id is arbitrary upon initial generation, but fixed afterwards for identification */
 DROP TABLE IF EXISTS suits CASCADE;
 CREATE TABLE suits (
     id                SERIAL PRIMARY KEY,
@@ -27,7 +27,7 @@ CREATE TABLE suits (
 );
 CREATE INDEX suits_name_idx ON suits (name);
 
-/* Available color clues. The indexing is arbitrary upon initial generation, but fixed for referentiability */
+/* Available color clues. The indexing is arbitrary upon initial generation, but fixed afterwards for identification */
 DROP TABLE IF EXISTS colors CASCADE;
 CREATE TABLE colors (
     id       SERIAL PRIMARY KEY,
@@ -99,7 +99,7 @@ CREATE TABLE variants (
      */
     special_rank_ranks  SMALLINT NOT NULL DEFAULT 1,
     /**
-      Encodes how cards of the special rank (if present) are touched by colorss,
+      Encodes how cards of the special rank (if present) are touched by colors,
       in the same manner how we encoded in @table suits
      */
     special_rank_colors SMALLINT NOT NULL DEFAULT 1,

src/hanabi/hanab_game.py

@@ -1,8 +1,12 @@
-from typing import Optional, List
+from typing import Optional, List, Generator
 from enum import Enum
 from termcolor import colored
 
-import constants
+from hanabi import constants
+
+
+class ParseError(ValueError):
+    pass
 
 
 class DeckCard:
@@ -13,7 +17,19 @@ class DeckCard:
 
     @staticmethod
     def from_json(deck_card):
-        return DeckCard(**deck_card)
+        suit_index = deck_card.get('suitIndex', None)
+        rank = deck_card.get('rank', None)
+        if suit_index is None:
+            raise ParseError("No suit index specified in deck_card")
+        if rank is None:
+            raise ParseError("No rank specified in deck_card")
+        return DeckCard(suit_index, rank)
+
+    def to_json(self):
+        return {
+            "suitIndex": self.suitIndex,
+            "rank": self.rank
+        }
 
     def colorize(self):
         color = ["green", "blue", "magenta", "yellow", "white", "cyan"][self.suitIndex]
@@ -23,6 +39,8 @@ class DeckCard:
         return self.suitIndex == other.suitIndex and self.rank == other.rank
 
     def __repr__(self):
+        if self.suitIndex == 0 and self.rank == 0:
+            return "kt"
         return constants.COLOR_INITIALS[self.suitIndex] + str(self.rank)
 
     def __hash__(self):
@@ -30,7 +48,7 @@ class DeckCard:
         return 1000 * self.suitIndex + self.rank
 
 
-def pp_deck(deck: List[DeckCard]) -> str:
+def pp_deck(deck: Generator[DeckCard, None, None]) -> str:
     return "[" + ", ".join(card.colorize() for card in deck) + "]"
 
 
@@ -54,12 +72,33 @@ class Action:
 
     @staticmethod
     def from_json(action):
+        action_type_int = action.get('type', None)
+        action_target = action.get('target', None)
+        action_value = action.get('value', None)
+        if action_type_int is None:
+            raise ParseError("No action type specified in action, found {}".format(action_type))
+        if action_target is None:
+            raise ParseError("No action target specified in action, found {}".format(action_target))
+        for val in [action_type_int, action_target, action_value]:
+            if val is not None and type(val) != int:
+                raise ParseError("Invalid data type in action, expected int, found {}".format(type(val)))
+        try:
+            action_type = ActionType(action_type_int)
+        except ValueError as e:
+            raise ParseError("Invalid action type, found {}".format(action_type_int)) from e
         return Action(
-            ActionType(action['type']),
+            action_type,
-            int(action['target']),
+            action_target,
-            action.get('value', None)
+            action_value
         )
 
+    def to_json(self):
+        return {
+            "type": self.type.value,
+            "target": self.target,
+            "value": self.value
+        }
+
     def __repr__(self):
         match self.type:
             case ActionType.Play:
@@ -81,6 +120,10 @@ class Action:
 
 
 class HanabiInstance:
+    # TODO Max: Deal with the following variants:
+    # - Critical fours (need to calculate dark suits differently)
+    # - Reversed (need to store information somehow and pass this to the hanabi game class)
+    # - Up or Down (in the long run we also want this, but seems a bit tedious, not needed now)
     def __init__(
             self,
             deck: List[DeckCard],
@@ -92,7 +135,8 @@ class HanabiInstance:
             clue_starved: bool = False,  # if true, discarding and playing fives only gives back half a clue
             fives_give_clue: bool = True,  # if false, then playing a five will not change the clue count
             deck_plays: bool = False,
-            all_or_nothing: bool = False
+            all_or_nothing: bool = False,
+            starting_player: int = 0  # defines index of player that starts the game
     ):
         # defining properties
         self.deck = deck
@@ -104,6 +148,7 @@ class HanabiInstance:
         self.deck_plays = deck_plays,
         self.all_or_nothing = all_or_nothing
         assert not self.all_or_nothing, "All or nothing not implemented"
+        self.starting_player = starting_player
 
         # normalize deck indices
         for (idx, card) in enumerate(self.deck):
@@ -144,9 +189,13 @@ class HanabiInstance:
     def clue_increment(self):
         return 0.5 if self.clue_starved else 1
 
+    @property
+    def dark_suits(self):
+        return list(range(self.num_suits - self.num_dark_suits, self.num_suits))
+
 
 class GameState:
-    def __init__(self, instance: HanabiInstance, starting_player: int = 0):
+    def __init__(self, instance: HanabiInstance):
         # will not be modified
         self.instance = instance
 
@@ -157,7 +206,7 @@ class GameState:
         self.stacks = [0 for i in range(0, self.instance.num_suits)]
         self.strikes = 0
         self.clues = 8
-        self.turn = starting_player
+        self.turn = self.instance.starting_player
         self.pace = self.instance.initial_pace
         self.remaining_extra_turns = self.instance.num_players + 1
         self.trash = []
@@ -205,6 +254,21 @@ class GameState:
         self.clues -= 1
         self._make_turn()
 
+    def make_action(self, action):
+        match action.type:
+            case ActionType.ColorClue | ActionType.RankClue:
+                assert self.clues >= 1
+                self.actions.append(action)
+                self.clues -= 1
+                self._make_turn()
+                # TODO: could check that the clue specified is in fact legal
+            case ActionType.Play:
+                self.play(action.target)
+            case ActionType.Discard:
+                self.discard(action.target)
+            case ActionType.EndGame | ActionType.VoteTerminate:
+                self.over = True
+
     # Forward some properties of the underlying instance
     @property
     def num_players(self):
@@ -230,6 +294,10 @@ class GameState:
     def deck_size(self):
         return self.instance.deck_size
 
+    @property
+    def draw_pile_size(self):
+        return self.deck_size - self.progress
+
     # Properties of GameState
 
     def is_over(self):
@@ -253,6 +321,23 @@ class GameState:
 
     # Utilities
 
+    def is_playable(self, card: DeckCard):
+        return self.stacks[card.suitIndex] + 1 == card.rank
+
+    def is_trash(self, card: DeckCard):
+        return self.stacks[card.suitIndex] >= card.rank
+
+    def is_critical(self, card: DeckCard):
+        if card.rank == 5:
+            return True
+        if self.is_trash(card):
+            return False
+        count = 0
+        for hand in self.hands:
+            count += hand.count(card)
+        count += self.deck[self.progress:].count(card)
+        return count == 1
+
     def holding_players(self, card):
         for (player, hand) in enumerate(self.hands):
             if card in hand:
@@ -267,9 +352,9 @@ class GameState:
             )
             )
         return {
-            "deck": self.instance.deck,
+            "deck": [card.to_json() for card in self.instance.deck],
             "players": self.instance.player_names,
-            "actions": self.actions,
+            "actions": [action.to_json() for action in self.actions],
             "first_player": 0,
             "options": {
                 "variant": "No Variant",

src/hanabi/live/check_game.py

@@ -1,12 +1,14 @@
 import copy
-from typing import Tuple, Optional
+from typing import Tuple
 
-from database.database import conn
+from hanabi import logger
-from compress import decompress_deck, decompress_actions, link
+from hanabi import database
-from hanabi import Action, GameState
+from hanabi import hanab_game
-from hanab_live import HanabLiveInstance, HanabLiveGameState
+from hanabi.live import hanab_live
-from sat import solve_sat
+from hanabi.live import compress
-from log_setup import logger
+from hanabi.solvers import sat
+
+from hanabi.database import games_db_interface
 
 
 # returns minimal number T of turns (from game) after which instance was infeasible
@@ -16,59 +18,55 @@ from log_setup import logger
 # returns 1 if instance is feasible but first turn is suboptimal
 # ...
 # # turns + 1 if the final state is still winning
-def check_game(game_id: int) -> Tuple[int, GameState]:
+def check_game(game_id: int) -> Tuple[int, hanab_game.GameState]:
     logger.debug("Analysing game {}".format(game_id))
-    with conn.cursor() as cur:
+    with database.conn.cursor() as cur:
-        cur.execute("SELECT games.num_players, deck, actions, score, games.variant_id FROM games "
+        cur.execute("SELECT games.num_players, score, games.variant_id, starting_player FROM games "
-                    "INNER JOIN seeds ON seeds.seed = games.seed "
                     "WHERE games.id = (%s)",
                     (game_id,)
                     )
         res = cur.fetchone()
         if res is None:
             raise ValueError("No game associated with id {} in database.".format(game_id))
-        (num_players, compressed_deck, compressed_actions, score, variant_id) = res
+        (num_players, score, variant_id, starting_player) = res
-        deck = decompress_deck(compressed_deck)
+        instance, actions = games_db_interface.load_game_parts(game_id)
-        actions = decompress_actions(compressed_actions)
-
-        instance = HanabLiveInstance(deck, num_players, variant_id=variant_id)
 
+        # check if the instance is already won
         if instance.max_score == score:
-            game = HanabLiveGameState(instance)
+            game = hanab_live.HanabLiveGameState(instance)
             for action in actions:
                 game.make_action(action)
             # instance has been won, nothing to compute here
             return len(actions) + 1, game
 
+        # first, check if the instance itself is feasible:
+        game = hanab_live.HanabLiveGameState(instance)
+        solvable, solution = sat.solve_sat(game)
+        if not solvable:
+            return 0, solution
+        logger.verbose("Instance {} is feasible after 0 turns: {}".format(game_id, compress.link(solution)))
+
         # store lower and upper bounds of numbers of turns after which we know the game was feasible / infeasible
         solvable_turn = 0
         unsolvable_turn = len(actions)
 
-        # first, check if the instance itself is feasible:
-        game = HanabLiveGameState(instance)
-        solvable, solution = solve_sat(game)
-        if not solvable:
-            logger.debug("Returning: Instance {} is not feasible.")
-            return 0, solution
-        logger.verbose("Instance {} is feasible after 0 turns: {}".format(game_id, link(solution)))
-
         while unsolvable_turn - solvable_turn > 1:
             try_turn = (unsolvable_turn + solvable_turn) // 2
             try_game = copy.deepcopy(game)
-            assert(len(try_game.actions) == solvable_turn)
+            assert len(try_game.actions) == solvable_turn
             for a in range(solvable_turn, try_turn):
                 try_game.make_action(actions[a])
             logger.debug("Checking if instance {} is feasible after {} turns.".format(game_id, try_turn))
-            solvable, potential_sol = solve_sat(try_game)
+            solvable, potential_sol = sat.solve_sat(try_game)
             if solvable:
                 solution = potential_sol
                 game = try_game
                 solvable_turn = try_turn
                 logger.verbose("Instance {} is feasible after {} turns: {}#{}"
-                               .format(game_id, solvable_turn, link(solution), solvable_turn + 1))
+                               .format(game_id, solvable_turn, compress.link(solution), solvable_turn + 1))
             else:
                 unsolvable_turn = try_turn
                 logger.verbose("Instance {} is not feasible after {} turns.".format(game_id, unsolvable_turn))
 
-        assert unsolvable_turn - 1 == solvable_turn, "Programming error"
+        assert unsolvable_turn - 1 == solvable_turn
         return unsolvable_turn, solution

src/hanabi/live/compress.py

@@ -0,0 +1,224 @@
+from typing import List, Union
+
+import more_itertools
+
+from hanabi import hanab_game
+from hanabi.live import hanab_live
+
+# use same BASE62 as on hanab.live to encode decks
+BASE62 = "abcdefghijklmnopqrstuvwxyz0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"
+
+
+# Helper method, iterate over chunks of length n in a string
+def chunks(s: str, n: int):
+    for i in range(0, len(s), n):
+        yield s[i:i + n]
+
+
+# exception thrown by decompression methods if parsing fails
+class InvalidFormatError(ValueError):
+    pass
+
+
+def compress_actions(actions: List[hanab_game.Action]) -> str:
+    min_type = 0
+    max_type = 0
+    if len(actions) != 0:
+        min_type = min(map(lambda a: a.type.value, actions))
+        max_type = max(map(lambda a: a.type.value, actions))
+    type_range = max_type - min_type + 1
+
+    def compress_action(action):
+        # We encode action values with +1 to differentiate
+        # null (encoded 0) and 0 (encoded 1)
+        value = 0 if action.value is None else action.value + 1
+        if action.type == hanab_game.ActionType.VoteTerminate:
+            # This is currently a hack, the actual format has a 10 here,
+            # but we cannot encode this
+            value = 0
+        try:
+            a = BASE62[type_range * value + (action.type.value - min_type)]
+            b = BASE62[action.target]
+        except IndexError as e:
+            raise ValueError("Encoding action failed, value too large, found {}".format(value)) from e
+        return a + b
+
+    return "{}{}{}".format(
+        min_type,
+        max_type,
+        ''.join(map(compress_action, actions))
+    )
+
+
+def decompress_actions(actions_str: str) -> List[hanab_game.Action]:
+    if not len(actions_str) >= 2:
+        raise InvalidFormatError("min/max range not specified, found: {}".format(actions_str))
+    try:
+        min_type = int(actions_str[0])
+        max_type = int(actions_str[1])
+    except ValueError as e:
+        raise InvalidFormatError(
+            "min/max range of actions not specified, expected two integers, found {}".format(actions_str[:2])
+        ) from e
+    if not min_type <= max_type:
+        raise InvalidFormatError("min/max range illegal, found [{},{}]".format(min_type, max_type))
+    type_range = max_type - min_type + 1
+
+    if not len(actions_str) % 2 == 0:
+        raise InvalidFormatError("Invalid action string length: Expected even number of characters")
+
+    for (index, char) in enumerate(actions_str[2:]):
+        if char not in BASE62:
+            raise InvalidFormatError(
+                "Invalid character at index {}: Found {}, expected one of {}".format(
+                    index, char, BASE62
+                )
+            )
+
+    def decompress_action(action_idx: int, action: str):
+        try:
+            action_type_value = (BASE62.index(action[0]) % type_range) + min_type
+            action_type = hanab_game.ActionType(action_type_value)
+        except ValueError as e:
+            raise InvalidFormatError(
+                "Invalid action type at action {}: Found {}, expected one of {}".format(
+                    action_idx, action_type_value,
+                    [action_type.value for action_type in hanab_game.ActionType]
+                )
+            ) from e
+
+        # We encode values with +1 to differentiate null (encoded 0) and 0 (encoded 1)
+        value = BASE62.index(action[0]) // type_range - 1
+        if value == -1:
+            value = None
+        if action_type in [hanab_game.ActionType.Play, hanab_game.ActionType.Discard]:
+            if value is not None:
+                raise InvalidFormatError(
+                    "Invalid action value: Action at action index {} is Play/Discard, expected value None, "
+                    "found: {}".format(action_idx, value)
+                )
+        target = BASE62.index(action[1])
+        return hanab_game.Action(action_type, target, value)
+
+    return [decompress_action(idx, a) for (idx, a) in enumerate(chunks(actions_str[2:], 2))]
+
+
+def compress_deck(deck: List[hanab_game.DeckCard]) -> str:
+    assert (len(deck) != 0)
+    min_rank = min(map(lambda card: card.rank, deck))
+    max_rank = max(map(lambda card: card.rank, deck))
+    rank_range = max_rank - min_rank + 1
+
+    def compress_card(card):
+        try:
+            return BASE62[rank_range * card.suitIndex + (card.rank - min_rank)]
+        except IndexError as e:
+            raise InvalidFormatError(
+                "Could not compress card, suit or rank too large. Found: {}".format(card)
+            ) from e
+
+    return "{}{}{}".format(
+        min_rank,
+        max_rank,
+        ''.join(map(compress_card, deck))
+    )
+
+
+def decompress_deck(deck_str: str) -> List[hanab_game.DeckCard]:
+    if len(deck_str) < 2:
+        raise InvalidFormatError("min/max rank range not specified, found: {}".format(deck_str))
+    try:
+        min_rank = int(deck_str[0])
+        max_rank = int(deck_str[1])
+    except ValueError as e:
+        raise InvalidFormatError(
+            "min/max rank range not specified, expected two integers, found {}".format(deck_str[:2])
+        ) from e
+    if not max_rank >= min_rank:
+        raise InvalidFormatError(
+            "Invalid rank range, found [{},{}]".format(min_rank, max_rank)
+        )
+    rank_range = max_rank - min_rank + 1
+
+    for (index, char) in enumerate(deck_str[2:]):
+        if char not in BASE62:
+            raise InvalidFormatError(
+                "Invalid character at index {}: Found {}, expected one of {}".format(
+                    index, char, BASE62
+                )
+            )
+
+    def decompress_card(card_char):
+        encoded = BASE62.index(card_char)
+        suit_index = encoded // rank_range
+        rank = encoded % rank_range + min_rank
+        return hanab_game.DeckCard(suit_index, rank)
+
+    return [decompress_card(card) for card in deck_str[2:]]
+
+
+# compresses a standard GameState object into hanab.live format
+# which can be used in json replay links
+# The GameState object has to be standard / fitting hanab.live variants,
+# otherwise compression is not possible
+def compress_game_state(state: Union[hanab_game.GameState, hanab_live.HanabLiveGameState]) -> str:
+    if isinstance(state, hanab_live.HanabLiveGameState):
+        var_id = state.instance.variant_id
+    else:
+        assert isinstance(state, hanab_game.GameState)
+        var_id = hanab_live.HanabLiveInstance.select_standard_variant_id(state.instance)
+    out = "{}{},{},{}".format(
+        state.instance.num_players,
+        compress_deck(state.instance.deck),
+        compress_actions(state.actions),
+        var_id
+    )
+    with_dashes = ''.join(more_itertools.intersperse("-", out, 20))
+    return with_dashes
+
+
+def decompress_game_state(game_str: str) -> hanab_live.HanabLiveGameState:
+    game_str = game_str.replace("-", "")
+    parts = game_str.split(",")
+    if not len(parts) == 3:
+        raise InvalidFormatError(
+            "Expected 3 comma-separated parts of game, found {}".format(
+                len(parts)
+            )
+        )
+    [players_deck, actions, variant_id] = parts
+    if len(players_deck) == 0:
+        raise InvalidFormatError("Expected nonempty first part")
+    try:
+        num_players = int(players_deck[0])
+    except ValueError as e:
+        raise InvalidFormatError(
+            "Expected number of players, found: {}".format(players_deck[0])
+        ) from e
+
+    try:
+        deck = decompress_deck(players_deck[1:])
+    except InvalidFormatError as e:
+        raise InvalidFormatError("Error while parsing deck") from e
+
+    try:
+        actions = decompress_actions(actions)
+    except InvalidFormatError as e:
+        raise InvalidFormatError("Error while parsing actions") from e
+
+    try:
+        variant_id = int(variant_id)
+    except ValueError:
+        raise ValueError("Expected variant id, found: {}".format(variant_id))
+
+    instance = hanab_live.HanabLiveInstance(deck, num_players, variant_id)
+    game = hanab_live.HanabLiveGameState(instance)
+
+    # TODO: game is not in consistent state
+    game.actions = actions
+    return game
+
+
+def link(game_state: hanab_game.GameState) -> str:
+    compressed = compress_game_state(game_state)
+    return "https://hanab.live/shared-replay-json/{}".format(compressed)

src/hanabi/live/download_data.py

@@ -0,0 +1,363 @@
+import alive_progress
+from typing import Dict, Optional, List
+
+import psycopg2.errors
+import psycopg2.extras
+import platformdirs
+import unidecode
+
+from hanabi import hanab_game
+from hanabi import constants
+from hanabi import logger
+from hanabi import database
+from hanabi.live import site_api
+from hanabi.live import variants
+from hanabi.live import hanab_live
+
+from hanabi.database import games_db_interface
+
+
+
+class GameExportError(ValueError):
+    def __init__(self, game_id, msg):
+        super().__init__("When exporting game {}: {}".format(game_id, msg))
+
+    pass
+
+
+class GameExportNoResponseFromSiteError(GameExportError):
+    def __init__(self, game_id):
+        super().__init__(game_id, "No response from site")
+
+
+class GameExportInvalidResponseTypeError(GameExportError):
+    def __init__(self, game_id, response_type):
+        super().__init__(game_id, "Invalid response type (expected json, got {})".format(
+            response_type, game_id
+        ))
+
+    pass
+
+
+class GameExportInvalidFormatError(GameExportError):
+    def __init__(self, game_id, msg):
+        super().__init__(game_id, "Invalid response format: {}".format(msg))
+
+
+class GameExportInvalidNumberOfPlayersError(GameExportInvalidFormatError):
+    def __init__(self, game_id, expected, received):
+        super().__init__(
+            game_id,
+            "Received invalid list of players: Expected {} many, got {}".format(expected, received)
+        )
+
+
+def ensure_users_in_db_and_get_ids(usernames: List[str]):
+    normalized_usernames = [unidecode.unidecode(username) for username in usernames]
+    psycopg2.extras.execute_values(
+        database.cur,
+        "INSERT INTO users (username, normalized_username)"
+        "VALUES %s "
+        "ON CONFLICT (username) DO NOTHING ",
+        zip(usernames, normalized_usernames)
+    )
+
+    # To only do one DB query, we sort by the normalized username.
+    ids = []
+    for username in usernames:
+        database.cur.execute(
+            "SELECT id FROM users "
+            "WHERE username = %s",
+            (username,)
+        )
+        (id, ) = database.cur.fetchone()
+        ids.append(id)
+
+    return ids
+
+#
+def detailed_export_game(
+          game_id: int
+        , score: Optional[int] = None
+        , var_id: Optional[int] = None
+        , seed_exists: bool = False
+) -> None:
+    """
+    Downloads full details of game from hanab.live, inserts seed and game into DB
+    If seed is already present, it is left as is
+    If game is already present, game details will be updated
+
+    :param game_id: id of game to export
+    :param score: If given, this will be inserted as score of the game. If not given, score is calculated
+    :param var_id: If given, this will be inserted as variant id of the game. If not given, this is looked up
+    :param seed_exists: If specified and true, assumes that the seed is already present in database.
+        If this is not the case, call will raise a DB insertion error
+
+    :raises GameExportError and its child classes
+    """
+
+    logger.debug("Importing game {}".format(game_id))
+
+    game_json = site_api.get("export/{}".format(game_id))
+    if game_json is None:
+        raise GameExportNoResponseFromSiteError(game_id)
+    if type(game_json) != dict:
+        raise GameExportInvalidResponseTypeError(game_id, type(game_json))
+
+    if game_json.get('id', None) != game_id:
+        raise GameExportInvalidFormatError(game_id, "Unexpected game_id {} received, expected {}".format(
+            game_json.get('id'), game_id
+        ))
+
+    players = game_json.get('players', [])
+    num_players = len(players)
+    if num_players < 2:
+        raise GameExportInvalidNumberOfPlayersError(game_id, "≥2", num_players)
+
+    seed = game_json.get('seed', None)
+    if type(seed) != str:
+        raise GameExportInvalidFormatError(game_id, "Unexpected seed, expected string, got {}".format(seed))
+
+    options = game_json.get('options', {})
+    var_id = var_id or variants.variant_id(options.get('variant', 'No Variant'))
+    timed = options.get('timed', False)
+    time_base = options.get('timeBase', 0)
+    time_per_turn = options.get('timePerTurn', 0)
+    speedrun = options.get('speedrun', False)
+    card_cycle = options.get('cardCycle', False)
+    deck_plays = options.get('deckPlays', False)
+    empty_clues = options.get('emptyClues', False)
+    one_extra_card = options.get('oneExtraCard', False)
+    one_less_card = options.get('oneLessCard', False)
+    all_or_nothing = options.get('allOrNothing', False)
+    detrimental_characters = options.get('detrimentalCharacters', False)
+
+    starting_player = options.get('startingPlayer', 0)
+
+    try:
+        actions = [hanab_game.Action.from_json(action) for action in game_json.get('actions', [])]
+    except hanab_game.ParseError as e:
+        raise GameExportInvalidFormatError(game_id, "Failed to parse actions") from e
+
+    try:
+        deck = [hanab_game.DeckCard.from_json(card) for card in game_json.get('deck', None)]
+    except hanab_game.ParseError as e:
+        raise GameExportInvalidFormatError(game_id, "Failed to parse deck") from e
+
+    if score is None:
+        # need to play through the game once to find out its score
+        if detrimental_characters:
+            raise NotImplementedError(
+                "detrimental characters not supported, cannot determine score of game {}".format(game_id)
+            )
+        game = hanab_live.HanabLiveGameState(
+            hanab_live.HanabLiveInstance(
+                deck, num_players, var_id,
+                deck_plays=deck_plays,
+                one_less_card=one_less_card,
+                one_extra_card=one_extra_card,
+                all_or_nothing=all_or_nothing,
+                starting_player=starting_player
+            )
+        )
+        for action in actions:
+            game.make_action(action)
+        score = game.score
+
+    if not seed_exists:
+        database.cur.execute(
+            "INSERT INTO seeds (seed, num_players, starting_player, variant_id)"
+            "VALUES (%s, %s, %s, %s)"
+            "ON CONFLICT (seed) DO NOTHING",
+            (seed, num_players, starting_player, var_id)
+        )
+        logger.debug("New seed {} imported.".format(seed))
+
+        games_db_interface.store_deck_for_seed(seed, deck)
+
+    database.cur.execute(
+        "INSERT INTO games ("
+        "id, num_players, starting_player, variant_id, timed, time_base, time_per_turn, speedrun, card_cycle, "
+        "deck_plays, empty_clues, one_extra_card, one_less_card,"
+        "all_or_nothing, detrimental_characters, seed, score"
+        ")"
+        "VALUES (%s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s)"
+        "ON CONFLICT (id) DO UPDATE SET ("
+        "timed, time_base, time_per_turn, speedrun, card_cycle, deck_plays, empty_clues, one_extra_card,"
+        "all_or_nothing, detrimental_characters"
+        ") = ("
+        "EXCLUDED.timed, EXCLUDED.time_base, EXCLUDED.time_per_turn, EXCLUDED.speedrun, EXCLUDED.card_cycle, "
+        "EXCLUDED.deck_plays, EXCLUDED.empty_clues, EXCLUDED.one_extra_card,"
+        "EXCLUDED.all_or_nothing, EXCLUDED.detrimental_characters"
+        ")",
+        (
+            game_id, num_players, starting_player, var_id, timed, time_base, time_per_turn, speedrun, card_cycle,
+            deck_plays, empty_clues, one_extra_card, one_less_card,
+            all_or_nothing, detrimental_characters, seed, score
+        )
+    )
+
+    # Insert participants into database
+    ids = ensure_users_in_db_and_get_ids(players)
+    game_participant_values = []
+    for index, user_id in enumerate(ids):
+        game_participant_values.append((game_id, user_id, index))
+    psycopg2.extras.execute_values(
+        database.cur,
+        "INSERT INTO game_participants (game_id, user_id, seat) VALUES %s "
+        "ON CONFLICT (game_id, user_id) DO UPDATE SET seat = excluded.seat",
+        game_participant_values
+    )
+
+    games_db_interface.store_actions(game_id, actions)
+
+    logger.debug("Imported game {}".format(game_id))
+
+
+def _process_game_row(game: Dict, var_id, export_all_games: bool = False):
+    game_id = game.get('id', None)
+    seed = game.get('seed', None)
+    num_players = game.get('num_players', None)
+    users = game.get('users', "").split(", ")
+    score = game.get('score', None)
+
+    if any(v is None for v in [game_id, seed, num_players, score]):
+        raise ValueError("Unknown response format on hanab.live")
+
+    if len(users) != num_players:
+        logger.error("Invalid number of players reported when processing row {}".format(game))
+        f = platformdirs.user_data_dir(constants.APP_NAME, ensure_exists=True) + '/invalid_game_ids.txt'
+        with open(f, "a+") as invalid_games_file:
+            invalid_games_file.writelines(
+                "{}, {}, {}, {}\n".format(game_id, var_id, num_players, ", ".join(users))
+            )
+        return
+#        raise GameExportInvalidNumberOfPlayersError(game_id, num_players, users)
+
+    # Ensure users in database and find out their ids
+
+    if export_all_games:
+        detailed_export_game(game_id, score=score, var_id=var_id)
+        logger.debug("Imported game {}".format(game_id))
+        return
+
+    database.cur.execute("SAVEPOINT seed_insert")
+    try:
+        database.cur.execute(
+            "INSERT INTO games (id, seed, num_players, score, variant_id)"
+            "VALUES"
+            "(%s, %s ,%s ,%s ,%s)"
+            "ON CONFLICT (id) DO NOTHING",
+            (game_id, seed, num_players, score, var_id)
+        )
+    except psycopg2.errors.ForeignKeyViolation:
+        # Sometimes, seed is not present in the database yet, then we will have to query the full game details
+        # (including the seed) to export it accordingly
+        database.cur.execute("ROLLBACK TO seed_insert")
+        detailed_export_game(game_id, score=score, var_id=var_id)
+    database.cur.execute("RELEASE seed_insert")
+
+    # Insert participants into database
+    ids = ensure_users_in_db_and_get_ids(users)
+    game_participant_values = []
+    for index, user_id in enumerate(ids):
+        game_participant_values.append((game_id, user_id, index))
+    psycopg2.extras.execute_values(
+        database.cur,
+        "INSERT INTO game_participants (game_id, user_id, seat) VALUES %s "
+        "ON CONFLICT (game_id, user_id) DO UPDATE SET seat = excluded.seat",
+        game_participant_values
+    )
+
+
+    logger.debug("Imported game {}".format(game_id))
+
+
+def download_all_games_not_in_db(download_known_but_not_exported=True):
+    database.cur.execute(
+        "SELECT id FROM games "
+        + "WHERE actions is not null" if download_known_but_not_exported else ""
+        + "ORDER BY id"
+    )
+    game_ids = [game_id for (game_id,) in database.cur.fetchall()]
+    largest_game_id = game_ids[-1]
+    with alive_progress.alive_bar(
+            total=largest_game_id - len(game_ids),
+            title='Downloading all games not in database'
+    ) as bar:
+        for game_id in range(1, largest_game_id):
+            if game_id == game_ids[0]:
+                game_ids = game_ids[1:]
+                continue
+            try:
+                detailed_export_game(game_id)
+                logger.info("Found new game {} that was not in DB before".format(game_id))
+                bar()
+            except GameExportNoResponseFromSiteError:
+                bar()
+                continue
+
+
+def download_games(var_id, export_all_games: bool = False):
+    name = variants.variant_name(var_id)
+    page_size = 100
+    if name is None:
+        raise ValueError("{} is not a known variant_id.".format(var_id))
+
+    url = "variants/{}".format(var_id)
+    r = site_api.api(url, refresh=True)
+    if not r:
+        raise RuntimeError("Failed to download request from hanab.live")
+
+    num_entries = r.get('total_rows', None)
+    if num_entries is None:
+        raise ValueError("Unknown response format on hanab.live")
+
+    database.cur.execute(
+        "SELECT COUNT(*) FROM games WHERE variant_id = %s AND id <= "
+        "(SELECT COALESCE (last_game_id, 0) FROM variant_game_downloads WHERE variant_id = %s)",
+        (var_id, var_id)
+    )
+    num_already_downloaded_games = database.cur.fetchone()[0]
+    assert num_already_downloaded_games <= num_entries, "Database inconsistent, too many games present."
+    next_page = num_already_downloaded_games // page_size
+    last_page = (num_entries - 1) // page_size
+
+    if num_already_downloaded_games == num_entries:
+        logger.info("Already downloaded all games ({:6} many) for variant {:4} [{}]".format(num_entries, var_id, name))
+        return
+
+    with alive_progress.alive_bar(
+            total=num_entries - num_already_downloaded_games,
+            title='Downloading remaining games for variant id {:4} [{}]'.format(var_id, name),
+            enrich_print=False
+    ) as bar:
+        for page in range(next_page, last_page + 1):
+            for refresh in [False, True]:
+                r = site_api.api(url + "?col[0]=0&page={}".format(page), refresh=(page == last_page) or refresh)
+                rows = r.get('rows', [])
+                if page == next_page:
+                    rows = rows[num_already_downloaded_games % 100:]
+                if not (page == last_page or len(rows) == page_size):
+                    if not refresh:
+                        # row count does not match, maybe this is due to an old cached version of the api query,
+                        # try again with a forced refresh of the query
+                        logger.verbose("refreshing page {} due to unexpected row count".format(page))
+                        continue
+                    # If refreshing did not fix the error, log a warning
+                    logger.warn('WARN: received unexpected row count ({}, expected {}) on page {}'.format(
+                        len(rows), page_size, page)
+                    )
+                for row in rows:
+                    _process_game_row(row, var_id, export_all_games)
+                    bar()
+                database.cur.execute(
+                    "INSERT INTO variant_game_downloads (variant_id, last_game_id) VALUES"
+                    "(%s, %s)"
+                    "ON CONFLICT (variant_id) DO UPDATE SET last_game_id = EXCLUDED.last_game_id",
+                    (var_id, r['rows'][-1]['id'])
+                )
+                database.conn.commit()
+                # we need this so that we don't execute the iteration with forced refresh
+                # if stuff already checked out without refreshing
+                break

src/hanabi/live/hanab_live.py

@@ -0,0 +1,146 @@
+from typing import List, Dict, Tuple
+
+from hanabi.hanab_game import Action, ParseError
+from hanabi import hanab_game
+from hanabi import constants
+from hanabi.live import variants
+
+
+class HanabLiveInstance(hanab_game.HanabiInstance):
+    def __init__(
+            self,
+            deck: List[hanab_game.DeckCard],
+            num_players: int,
+            variant_id: int,
+            one_extra_card: bool = False,
+            one_less_card: bool = False,
+            *args, **kwargs
+    ):
+        self.one_extra_card = one_extra_card
+        self.one_less_card = one_less_card
+        assert 2 <= num_players <= 6
+        hand_size = constants.HAND_SIZES[num_players]
+        if one_less_card:
+            hand_size -= 1
+        if one_extra_card:
+            hand_size += 1
+
+        super().__init__(deck, num_players, hand_size=hand_size, *args, **kwargs)
+        self.variant_id = variant_id
+        self.variant = variants.Variant.from_db(self.variant_id)
+
+
+    @staticmethod
+    def select_standard_variant_id(instance: hanab_game.HanabiInstance):
+        err_msg = "Hanabi instance not supported by hanab.live, cannot convert to HanabLiveInstance: "
+        assert 3 <= instance.num_suits <= 6, \
+            err_msg + "Illegal number of suits ({}) found, must be in range [3,6]".format(instance.num_suits)
+        assert 0 <= instance.num_dark_suits <= 2, \
+            err_msg + "Illegal number of dark suits ({}) found, must be in range [0,2]".format(instance.num_dark_suits)
+        assert 4 <= max(instance.num_suits, 4) - instance.num_dark_suits, \
+            err_msg + "Illegal ratio of dark suits to suits, can have at most {} dark suits with {} total suits".format(
+                max(instance.num_suits - 4, 0), instance.num_suits
+            )
+        return constants.VARIANT_IDS_STANDARD_DISTRIBUTIONS[instance.num_suits][instance.num_dark_suits]
+
+
+def parse_json_game(game_json: Dict, as_hanab_live_instance: bool = True) \
+        -> Tuple[HanabLiveInstance | hanab_game.HanabiInstance, List[Action]]:
+    game_id = game_json.get('id', None)
+    players = game_json.get('players', [])
+    num_players = len(players)
+    if num_players < 2 or num_players > 6:
+        raise ParseError(num_players)
+
+    options = game_json.get('options', {})
+    var_name = options.get('variant', 'No Variant')
+    deck_plays = options.get('deckPlays', False)
+    one_extra_card = options.get('oneExtraCard', False)
+    one_less_card = options.get('oneLessCard', False)
+    all_or_nothing = options.get('allOrNothing', False)
+    starting_player = options.get('startingPlayer', 0)
+    detrimental_characters = options.get('detrimentalCharacters', False)
+
+    try:
+        actions = [hanab_game.Action.from_json(action) for action in game_json.get('actions', [])]
+    except hanab_game.ParseError as e:
+        raise ParseError("Failed to parse actions") from e
+
+    try:
+        deck = [hanab_game.DeckCard.from_json(card) for card in game_json.get('deck', None)]
+    except hanab_game.ParseError as e:
+        raise ParseError("Failed to parse deck") from e
+
+    if detrimental_characters:
+        raise NotImplementedError(
+            "detrimental characters not supported, cannot determine score of game {}".format(game_id)
+        )
+    if as_hanab_live_instance:
+        var_id = variants.variant_id(var_name)
+        return HanabLiveInstance(
+            deck, num_players, var_id,
+            deck_plays=deck_plays,
+            one_less_card=one_less_card,
+            one_extra_card=one_extra_card,
+            all_or_nothing=all_or_nothing,
+            starting_player=starting_player
+        ), actions
+    else:
+        hand_size = constants.HAND_SIZES[num_players]
+        if one_less_card:
+            hand_size -= 1
+        if one_extra_card:
+            hand_size += 1
+
+        clue_starved = 'Clue Starved' in var_name
+
+        return hanab_game.HanabiInstance(
+            deck, num_players, hand_size,
+            clue_starved=clue_starved,
+            deck_plays=deck_plays,
+            all_or_nothing=all_or_nothing,
+            starting_player=starting_player
+        ), actions
+
+
+
+class HanabLiveGameState(hanab_game.GameState):
+    def __init__(self, instance: HanabLiveInstance):
+        super().__init__(instance)
+        self.instance: HanabLiveInstance = instance
+
+    def to_json(self):
+        return {
+            "actions": [action.to_json() for action in self.actions],
+            "deck": [card.to_json() for card in self.deck],
+            "players": ["Alice", "Bob", "Cathy", "Donald", "Emily", "Frank"][:self.num_players],
+            "notes": [[]] * self.num_players,
+            "options": {
+                "variant": self.instance.variant_id,
+                "deckPlays": self.instance.deck_plays,
+                "oneExtraCard": self.instance.one_extra_card,
+                "oneLessCard": self.instance.one_less_card,
+                "allOrNothing": self.instance.all_or_nothing,
+                "startingPlayer": self.instance.starting_player
+            }
+        }
+
+    def _waste_clue(self) -> hanab_game.Action:
+        for player in range(self.turn + 1, self.turn + self.num_players):
+            for card in self.hands[player % self.num_players]:
+                for rank in self.instance.variant.ranks:
+                    if self.instance.variant.rank_touches(card, rank):
+                        return hanab_game.Action(
+                            hanab_game.ActionType.RankClue,
+                            player % self.num_players,
+                            rank
+                        )
+                for color in range(self.instance.variant.num_colors):
+                    if self.instance.variant.color_touches(card, color):
+                        return hanab_game.Action(
+                            hanab_game.ActionType.ColorClue,
+                            player % self.num_players,
+                            color
+                        )
+        raise RuntimeError("Current game state did not permit any legal clue."
+                           "This case is incredibly rare and currently not handled.")

src/hanabi/live/instance_finder.py

@@ -0,0 +1,184 @@
+from typing import Optional
+import pebble.concurrent
+import concurrent.futures
+
+import traceback
+import alive_progress
+import threading
+import time
+
+from hanabi import logger
+from hanabi.solvers.sat import solve_sat
+from hanabi import database
+from hanabi.live import download_data
+from hanabi.live import compress
+from hanabi import hanab_game
+from hanabi.solvers import greedy_solver
+from hanabi.solvers import deck_analyzer
+from hanabi.live import variants
+
+MAX_PROCESSES = 6
+
+
+def update_trivially_feasible_games(variant_id):
+    variant: variants.Variant = variants.Variant.from_db(variant_id)
+    database.cur.execute("SELECT seed FROM seeds WHERE variant_id = (%s) AND feasible is null", (variant_id,))
+    seeds = database.cur.fetchall()
+    logger.verbose('Checking variant {} (id {}), found {} seeds to check...'.format(variant.name, variant_id, len(seeds)))
+
+    with alive_progress.alive_bar(total=len(seeds), title='{} ({})'.format(variant.name, variant_id)) as bar:
+        for (seed,) in seeds:
+            database.cur.execute(
+                "SELECT id, deck_plays, one_extra_card, one_less_card, all_or_nothing, detrimental_characters "
+                "FROM games WHERE score = (%s) AND seed = (%s) ORDER BY id;",
+                (variant.max_score, seed)
+            )
+            res = database.cur.fetchall()
+            logger.debug("Checking seed {}: {:3} results".format(seed, len(res)))
+            for (game_id, a, b, c, d, e) in res:
+                if None in [a, b, c, d, e]:
+                    logger.debug('  Game {} not found in database, exporting...'.format(game_id))
+                    download_data.detailed_export_game(
+                        game_id, var_id=variant_id, score=variant.max_score, seed_exists=True
+                    )
+                    database.cur.execute("SELECT deck_plays, one_extra_card, one_less_card, all_or_nothing, "
+                                         "detrimental_characters "
+                                         "FROM games WHERE id = (%s)",
+                                         (game_id,))
+                    (a, b, c, d, e) = database.cur.fetchone()
+                else:
+                    logger.debug('  Game {} already in database'.format(game_id))
+                valid = not any([a, b, c, d, e])
+                if valid:
+                    print(a, b, c, d, e)
+                    logger.verbose(
+                        'Seed {:10} (variant {}) found to be feasible via game {:6}'.format(seed, variant_id, game_id))
+                    database.cur.execute("UPDATE seeds SET (feasible, max_score_theoretical) = (%s, %s) WHERE seed = "
+                                         "(%s)", (True, variant.max_score, seed))
+                    database.cur.execute(
+                        "INSERT INTO score_lower_bounds (seed, score_lower_bound, game_id) VALUES (%s, %s, %s)",
+                        (seed, variant.max_score, game_id)
+                    )
+                    database.conn.commit()
+                    break
+                else:
+                    logger.verbose('  Cheaty game {} found'.format(game_id))
+            bar()
+
+
+def get_decks_for_all_seeds():
+    cur = database.conn.database.cursor()
+    cur.execute("SELECT id "
+                "FROM games "
+                "  INNER JOIN seeds "
+                "  ON seeds.seed = games.seed"
+                "    WHERE"
+                "      seeds.deck is null"
+                "      AND"
+                "      games.id = ("
+                "         SELECT id FROM games WHERE games.seed = seeds.seed LIMIT 1"
+                "     )"
+                )
+    print("Exporting decks for all seeds")
+    res = cur.fetchall()
+    with alive_progress.alive_bar(len(res), title="Exporting decks") as bar:
+        for (game_id,) in res:
+            download_data.detailed_export_game(game_id)
+            bar()
+
+
+mutex = threading.Lock()
+
+
+def solve_instance(instance: hanab_game.HanabiInstance):
+    # first, sanity check on running out of pace
+    result = deck_analyzer.analyze(instance)
+    if len(result) != 0:
+        logger.info("found infeasible deck by foreward analysis")
+        return False, None, None
+    for num_remaining_cards in [0, 20]:
+        #        logger.info("trying with {} remaining cards".format(num_remaining_cards))
+        game = hanab_game.GameState(instance)
+        strat = greedy_solver.GreedyStrategy(game)
+
+        # make a number of greedy moves
+        while not game.is_over() and not game.is_known_lost():
+            if num_remaining_cards != 0 and game.progress == game.deck_size - num_remaining_cards:
+                break  # stop solution here
+            strat.make_move()
+
+        # check if we won already
+        if game.is_won():
+            #            print("won with greedy strat")
+            return True, game, num_remaining_cards
+
+        # now, apply sat solver
+        if not game.is_over():
+            logger.debug("continuing greedy sol with SAT")
+            solvable, sol = solve_sat(game)
+            if solvable is None:
+                return True, sol, num_remaining_cards
+        logger.debug(
+            "No success with {} remaining cards, reducing number of greedy moves, failed attempt was: {}".format(
+                num_remaining_cards, compress.link(game)))
+    #    print("Aborting trying with greedy strat")
+    logger.debug("Starting full SAT solver")
+    game = hanab_game.GameState(instance)
+    a, b = solve_sat(game)
+    return a, b, instance.draw_pile_size
+
+
+@pebble.concurrent.process(timeout=150)
+def solve_seed_with_timeout(seed, num_players, deck_compressed, var_name: Optional[str] = None):
+    try:
+        logger.verbose("Starting to solve seed {}".format(seed))
+        deck = compress.decompress_deck(deck_compressed)
+        t0 = time.perf_counter()
+        solvable, solution, num_remaining_cards = solve_instance(hanab_game.HanabiInstance(deck, num_players))
+        t1 = time.perf_counter()
+        logger.verbose("Solved instance {} in {} seconds: {}".format(seed, round(t1 - t0, 2), solvable))
+
+        mutex.acquire()
+        if solvable is not None:
+            database.cur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (solvable, seed))
+            database.conn.commit()
+        mutex.release()
+
+        if solvable == True:
+            logger.verbose("Success with {} cards left in draw by greedy solver on seed {}: {}\n".format(
+                num_remaining_cards, seed, compress.link(solution))
+            )
+        elif solvable == False:
+            logger.debug("seed {} was not solvable".format(seed))
+            logger.debug('{}-player, seed {:10}, {}\n'.format(num_players, seed, var_name))
+        elif solvable is None:
+            logger.verbose("seed {} skipped".format(seed))
+        else:
+            raise Exception("Programming Error")
+
+    except Exception as e:
+        print("exception in subprocess:")
+        traceback.print_exc()
+
+
+def solve_seed(seed, num_players, deck_compressed, var_name: Optional[str] = None):
+    f = solve_seed_with_timeout(seed, num_players, deck_compressed, var_name)
+    try:
+        return f.result()
+    except TimeoutError:
+        logger.verbose("Solving on seed {} timed out".format(seed))
+        return
+
+
+def solve_unknown_seeds(variant_id, variant_name: Optional[str] = None):
+    database.cur.execute(
+        "SELECT seed, num_players, deck FROM seeds WHERE variant_id = (%s) AND feasible IS NULL",
+        (variant_id,)
+    )
+    res = database.cur.fetchall()
+
+    with concurrent.futures.ProcessPoolExecutor(max_workers=MAX_PROCESSES) as executor:
+        fs = [executor.submit(solve_seed, r[0], r[1], r[2], variant_name) for r in res]
+        with alive_progress.alive_bar(len(res), title='Seed solving on {}'.format(variant_name)) as bar:
+            for f in concurrent.futures.as_completed(fs):
+                bar()

src/hanabi/live/site_api.py

@@ -1,25 +1,35 @@
 import json
-import requests
+from typing import Optional, Dict
-import requests_cache
-from log_setup import logger
 
+import requests_cache
+import platformdirs
+
+from hanabi import logger
+from hanabi import constants
 
 # Cache all requests to site to reduce traffic and latency
-session = requests_cache.CachedSession('hanab.live')
+session = requests_cache.CachedSession(
+    platformdirs.user_cache_dir(constants.APP_NAME) + '/hanab.live',
+    urls_expire_after={
+        'hanab.live/export/*': requests_cache.NEVER_EXPIRE
+    }
+)
 
 
-def get(url, refresh=False):
+def get(url, refresh=False) -> Optional[Dict | str]:
     #    print("sending request for " + url)
     query = "https://hanab.live/" + url
     logger.debug("GET {} (force_refresh={})".format(query, refresh))
     response = session.get(query, force_refresh=refresh)
     if not response:
-        logger.error("Failed to get request {} from hanab.live".format(query))
+        logger.debug("Failed to get request {} from hanab.live".format(query))
         return None
     if not response.status_code == 200:
+        logger.debug("Request {} from hanab.live produced status code {}".format(query, response.status_code))
         return None
     if "application/json" in response.headers['content-type']:
         return json.loads(response.text)
+    return response.text
 
 
 def api(url, refresh=False):

src/hanabi/live/variants.py

@@ -1,36 +1,44 @@
 import enum
 from typing import List, Optional
-from hanabi import DeckCard, ActionType
+from hanabi import hanab_game
 
-from database.database import cur
+from hanabi import database
 
 
 def variant_id(name) -> Optional[int]:
-    cur.execute(
+    database.cur.execute(
         "SELECT id FROM variants WHERE name = %s",
         (name,)
     )
-    var_id = cur.fetchone()
+    var_id = database.cur.fetchone()
     if var_id is not None:
         return var_id[0]
 
 
+def get_all_variant_ids() -> List[int]:
+    database.cur.execute(
+        "SELECT id FROM variants "
+        "ORDER BY id"
+    )
+    return [var_id for (var_id,) in database.cur.fetchall()]
+
+
 def variant_name(var_id) -> Optional[int]:
-    cur.execute(
+    database.cur.execute(
         "SELECT name FROM variants WHERE id = %s",
         (var_id,)
     )
-    name = cur.fetchone()
+    name = database.cur.fetchone()
     if name is not None:
         return name[0]
 
 
 def num_suits(var_id) -> Optional[int]:
-    cur.execute(
+    database.cur.execute(
         "SELECT num_suits FROM variants WHERE id = %s",
         (var_id,)
     )
-    num = cur.fetchone()
+    num = database.cur.fetchone()
     if num is not None:
         return num
 
@@ -82,19 +90,19 @@ class Suit:
 
     @staticmethod
     def from_db(suit_id):
-        cur.execute(
+        database.cur.execute(
             "SELECT name, display_name, abbreviation, rank_clues, color_clues, prism, dark, reversed "
             "FROM suits "
             "WHERE id = %s",
             (suit_id,)
         )
-        suit_properties = cur.fetchone()
+        suit_properties = database.cur.fetchone()
 
-        cur.execute(
+        database.cur.execute(
             "SELECT color_id FROM suit_colors WHERE suit_id = %s",
             (suit_id,)
         )
-        colors = list(map(lambda t: t[0], cur.fetchall()))
+        colors = list(map(lambda t: t[0], database.cur.fetchall()))
         return Suit(*suit_properties, colors)
 
 
@@ -161,7 +169,7 @@ class Variant:
     def _synesthesia_ranks(self, color_value: int) -> List[int]:
         return [rank for rank in self.ranks if (rank - color_value) % len(self.colors) == 0]
 
-    def rank_touches(self, card: DeckCard, value: int):
+    def rank_touches(self, card: hanab_game.DeckCard, value: int):
         assert 0 <= card.suitIndex < self.num_suits,\
             f"Unexpected card {card}, suitIndex {card.suitIndex} out of bounds for {self.num_suits} suits."
         assert not self.no_rank_clues, "Cluing rank not allowed in this variant."
@@ -186,7 +194,7 @@ class Variant:
         ranks = self._preprocess_rank(value)
         return any(self.suits[card.suitIndex].rank_touches(card.rank, rank) for rank in ranks)
 
-    def color_touches(self, card: DeckCard, value: int):
+    def color_touches(self, card: hanab_game.DeckCard, value: int):
         assert 0 <= card.suitIndex < self.num_suits, \
             f"Unexpected card {card}, suitIndex {card.suitIndex} out of bounds for {self.num_suits} suits."
         assert not self.no_color_clues, "Cluing color not allowed in this variant."
@@ -224,7 +232,7 @@ class Variant:
 
     @staticmethod
     def from_db(var_id):
-        cur.execute(
+        database.cur.execute(
             "SELECT "
             "name, clue_starved, throw_it_in_a_hole, alternating_clues, synesthesia, chimneys, funnels, "
             "no_color_clues, no_rank_clues, empty_color_clues, empty_rank_clues, odds_and_evens, up_or_down,"
@@ -232,14 +240,14 @@ class Variant:
             "FROM variants WHERE id = %s",
             (var_id,)
         )
-        var_properties = cur.fetchone()
+        var_properties = database.cur.fetchone()
 
-        cur.execute(
+        database.cur.execute(
             "SELECT suit_id FROM variant_suits "
             "WHERE variant_id = %s "
             "ORDER BY index",
             (var_id,)
         )
-        var_suits = [Suit.from_db(*s) for s in cur.fetchall()]
+        var_suits = [Suit.from_db(*s) for s in database.cur.fetchall()]
 
         return Variant(*var_properties, var_suits)

src/hanabi/logger_setup.py

@@ -1,5 +1,10 @@
 import logging
+import os
+
 import verboselogs
+import platformdirs
+
+from hanabi import constants
 
 
 class LoggerManager:
@@ -24,20 +29,22 @@ class LoggerManager:
             '%(message)s'
         )
 
-
         self.console_handler = logging.StreamHandler()
         self.console_handler.setLevel(console_level)
         self.console_handler.setFormatter(self.nothing_formatter)
 
-        self.debug_file_handler = logging.FileHandler("debug_log.txt")
+        log_dir = platformdirs.user_log_dir(constants.APP_NAME)
+        os.makedirs(log_dir, exist_ok=True)
+
+        self.debug_file_handler = logging.FileHandler(log_dir + "/debug_log.txt")
         self.debug_file_handler.setFormatter(self.file_formatter)
         self.debug_file_handler.setLevel(logging.DEBUG)
 
-        self.verbose_file_handler = logging.FileHandler("verbose_log.txt")
+        self.verbose_file_handler = logging.FileHandler(log_dir + "/verbose_log.txt")
         self.verbose_file_handler.setFormatter(self.file_formatter)
         self.verbose_file_handler.setLevel(verboselogs.VERBOSE)
 
-        self.info_file_handler = logging.FileHandler("log.txt")
+        self.info_file_handler = logging.FileHandler(log_dir + "/log.txt")
         self.info_file_handler.setFormatter(self.info_file_formatter)
         self.info_file_handler.setLevel(logging.INFO)
 

src/hanabi/solvers/deck_analyzer.py

@@ -0,0 +1,195 @@
+from enum import Enum
+from typing import List
+
+import alive_progress
+
+from hanabi import database
+from hanabi import logger
+from hanabi import hanab_game
+from hanabi.live import compress
+
+
+class InfeasibilityType(Enum):
+    OutOfPace = 0  # idx denotes index of last card drawn before being forced to reduce pace, value denotes how bad pace is
+    OutOfHandSize = 1  # idx denotes index of last card drawn before being forced to discard a crit
+    CritAtBottom = 3
+
+
+class InfeasibilityReason:
+    def __init__(self, infeasibility_type: InfeasibilityType, score_upper_bound, value=None):
+        self.type = infeasibility_type
+        self.score_upper_bound = score_upper_bound
+        self.value = value
+
+    def __repr__(self):
+        match self.type:
+            case InfeasibilityType.OutOfPace:
+                return "Upper bound {}, since deck runs out of pace after drawing card {}".format(self.score_upper_bound, self.value)
+            case InfeasibilityType.OutOfHandSize:
+                return "Upper bound {}, since deck runs out of hand size after drawing card {}".format(self.score_upper_bound, self.value)
+            case InfeasibilityType.CritAtBottom:
+                return "Upper bound {}, sicne deck has critical non-5 at bottom".format(self.score_upper_bound)
+
+
+def analyze(instance: hanab_game.HanabiInstance, only_find_first=False) -> List[InfeasibilityReason]:
+    """
+    Checks instance for the following (easy) certificates for unfeasibility
+    - There is a critical non-5 at the bottom
+    - We necessarily run out of pace when playing this deck:
+        At some point, among all drawn cards, there are too few playable ones so that the next discard
+        reduces pace to a negative amount
+    - We run out of hand size when playing this deck:
+        At some point, there are too many critical cards (that also could not have been played) for the players
+        to hold collectively
+    :param instance: Instance to be analyzed
+    :param only_find_first: If true, we immediately return when finding the first infeasibility reason and don't
+        check for further ones. Might be slightly faster on some instances, especially dark ones.
+    :return: List with all reasons found. Empty if none is found.
+        In particular, if return value is not the empty list, the analyzed instance is unfeasible
+    """
+    reasons = []
+
+    # check for critical non-fives at bottom of the deck
+    bottom_card = instance.deck[-1]
+    if bottom_card.rank != 5 and bottom_card.suitIndex in instance.dark_suits:
+        reasons.append(InfeasibilityReason(
+            InfeasibilityType.CritAtBottom,
+            instance.max_score - 5 + bottom_card.rank,
+            instance.deck_size - 1
+        ))
+        if only_find_first:
+            return reasons
+
+    # we will sweep through the deck and pretend that
+    # - we keep all non-trash cards in our hands
+    # - we instantly play all playable cards as soon as we have them
+    # - we recurse on this instant-play
+    #
+    # For example, we assume that once we draw r2, we check if we can play r2.
+    # If yes, then we also check if we drew r3 earlier and so on.
+    # If not, then we keep r2 in our hands
+    #
+    # In total, this is equivalent to assuming that we infinitely many clues
+    # and infinite storage space in our hands (which is of course not true),
+    # but even in this setting, some games are infeasible due to pace issues
+    # that we can detect
+    #
+    # A small refinement is to pretend that we only have infinite storage for non-crit cards,
+    # for crit-cards, the usual hand card limit applies.
+    # This allows us to detect some seeds where there are simply too many unplayable cards to hold at some point
+    # that also can't be discarded
+    # this allows us to detect standard pace issue arguments
+
+    stacks = [0] * instance.num_suits
+
+    # we will ensure that stored_crits is a subset of stored_cards
+    stored_cards = set()
+    stored_crits = set()
+
+    min_forced_pace = instance.initial_pace
+    worst_pace_index = 0
+
+    max_forced_crit_discard = 0
+    worst_crit_index = 0
+
+    for (i, card) in enumerate(instance.deck):
+        if card.rank == stacks[card.suitIndex] + 1:
+            # card is playable
+            stacks[card.suitIndex] += 1
+            # check for further playables that we stored
+            for check_rank in range(card.rank + 1, 6):
+                check_card = hanab_game.DeckCard(card.suitIndex, check_rank)
+                if check_card in stored_cards:
+                    stacks[card.suitIndex] += 1
+                    stored_cards.remove(check_card)
+                    if check_card in stored_crits:
+                        stored_crits.remove(check_card)
+                else:
+                    break
+        elif card.rank <= stacks[card.suitIndex]:
+            pass  # card is trash
+        elif card.rank > stacks[card.suitIndex] + 1:
+            # need to store card
+            if card in stored_cards or card.rank == 5:
+                stored_crits.add(card)
+            stored_cards.add(card)
+
+        # check for out of handsize (this number can be negative, in which case nothing applies)
+        # Note the +1 at the end, which is there because we have to discard next,
+        # so even if we currently have as many crits as we can hold, we have to discard one
+        num_forced_crit_discards = len(stored_crits) - instance.num_players * instance.hand_size + 1
+        if len(stored_crits) - instance.num_players * instance.hand_size > max_forced_crit_discard:
+            worst_crit_index = i
+            max_forced_crit_discard = num_forced_crit_discards
+            if only_find_first:
+                reasons.append(InfeasibilityReason(
+                    InfeasibilityType.OutOfPace,
+                    instance.max_score + min_forced_pace,
+                    worst_pace_index
+                ))
+                return reasons
+
+        # the last - 1 is there because we have to discard 'next', causing a further draw
+        max_remaining_plays = (instance.deck_size - i - 1) + instance.num_players - 1
+        needed_plays = instance.max_score - sum(stacks)
+        cur_pace = max_remaining_plays - needed_plays
+        if cur_pace < min(0, min_forced_pace):
+            min_forced_pace = cur_pace
+            worst_pace_index = i
+            if only_find_first:
+                reasons.append(InfeasibilityReason(
+                    InfeasibilityType.OutOfPace,
+                    instance.max_score + min_forced_pace,
+                    worst_pace_index
+                ))
+                return reasons
+
+    # check that we correctly walked through the deck
+    assert (len(stored_cards) == 0)
+    assert (len(stored_crits) == 0)
+    assert (sum(stacks) == instance.max_score)
+
+    if max_forced_crit_discard > 0:
+        reasons.append(
+            InfeasibilityReason(
+                InfeasibilityType.OutOfHandSize,
+                instance.max_score - max_forced_crit_discard,
+                worst_crit_index
+            )
+        )
+
+    if min_forced_pace < 0:
+        reasons.append(InfeasibilityReason(
+            InfeasibilityType.OutOfPace,
+            instance.max_score + min_forced_pace,
+            worst_pace_index
+        ))
+
+    return reasons
+
+
+def run_on_database(variant_id):
+    database.cur.execute(
+        "SELECT seed, num_players, deck FROM seeds WHERE variant_id = (%s) ORDER BY (num_players, seed)",
+        (variant_id,)
+    )
+    res = database.cur.fetchall()
+    logger.verbose("Checking {} seeds of variant {} for infeasibility".format(len(res), variant_id))
+    with alive_progress.alive_bar(total=len(res), title='Check for infeasibility reasons in var {}'.format(variant_id)) as bar:
+        for (seed, num_players, deck_str) in res:
+            deck = compress.decompress_deck(deck_str)
+            reasons = analyze(hanab_game.HanabiInstance(deck, num_players))
+            for reason in reasons:
+                database.cur.execute(
+                    "INSERT INTO score_upper_bounds (seed, score_upper_bound, reason) "
+                    "VALUES (%s,%s,%s) "
+                    "ON CONFLICT (seed, reason) DO UPDATE "
+                    "SET score_upper_bound = EXCLUDED.score_upper_bound",
+                    (seed, reason.score_upper_bound, reason.type.value)
+                )
+                database.cur.execute(
+                    "UPDATE seeds SET feasible = (%s) WHERE seed = (%s)",
+                    (False, seed)
+                )
+            bar()
+    database.conn.commit()

src/hanabi/solvers/greedy_solver.py

@@ -1,14 +1,14 @@
 #! /bin/python3
 import collections
 import sys
-from enum import Enum
-from log_setup import logger
-from typing import Tuple, List, Optional
-from time import sleep
 
-from hanabi import DeckCard, Action, ActionType, GameState, HanabiInstance
+from enum import Enum
-from compress import link, decompress_deck
+from typing import Optional
-from database.database import conn
+
+from hanabi import logger
+from hanabi import hanab_game
+from hanabi.live import compress
+from hanabi import database
 
 
 class CardType(Enum):
@@ -20,8 +20,8 @@ class CardType(Enum):
     UniqueVisible = 4
 
 
-class CardState():
+class CardState:
-    def __init__(self, card_type: CardType, card: DeckCard, weight=1):
+    def __init__(self, card_type: CardType, card: hanab_game.DeckCard, weight: Optional[int] = 1):
         self.card_type = card_type
         self.card = card
         self.weight = weight
@@ -67,7 +67,7 @@ class WeightedCard:
 
 
 class HandState:
-    def __init__(self, player: int, game_state: GameState):
+    def __init__(self, player: int, game_state: hanab_game.GameState):
         self.trash = []
         self.playable = []
         self.critical = []
@@ -112,14 +112,14 @@ class HandState:
         else:
             assert len(self.critical) > 0, "Programming error."
             self.best_discard = self.critical[-1]
-            self.discard_badness = 600 - 100*self.best_discard.card.rank
+            self.discard_badness = 600 - 100 * self.best_discard.card.rank
 
     def num_useful_cards(self):
         return len(self.dupes) + len(self.uniques) + len(self.playable) + len(self.critical)
 
 
 class CheatingStrategy:
-    def __init__(self, game_state: GameState):
+    def __init__(self, game_state: hanab_game.GameState):
         self.game_state = game_state
 
     def make_move(self):
@@ -136,10 +136,8 @@ class CheatingStrategy:
         exit(0)
 
 
-
-
 class GreedyStrategy():
-    def __init__(self, game_state: GameState):
+    def __init__(self, game_state: hanab_game.GameState):
         self.game_state = game_state
 
         self.earliest_draw_times = []
@@ -147,7 +145,7 @@ class GreedyStrategy():
             self.earliest_draw_times.append([])
             for r in range(1, 6):
                 self.earliest_draw_times[s].append(max(
-                    game_state.deck.index(DeckCard(s, r)) - game_state.hand_size * game_state.num_players + 1,
+                    game_state.deck.index(hanab_game.DeckCard(s, r)) - game_state.hand_size * game_state.num_players + 1,
                     0 if r == 1 else self.earliest_draw_times[s][r - 2]
                 ))
 
@@ -189,7 +187,7 @@ class GreedyStrategy():
                     copy_holders = set(self.game_state.holding_players(state.card))
                     copy_holders.remove(player)
                     connecting_holders = set(
-                        self.game_state.holding_players(DeckCard(state.card.suitIndex, state.card.rank + 1)))
+                        self.game_state.holding_players(hanab_game.DeckCard(state.card.suitIndex, state.card.rank + 1)))
 
                     if len(copy_holders) == 0:
                         # card is unique, imortancy is based lexicographically on whether somebody has the conn. card and the rank
@@ -245,8 +243,8 @@ class GreedyStrategy():
             self.game_state.clue()
 
 
-def run_deck(instance: HanabiInstance) -> GameState:
+def run_deck(instance: hanab_game.HanabiInstance) -> hanab_game.GameState:
-    gs = GameState(instance)
+    gs = hanab_game.GameState(instance)
     strat = CheatingStrategy(gs)
     while not gs.is_over():
         strat.make_move()
@@ -257,7 +255,7 @@ def run_samples(num_players, sample_size):
     logger.info("Running {} test games on {} players using greedy strategy.".format(sample_size, num_players))
     won = 0
     lost = 0
-    cur = conn.cursor()
+    cur = database.conn.cursor()
     cur.execute(
         "SELECT seed, num_players, deck, variant_id "
         "FROM seeds WHERE variant_id = 0 AND num_players = (%s)"
@@ -265,13 +263,13 @@ def run_samples(num_players, sample_size):
         (num_players, sample_size))
     for r in cur:
         seed, num_players, deck_str, var_id = r
-        deck = decompress_deck(deck_str)
+        deck = compress.decompress_deck(deck_str)
-        instance = HanabiInstance(deck, num_players)
+        instance = hanab_game.HanabiInstance(deck, num_players)
         final_game_state = run_deck(instance)
         if final_game_state.score != instance.max_score:
             logger.verbose(
                 "Greedy strategy lost {}-player seed {:10} {}:\n{}"
-                .format(num_players, seed, str(deck), link(final_game_state))
+                .format(num_players, seed, str(deck), compress.link(final_game_state))
             )
             lost += 1
         else:
@@ -280,9 +278,3 @@ def run_samples(num_players, sample_size):
     logger.info("Won {} ({}%) and lost {} ({}%) from sample of {} test games using greedy strategy.".format(
         won, round(100 * won / sample_size, 2), lost, round(100 * lost / sample_size, 2), sample_size
     ))
-
-
-if __name__ == "__main__":
-    for p in range(2, 6):
-        run_samples(p, int(sys.argv[1]))
-        print()

src/hanabi/solvers/sat.py

@@ -0,0 +1,372 @@
+import copy
+from typing import Optional, Tuple
+
+from pysmt.shortcuts import Symbol, Bool, Not, Implies, Iff, And, Or, AtMostOne, get_model, Equals, GE, NotEquals, Int
+from pysmt.typing import INT
+
+from hanabi import logger
+from hanabi import constants
+from hanabi import hanab_game
+
+
+# literals to model game as sat instance to check for feasibility
+# variants 'throw it in a hole not handled', 'clue starved' and 'up or down' currently not handled
+class Literals():
+    # num_suits is total number of suits, i.e. also counts the dark suits
+    # default distribution among all suits is assumed
+    def __init__(self, instance: hanab_game.HanabiInstance):
+        # clues[m][i] == "after move m we have i clues", in clue starved, this counts half clues
+        self.clues = {
+            -1: Int(16 if instance.clue_starved else 8)  # we have 8 clues after turn
+            , **{
+                m: Symbol('m{}clues'.format(m), INT)
+                for m in range(instance.max_winning_moves)
+            }
+        }
+
+        self.pace = {
+            -1: Int(instance.initial_pace)
+            , **{
+                m: Symbol('m{}pace'.format(m), INT)
+                for m in range(instance.max_winning_moves)
+            }
+        }
+
+        # strikes[m][i] == "after move m we have at least i strikes"
+        self.strikes = {
+            -1: {i: Bool(i == 0) for i in range(0, instance.num_strikes + 1)}  # no strikes when we start
+            , **{
+                m: {
+                    0: Bool(True),
+                    **{s: Symbol('m{}strikes{}'.format(m, s)) for s in range(1, instance.num_strikes)},
+                    instance.num_strikes: Bool(False)
+                    # never so many clues that we lose. Implicitly forbids striking out
+                }
+                for m in range(instance.max_winning_moves)
+            }
+        }
+
+        # extraturn[m] = "turn m is a move part of the extra round or a dummy turn"
+        self.extraround = {
+            -1: Bool(False)
+            , **{
+                m: Bool(False) if m < instance.draw_pile_size else Symbol('m{}extra'.format(m))
+                # it takes at least as many turns as cards in the draw pile to start the extra round
+                for m in range(0, instance.max_winning_moves)
+            }
+        }
+
+        # dummyturn[m] = "turn m is a dummy nurn and not actually part of the game"
+        self.dummyturn = {
+            -1: Bool(False)
+            , **{
+                m: Bool(False) if m < instance.draw_pile_size + instance.num_players else Symbol('m{}dummy'.format(m))
+                for m in range(0, instance.max_winning_moves)
+            }
+        }
+
+        # draw[m][i] == "at move m we play/discard deck[i]"
+        self.discard = {
+            m: {i: Symbol('m{}discard{}'.format(m, i)) for i in range(instance.deck_size)}
+            for m in range(instance.max_winning_moves)
+        }
+
+        # draw[m][i] == "at move m we draw deck card i"
+        self.draw = {
+            -1: {i: Bool(i == instance.num_dealt_cards - 1) for i in
+                 range(instance.num_dealt_cards - 1, instance.deck_size)}
+            , **{
+                m: {
+                    instance.num_dealt_cards - 1: Bool(False),
+                    **{i: Symbol('m{}draw{}'.format(m, i)) for i in range(instance.num_dealt_cards, instance.deck_size)}
+                }
+                for m in range(instance.max_winning_moves)
+            }
+        }
+
+        # strike[m] = "at move m we get a strike"
+        self.strike = {
+            -1: Bool(False)
+            , **{
+                m: Symbol('m{}newstrike'.format(m))
+                for m in range(instance.max_winning_moves)
+            }
+        }
+
+        # progress[m][card = (suitIndex, rank)] == "after move m we have played in suitIndex up to rank"
+        self.progress = {
+            -1: {(s, r): Bool(r == 0) for s in range(0, instance.num_suits) for r in range(0, 6)}
+            # at start, have only played rank zero
+            , **{
+                m: {
+                    **{(s, 0): Bool(True) for s in range(0, instance.num_suits)},
+                    **{(s, r): Symbol('m{}progress{}{}'.format(m, s, r)) for s in range(0, instance.num_suits) for r in
+                       range(1, 6)}
+                }
+                for m in range(instance.max_winning_moves)
+            }
+        }
+
+        ## Utility variables
+
+        # discard_any[m] == "at move m we play/discard a card"
+        self.discard_any = {m: Symbol('m{}discard_any'.format(m)) for m in range(instance.max_winning_moves)}
+
+        # draw_any[m] == "at move m we draw a card"
+        self.draw_any = {m: Symbol('m{}draw_any'.format(m)) for m in range(instance.max_winning_moves)}
+
+        # play[m] == "at move m we play a card"
+        self.play = {m: Symbol('m{}play'.format(m)) for m in range(instance.max_winning_moves)}
+
+        # play5[m] == "at move m we play a 5"
+        self.play5 = {m: Symbol('m{}play5'.format(m)) for m in range(instance.max_winning_moves)}
+
+        # incr_clues[m] == "at move m we obtain a clue"
+        self.incr_clues = {m: Symbol('m{}c+'.format(m)) for m in range(instance.max_winning_moves)}
+
+
+def solve_sat(starting_state: hanab_game.GameState | hanab_game.HanabiInstance, min_pace: Optional[int] = 0) -> Tuple[
+    bool, Optional[hanab_game.GameState]]:
+    if isinstance(starting_state, hanab_game.HanabiInstance):
+        instance = starting_state
+        game_state = hanab_game.GameState(instance)
+    elif isinstance(starting_state, hanab_game.GameState):
+        instance = starting_state.instance
+        game_state = starting_state
+    else:
+        raise ValueError("Bad argument type")
+
+    ls = Literals(instance)
+
+    ##### setup of initial game state
+
+    # properties used later to model valid moves
+
+    starting_hands = [[card.deck_index for card in hand] for hand in game_state.hands]
+    first_turn = len(game_state.actions)
+
+    if isinstance(starting_state, hanab_game.GameState):
+        # have to set additional variables
+
+        # set initial clues
+        for i in range(0, 10):
+            ls.clues[first_turn - 1] = Int(game_state.clues)
+
+        # set initial pace
+        ls.pace[first_turn - 1] = Int(game_state.pace)
+
+        # set initial strikes
+        for i in range(0, instance.num_strikes + 1):
+            ls.strikes[first_turn - 1][i] = Bool(i <= game_state.strikes)
+
+        # check if extraround has started (usually not)
+        ls.extraround[first_turn - 1] = Bool(game_state.remaining_extra_turns < game_state.num_players)
+        ls.dummyturn[first_turn - 1] = Bool(False)
+
+        # set recent draws: important to model progress
+        # we just pretend that the last card drawn was in fact drawn last turn,
+        # regardless of when it was actually drawn
+        for neg_turn in range(1, min(9, first_turn + 2)):
+            for i in range(instance.num_players * instance.hand_size, instance.deck_size):
+                ls.draw[first_turn - neg_turn][i] = Bool(neg_turn == 1 and i == game_state.progress - 1)
+        # forbid re-drawing of the last card drawn
+        for m in range(first_turn, instance.max_winning_moves):
+            ls.draw[m][game_state.progress - 1] = Bool(False)
+
+        # model initial progress
+        for s in range(0, game_state.num_suits):
+            for r in range(0, 6):
+                ls.progress[first_turn - 1][s, r] = Bool(r <= game_state.stacks[s])
+
+    ### Now, model all valid moves
+
+    valid_move = lambda m: And(
+        # in dummy turns, nothing can be discarded
+        Implies(ls.dummyturn[m], Not(ls.discard_any[m])),
+
+        # definition of discard_any
+        Iff(ls.discard_any[m], Or(ls.discard[m][i] for i in range(instance.deck_size))),
+
+        # definition of draw_any
+        Iff(ls.draw_any[m], Or(ls.draw[m][i] for i in range(game_state.progress, instance.deck_size))),
+
+        # ls.draw implies ls.discard (and converse true before the ls.extraround)
+        Implies(ls.draw_any[m], ls.discard_any[m]),
+        Implies(ls.discard_any[m], Or(ls.extraround[m], ls.draw_any[m])),
+
+        # ls.play requires ls.discard
+        Implies(ls.play[m], ls.discard_any[m]),
+
+        # definition of ls.play5
+        Iff(ls.play5[m],
+            And(ls.play[m], Or(ls.discard[m][i] for i in range(instance.deck_size) if instance.deck[i].rank == 5))),
+
+        # definition of ls.incr_clues
+        Iff(ls.incr_clues[m],
+            And(ls.discard_any[m], NotEquals(ls.clues[m - 1], Int(16 if instance.clue_starved else 8)),
+                Implies(ls.play[m], ls.play5[m]))),
+
+        # change of ls.clues
+        Implies(And(Not(ls.discard_any[m]), Not(ls.dummyturn[m])),
+                Equals(ls.clues[m], ls.clues[m - 1] - (2 if instance.clue_starved else 1))),
+        Implies(ls.incr_clues[m], Equals(ls.clues[m], ls.clues[m - 1] + 1)),
+        Implies(And(Or(ls.discard_any[m], ls.dummyturn[m]), Not(ls.incr_clues[m])),
+                Equals(ls.clues[m], ls.clues[m - 1])),
+
+        # change of pace
+        Implies(And(ls.discard_any[m], Or(ls.strike[m], Not(ls.play[m]))), Equals(ls.pace[m], ls.pace[m - 1] - 1)),
+        Implies(Or(Not(ls.discard_any[m]), And(Not(ls.strike[m]), ls.play[m])), Equals(ls.pace[m], ls.pace[m - 1])),
+
+        # pace is nonnegative
+        GE(ls.pace[m], Int(min_pace)),
+
+        ## more than 8 clues not allowed, ls.discarding produces a strike
+        # Note that this means that we will never strike while not at 8 clues.
+        # It's easy to see that if there is any solution to the instance, then there is also one where we only strike at 8 clues
+        # (or not at all) -> Just strike later if neccessary
+        # So, we decrease the solution space with this formulation, but do not change whether it's empty or not
+        Iff(ls.strike[m],
+            And(ls.discard_any[m], Not(ls.play[m]), Equals(ls.clues[m - 1], Int(16 if instance.clue_starved else 8)))),
+
+        # change of strikes
+        *[Iff(ls.strikes[m][i], Or(ls.strikes[m - 1][i], And(ls.strikes[m - 1][i - 1], ls.strike[m]))) for i in
+          range(1, instance.num_strikes + 1)],
+
+        # less than 0 clues not allowed
+        Implies(Not(ls.discard_any[m]), Or(GE(ls.clues[m - 1], Int(1)), ls.dummyturn[m])),
+
+        # we can only draw card i if the last ls.drawn card was i-1
+        *[Implies(ls.draw[m][i], Or(
+            And(ls.draw[m0][i - 1], *[Not(ls.draw_any[m1]) for m1 in range(m0 + 1, m)]) for m0 in
+            range(max(first_turn - 1, m - 9), m))) for i in range(game_state.progress, instance.deck_size)],
+
+        # we can only draw at most one card (NOTE: redundant, FIXME: avoid quadratic formula)
+        AtMostOne(ls.draw[m][i] for i in range(game_state.progress, instance.deck_size)),
+
+        # we can only discard a card if we drew it earlier...
+        *[Implies(ls.discard[m][i],
+                  Or(ls.draw[m0][i] for m0 in range(m - instance.num_players, first_turn - 1, -instance.num_players)))
+          for i in range(game_state.progress, instance.deck_size)],
+
+        # ...or if it was part of the initial hand
+        *[Not(ls.discard[m][i]) for i in range(0, game_state.progress) if
+          i not in starting_hands[m % instance.num_players]],
+
+        # we can only discard a card if we did not discard it yet
+        *[Implies(ls.discard[m][i], And(
+            Not(ls.discard[m0][i]) for m0 in range(m - instance.num_players, first_turn - 1, -instance.num_players)))
+          for i in range(instance.deck_size)],
+
+        # we can only discard at most one card (FIXME: avoid quadratic formula)
+        AtMostOne(ls.discard[m][i] for i in range(instance.deck_size)),
+
+        # we can only play a card if it matches the progress
+        *[Implies(
+            And(ls.discard[m][i], ls.play[m]),
+            And(
+                Not(ls.progress[m - 1][instance.deck[i].suitIndex, instance.deck[i].rank]),
+                ls.progress[m - 1][instance.deck[i].suitIndex, instance.deck[i].rank - 1]
+            )
+        )
+            for i in range(instance.deck_size)
+        ],
+
+        # change of progress
+        *[
+            Iff(
+                ls.progress[m][s, r],
+                Or(
+                    ls.progress[m - 1][s, r],
+                    And(ls.play[m], Or(ls.discard[m][i]
+                                       for i in range(0, instance.deck_size)
+                                       if instance.deck[i] == hanab_game.DeckCard(s, r)))
+                )
+            )
+            for s in range(0, instance.num_suits)
+            for r in range(1, 6)
+        ],
+
+        # extra round bool
+        Iff(ls.extraround[m], Or(ls.extraround[m - 1], ls.draw[m - 1][instance.deck_size - 1])),
+
+        # dummy turn bool
+        *[Iff(ls.dummyturn[m], Or(ls.dummyturn[m - 1], ls.draw[m - 1 - instance.num_players][instance.deck_size - 1]))
+          for i in range(0, 1) if m >= instance.num_players]
+    )
+
+    win = And(
+        # maximum progress at each color
+        *[ls.progress[instance.max_winning_moves - 1][s, 5] for s in range(0, instance.num_suits)],
+
+        # played every color/value combination (NOTE: redundant, but makes solving faster)
+        *[
+            Or(
+                And(ls.discard[m][i], ls.play[m])
+                for m in range(first_turn, instance.max_winning_moves)
+                for i in range(instance.deck_size)
+                if game_state.deck[i] == hanab_game.DeckCard(s, r)
+            )
+            for s in range(0, instance.num_suits)
+            for r in range(1, 6)
+            if r > game_state.stacks[s]
+        ]
+    )
+
+    constraints = And(*[valid_move(m) for m in range(first_turn, instance.max_winning_moves)], win)
+    #    print('Solving instance with {} variables, {} nodes'.format(len(get_atoms(constraints)), get_formula_size(constraints)))
+
+    model = get_model(constraints)
+    if model:
+        log_model(model, game_state, ls)
+        solution = evaluate_model(model, copy.deepcopy(game_state), ls)
+        return True, solution
+    else:
+        # conj = list(conjunctive_partition(constraints))
+        # print('statements: {}'.format(len(conj)))
+        # ucore = get_unsat_core(conj)
+        # print('unsat core size: {}'.format(len(ucore)))
+        # for f in ucore:
+        #    print(f.serialize())
+        return False, None
+
+
+def log_model(model, cur_game_state, ls: Literals):
+    deck = cur_game_state.deck
+    first_turn = len(cur_game_state.actions)
+    if first_turn > 0:
+        logger.debug('[print_model] Note: Omitting first {} turns, since they were fixed already.'.format(first_turn))
+    for m in range(first_turn, cur_game_state.instance.max_winning_moves):
+        logger.debug('=== move {} ==='.format(m))
+        logger.debug('clues: {}'.format(model.get_py_value(ls.clues[m])))
+        logger.debug('strikes: ' + ''.join(str(i) for i in range(1, 3) if model.get_py_value(ls.strikes[m][i])))
+        logger.debug('draw: ' + ', '.join(
+            '{}: {}'.format(i, deck[i]) for i in range(cur_game_state.progress, cur_game_state.instance.deck_size) if
+            model.get_py_value(ls.draw[m][i])))
+        logger.debug('discard: ' + ', '.join(
+            '{}: {}'.format(i, deck[i]) for i in range(cur_game_state.instance.deck_size) if
+            model.get_py_value(ls.discard[m][i])))
+        logger.debug('pace: {}'.format(model.get_py_value(ls.pace[m])))
+        for s in range(0, cur_game_state.instance.num_suits):
+            logger.debug('progress {}: '.format(constants.COLOR_INITIALS[s]) + ''.join(
+                str(r) for r in range(1, 6) if model.get_py_value(ls.progress[m][s, r])))
+        flags = ['discard_any', 'draw_any', 'play', 'play5', 'incr_clues', 'strike', 'extraround', 'dummyturn']
+        logger.debug(', '.join(f for f in flags if model.get_py_value(getattr(ls, f)[m])))
+
+
+# given the initial game state and the model found by the SAT solver,
+# evaluates the model to produce a full game history
+def evaluate_model(model, cur_game_state: hanab_game.GameState, ls: Literals) -> hanab_game.GameState:
+    for m in range(len(cur_game_state.actions), cur_game_state.instance.max_winning_moves):
+        if model.get_py_value(ls.dummyturn[m]) or cur_game_state.is_over():
+            break
+        if model.get_py_value(ls.discard_any[m]):
+            card_idx = next(
+                i for i in range(0, cur_game_state.instance.deck_size) if model.get_py_value(ls.discard[m][i]))
+            if model.get_py_value(ls.play[m]) or model.get_py_value(ls.strike[m]):
+                cur_game_state.play(card_idx)
+            else:
+                cur_game_state.discard(card_idx)
+        else:
+            cur_game_state.clue()
+
+    return cur_game_state

test.py

@@ -1,94 +0,0 @@
-import json
-
-import alive_progress
-import requests
-
-from variants import Variant
-from variants import Suit, variant_name
-from site_api import *
-from download_data import download_games, detailed_export_game
-from check_game import check_game
-from compress import link
-from database.database import conn, cur
-
-from database.init_database import init_database_tables, populate_static_tables
-
-
-def find_double_dark_games():
-    cur.execute("SELECT variants.id, variants.name, count(suits.id) from variants "
-                "inner join variant_suits on variants.id = variant_suits.variant_id "
-                "left join suits on suits.id = variant_suits.suit_id "
-                "where suits.dark = (%s) "
-                "group by variants.id "
-                "order by count(suits.id), variants.id",
-                (True,)
-                )
-    cur2 = conn.cursor()
-    r = []
-    for (var_id, var_name, num_dark_suits) in cur.fetchall():
-        if num_dark_suits == 2:
-            cur2.execute("select count(*) from games where variant_id = (%s)", (var_id,))
-            games = cur2.fetchone()[0]
-            cur2.execute("select count(*) from seeds where variant_id = (%s)", (var_id, ))
-            r.append((var_name, games, cur2.fetchone()[0]))
-    l = sorted(r, key=lambda e: -e[1])
-    for (name, games, seeds) in l:
-        print("{}: {} games on {} seeds".format(name, games, seeds))
-
-
-def test_suits():
-    suit = Suit.from_db(55)
-    print(suit.__dict__)
-
-
-def test_variant():
-    var = Variant.from_db(926)
-    print(var.__dict__)
-
-
-def check_missing_ids():
-    #    start = 357849
-    #    end = 358154
-    start = 358393
-    end = 358687
-    #    broken_ids = [357913, 357914, 357915] # two of these are no variant
-    #    not_supported_ids = [357925, 357957, 358081]
-    broken_ids = [358627, 358630, 358632]
-    not_supported_ids = [
-    ]
-    for game_id in range(start, end):
-        if game_id in broken_ids or game_id in not_supported_ids:
-            continue
-        print(game_id)
-        detailed_export_game(game_id)
-        conn.commit()
-
-
-def export_all_seeds():
-    cur.execute(
-        "SELECT id FROM variants ORDER BY ID"
-    )
-    var_ids = cur.fetchall()
-    for var in var_ids:
-        download_games(*var)
-
-
-if __name__ == "__main__":
-    find_double_dark_games()
-    exit(0)
-    var_id = 964532
-    export_all_seeds()
-    exit(0)
-
-#    init_database_tables()
-#    populate_static_tables()
-    download_games(1)
-    print(variant_name(17888))
-    for page in range(0, 4):
-        r = api("variants/0?size=20&col[0]=0&page={}".format(page))
-        ids = []
-        for game in r['rows']:
-            ids.append(game['id'])
-        r['rows'] = None
-        print(json.dumps(r, indent=2))
-        print(ids)