NLSOL: a NonLinear aritmetic SOLver (under construction!)
NLSOL is a solver for non-linear arithmetic over finite rational
domains. The solver is based on a translation from a non-linear
constraint to a linear formula, which is finally sent to an SMT-solver
handling linear arithmetic (see our
paper for details). The current version of NLSOL, gets a
conjunction of non-linear polynomial constrains in a
given input format and
returns whether it is satisfiable and if so provides
a solution. The domain
to be considered for solving the constraint is provided in
the call. Currently our
solver can only handle conjunctions of constraints, but very soon it
will be adapted to consider general formulas using the same syntax as
for linear formulas in
the SMT-LIB.
NLSOL can be easily adapted to use any linear arithmetic solver
working on formulas in
the SMT-LIB
format.
We have experimented with NLSOL as a solver in two state of the art
automatic termination
provers: AProVE and
Mu-Term. Our solver is compared with the SAT-based solver
of AProVE, the CSP-based solver of MuTerm and
the HySAT solver based on interval analysis.
Solver:
Download our solver NLSOL
. Binary for Linux 2.4/i686 (32bit Intel Pentium
and compatible).