invariant_synthesis Namespace Reference

The recogniser's pure syntactic predicates. More...

Functions
bool	split_bound (const expr2tc &cond, expr2tc &counter, expr2tc &bound, bool &inclusive)
	Split cond into counter and bound for the </<= shapes this pass handles, and report which one it was.
bool	is_self_increment (const expr2tc &target, const expr2tc &source, expr2tc &addend)
	lhs = lhs + addend — the only body assignment shape recognised here.
bool	entry_admits_two_disjunct_bound (const expr2tc &entry, bool inclusive)
	The two-disjunct bound (i <op> B) || i == E is established only when the counter's entry value cannot sit past the loop's exit value.

Detailed Description

The recogniser's pure syntactic predicates.

Exposed for unit testing: every other route to them runs through a frontend and a solver, where a predicate that never fires is indistinguishable from one that answers correctly.

Function Documentation

entry_admits_two_disjunct_bound()

bool invariant_synthesis::entry_admits_two_disjunct_bound	(	const expr2tc &	entry,
		bool	inclusive )

The two-disjunct bound (i <op> B) || i == E is established only when the counter's entry value cannot sit past the loop's exit value.

Whether the two-disjunct bound (i <op> B) || i == E is established from a counter entry value of entry.

Working the cases through for a constant i0:

<=, E = B+1: establishment fails iff i0 > B and i0 != B+1. At i0 == 1 the first conjunct forces B == 0, which makes E == 1 == i0, so it cannot fail; at i0 == 0 it cannot fail either. i0 >= 2 admits B <= i0 - 2 and does fail. <, E = B: establishment fails iff i0 > B, which only i0 == 0 rules out.

Anything else needs the third disjunct, which only the constant-addend regime can afford; see the header.

See the definition for the case analysis.

is_self_increment()

bool invariant_synthesis::is_self_increment	(	const expr2tc &	target,
		const expr2tc &	source,
		expr2tc &	addend )

lhs = lhs + addend — the only body assignment shape recognised here.

lhs = lhs + addend – the only body assignment shape recognised here.

split_bound()

bool invariant_synthesis::split_bound	(	const expr2tc &	cond,
		expr2tc &	counter,
		expr2tc &	bound,
		bool &	inclusive )

Split cond into counter and bound for the </<= shapes this pass handles, and report which one it was.

Other comparisons (and decrementing loops) are left to a later revision.