Script for Generating Polynomial Constraints (SMT QF_NRA)
python3 smt2_gen.py --config <config file> --output <output file>
<config file>: Configuration file in JSON format., default is config.json
<output file>: Output SMT-LIB 2.0 file, default is output.smt2
| Parameter |
Type |
Description |
var_lower |
integer |
Lower bound of the variable number |
var_upper |
integer |
Upper bound of the variable number |
clause_lower |
integer |
Lower bound of the number of clauses |
clause_upper |
integer |
Upper bound of the number of clauses |
| Parameter |
Type |
Description |
degree_lower |
integer |
Lower bound of the degree of the polynomial |
degree_upper |
integer |
Upper bound of the degree of the polynomial |
monomial_lower |
integer |
Lower bound of the number of monomials in the polynomial |
monomial_upper |
integer |
Upper bound of the number of monomials in the polynomial |
coefficient_lower |
integer |
Lower bound of the value of the coefficients of the monomials |
coefficient_upper |
integer |
Upper bound of the value of the coefficients of the monomials |
| Parameter |
Type |
Description |
coefficient_lower |
integer |
Lower bound of the value of the coefficient of the monomial |
coefficient_upper |
integer |
Upper bound of the value of the coefficient of the monomial |
| Parameter |
Type |
Description |
var_lower |
integer |
Lower bound of the number of variables in the clause |
var_upper |
integer |
Upper bound of the number of variables in the clause |
literal_lower |
integer |
Lower bound of the number of the literals in the clause |
literal_upper |
integer |
Upper bound of the number of the literals in the clause |