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.