PolyHorn is a solver for Polynomial Horn Clauses (PHC).

Given an input PHC in SMT-LIB format and an optional config file, PolyHorn finds a valuation of the unknown variables in the input such that all the PHCs are satisfied.

PolyHorn is written in Python and can be run as a standalone tool or as a Python library. Either way, the input to PolyHorn is an SMT-LIB instance containing the PHC and an optional config file specifying the theorem and solver to be used.

The tool is tested for Python >=3.9 and requires the installation of:

• Z3 many package managers provide Z3 as a package. For example, in Ubuntu, Z3 can be installed using apt-get install z3. Otherwise, you can find more information here
• MathSAT can be downloaded from here.
• GNU C library glibc and Gnu Multiprecision Library GMP are also required.
• pysmt python library.

Next, we can install the package using the following command:

pip install polyhorn

The experiments folder contains the material to run all the experiments presented in the tool paper. Please see experiments/README.md for detailed instructions.

To try PolyHorn, first, clone this repository. When using the tool via the commandline, you can use the accompanying solvers from the subfolder solver/. For this you do not require any installation, however, in order to run PolyHorn, Z3 and MathSAT, the following command should be executed first:

chmod +x PolyHorn solver/z3 solver/mathsat

Also add solvers to PATH:

export PATH=$PATH:[polyhorn]/solver

where [polyhorn] is the directory where PolyHorn is cloned.

To run PolyHorn on input-example.smt2 the following command should be executed:

./PolyHorn input-example.smt2

To run PolyHorn on input-example.smt2 with config-example.json the following command should be executed:

./PolyHorn input-example.smt2 config-example.json

Alternatively, you can directly run PolyHorn's main python source file as follows:

python3 src/polyhorn/main.py --smt2 input-example.smt2 --config config-example.json

PolyHorn can be used as a Python library. The following code snippet shows how to use PolyHorn as a library after the whole installation process is completed.

from polyhorn.main import execute

input_file = "input-example.smt2"
config_file = "config-example.json"

is_sat, model = execute(input_file, config_file)

The execute function allows for several different input combinations. The first argument can be the path to an .smt2 input file or an instance os the pysmt.solvers.solver.Solver class with the assertions already added. The second argument can be the path to a .json config file or a dictionary with the configuration parameters.

A further example of how to use PolyHorn as a library can be found in the example_api.py file.

The input syntax of PolyHorn follows the SMTLIB syntax:

• (declare-const [var name] Real) is used for defining new unknown variables.
• (assert phi) is used for adding either (i) a quantifier free constraint on the unknown variables, or (ii) a PHC of the following form:

(assert (forall ((variable type) ... ) (=> phi psi) ))

where phi and psi are polynomial predicates over the unknown variables and the variables defined in the forall fragment of the assertion.

• the (check-sat) command at the end specifies that PolyHorn should run an SMT-solver after obtaining a fully existential system of polynomials.
• the (get-model) command means that in case the SMT-solver returned sat, the values for unknown variables should be printed.

See input-example.smt2 as an example.

The config file must be in .json format containing the following fields:

• theorem_name which is one of "farkas", "handelman" or "putinar".
• solver_name which is one of "z3" or "mathsat".
• (optional) output_path which should be the path to a file where PolyHorn will store the obtained polynomial system. If not set, PolyHorn will create a temporary file for it and will delete it in the end of execution.
• (optional) int_value which is assigned false or true. When true, PolyHorn tries to find integer values for unknown variables.
• In case handelman is chosen for theorem_name, an additional integer parameter degree_of_sat should be specified. This is the only parameter required by Handelman's Positivestellensatz. See [1] appendix E for more details.
• In case putinar is chosen for theorem_name, four parameters should be specified in the config file: (i) degree_of_sat the degree of SOS polynomials considered when the LHS of PHCs are assumed satisfying, (ii) degree_of_nonstrict_unsat, (iii) degree_of_strict_unsat and (iv) max_d_of_strict, for the remaining three degree parameters of Putinar's positivestellensatz. The names are self-explanatory and the details can be found in [1] section 3.
• SAT_heuristic which should be set to true if the Assume-SAT heuristic should be used.
• unsat_core_heuristic which should be set to true if the UNSAT Core heuristic should be used.

The default value is 0 for all integer parameters and false for all boolean parameters. Default theorem is set based on the degree of Horn Clauses and default solver is z3. Also, all heuristics are set t false as default.

See config-example.json as an example.

[1] Polynomial Reachability Witnesses via Stellensätze. Asadi et. al. PLDI 2021.

To cite PolyHorn, please use the following reference:
K. Chatterjee, A. K. Goharshady, E. K. Goharshady, M. Karrabi, M. Saadat, M. Seeliger, D. Zikelic
PolyHorn: A Polynomial Horn Clause Solver
arXiv 2024, [https://arxiv.org/abs/2408.03796]