Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Moved number-related files into separate directory #805

Merged
merged 1 commit into from
Nov 6, 2024
Merged

Moved number-related files into separate directory #805

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions .clang-files
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,16 @@
./src/cnfizers/Tseitin.cc
./src/cnfizers/Tseitin.h

./src/common/numbers/Integer.h
./src/common/numbers/Number.h
./src/common/numbers/Real.h
./src/common/ApiException.h
./src/common/FlaPartitionMap.cc
./src/common/FlaPartitionMap.h
./src/common/InternalException.h
./src/common/Number.h
./src/common/PartitionInfo.cc
./src/common/PartitionInfo.h
./src/common/Random.h
./src/common/Real.h
./src/common/ScopedVector.h
./src/common/StringMap.h
./src/common/TermNames.h
Expand Down
13 changes: 5 additions & 8 deletions src/common/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,10 @@ add_library(common OBJECT)

target_sources(common
PUBLIC
"${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
"${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
"${CMAKE_CURRENT_LIST_DIR}/Real.h"
"${CMAKE_CURRENT_LIST_DIR}/TermNames.h"
PRIVATE
"${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
"${CMAKE_CURRENT_LIST_DIR}/Integer.h"
"${CMAKE_CURRENT_LIST_DIR}/Number.h"
"${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h"
"${CMAKE_CURRENT_LIST_DIR}/inttypes.h"
"${CMAKE_CURRENT_LIST_DIR}/StringMap.h"
"${CMAKE_CURRENT_LIST_DIR}/StringConv.h"
Expand All @@ -22,8 +17,10 @@ PRIVATE
"${CMAKE_CURRENT_LIST_DIR}/ReportUtils.h"
)

include(numbers/CMakeLists.txt)

install(FILES
Integer.h Number.h FastRational.h StringMap.h Timer.h inttypes.h
TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h ApiException.h TypeUtils.h
NumberUtils.h NatSet.h ScopedVector.h TermNames.h
StringMap.h Timer.h inttypes.h
TreeOps.h FlaPartitionMap.h PartitionInfo.h ApiException.h TypeUtils.h
NatSet.h ScopedVector.h TermNames.h
DESTINATION ${INSTALL_HEADERS_DIR}/common)
2 changes: 1 addition & 1 deletion src/common/StringConv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
#ifndef OPENSMT_STRINGCONV_H
#define OPENSMT_STRINGCONV_H

#include "NumberUtils.h"
#include "numbers/NumberUtils.h"

namespace opensmt {

Expand Down
17 changes: 17 additions & 0 deletions src/common/numbers/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
target_sources(common
PUBLIC
"${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
"${CMAKE_CURRENT_LIST_DIR}/Integer.h"
"${CMAKE_CURRENT_LIST_DIR}/Number.h"
"${CMAKE_CURRENT_LIST_DIR}/Real.h"
PRIVATE
"${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h"
)

install(FILES
${CMAKE_CURRENT_LIST_DIR}/Integer.h
${CMAKE_CURRENT_LIST_DIR}/Number.h
${CMAKE_CURRENT_LIST_DIR}/FastRational.h
${CMAKE_CURRENT_LIST_DIR}/Real.h
${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h
DESTINATION ${INSTALL_HEADERS_DIR}/common/numbers)
0 src/common/FastRational.cc → src/common/numbers/FastRational.cc
View file
Open in desktop
File renamed without changes.
0 src/common/FastRational.h → src/common/numbers/FastRational.h
View file
Open in desktop
File renamed without changes.
4 changes: 2 additions & 2 deletions src/common/Integer.h → src/common/numbers/Integer.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
#include "Number.h"

namespace opensmt {
typedef Number Integer2;
typedef Number Integer2;
}

#endif //OPENSMT_INTEGER_H
#endif // OPENSMT_INTEGER_H
0 src/common/Number.h → src/common/numbers/Number.h
View file
Open in desktop
File renamed without changes.
0 src/common/NumberUtils.h → src/common/numbers/NumberUtils.h
View file
Open in desktop
File renamed without changes.
0 src/common/Real.h → src/common/numbers/Real.h
View file
Open in desktop
File renamed without changes.
1 change: 0 additions & 1 deletion src/logics/ArithLogic.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
#include "ArithLogic.h"

#include <common/ApiException.h>
#include <common/FastRational.h>
#include <common/InternalException.h>
#include <common/StringConv.h>
#include <common/TreeOps.h>
Expand Down
2 changes: 1 addition & 1 deletion src/logics/ArithLogic.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

#include "Logic.h"

#include <common/Number.h>
#include <common/numbers/Number.h>

#include <numeric>

Expand Down
2 changes: 1 addition & 1 deletion src/logics/BVLogic.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Module: New Logic for BitVector

#include "Logic.h"

#include <common/NumberUtils.h>
#include <common/numbers/NumberUtils.h>

namespace opensmt {

Expand Down
2 changes: 1 addition & 1 deletion src/simplifiers/LA.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

#include <pterms/PtStructs.h>
#include <logics/ArithLogic.h>
#include <common/Real.h>
#include <common/numbers/Real.h>

#include <map>

Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/bvsolver/BitBlaster.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

#include <models/ModelBuilder.h>
#include <api/MainSolver.h>
#include <common/Real.h>
#include <common/numbers/Real.h>

namespace opensmt {

Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/lasolver/CutCreator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@
#include "Polynomial.h"
#include "SparseMatrix.h"

#include <common/Real.h>
#include <common/TypeUtils.h>
#include <common/numbers/Real.h>
#include <pterms/PTRef.h>

namespace opensmt {
Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/lasolver/Delta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
#ifndef DELTA_H
#define DELTA_H

#include <common/Real.h>
#include <common/numbers/Real.h>

#include <iosfwd>

Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/lasolver/FarkasInterpolator.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@

#include <common/ApiException.h>
#include <common/InternalException.h>
#include <common/Real.h>
#include <common/numbers/Real.h>
#include <logics/ArithLogic.h>
#include <simplifiers/LA.h>

Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/lasolver/FarkasInterpolator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
#ifndef OPENSMT_FARKASINTERPOLATOR_H
#define OPENSMT_FARKASINTERPOLATOR_H

#include <common/Real.h>
#include <common/numbers/Real.h>
#include <pterms/PtStructs.h>
#include <smtsolvers/TheoryInterpolator.h>

Expand Down
4 changes: 2 additions & 2 deletions src/tsolvers/lasolver/LASolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@

#include "LASolver.h"
#include "FarkasInterpolator.h"
#include <simplifiers/LA.h>
#include "LIAInterpolator.h"
#include "CutCreator.h"

#include <models/ModelBuilder.h>
#include <common/Random.h>
#include <models/ModelBuilder.h>
#include <simplifiers/LA.h>

#include <unordered_set>

Expand Down
1 change: 1 addition & 0 deletions src/tsolvers/lasolver/LASolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
#include "Tableau.h"

#include <common/Timer.h>
#include <common/numbers/Real.h>
#include <logics/ArithLogic.h>
#include <tsolvers/TSolver.h>

Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/lasolver/Polynomial.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
#ifndef OPENSMT_POLYNOMIAL_H
#define OPENSMT_POLYNOMIAL_H

#include <common/Real.h>
#include <common/numbers/Real.h>

#include <vector>
#include <unordered_map>
Expand Down
1 change: 1 addition & 0 deletions src/tsolvers/lasolver/Simplex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#include "LRAModel.h"
#include "Tableau.h"

#include <common/numbers/Real.h>
#include <options/SMTConfig.h>

namespace opensmt {
Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/lasolver/Tableau.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
#include "LAVar.h"
#include "Polynomial.h"

#include <common/Real.h>
#include <common/numbers/Real.h>

#include <algorithm>
#include <functional>
Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/stpsolver/Converter.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#ifndef OPENSMT_CONVERTER_H
#define OPENSMT_CONVERTER_H

#include <common/Number.h>
#include <common/numbers/Number.h>

#include <concepts>
#include <cstddef>
Expand Down
2 changes: 1 addition & 1 deletion src/tsolvers/stpsolver/STPStore.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#ifndef OPENSMT_STPSTORE_H
#define OPENSMT_STPSTORE_H

#include <common/Number.h>
#include <common/numbers/Number.h>
#include <pterms/PtStructs.h>

#include <cstdint>
Expand Down
2 changes: 1 addition & 1 deletion test/unit/test_LIACutSolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include <gtest/gtest.h>
#include <common/Real.h>
#include <common/numbers/Real.h>
#include <options/SMTConfig.h>
#include <tsolvers/lasolver/Simplex.h>

Expand Down
2 changes: 1 addition & 1 deletion test/unit/test_LIAStrengthening.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// Created by prova on 30.09.20.
//
#include <gtest/gtest.h>
#include <common/Real.h>
#include <common/numbers/Real.h>
#include <logics/ArithLogic.h>

namespace opensmt {
Expand Down
2 changes: 1 addition & 1 deletion test/unit/test_Rationals.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include <gtest/gtest.h>
#include <common/Real.h>
#include <common/numbers/Real.h>

#include <vector>

Expand Down