Moved incremental smt struct encoding to subfolder

Enrico Steffinlongo · Enrico Steffinlongo · commit 7630989903b3 · 2023-06-14T10:34:06.000+01:00
As support for non-native C types (e.g. enums) is added in the
incremental smt2 solver, other new encoding functions will be added. For
this reason, to avoid putting all the encoding functions in the
incremental smt2 solver root folder a new `encoding` folder has been
created and the struct encoding functions have been moved there.
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -210,7 +210,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
-      smt2_incremental/struct_encoding.cpp \
+      smt2_incremental/encoding/struct_encoding.cpp \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \
diff --git a/src/solvers/smt2_incremental/encoding/module_dependencies.txt b/src/solvers/smt2_incremental/encoding/module_dependencies.txt
@@ -0,0 +1 @@
+util
diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp
diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.h b/src/solvers/smt2_incremental/encoding/struct_encoding.h
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -10,10 +10,10 @@
 #include <util/std_expr.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
+#include <solvers/smt2_incremental/encoding/struct_encoding.h>
 #include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
-#include <solvers/smt2_incremental/struct_encoding.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
 
diff --git a/unit/Makefile b/unit/Makefile
@@ -114,7 +114,7 @@ SRC += analyses/ai/ai.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/struct_encoding.cpp \
+       solvers/smt2_incremental/encoding/struct_encoding.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 \
diff --git a/unit/solvers/smt2_incremental/encoding/module_dependencies.txt b/unit/solvers/smt2_incremental/encoding/module_dependencies.txt
@@ -0,0 +1,3 @@
+solvers/smt2_incremental/encoding
+testing-utils
+util
diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp
@@ -6,7 +6,7 @@
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
-#include <solvers/smt2_incremental/struct_encoding.h>
+#include <solvers/smt2_incremental/encoding/struct_encoding.h>
 #include <testing-utils/use_catch.h>
 
 struct struct_encoding_test_environmentt

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+solvers/smt2_incremental/encoding`
	`2`	`+testing-utils`
	`3`	`+util`