Module t2 

Bounded-degree positivity certificates for non-linear goals.

Given the code:

fn blocks{A, B}(arr: f32[A*B]) -> f32[A, B]:
    for i from 0 to A:
        for j from 0 to B:
            yield arr[i*B + j]

The solver is given the goal i*B + j < A*B to verify the arr access. Linearization replaces i*B and A*B with fresh atoms, so t1 cannot solve the system using the constraint i < A.

The goal and all other Constraints (except Ne, a conjunction for Eq) can be written as non-negative facts:

$$iB + j < AB \iff AB - iB - j - 1 \geq 0$$

Then the goal is a non-negative combination of products of facts already given:

$$AB - iB - j - 1 = B(A - i - 1) + 1(B - j - 1)$$

Or generally,

$$s \cdot \text{goal} = \sum_{k} c_kp_k$$ for some constant integers $c\geq0$, products $p$ of non-negative facts, and a scale factor $s$ to permit rational certificates. This is a Handelman representation (in this case, degree-2).

This module searches for such solutions to non-linear systems. We do so by generating $p$ candidates using non-negative monomial divisors of the goal and non-negative facts from context $h$. For example, supposing these six candidate products are generated:

$p_1$	$1 = 1$
$p_2$	$h_1 = A - i - 1$
$p_3$	$h_2 = B - j - 1$
$p_4$	$Bh_1 = AB - iB - B$
$p_5$	$Bh_2 = B^2 - jB - B$
$p_6$	$h_1h_2 = AB − jA − A − iB + ij + i − B + j + 1$

We can construct a linear system of equations in $c$ and $s$ which builds the goal, monomial by monomial. Satisfying each equation means selecting $c$ such that the sum-of-products has the correct $M$ term; $\sum_k c_k \cdot \text{coef}_{p_k}(M) = s \cdot \text{coef}_{\text{goal}}(M)$.

$M$	$c_1$	$c_2$	$c_3$	$c_4$	$c_5$	$c_6$	$=s \cdot$
$AB$				$1$		$1$	$1$
$iB$				$-1$		$-1$	$-1$
$j$			$-1$			$1$	$-1$
$1$	$1$	$-1$	$-1$			$1$	$-1$
$A$		$1$				$-1$
$i$		$-1$				$1$
$B$			$1$	$-1$	$-1$	$-1$
$B^2$					$1$
$jB$					$-1$
$jA$						$-1$
$ij$						$1$

This system can be solved in t1, giving $c_3=1, c_4=1$, $s=1$, $\text{rest}=0$. The final sum is $p_3 + p_4 = \text{goal}$.

use sirius::solver::{Constraint, Cmp, poly::{poly, Var}, t1::Z3, t2::prove};

let mut z3 = Z3::new_cli(None).unwrap();
let goal = Constraint::new(poly!(i*B + j), Cmp::Lt, poly!(A*B));
let facts = [
    Constraint::new(poly!(i), Cmp::Lt, poly!(A)),
    Constraint::new(poly!(j), Cmp::Lt, poly!(B)),
];
let nonneg = [
    'i' as Var,
    'j' as Var,
    'A' as Var,
    'B' as Var,
];

assert!(prove(&mut z3, &facts, &goal, &nonneg));

Constants

MAX_FACTS

Facts considered, starting with non-negative Vars, after filtering to those sharing a variable with the goal. Cmp::Eq constraints generate two facts.

MAX_MULTIPLIERS

Monomial multipliers considered.

Functions

prove

Try to prove nonlinear goal from facts.