ranking_synthesis.cpp File Reference

#include <esbmc/ranking_synthesis.h>
#include <goto-programs/goto_loops.h>
#include <goto-programs/loopst.h>
#include <solvers/solve.h>
#include <solvers/smt/smt_conv.h>
#include <irep2/irep2_expr.h>
#include <langapi/language_util.h>
#include <util/lang/c_types.h>
#include <util/arith/arith_tools.h>
#include <util/expr/expr_util.h>
#include <util/message/message.h>
#include <util/irep/std_expr.h>
#include <algorithm>
#include <functional>
#include <map>
#include <memory>
#include <set>
#include <unordered_map>
#include <vector>

Include dependency graph for ranking_synthesis.cpp:

Functions
tvt	try_prove_termination_by_ranking (goto_functionst &goto_functions, optionst &options, const namespacet &ns)
	Linear ranking-function termination check.

Function Documentation

try_prove_termination_by_ranking()

tvt try_prove_termination_by_ranking	(	goto_functionst &	goto_functions,
		optionst &	options,
		const namespacet &	ns )

Linear ranking-function termination check.

For each loop in the program that matches a supported shape, try a small fixed set of candidate linear ranking functions and discharge two SMT obligations per candidate:

• decrease: guard ∧ ¬(m' < m) is UNSAT (m strictly decreases each iteration), where m' is m with the body's transition applied;
• bounded: guard ∧ (m < L) is UNSAT (m is bounded below by a guard-implied constant L).

If every loop has some candidate for which both obligations hold, the program terminates (return TV_TRUE). If any loop cannot be proven (unsupported shape, no candidate works), the check is inconclusive (return TV_UNKNOWN) and the caller falls back to the marker / forward-condition / inductive-step machinery. The check never returns TV_FALSE — it can prove termination but never refute it, so it can only ever turn an UNKNOWN into a SUCCESSFUL, never produce a wrong verdict.

Must be called BEFORE goto_termination()'s havoc transform, on the original (un-havoced) goto program — the obligations are built from the real loop transition relation.

The measure is computed in a type wider than its operands so the difference / decrement cannot overflow (signed overflow would be UB and unsound); the lower bound L is derived from the guard, never hardcoded.