Skip to content

Commit f6d0556

Browse files
committed
Move incremental SMT ast into sub directory
So that the ast data structure files are kept together and separated from the non data structure components of the incremental SMT decision procedure.
1 parent dcb99a2 commit f6d0556

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

49 files changed

+110
-101
lines changed

src/solvers/Makefile

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -193,23 +193,23 @@ SRC = $(BOOLEFORCE_SRC) \
193193
smt2/smt2_parser.cpp \
194194
smt2/smt2_tokenizer.cpp \
195195
smt2/smt2irep.cpp \
196+
smt2_incremental/ast/smt_commands.cpp \
197+
smt2_incremental/ast/smt_index.cpp \
198+
smt2_incremental/ast/smt_logics.cpp \
199+
smt2_incremental/ast/smt_options.cpp \
200+
smt2_incremental/ast/smt_responses.cpp \
201+
smt2_incremental/ast/smt_sorts.cpp \
202+
smt2_incremental/ast/smt_terms.cpp \
196203
smt2_incremental/construct_value_expr_from_smt.cpp \
197204
smt2_incremental/convert_expr_to_smt.cpp \
198205
smt2_incremental/object_tracking.cpp \
199206
smt2_incremental/type_size_mapping.cpp \
200207
smt2_incremental/smt_array_theory.cpp \
201208
smt2_incremental/smt_bit_vector_theory.cpp \
202-
smt2_incremental/smt_commands.cpp \
203209
smt2_incremental/smt_core_theory.cpp \
204-
smt2_incremental/smt_index.cpp \
205-
smt2_incremental/smt_logics.cpp \
206210
smt2_incremental/smt_object_size.cpp \
207-
smt2_incremental/smt_options.cpp \
208211
smt2_incremental/smt_response_validation.cpp \
209-
smt2_incremental/smt_responses.cpp \
210212
smt2_incremental/smt_solver_process.cpp \
211-
smt2_incremental/smt_sorts.cpp \
212-
smt2_incremental/smt_terms.cpp \
213213
smt2_incremental/smt_to_smt2_string.cpp \
214214
smt2_incremental/smt2_incremental_decision_procedure.cpp \
215215
# Empty last line
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
solvers
2+
util

src/solvers/smt2_incremental/smt_commands.cpp renamed to src/solvers/smt2_incremental/ast/smt_commands.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
// Author: Diffblue Ltd.
22

3-
#include <solvers/smt2_incremental/smt_commands.h>
3+
#include "smt_commands.h"
44

55
#include <util/range.h>
66

77
// Define the irep_idts for commands.
88
#define COMMAND_ID(the_id) \
99
const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
10-
#include <solvers/smt2_incremental/smt_commands.def>
10+
#include "smt_commands.def"
1111
#undef COMMAND_ID
1212

1313
bool smt_commandt::operator==(const smt_commandt &other) const
@@ -184,7 +184,7 @@ void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
184184
return visitor.visit(static_cast<const smt_##the_id##_commandt &>(command));
185185
// The include below is marked as nolint because including the same file
186186
// multiple times is required as part of the x macro pattern.
187-
#include <solvers/smt2_incremental/smt_commands.def> // NOLINT(build/include)
187+
#include "smt_commands.def" // NOLINT(build/include)
188188
#undef COMMAND_ID
189189
UNREACHABLE;
190190
}

src/solvers/smt2_incremental/smt_commands.h renamed to src/solvers/smt2_incremental/ast/smt_commands.h

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,12 @@
33
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
44
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
55

6-
#include <solvers/smt2_incremental/smt_logics.h>
7-
#include <solvers/smt2_incremental/smt_options.h>
8-
#include <solvers/smt2_incremental/smt_terms.h>
96
#include <util/irep.h>
107

8+
#include "smt_logics.h"
9+
#include "smt_options.h"
10+
#include "smt_terms.h"
11+
1112
class smt_command_const_downcast_visitort;
1213

1314
class smt_commandt : protected irept

src/solvers/smt2_incremental/smt_logics.cpp renamed to src/solvers/smt2_incremental/ast/smt_logics.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
11
// Author: Diffblue Ltd.
22

3-
#include <solvers/smt2_incremental/smt_logics.h>
3+
#include "smt_logics.h"
44

55
// Define the irep_idts for logics.
66
#define LOGIC_ID(the_id, the_name) \
77
const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
8-
#include <solvers/smt2_incremental/smt_logics.def>
8+
#include "smt_logics.def"
9+
910
#undef LOGIC_ID
1011

1112
bool smt_logict::operator==(const smt_logict &other) const
@@ -26,7 +27,7 @@ void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
2627
return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
2728
// The include below is marked as nolint because including the same file
2829
// multiple times is required as part of the x macro pattern.
29-
#include <solvers/smt2_incremental/smt_logics.def> // NOLINT(build/include)
30+
#include "smt_logics.def" // NOLINT(build/include)
3031
#undef LOGIC_ID
3132
UNREACHABLE;
3233
}

0 commit comments

Comments
 (0)