Artifact for the ATVA 2025 paper "PolyQEnt: A Polynomial Quantified Entailment Solver"

<p dir="ltr">Artifact for the ATVA 2025 paper "PolyQEnt: A Polynomial Quantified Entailment Solver". </p>PolyQEnt<p dir="ltr">PolyQEnt is a solver for Polynomial Quantified Entailments (PQE).</p><p dir="ltr">Given an input PQE in SMT-LIB format and an optional config file, PolyQEnt finds a valuation of the unknown variables in the input such that all the PQEs are satisfied.</p><p dir="ltr">PolyQEnt is written in Python and can be run as a standalone tool or as a Python library. Either way, the input to PolyQEnt is an SMT-LIB instance containing the PQE and an optional config file specifying the theorem and solver to be used.</p><p dir="ltr">The tool is tested for Python >=3.9 and requires the installation of:</p><ul><li><code>Z3</code> many package managers provide Z3 as a package. For example, in Ubuntu, Z3 can be installed using <code>apt-get install z3</code>. Otherwise, you can find more information <a href="https://github.com/Z3Prover/z3" target="_blank">here</a></li><li><code>MathSAT</code> can be downloaded from <a href="http://mathsat.fbk.eu/download.html" rel="nofollow" target="_blank">here</a>.</li><li>GNU C library <code>glibc</code> and Gnu Multiprecision Library <code>GMP</code> are also required.</li><li><code>pysmt</code> python library.</li></ul><p><br></p>