loop_invariant_synthesizer_base.h File Reference

#include <goto-programs/goto_model.h>
#include "synthesizer_utils.h"

Include dependency graph for loop_invariant_synthesizer_base.h:

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

Go to the source code of this file.

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

Macros
#define	OPT_SYNTHESIZE_LOOP_INVARIANTS   "(synthesize-loop-invariants)"
#define	HELP_LOOP_INVARIANT_SYNTHESIZER

Detailed Description

Loop Invariant Synthesizer Interface

Definition in file loop_invariant_synthesizer_base.h.

Macro Definition Documentation

HELP_LOOP_INVARIANT_SYNTHESIZER

#define HELP_LOOP_INVARIANT_SYNTHESIZER

Value:

  " --synthesize-loop-invariants\n"                                            \
  "                              synthesize and apply loop invariants\n"

Definition at line 20 of file loop_invariant_synthesizer_base.h.

OPT_SYNTHESIZE_LOOP_INVARIANTS

#define OPT_SYNTHESIZE_LOOP_INVARIANTS   "(synthesize-loop-invariants)"

Definition at line 19 of file loop_invariant_synthesizer_base.h.