Move incremental SMT theories into sub directory

thomasspriggs · thomasspriggs · commit 4f403c751ff4 · 2022-10-11T12:40:09.000+01:00
So that the theory files are kept together and separated from the other
components of the incremental SMT decision procedure.
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -204,14 +204,14 @@ SRC = $(BOOLEFORCE_SRC) \
       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_core_theory.cpp \
       smt2_incremental/smt_object_size.cpp \
       smt2_incremental/smt_response_validation.cpp \
       smt2_incremental/smt_solver_process.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
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -18,9 +18,9 @@
 
 #include <solvers/prop/literal_expr.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
-#include <solvers/smt2_incremental/smt_array_theory.h>
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
+#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 
 #include <functional>
 #include <numeric>
diff --git a/src/solvers/smt2_incremental/module_dependencies.txt b/src/solvers/smt2_incremental/module_dependencies.txt
@@ -1,2 +1,3 @@
 solvers
+theories
 util
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -16,9 +16,9 @@
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
-#include <solvers/smt2_incremental/smt_array_theory.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 
 #include <stack>
diff --git a/src/solvers/smt2_incremental/smt_object_size.cpp b/src/solvers/smt2_incremental/smt_object_size.cpp
@@ -7,7 +7,7 @@
 
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 
 static smt_declare_function_commandt make_object_size_function_declaration()
 {
diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -21,7 +21,8 @@
 #include <util/mp_arith.h>
 #include <util/range.h>
 
-#include "smt_array_theory.h"
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
+
 #include "smt_to_smt2_string.h"
 
 #include <regex>
diff --git a/src/solvers/smt2_incremental/theories/module_dependencies.txt b/src/solvers/smt2_incremental/theories/module_dependencies.txt
diff --git a/src/solvers/smt2_incremental/theories/smt_array_theory.cpp b/src/solvers/smt2_incremental/theories/smt_array_theory.cpp
diff --git a/src/solvers/smt2_incremental/theories/smt_array_theory.h b/src/solvers/smt2_incremental/theories/smt_array_theory.h
diff --git a/src/solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp
@@ -1,6 +1,6 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
+#include "smt_bit_vector_theory.h"
 
 #include <util/invariant.h>
 
diff --git a/src/solvers/smt2_incremental/theories/smt_bit_vector_theory.h b/src/solvers/smt2_incremental/theories/smt_bit_vector_theory.h
diff --git a/src/solvers/smt2_incremental/theories/smt_core_theory.cpp b/src/solvers/smt2_incremental/theories/smt_core_theory.cpp
@@ -1,6 +1,6 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/smt_core_theory.h>
+#include "smt_core_theory.h"
 
 const char *smt_core_theoryt::nott::identifier()
 {
diff --git a/src/solvers/smt2_incremental/theories/smt_core_theory.h b/src/solvers/smt2_incremental/theories/smt_core_theory.h
diff --git a/unit/Makefile b/unit/Makefile
@@ -109,12 +109,12 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/convert_expr_to_smt.cpp \
        solvers/smt2_incremental/object_tracking.cpp \
        solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
-       solvers/smt2_incremental/smt_array_theory.cpp \
-       solvers/smt2_incremental/smt_bit_vector_theory.cpp \
-       solvers/smt2_incremental/smt_core_theory.cpp \
        solvers/smt2_incremental/smt_object_size.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \
+       solvers/smt2_incremental/theories/smt_array_theory.cpp \
+       solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp \
+       solvers/smt2_incremental/theories/smt_core_theory.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
diff --git a/unit/solvers/smt2_incremental/ast/module_dependencies.txt b/unit/solvers/smt2_incremental/ast/module_dependencies.txt
@@ -1,2 +1,3 @@
 solvers/smt2_incremental/ast
+solvers/smt2_incremental/theories
 testing-utils
diff --git a/unit/solvers/smt2_incremental/ast/smt_commands.cpp b/unit/solvers/smt2_incremental/ast/smt_commands.cpp
@@ -1,7 +1,7 @@
 // Author: Diffblue Ltd.
 
 #include <solvers/smt2_incremental/ast/smt_commands.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE("Test smt_commandt.pretty is accessible.", "[core][smt2_incremental]")
diff --git a/unit/solvers/smt2_incremental/ast/smt_terms.cpp b/unit/solvers/smt2_incremental/ast/smt_terms.cpp
@@ -3,7 +3,7 @@
 #include <util/mp_arith.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 
diff --git a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp
@@ -9,8 +9,8 @@
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 
diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -15,10 +15,10 @@
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/object_tracking.h>
-#include <solvers/smt2_incremental/smt_array_theory.h>
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
+#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -13,9 +13,9 @@
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
-#include <solvers/smt2_incremental/smt_array_theory.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 
diff --git a/unit/solvers/smt2_incremental/smt_object_size.cpp b/unit/solvers/smt2_incremental/smt_object_size.cpp
@@ -3,8 +3,8 @@
 #include <util/c_types.h>
 #include <util/config.h>
 
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE("Test smt_object_sizet", "[core][smt2_incremental]")
diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
@@ -2,8 +2,8 @@
 
 #include <util/mp_arith.h>
 
-#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_response_validation.h>
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
 #include <testing-utils/smt2irep.h>
 #include <testing-utils/use_catch.h>
 
diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
@@ -6,9 +6,9 @@
 #include <solvers/smt2_incremental/ast/smt_logics.h>
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE("Test smt_indext to string conversion", "[core][smt2_incremental]")
diff --git a/unit/solvers/smt2_incremental/theories/module_dependencies.txt b/unit/solvers/smt2_incremental/theories/module_dependencies.txt
@@ -0,0 +1,4 @@
+solvers/smt2_incremental/ast
+solvers/smt2_incremental/theories
+testing-utils
+util
diff --git a/unit/solvers/smt2_incremental/theories/smt_array_theory.cpp b/unit/solvers/smt2_incremental/theories/smt_array_theory.cpp
@@ -2,12 +2,11 @@
 
 #include <util/mp_arith.h>
 
-#include <solvers/smt2_incremental/smt_array_theory.h>
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
+#include <solvers/smt2_incremental/theories/smt_array_theory.h>
+#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
+#include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 
-#include "testing-utils/invariant.h"
-
 TEST_CASE("SMT array theory \"select\".", "[core][smt2_incremental]")
 {
   const smt_identifier_termt index_term("index", smt_bit_vector_sortt(64));
diff --git a/unit/solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp b/unit/solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp
@@ -3,7 +3,7 @@
 #include <util/mp_arith.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
+#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE("SMT bit vector concatenation", "[core][smt2_incremental]")
diff --git a/unit/solvers/smt2_incremental/theories/smt_core_theory.cpp b/unit/solvers/smt2_incremental/theories/smt_core_theory.cpp
@@ -3,7 +3,7 @@
 #include <util/mp_arith.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]")

Original file line number	Diff line number	Diff line change
`@@ -7,7 +7,7 @@`
`7`	`7`
`8`	`8`	`#include <solvers/smt2_incremental/ast/smt_sorts.h>`
`9`	`9`	`#include <solvers/smt2_incremental/convert_expr_to_smt.h>`
`10`		`-#include <solvers/smt2_incremental/smt_core_theory.h>`
	`10`	`+#include <solvers/smt2_incremental/theories/smt_core_theory.h>`
`11`	`11`
`12`	`12`	`static smt_declare_function_commandt make_object_size_function_declaration()`
`13`	`13`	`{`