Struct PolynomialInterpretation 

pub struct PolynomialInterpretation {
    pub interpretations: HashMap<String, Vec<i64>>,
}

A polynomial interpretation for proving termination of a TRS.

Each function symbol f of arity n is mapped to a polynomial p_f(x_1, …, x_n) with natural-number coefficients. A TRS is terminating if for every rule l → r, the polynomial interpretation satisfies Pol(l) > Pol(r) (as natural numbers for all assignments ≥ 0).

Fields

interpretations: HashMap<String, Vec<i64>>

Maps function symbol names to their polynomial coefficients.

For a unary symbol the vector [c0, c1] represents c0 + c1 * x1. For a binary symbol [c0, c1, c2] represents c0 + c1x1 + c2x2. Constants (arity 0) are represented as [c0].

Implementations

impl PolynomialInterpretation

pub fn new() -> Self

Create an empty polynomial interpretation.

pub fn set(&mut self, symbol: impl Into<String>, coefficients: Vec<i64>)

Register an interpretation for symbol f: coefficients [c0, c1, …].

pub fn eval(&self, t: &Term, assignment: &[i64]) -> i64

Evaluate the polynomial interpretation of term t given variable assignment.

Variable Var(i) maps to assignment[i].

pub fn orients_rule(&self, rule: &Rule, max_val: i64) -> bool

Check whether rule lhs → rhs is oriented by this interpretation for all variable assignments in [0, max_val]^n.

pub fn proves_termination(&self, trs: &Trs, max_val: i64) -> bool

Check whether this interpretation proves termination of the given TRS (all rules are strictly oriented for assignments in [0, max_val]^n).

Trait Implementations

impl Clone for PolynomialInterpretation

fn clone(&self) -> PolynomialInterpretation

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PolynomialInterpretation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for PolynomialInterpretation

fn default() -> Self

Returns the “default value” for a type.