Skip to content

Commit 5d80ef9

Browse files
author
Daniel Kroening
committed
clean up the includes in prop_conv.h
1 parent 20cd882 commit 5d80ef9

File tree

6 files changed

+12
-12
lines changed

6 files changed

+12
-12
lines changed

src/goto-checker/goto_symex_property_decider.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,11 @@ Author: Daniel Kroening, Peter Schrammel
1111

1212
#include "goto_symex_property_decider.h"
1313

14+
#include <solvers/prop/literal_expr.h>
15+
#include <solvers/prop/prop.h>
16+
17+
#include <util/threeval.h>
18+
1419
goto_symex_property_decidert::goto_symex_property_decidert(
1520
const optionst &options,
1621
ui_message_handlert &ui_message_handler,

src/solvers/flattening/functions.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
1313
#define CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
1414

15+
#include <map>
1516
#include <set>
1617

1718
#include <util/mathematical_expr.h>

src/solvers/prop/cover_goals.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "cover_goals.h"
1313

1414
#include <util/message.h>
15+
#include <util/threeval.h>
1516

1617
#include "literal_expr.h"
1718
#include "prop_conv.h"

src/solvers/prop/prop_conv.h

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,17 +10,7 @@ Author: Daniel Kroening, [email protected]
1010
#ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
1111
#define CPROVER_SOLVERS_PROP_PROP_CONV_H
1212

13-
#include <string>
14-
#include <map>
15-
16-
#include <util/expr.h>
17-
#include <util/message.h>
18-
#include <util/std_expr.h>
19-
2013
#include "decision_procedure.h"
21-
#include "literal.h"
22-
#include "literal_expr.h"
23-
#include "prop.h"
2414

2515
// API that provides a "handle" in the form of a literalt
2616
// for expressions.

src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
3131
#include <solvers/flattening/c_bit_field_replacement_type.h>
3232
#include <solvers/floatbv/float_bv.h>
3333
#include <solvers/lowering/expr_lowering.h>
34+
#include <solvers/prop/literal_expr.h>
3435

3536
// Mark different kinds of error conditions
3637

src/solvers/smt2/smt2_dec.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,12 @@ Author: Daniel Kroening, [email protected]
1010
#ifndef CPROVER_SOLVERS_SMT2_SMT2_DEC_H
1111
#define CPROVER_SOLVERS_SMT2_SMT2_DEC_H
1212

13-
#include <fstream>
14-
1513
#include "smt2_conv.h"
1614

15+
#include <util/message.h>
16+
17+
#include <fstream>
18+
1719
class smt2_stringstreamt
1820
{
1921
protected:

0 commit comments

Comments
 (0)