Merge pull request #7231 from thomasspriggs/tas/incremental_smt_directories

Move related sub components of incremental smt decision procedure into sub directories

Author: thomasspriggs

src/solvers/Makefile

@@ -193,25 +193,25 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
+      smt2_incremental/ast/smt_commands.cpp \
+      smt2_incremental/ast/smt_index.cpp \
+      smt2_incremental/ast/smt_logics.cpp \
+      smt2_incremental/ast/smt_options.cpp \
+      smt2_incremental/ast/smt_responses.cpp \
+      smt2_incremental/ast/smt_sorts.cpp \
+      smt2_incremental/ast/smt_terms.cpp \
       smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/object_tracking.cpp \
       smt2_incremental/type_size_mapping.cpp \
-      smt2_incremental/smt_array_theory.cpp \
-      smt2_incremental/smt_bit_vector_theory.cpp \
-      smt2_incremental/smt_commands.cpp \
-      smt2_incremental/smt_core_theory.cpp \
-      smt2_incremental/smt_index.cpp \
-      smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_object_size.cpp \
-      smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_response_validation.cpp \
-      smt2_incremental/smt_responses.cpp \
       smt2_incremental/smt_solver_process.cpp \
-      smt2_incremental/smt_sorts.cpp \
-      smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
+      smt2_incremental/theories/smt_array_theory.cpp \
+      smt2_incremental/theories/smt_bit_vector_theory.cpp \
+      smt2_incremental/theories/smt_core_theory.cpp \
       # Empty last line
 
 include ../common

src/solvers/smt2_incremental/internal_ast.txt renamed to src/solvers/smt2_incremental/ast/internal_ast.txt

@@ -0,0 +1,2 @@
+solvers
+util

src/solvers/smt2_incremental/ast/module_dependencies.txt

@@ -1,13 +1,13 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/smt_commands.h>
+#include "smt_commands.h"
 
 #include <util/range.h>
 
 // Define the irep_idts for commands.
 #define COMMAND_ID(the_id)                                                     \
   const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
-#include <solvers/smt2_incremental/smt_commands.def>
+#include "smt_commands.def"
 #undef COMMAND_ID
 
 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)
     return visitor.visit(static_cast<const smt_##the_id##_commandt &>(command));
 // The include below is marked as nolint because including the same file
 // multiple times is required as part of the x macro pattern.
-#include <solvers/smt2_incremental/smt_commands.def> // NOLINT(build/include)
+#include "smt_commands.def" // NOLINT(build/include)
 #undef COMMAND_ID
   UNREACHABLE;
 }

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

@@ -3,11 +3,12 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
 
-#include <solvers/smt2_incremental/smt_logics.h>
-#include <solvers/smt2_incremental/smt_options.h>
-#include <solvers/smt2_incremental/smt_terms.h>
 #include <util/irep.h>
 
+#include "smt_logics.h"
+#include "smt_options.h"
+#include "smt_terms.h"
+
 class smt_command_const_downcast_visitort;
 
 class smt_commandt : protected irept

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

@@ -1,11 +1,12 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/smt_logics.h>
+#include "smt_logics.h"
 
 // Define the irep_idts for logics.
 #define LOGIC_ID(the_id, the_name)                                             \
   const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
-#include <solvers/smt2_incremental/smt_logics.def>
+#include "smt_logics.def"
+
 #undef LOGIC_ID
 
 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)
     return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
 // The include below is marked as nolint because including the same file
 // multiple times is required as part of the x macro pattern.
-#include <solvers/smt2_incremental/smt_logics.def> // NOLINT(build/include)
+#include "smt_logics.def" // NOLINT(build/include)
 #undef LOGIC_ID
   UNREACHABLE;
 }