Skip to content

Commit decbdc9

Browse files
committed
Move unnecessarily inlined implementations to otherwise empty cpp file
This provides guidance to the compiler on where to place virtual tables, and also silences a linker warning.
1 parent d6bdee6 commit decbdc9

File tree

4 files changed

+15
-7
lines changed

4 files changed

+15
-7
lines changed

src/util/decision_procedure.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,10 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "decision_procedure.h"
1313

14+
decision_proceduret::decision_proceduret(const namespacet &_ns) : ns(_ns)
15+
{
16+
}
1417

18+
decision_proceduret::~decision_proceduret()
19+
{
20+
}

src/util/decision_procedure.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,9 @@ class namespacet;
2020
class decision_proceduret:public messaget
2121
{
2222
public:
23-
explicit decision_proceduret(const namespacet &_ns):ns(_ns)
24-
{
25-
}
23+
explicit decision_proceduret(const namespacet &_ns);
24+
25+
virtual ~decision_proceduret();
2626

2727
// get a value from satisfying instance if satisfiable
2828
// returns nil if not available

src/util/dstring.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,8 @@ Author: Daniel Kroening, [email protected]
1010
/// Container for C-Strings
1111

1212
#include "dstring.h"
13+
14+
std::ostream &dstringt::operator<<(std::ostream &out) const
15+
{
16+
return out << as_string();
17+
}

src/util/dstring.h

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -123,10 +123,7 @@ class dstringt final
123123

124124
// output
125125

126-
std::ostream &operator<<(std::ostream &out) const
127-
{
128-
return out << as_string();
129-
}
126+
std::ostream &operator<<(std::ostream &out) const;
130127

131128
// non-standard
132129

0 commit comments

Comments
 (0)