27
27
class prop_convt :public decision_proceduret
28
28
{
29
29
public:
30
- explicit prop_convt (
31
- const namespacet &_ns):
32
- decision_proceduret(_ns) { }
33
- virtual ~prop_convt () { }
30
+ explicit prop_convt (const namespacet &_ns) : decision_proceduret(_ns)
31
+ {
32
+ }
33
+
34
+ virtual ~prop_convt ()
35
+ {
36
+ }
34
37
35
38
// conversion to handle
36
39
virtual literalt convert (const exprt &expr)=0;
@@ -49,15 +52,27 @@ class prop_convt:public decision_proceduret
49
52
virtual void set_frozen (literalt a);
50
53
virtual void set_frozen (const bvt &);
51
54
virtual void set_assumptions (const bvt &_assumptions);
52
- virtual bool has_set_assumptions () const { return false ; }
53
- virtual void set_all_frozen () {}
55
+
56
+ virtual bool has_set_assumptions () const
57
+ {
58
+ return false ;
59
+ }
60
+
61
+ virtual void set_all_frozen ()
62
+ {
63
+ }
54
64
55
65
// returns true if an assumption is in the final conflict
56
66
virtual bool is_in_conflict (literalt l) const ;
57
- virtual bool has_is_in_conflict () const { return false ; }
67
+ virtual bool has_is_in_conflict () const
68
+ {
69
+ return false ;
70
+ }
58
71
59
72
// Resource limits:
60
- virtual void set_time_limit_seconds (uint32_t ) {}
73
+ virtual void set_time_limit_seconds (uint32_t )
74
+ {
75
+ }
61
76
};
62
77
63
78
//
@@ -70,9 +85,10 @@ class prop_convt:public decision_proceduret
70
85
class prop_conv_solvert :public prop_convt
71
86
{
72
87
public:
73
- prop_conv_solvert (const namespacet &_ns, propt &_prop):
74
- prop_convt (_ns),
75
- prop (_prop) { }
88
+ prop_conv_solvert (const namespacet &_ns, propt &_prop)
89
+ : prop_convt(_ns), prop(_prop)
90
+ {
91
+ }
76
92
77
93
virtual ~prop_conv_solvert () = default ;
78
94
@@ -81,34 +97,50 @@ class prop_conv_solvert:public prop_convt
81
97
decision_proceduret::resultt dec_solve () override ;
82
98
void print_assignment (std::ostream &out) const override ;
83
99
std::string decision_procedure_text () const override
84
- { return " propositional reduction" ; }
100
+ {
101
+ return " propositional reduction" ;
102
+ }
85
103
exprt get (const exprt &expr) const override ;
86
104
87
105
// overloading from prop_convt
88
106
using prop_convt::set_frozen;
89
- virtual tvt l_get (literalt a) const override { return prop.l_get (a); }
107
+ virtual tvt l_get (literalt a) const override
108
+ {
109
+ return prop.l_get (a);
110
+ }
90
111
void set_frozen (literalt a) override
91
112
{
92
113
prop.set_frozen (a);
93
114
}
94
115
void set_assumptions (const bvt &_assumptions) override
95
- { prop.set_assumptions (_assumptions); }
116
+ {
117
+ prop.set_assumptions (_assumptions);
118
+ }
96
119
bool has_set_assumptions () const override
97
- { return prop.has_set_assumptions (); }
120
+ {
121
+ return prop.has_set_assumptions ();
122
+ }
98
123
void set_all_frozen () override
99
124
{
100
125
freeze_all = true ;
101
126
}
102
127
literalt convert (const exprt &expr) override ;
103
128
bool is_in_conflict (literalt l) const override
104
- { return prop.is_in_conflict (l); }
129
+ {
130
+ return prop.is_in_conflict (l);
131
+ }
105
132
bool has_is_in_conflict () const override
106
- { return prop.has_is_in_conflict (); }
133
+ {
134
+ return prop.has_is_in_conflict ();
135
+ }
107
136
108
137
// get literal for expression, if available
109
138
virtual optionalt<literalt> literal (const exprt &expr) const ;
110
139
111
- virtual void clear_cache () { cache.clear ();}
140
+ virtual void clear_cache ()
141
+ {
142
+ cache.clear ();
143
+ }
112
144
113
145
bool use_cache = true ;
114
146
bool equality_propagation = true ;
0 commit comments