Skip to content

Commit a7b8510

Browse files
tautschnigtautschnig
authored
Merge pull request #800 from diffblue/ltl_h
extract LTL and CTL classes into separate header files
2 parents bbe56b6 + 3c25a2d commit a7b8510

13 files changed

+429
-394
lines changed

‎src/ebmc/bdd_engine.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@ Author: Daniel Kroening, [email protected]
1515
#include <ebmc/transition_system.h>
1616
#include <solvers/bdd/miniBDD/miniBDD.h>
1717
#include <solvers/sat/satcheck.h>
18-
#include <temporal-logic/temporal_expr.h>
18+
#include <temporal-logic/ctl.h>
19+
#include <temporal-logic/ltl.h>
1920
#include <temporal-logic/temporal_logic.h>
2021
#include <trans-netlist/aig_prop.h>
2122
#include <trans-netlist/instantiate_netlist.h>

‎src/ebmc/live_signal.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include "live_signal.h"
1010

11-
#include <temporal-logic/temporal_expr.h>
11+
#include <temporal-logic/ctl.h>
1212
#include <verilog/sva_expr.h>
1313

1414
#include "transition_system.h"

‎src/ebmc/ranking_function.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
1515

1616
#include <langapi/language.h>
1717
#include <langapi/mode.h>
18-
#include <temporal-logic/temporal_expr.h>
18+
#include <temporal-logic/ctl.h>
1919
#include <trans-word-level/instantiate_word_level.h>
2020
#include <trans-word-level/trans_trace_word_level.h>
2121
#include <trans-word-level/unwind.h>

‎src/ic3/m1ain.cc

+2-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,8 @@ Author: Eugene Goldberg, [email protected]
1818
#include <trans-netlist/netlist.h>
1919
#include <trans-netlist/trans_to_netlist.h>
2020

21-
#include <temporal-logic/temporal_expr.h>
21+
#include <temporal-logic/ctl.h>
22+
#include <temporal-logic/ltl.h>
2223
#include <temporal-logic/temporal_logic.h>
2324

2425
#include <verilog/sva_expr.h>

‎src/temporal-logic/ctl.h

+238
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,238 @@
1+
/*******************************************************************\
2+
3+
Module: CTL Temporal Operators
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_TEMPORAL_LOGIC_CTL_H
10+
#define CPROVER_TEMPORAL_LOGIC_CTL_H
11+
12+
#include <util/std_expr.h>
13+
14+
class AG_exprt : public unary_predicate_exprt
15+
{
16+
public:
17+
explicit AG_exprt(exprt op) : unary_predicate_exprt(ID_AG, std::move(op))
18+
{
19+
}
20+
};
21+
22+
static inline const AG_exprt &to_AG_expr(const exprt &expr)
23+
{
24+
PRECONDITION(expr.id() == ID_AG);
25+
AG_exprt::check(expr, validation_modet::INVARIANT);
26+
return static_cast<const AG_exprt &>(expr);
27+
}
28+
29+
static inline AG_exprt &to_AG_expr(exprt &expr)
30+
{
31+
PRECONDITION(expr.id() == ID_AG);
32+
AG_exprt::check(expr, validation_modet::INVARIANT);
33+
return static_cast<AG_exprt &>(expr);
34+
}
35+
36+
class AF_exprt : public unary_predicate_exprt
37+
{
38+
public:
39+
explicit AF_exprt(exprt op) : unary_predicate_exprt(ID_AF, std::move(op))
40+
{
41+
}
42+
};
43+
44+
static inline const AF_exprt &to_AF_expr(const exprt &expr)
45+
{
46+
PRECONDITION(expr.id() == ID_AF);
47+
AF_exprt::check(expr, validation_modet::INVARIANT);
48+
return static_cast<const AF_exprt &>(expr);
49+
}
50+
51+
static inline AF_exprt &to_AF_expr(exprt &expr)
52+
{
53+
PRECONDITION(expr.id() == ID_AF);
54+
AF_exprt::check(expr, validation_modet::INVARIANT);
55+
return static_cast<AF_exprt &>(expr);
56+
}
57+
58+
class EG_exprt : public unary_predicate_exprt
59+
{
60+
public:
61+
explicit EG_exprt(exprt op) : unary_predicate_exprt(ID_EG, std::move(op))
62+
{
63+
}
64+
};
65+
66+
static inline const EG_exprt &to_EG_expr(const exprt &expr)
67+
{
68+
PRECONDITION(expr.id() == ID_EG);
69+
EG_exprt::check(expr, validation_modet::INVARIANT);
70+
return static_cast<const EG_exprt &>(expr);
71+
}
72+
73+
static inline EG_exprt &to_EG_expr(exprt &expr)
74+
{
75+
PRECONDITION(expr.id() == ID_EG);
76+
EG_exprt::check(expr, validation_modet::INVARIANT);
77+
return static_cast<EG_exprt &>(expr);
78+
}
79+
80+
class EF_exprt : public unary_predicate_exprt
81+
{
82+
public:
83+
explicit EF_exprt(exprt op) : unary_predicate_exprt(ID_EF, std::move(op))
84+
{
85+
}
86+
};
87+
88+
static inline const EF_exprt &to_EF_expr(const exprt &expr)
89+
{
90+
PRECONDITION(expr.id() == ID_EF);
91+
EF_exprt::check(expr, validation_modet::INVARIANT);
92+
return static_cast<const EF_exprt &>(expr);
93+
}
94+
95+
static inline EF_exprt &to_EF_expr(exprt &expr)
96+
{
97+
PRECONDITION(expr.id() == ID_EF);
98+
EF_exprt::check(expr, validation_modet::INVARIANT);
99+
return static_cast<EF_exprt &>(expr);
100+
}
101+
102+
class EU_exprt : public binary_predicate_exprt
103+
{
104+
public:
105+
explicit EU_exprt(exprt op0, exprt op1)
106+
: binary_predicate_exprt(std::move(op0), ID_EU, std::move(op1))
107+
{
108+
}
109+
};
110+
111+
static inline const EU_exprt &to_EU_expr(const exprt &expr)
112+
{
113+
PRECONDITION(expr.id() == ID_EU);
114+
EU_exprt::check(expr);
115+
return static_cast<const EU_exprt &>(expr);
116+
}
117+
118+
static inline EU_exprt &to_EU_expr(exprt &expr)
119+
{
120+
PRECONDITION(expr.id() == ID_EU);
121+
EU_exprt::check(expr);
122+
return static_cast<EU_exprt &>(expr);
123+
}
124+
125+
class AU_exprt : public binary_predicate_exprt
126+
{
127+
public:
128+
explicit AU_exprt(exprt op0, exprt op1)
129+
: binary_predicate_exprt(std::move(op0), ID_AU, std::move(op1))
130+
{
131+
}
132+
};
133+
134+
static inline const AU_exprt &to_AU_expr(const exprt &expr)
135+
{
136+
PRECONDITION(expr.id() == ID_AU);
137+
AU_exprt::check(expr);
138+
return static_cast<const AU_exprt &>(expr);
139+
}
140+
141+
static inline AU_exprt &to_AU_expr(exprt &expr)
142+
{
143+
PRECONDITION(expr.id() == ID_AU);
144+
AU_exprt::check(expr);
145+
return static_cast<AU_exprt &>(expr);
146+
}
147+
148+
class ER_exprt : public binary_predicate_exprt
149+
{
150+
public:
151+
explicit ER_exprt(exprt op0, exprt op1)
152+
: binary_predicate_exprt(std::move(op0), ID_ER, std::move(op1))
153+
{
154+
}
155+
};
156+
157+
static inline const ER_exprt &to_ER_expr(const exprt &expr)
158+
{
159+
PRECONDITION(expr.id() == ID_ER);
160+
ER_exprt::check(expr);
161+
return static_cast<const ER_exprt &>(expr);
162+
}
163+
164+
static inline ER_exprt &to_ER_expr(exprt &expr)
165+
{
166+
PRECONDITION(expr.id() == ID_ER);
167+
ER_exprt::check(expr);
168+
return static_cast<ER_exprt &>(expr);
169+
}
170+
171+
class AR_exprt : public binary_predicate_exprt
172+
{
173+
public:
174+
explicit AR_exprt(exprt op0, exprt op1)
175+
: binary_predicate_exprt(std::move(op0), ID_AR, std::move(op1))
176+
{
177+
}
178+
};
179+
180+
static inline const AR_exprt &to_AR_expr(const exprt &expr)
181+
{
182+
PRECONDITION(expr.id() == ID_AR);
183+
AR_exprt::check(expr);
184+
return static_cast<const AR_exprt &>(expr);
185+
}
186+
187+
static inline AR_exprt &to_AR_expr(exprt &expr)
188+
{
189+
PRECONDITION(expr.id() == ID_AR);
190+
AR_exprt::check(expr);
191+
return static_cast<AR_exprt &>(expr);
192+
}
193+
194+
class AX_exprt : public unary_predicate_exprt
195+
{
196+
public:
197+
explicit AX_exprt(exprt op) : unary_predicate_exprt(ID_AX, std::move(op))
198+
{
199+
}
200+
};
201+
202+
static inline const AX_exprt &to_AX_expr(const exprt &expr)
203+
{
204+
PRECONDITION(expr.id() == ID_AX);
205+
AX_exprt::check(expr, validation_modet::INVARIANT);
206+
return static_cast<const AX_exprt &>(expr);
207+
}
208+
209+
static inline AX_exprt &to_AX_expr(exprt &expr)
210+
{
211+
PRECONDITION(expr.id() == ID_AX);
212+
AX_exprt::check(expr, validation_modet::INVARIANT);
213+
return static_cast<AX_exprt &>(expr);
214+
}
215+
216+
class EX_exprt : public unary_predicate_exprt
217+
{
218+
public:
219+
explicit EX_exprt(exprt op) : unary_predicate_exprt(ID_EX, std::move(op))
220+
{
221+
}
222+
};
223+
224+
static inline const EX_exprt &to_EX_expr(const exprt &expr)
225+
{
226+
PRECONDITION(expr.id() == ID_EX);
227+
EX_exprt::check(expr, validation_modet::INVARIANT);
228+
return static_cast<const EX_exprt &>(expr);
229+
}
230+
231+
static inline EX_exprt &to_EX_expr(exprt &expr)
232+
{
233+
PRECONDITION(expr.id() == ID_EX);
234+
EX_exprt::check(expr, validation_modet::INVARIANT);
235+
return static_cast<EX_exprt &>(expr);
236+
}
237+
238+
#endif

0 commit comments

Comments
 (0)