## GUBS Upper Bound Solver

Given a set of (in)equalities over arithmetical expressions and uninterpreted functions, GUBS is trying to find a model, i.e. interpretation into the naturals. In its current form, these interpretations are weakly monotone polynomials, possibly containing max.
GUBS incorporates a dedicated synthesis technique relying on SMT-solvers, using either minismt or z3, various simplification techniques and a per SCC analysis.

`$ gubs/examples> cat ugo1.cs `

(>= (f (var x))
(g (h (var x))))
(>= (h 0) 1)
(>= (h (+ (var x) 1))
(f (var x)))
(>= (g (var x))
(+ 1 (var x)))
`$ gubs/examples> gubs ugo1.cs`

SUCCESS
f(x0) = 2 + x0;
g(x0) = 1 + x0;
h(x0) = 1 + x0;

For more information see

README.

## Source Code

The development version of GUBS is hosted on

GitHub.