A base class for loop invariant synthesizers. More...

#include <loop_invariant_synthesizer_base.h>

Inheritance diagram for loop_invariant_synthesizer_baset:

Collaboration diagram for loop_invariant_synthesizer_baset:

Public Member Functions
	loop_invariant_synthesizer_baset (const goto_modelt &goto_model, messaget &log)

virtual	~loop_invariant_synthesizer_baset ()=default

virtual invariant_mapt	synthesize_all ()=0
	Synthesize loop invariants that are inductive in the given GOTO program. More...

virtual exprt	synthesize (loop_idt)=0
	Synthesize loop invariant for a specified loop in the `goto_model`. More...

Protected Attributes
const goto_modelt &	goto_model

messaget &	log

Detailed Description

A base class for loop invariant synthesizers.

Provides a method for synthesizing loop invariants in a given goto_model.

Derived class should clarify what types of goto_model they targets, e.g., a goto_model contains only memory safety checks, or a goto_model contains both memory safety checks and correctness checks.

Definition at line 32 of file loop_invariant_synthesizer_base.h.

Constructor & Destructor Documentation

◆ loop_invariant_synthesizer_baset()

loop_invariant_synthesizer_baset::loop_invariant_synthesizer_baset	(	const goto_modelt &	goto_model,
		messaget &	log
	)

inline

Definition at line 35 of file loop_invariant_synthesizer_base.h.

◆ ~loop_invariant_synthesizer_baset()

virtual loop_invariant_synthesizer_baset::~loop_invariant_synthesizer_baset ( )

virtualdefault

Member Function Documentation

◆ synthesize()

virtual exprt loop_invariant_synthesizer_baset::synthesize ( loop_idt )

pure virtual

Synthesize loop invariant for a specified loop in the goto_model.

Implemented in enumerative_loop_invariant_synthesizert.

◆ synthesize_all()

virtual invariant_mapt loop_invariant_synthesizer_baset::synthesize_all ( )

pure virtual

Synthesize loop invariants that are inductive in the given GOTO program.

The result is a map from loop_idt ids of loops to exprt the GOTO-expression representation of synthesized invariants.

Implemented in enumerative_loop_invariant_synthesizert.

Member Data Documentation

◆ goto_model

const goto_modelt& loop_invariant_synthesizer_baset::goto_model

protected

Definition at line 51 of file loop_invariant_synthesizer_base.h.

◆ log

messaget& loop_invariant_synthesizer_baset::log