NLFIntp
Home
Examples
Executable
Documentation
Contact
About
NLFIntp is an online tool for synthesizing nonlinear interpolants.
Type the input in the left container and click
Synthesize Interpolant!
Example 1. CQI+EUF
Example 2. CQI
Example 3. LA+EUF
Example 4. CQI
Example 5. LA+nested EUF
Example 6. CQI+EUF
Example 7. General NLA
# Demonstrating example. # Constraint is tailored to end with >0 | =0 | >=0. phi: - y1^2 - x1^2 - 1 + x1 - 2 * y1 + 2 * x1 * y1 + x2 >= 0 y2 - alpha(y1) - 1 = 0 - x1^2 - x2^2 - y2^2 + 1 > 0 # Make sure that phi and psi are mutually contradictory, otherwise the answer given is meaningless. psi: - z1^2 - x2^2 - 1 + x2 - 2 * z1 + 2 * x2 * z1 + x1 >= 0 z2 - alpha(z1) + 1 = 0 - x1^2 - x2^2 - z2^2 + 1 > 0
input
template
result
Synthesize Interpolant