cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
guard.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Guard Data Structure
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_ANALYSES_GUARD_H
13
#define CPROVER_ANALYSES_GUARD_H
14
15
#ifdef BDD_GUARDS
16
17
# include <
solvers/prop/bdd_expr.h
>
18
19
# include "
guard_bdd.h
"
20
21
using
guard_managert
=
bdd_exprt
;
22
using
guardt
=
guard_bddt
;
23
24
#else
25
26
#include "
guard_expr.h
"
27
28
using
guard_managert
=
guard_expr_managert
;
29
using
guardt
=
guard_exprt
;
30
31
#endif
// BDD_GUARDS
32
33
#endif
// CPROVER_ANALYSES_GUARD_H
bdd_expr.h
Conversion between exprt and miniBDD.
bdd_exprt
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
Definition
bdd_expr.h:34
guard_bddt
Definition
guard_bdd.h:22
guard_exprt
Definition
guard_expr.h:24
guard_managert
guard_expr_managert guard_managert
Definition
guard.h:28
guardt
guard_exprt guardt
Definition
guard.h:29
guard_bdd.h
Guard Data Structure Implementation using BDDs.
guard_expr.h
Guard Data Structure.
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition
guard_expr.h:20
analyses
guard.h
Generated by
1.17.0