#include <atomic>
#include <cstdint>
#include <filesystem>
#include <string>
#include <util/config/options.h>

Include dependency graph for proof_cache.h:

This graph shows which files directly or indirectly include this file:

Classes
class	proof_cachet
	Content-addressed store of claims already proved unsatisfiable. More...

Functions
std::string	proof_cache_context (const optionst &options, const std::string &build_identity)
	Digest of everything outside the cone that the verdict depends on.
std::string	proof_cache_inactive_reason (const optionst &options)
	Why a proof cache would not be consulted under `options`, or empty when it would be.
void	report_proof_cache_inactive (const std::string &why)
	Say, once per run, that a named cache directory will not be consulted.
bool	proof_cache_contradicted (bool was_hit, bool counterexample_found)
	True when the solver has just contradicted a proof the cache stood in for.
std::string	proof_cache_build_identity (const std::string &build_id)
	The ESBMC that is running, as far as it can be established: `build_id` alone when that names one build, otherwise it plus a digest of the executable.

Function Documentation

◆ proof_cache_build_identity()

std::string proof_cache_build_identity ( const std::string & build_id )

The ESBMC that is running, as far as it can be established: build_id alone when that names one build, otherwise it plus a digest of the executable.

Empty when neither is available – a key that cannot name the verifier must not be used to skip it.

◆ proof_cache_context()

std::string proof_cache_context	(	const optionst &	options,
		const std::string &	build_identity )

Digest of everything outside the cone that the verdict depends on.

Every option is folded in unabridged bar a short allowlist of ones that reach nothing but the report: a curated list of "options that matter" is the classic way a cache like this goes unsound.

◆ proof_cache_contradicted()

bool proof_cache_contradicted	(	bool	was_hit,
		bool	counterexample_found )

True when the solver has just contradicted a proof the cache stood in for.

Only a counterexample does: a vacuous discharge, a solver error and an SMT-LIB-only emission all mean the claim was not re-checked, not that the stored proof was wrong.

◆ proof_cache_inactive_reason()

std::string proof_cache_inactive_reason ( const optionst & options )

Why a proof cache would not be consulted under options, or empty when it would be.

Covers what the option set alone decides; a run adds the thread-interleaving exclusion on top.

◆ report_proof_cache_inactive()

void report_proof_cache_inactive ( const std::string & why )

Say, once per run, that a named cache directory will not be consulted.

A run that reuses nothing is otherwise indistinguishable from one whose cache is working.