Skip to content

Commit 67e50f5

Browse files
kroeningkroening
committed
extract expr2smvt into a separate header file
1 parent bad2f99 commit 67e50f5

File tree

2 files changed

+123
-123
lines changed

2 files changed

+123
-123
lines changed

‎src/smvlang/expr2smv.cpp

Lines changed: 1 addition & 123 deletions
Original file line numberDiff line numberDiff line change
@@ -7,129 +7,7 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include "expr2smv.h"
10-
11-
#include <util/arith_tools.h>
12-
#include <util/bitvector_types.h>
13-
#include <util/lispexpr.h>
14-
#include <util/lispirep.h>
15-
#include <util/namespace.h>
16-
#include <util/std_expr.h>
17-
#include <util/symbol.h>
18-
19-
class expr2smvt
20-
{
21-
public:
22-
explicit expr2smvt(const namespacet &__ns) : ns(__ns)
23-
{
24-
}
25-
26-
protected:
27-
// In NuSMV 2.6., ! (not) has a high precedence (above ::), whereas
28-
// in the CMU SMV implementation it has the same as other boolean operators.
29-
// We use the CMU SMV precedence for !.
30-
// Like CMU SMV, we give the same precedence to -> and <->, to avoid ambiguity.
31-
// Note that the precedence of mod in the CMU SMV differs from NuSMV's.
32-
// We use NuSMV's.
33-
enum class precedencet
34-
{
35-
MAX = 16,
36-
INDEX = 15, // [ ] , [ : ]
37-
CONCAT = 14, // ::
38-
UMINUS = 13, // - (unary minus)
39-
MULT = 12, // * / mod
40-
PLUS = 11, // + -
41-
SHIFT = 10, // << >>
42-
UNION = 9, // union
43-
IN = 8, // in
44-
REL = 7, // = != < > <= >=
45-
TEMPORAL = 6, // AX, AF, etc.
46-
NOT = 5, // !
47-
AND = 4, // &
48-
OR = 3, // | xor xnor
49-
IF = 2, // (• ? • : •)
50-
IFF = 1, // <->
51-
IMPLIES = 1 // ->
52-
};
53-
54-
/*
55-
From http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.ps
56-
57-
The order of precedence from high to low is
58-
* /
59-
+ -
60-
mod
61-
= != < > <= >=
62-
!
63-
&
64-
|
65-
-> <->
66-
*/
67-
68-
public:
69-
bool convert_nondet_choice(
70-
const exprt &src,
71-
std::string &dest,
72-
precedencet precedence);
73-
74-
bool convert_binary(
75-
const exprt &src,
76-
std::string &dest,
77-
const std::string &symbol,
78-
precedencet precedence);
79-
80-
bool convert_rtctl(
81-
const ternary_exprt &src,
82-
std::string &dest,
83-
const std::string &symbol,
84-
precedencet precedence);
85-
86-
bool convert_rtctl(
87-
const multi_ary_exprt &src,
88-
std::string &dest,
89-
const std::string &symbol1,
90-
const std::string &symbol2,
91-
precedencet precedence);
92-
93-
bool convert_unary(
94-
const unary_exprt &,
95-
std::string &dest,
96-
const std::string &symbol,
97-
precedencet precedence);
98-
99-
bool
100-
convert_index(const index_exprt &, std::string &dest, precedencet precedence);
101-
102-
bool convert(const exprt &src, std::string &dest, precedencet &precedence);
103-
104-
bool convert_if(const if_exprt &, std::string &dest, precedencet precedence);
105-
106-
std::string convert(const exprt &);
107-
108-
bool convert(const exprt &, std::string &dest);
109-
110-
bool convert_symbol(
111-
const symbol_exprt &,
112-
std::string &dest,
113-
precedencet &precedence);
114-
115-
bool convert_next_symbol(
116-
const exprt &src,
117-
std::string &dest,
118-
precedencet &precedence);
119-
120-
bool convert_constant(
121-
const constant_exprt &,
122-
std::string &dest,
123-
precedencet &precedence);
124-
125-
bool convert_cond(const exprt &src, std::string &dest);
126-
127-
bool
128-
convert_norep(const exprt &src, std::string &dest, precedencet &precedence);
129-
130-
protected:
131-
const namespacet &ns;
132-
};
10+
#include "expr2smv_class.h"
13311

13412
/*******************************************************************\
13513

‎src/smvlang/expr2smv_class.h

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
/*******************************************************************\
2+
3+
Module: SMV Expression Output
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_SMV_EXPR2SMV_CLASS_H
10+
#define CPROVER_SMV_EXPR2SMV_CLASS_H
11+
12+
#include <util/arith_tools.h>
13+
#include <util/bitvector_types.h>
14+
#include <util/namespace.h>
15+
#include <util/std_expr.h>
16+
#include <util/symbol.h>
17+
18+
#include "expr2smv.h"
19+
20+
class expr2smvt
21+
{
22+
public:
23+
explicit expr2smvt(const namespacet &__ns) : ns(__ns)
24+
{
25+
}
26+
27+
protected:
28+
// In NuSMV 2.6., ! (not) has a high precedence (above ::), whereas
29+
// in the CMU SMV implementation it has the same as other boolean operators.
30+
// We use the CMU SMV precedence for !.
31+
// Like CMU SMV, we give the same precedence to -> and <->, to avoid ambiguity.
32+
// Note that the precedence of mod in the CMU SMV differs from NuSMV's.
33+
// We use NuSMV's.
34+
enum class precedencet
35+
{
36+
MAX = 16,
37+
INDEX = 15, // [ ] , [ : ]
38+
CONCAT = 14, // ::
39+
UMINUS = 13, // - (unary minus)
40+
MULT = 12, // * / mod
41+
PLUS = 11, // + -
42+
SHIFT = 10, // << >>
43+
UNION = 9, // union
44+
IN = 8, // in
45+
REL = 7, // = != < > <= >=
46+
TEMPORAL = 6, // AX, AF, etc.
47+
NOT = 5, // !
48+
AND = 4, // &
49+
OR = 3, // | xor xnor
50+
IF = 2, // (• ? • : •)
51+
IFF = 1, // <->
52+
IMPLIES = 1 // ->
53+
};
54+
55+
/*
56+
From http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.ps
57+
58+
The order of precedence from high to low is
59+
* /
60+
+ -
61+
mod
62+
= != < > <= >=
63+
!
64+
&
65+
|
66+
-> <->
67+
*/
68+
69+
public:
70+
bool convert_nondet_choice(const exprt &src, std::string &dest, precedencet);
71+
72+
bool convert_binary(
73+
const exprt &src,
74+
std::string &dest,
75+
const std::string &symbol,
76+
precedencet);
77+
78+
bool convert_rtctl(
79+
const ternary_exprt &src,
80+
std::string &dest,
81+
const std::string &symbol,
82+
precedencet);
83+
84+
bool convert_rtctl(
85+
const multi_ary_exprt &src,
86+
std::string &dest,
87+
const std::string &symbol1,
88+
const std::string &symbol2,
89+
precedencet);
90+
91+
bool convert_unary(
92+
const unary_exprt &,
93+
std::string &dest,
94+
const std::string &symbol,
95+
precedencet);
96+
97+
bool convert_index(const index_exprt &, std::string &dest, precedencet);
98+
99+
bool convert(const exprt &src, std::string &dest, precedencet &);
100+
101+
bool convert_if(const if_exprt &, std::string &dest, precedencet);
102+
103+
std::string convert(const exprt &);
104+
105+
bool convert(const exprt &, std::string &dest);
106+
107+
bool convert_symbol(const symbol_exprt &, std::string &dest, precedencet &);
108+
109+
bool convert_next_symbol(const exprt &src, std::string &dest, precedencet &);
110+
111+
bool
112+
convert_constant(const constant_exprt &, std::string &dest, precedencet &);
113+
114+
bool convert_cond(const exprt &src, std::string &dest);
115+
116+
bool convert_norep(const exprt &src, std::string &dest, precedencet &);
117+
118+
protected:
119+
const namespacet &ns;
120+
};
121+
122+
#endif // CPROVER_SMV_EXPR2SMV_CLASS_H

0 commit comments

Comments
 (0)