chore: rename Solver to SmtSolver

benchmark/util/InfoGatherer.cpp

@@ -86,7 +86,7 @@ void InfoGatherer::ParseResults(shared_results *results) {
 
 void InfoGatherer::GatherInfo(shared_results *results) {
   auto start = std::chrono::high_resolution_clock::now();
-  Solver solver{config_};
+  SmtSolver solver{config_};
   auto res = solver.CheckSat();
 
   results->nAssertions = res.n_assertions();

benchmark/util/InfoGatherer.h

@@ -8,7 +8,7 @@
 #include <regex>
 #include <sstream>
 
-#include "dlinear/solver/Solver.h"
+#include "dlinear/solver/SmtSolver.h"
 #include "dlinear/util/Config.h"
 
 namespace dlinear::benchmark {

dlinear/main.cpp

@@ -10,8 +10,8 @@
  */
 #include <csignal>
 
-#include "dlinear/solver/Solver.h"
-#include "dlinear/solver/SolverOutput.h"
+#include "dlinear/solver/SmtSolver.h"
+#include "dlinear/solver/SmtSolverOutput.h"
 #include "dlinear/util/ArgParser.h"
 #include "dlinear/util/Config.h"
 #include "dlinear/util/Timer.h"
@@ -35,7 +35,7 @@ int main(int argc, const char* argv[]) {
   dlinear::Config config = parser.toConfig();
 
   // Setup the infinity values.
-  dlinear::Solver solver{config};
+  dlinear::SmtSolver solver{config};
 
   // Start the main timer and run the solver.
   dlinear::main_timer.start();

dlinear/solver/BUILD.bazel

@@ -178,12 +178,12 @@ dlinear_cc_library(
 dlinear_cc_library(
     name = "solver",
     srcs = [
-        "Solver.cpp",
-        "SolverOutput.cpp",
+        "SmtSolver.cpp",
+        "SmtSolverOutput.cpp",
     ],
     hdrs = [
-        "Solver.h",
-        "SolverOutput.h",
+        "SmtSolver.h",
+        "SmtSolverOutput.h",
     ],
     local_defines = select({
         "//tools:dynamic_build": ["DLINEAR_PYDLINEAR"],

dlinear/solver/Solver.cpp → dlinear/solver/SmtSolver.cpp

@@ -1,17 +1,17 @@
 /**
- * @file Solver.cpp
+ * @file SmtSolver.cpp
  * @author dlinear (https://github.com/TendTo/dlinear)
  * @copyright 2024 dlinear
  * @licence Apache-2.0 license
  */
-#include "Solver.h"
+#include "SmtSolver.h"
 
 #include <optional>
 #include <utility>
 
 #include "dlinear/mps/Driver.h"
 #include "dlinear/smt2/Driver.h"
-#include "dlinear/solver/SolverOutput.h"
+#include "dlinear/solver/SmtSolverOutput.h"
 #include "dlinear/symbolic/symbolic.h"
 #include "dlinear/util/Infinity.h"
 #include "dlinear/util/Timer.h"
@@ -20,26 +20,26 @@
 
 namespace dlinear {
 
-Solver::Solver() : Solver{Config{true}} {}
-Solver::Solver(const std::string &filename) : Solver{Config{filename}} {}
-Solver::Solver(Config config)
+SmtSolver::SmtSolver() : SmtSolver{Config{true}} {}
+SmtSolver::SmtSolver(const std::string &filename) : SmtSolver{Config{filename}} {}
+SmtSolver::SmtSolver(Config config)
     : config_{std::move(config)},
       guard_{config_},
       context_{config_},
       output_{config_.precision(), config_.produce_models(), config_.with_timings()} {}
 
 #ifdef DLINEAR_PYDLINEAR
 
-Solver &Solver::Enter() { return *this; }
+SmtSolver &SmtSolver::Enter() { return *this; }
 
-void Solver::Exit() { guard_.DeInit(); }
+void SmtSolver::Exit() { guard_.DeInit(); }
 
 #endif
 
-SolverOutput Solver::CheckSat() {
-  DLINEAR_TRACE("Solver::CheckSat");
+SmtSolverOutput SmtSolver::CheckSat() {
+  DLINEAR_TRACE("SmtSolver::CheckSat");
   if (output_.result != SolverResult::UNSOLVED) return output_;
-  DLINEAR_DEBUG("Solver::CheckSat -- No cached result fond.");
+  DLINEAR_DEBUG("SmtSolver::CheckSat -- No cached result fond.");
   if (!ParseInput()) DLINEAR_RUNTIME_ERROR_FMT("Failed to parse input file: {}", config_.filename());
   output_.n_assertions = context_.assertions().size();
 
@@ -53,14 +53,14 @@ SolverOutput Solver::CheckSat() {
   return output_;
 }
 
-void Solver::Visualize() {
-  DLINEAR_TRACE("Solver::Visualize");
+void SmtSolver::Visualize() {
+  DLINEAR_TRACE("SmtSolver::Visualize");
   if (!ParseInput()) DLINEAR_RUNTIME_ERROR_FMT("Failed to parse input file: {}", config_.filename());
   for (const auto &a : context_.assertions()) std::cout << a << std::endl;
 }
 
-bool Solver::ParseInput() {
-  DLINEAR_TRACE("Solver::ParseInput");
+bool SmtSolver::ParseInput() {
+  DLINEAR_TRACE("SmtSolver::ParseInput");
   TimerGuard timer_guard{&output_.parser_timer, true};
   switch (config_.format()) {
     case Config::Format::AUTO:
@@ -77,22 +77,22 @@ bool Solver::ParseInput() {
   }
 }
 
-bool Solver::ParseSmt2() {
-  DLINEAR_DEBUG("Solver::ParseSmt2");
+bool SmtSolver::ParseSmt2() {
+  DLINEAR_DEBUG("SmtSolver::ParseSmt2");
   smt2::Smt2Driver smt2_driver{context_};
   if (config_.read_from_stdin()) return smt2_driver.parse_stream(std::cin, "(stdin)");
   return smt2_driver.parse_file(config_.filename());
 }
 
-bool Solver::ParseMps() {
-  DLINEAR_DEBUG("Solver::ParseMps");
+bool SmtSolver::ParseMps() {
+  DLINEAR_DEBUG("SmtSolver::ParseMps");
   mps::MpsDriver mps_driver{context_};
   if (config_.read_from_stdin()) return mps_driver.parse_stream(std::cin, "(stdin)");
   return mps_driver.parse_file(config_.filename());
 }
 
-void Solver::CheckObjCore() {
-  DLINEAR_DEBUG("Solver::CheckObjCore");
+void SmtSolver::CheckObjCore() {
+  DLINEAR_DEBUG("SmtSolver::CheckObjCore");
   TimerGuard timer_guard{&output_.smt_solver_timer, true};
   LpResult status = context_.CheckOpt(&output_.lower_bound, &output_.upper_bound);
   if (LpResult::LP_DELTA_OPTIMAL == status) {
@@ -107,8 +107,8 @@ void Solver::CheckObjCore() {
   output_.model = context_.model();
 }
 
-void Solver::CheckSatCore() {
-  DLINEAR_DEBUG("Solver::CheckSatCore");
+void SmtSolver::CheckSatCore() {
+  DLINEAR_DEBUG("SmtSolver::CheckSatCore");
   TimerGuard timer_guard{&output_.smt_solver_timer, true};
   const SatResult res = context_.CheckSat(&output_.actual_precision);
   if (res == SatResult::SAT_SATISFIABLE) {
@@ -122,9 +122,9 @@ void Solver::CheckSatCore() {
   }
   output_.model = context_.model();
 }
-std::string Solver::GetInfo(const std::string &key) const { return context_.GetInfo(key); }
-std::string Solver::GetOption(const std::string &key) const { return context_.GetOption(key); }
-SolverResult Solver::GetExpected() const {
+std::string SmtSolver::GetInfo(const std::string &key) const { return context_.GetInfo(key); }
+std::string SmtSolver::GetOption(const std::string &key) const { return context_.GetOption(key); }
+SolverResult SmtSolver::GetExpected() const {
   std::string status = context_.GetOption(":status");
   if (status == "sat") return SolverResult::SAT;
   if (status == "unsat") return SolverResult::UNSAT;

dlinear/solver/Solver.h → dlinear/solver/SmtSolver.h

@@ -1,13 +1,13 @@
 /**
- * @file Solver.h
+ * @file SmtSolver.h
  * @author dlinear (https://github.com/TendTo/dlinear)
  * @copyright 2024 dlinear
  * @licence Apache-2.0 license
- * @brief Solver interface class.
+ * @brief SmtSolver interface class.
  *
  * This class provides an easy interface for using the underling solver.
  * Once the correct configuration is set, the user can simply call
- * `Solver::CheckSat()` to get the result.
+ * `SmtSolver::CheckSat()` to get the result.
  * It will handle the parsing of the input.
  */
 #pragma once
@@ -17,41 +17,41 @@
 
 #include "dlinear/libs/gmp.h"
 #include "dlinear/solver/Context.h"
+#include "dlinear/solver/SmtSolverOutput.h"
 #include "dlinear/solver/SolverGuard.h"
-#include "dlinear/solver/SolverOutput.h"
 #include "dlinear/util/Config.h"
 
 namespace dlinear {
 
-class Solver {
+class SmtSolver {
  public:
-  Solver();
-  explicit Solver(const std::string &filename);
-  explicit Solver(Config config);
-  Solver(const Solver &) = delete;
-  Solver(Solver &&) = delete;
-  Solver &operator=(const Solver &) = delete;
-  Solver &operator=(Solver &&) = delete;
+  SmtSolver();
+  explicit SmtSolver(const std::string &filename);
+  explicit SmtSolver(Config config);
+  SmtSolver(const SmtSolver &) = delete;
+  SmtSolver(SmtSolver &&) = delete;
+  SmtSolver &operator=(const SmtSolver &) = delete;
+  SmtSolver &operator=(SmtSolver &&) = delete;
 
   [[nodiscard]] std::string GetInfo(const std::string &key) const;
   [[nodiscard]] std::string GetOption(const std::string &key) const;
   [[nodiscard]] SolverResult GetExpected() const;
 
   /**
    * Check the satisfiability of the current context.
-   * @return SolverOutput
+   * @return SmtSolverOutput
    */
-  SolverOutput CheckSat();
+  SmtSolverOutput CheckSat();
 
   void Visualize();
 
 #ifdef DLINEAR_PYDLINEAR
   /**
    * Enter the solver.
    * Allows to use the with statement in python.
-   * @return Solver reference
+   * @return SmtSolver reference
    */
-  Solver &Enter();
+  SmtSolver &Enter();
 
   /**
    * Cleanup the infinity values forcefully.
@@ -67,7 +67,7 @@ class Solver {
   const Config config_;  ///< Configuration of the solver.
   SolverGuard guard_;    ///< Takes care of initializing and de-initializing the correct infinity values.
   Context context_;      ///< Context obtained from the input file and passed to the SAT and SMT solvers.
-  SolverOutput output_;  ///< Output of the solver.
+  SmtSolverOutput output_;  ///< Output of the solver.
 
   bool ParseInput();
   bool ParseSmt2();

dlinear/solver/SolverOutput.cpp → dlinear/solver/SmtSolverOutput.cpp

@@ -1,10 +1,10 @@
 /**
- * @file SolverOutput.cpp
+ * @file SmtSolverOutput.cpp
  * @author dlinear (https://github.com/TendTo/dlinear)
  * @copyright 2024 dlinear
  * @licence Apache-2.0 license
  */
-#include "SolverOutput.h"
+#include "SmtSolverOutput.h"
 
 #include <spdlog/fmt/fmt.h>
 #include <spdlog/fmt/ostr.h>
@@ -18,11 +18,11 @@
 
 namespace dlinear {
 
-double SolverOutput::precision_upper_bound() const {
+double SmtSolverOutput::precision_upper_bound() const {
   return nextafter(actual_precision.get_d(), std::numeric_limits<double>::infinity());
 }
 
-std::string SolverOutput::ToString() const {
+std::string SmtSolverOutput::ToString() const {
   std::ostringstream oss;
   oss << *this;
   return oss.str();
@@ -57,7 +57,7 @@ std::ostream& operator<<(std::ostream& os, const SolverResult& bound) {
   }
 }
 
-std::ostream& operator<<(std::ostream& os, const SolverOutput& s) {
+std::ostream& operator<<(std::ostream& os, const SmtSolverOutput& s) {
   switch (s.result) {
     case SolverResult::UNSOLVED:
       return os << "unsolved";

dlinear/solver/SolverOutput.h → dlinear/solver/SmtSolverOutput.h

@@ -1,5 +1,5 @@
 /**
- * @file SolverOutput.h
+ * @file SmtSolverOutput.h
  * @author dlinear (https://github.com/TendTo/dlinear)
  * @copyright 2024 dlinear
  * @licence Apache-2.0 license
@@ -45,8 +45,8 @@ enum class SolverResult {
   ERROR,          // An error occurred.
 };
 
-struct SolverOutput {
-  explicit SolverOutput(mpq_class _precision, bool _produce_models = false, bool _with_timings = false)
+struct SmtSolverOutput {
+  explicit SmtSolverOutput(mpq_class _precision, bool _produce_models = false, bool _with_timings = false)
       : actual_precision{std::move(_precision)}, produce_models{_produce_models}, with_timings{_with_timings} {}
 
   [[nodiscard]] double precision_upper_bound() const;
@@ -70,6 +70,6 @@ struct SolverOutput {
 };
 
 std::ostream &operator<<(std::ostream &os, const SolverResult &result);
-std::ostream &operator<<(std::ostream &os, const SolverOutput &output);
+std::ostream &operator<<(std::ostream &os, const SmtSolverOutput &output);
 
 }  // namespace dlinear

pydlinear/pydlinear.cpp

@@ -16,8 +16,8 @@
 #include "dlinear/api/api.h"
 #include "dlinear/libs/gmp.h"
 #include "dlinear/libs/qsopt_ex.h"
-#include "dlinear/solver/Solver.h"
-#include "dlinear/solver/SolverOutput.h"
+#include "dlinear/solver/SmtSolver.h"
+#include "dlinear/solver/SmtSolverOutput.h"
 #include "dlinear/symbolic/symbolic.h"
 #include "dlinear/util/ArgParser.h"
 #include "dlinear/util/Box.h"
@@ -103,7 +103,7 @@ PYBIND11_MODULE(_pydlinear, m) {
   auto ConfigClass = py::class_<Config>(m, "Config");
   auto SolverClass = py::class_<Solver>(m, "Solver");
   auto ContextClass = py::class_<Context>(m, "Context");
-  auto SolverOutputClass = py::class_<SolverOutput>(m, "SolverOutput");
+  auto SolverOutputClass = py::class_<SmtSolverOutput>(m, "SmtSolverOutput");
   auto BoxClass = py::class_<Box>(m, "Box");
   auto BoxIntervalClass = py::class_<Box::Interval>(m, "Interval");
 
@@ -114,16 +114,16 @@ PYBIND11_MODULE(_pydlinear, m) {
       .def("__exit__", [](Solver &self, py::object, py::object, py::object) { self.Exit(); })
       .def("CheckSat", &Solver::CheckSat);
 
-  SolverOutputClass.def_property_readonly("result", &SolverOutput::m_result)
-      .def_property_readonly("actual_precision", &SolverOutput::m_actual_precision)
-      .def_property_readonly("lower_bound", &SolverOutput::m_lower_bound)
-      .def_property_readonly("upper_bound", &SolverOutput::m_upper_bound)
-      .def_property_readonly("model", &SolverOutput::m_model)
-      .def_property_readonly("with_timings", &SolverOutput::with_timings)
-      .def_property_readonly("produce_models", &SolverOutput::produce_models)
-      .def_property_readonly("n_assertions", &SolverOutput::n_assertions)
-      .def_property_readonly("is_sat", &SolverOutput::is_sat)
-      .def("__str__", [](const SolverOutput &self) { return (std::stringstream() << self).str(); });
+  SolverOutputClass.def_property_readonly("result", &SmtSolverOutput::m_result)
+      .def_property_readonly("actual_precision", &SmtSolverOutput::m_actual_precision)
+      .def_property_readonly("lower_bound", &SmtSolverOutput::m_lower_bound)
+      .def_property_readonly("upper_bound", &SmtSolverOutput::m_upper_bound)
+      .def_property_readonly("model", &SmtSolverOutput::m_model)
+      .def_property_readonly("with_timings", &SmtSolverOutput::with_timings)
+      .def_property_readonly("produce_models", &SmtSolverOutput::produce_models)
+      .def_property_readonly("n_assertions", &SmtSolverOutput::n_assertions)
+      .def_property_readonly("is_sat", &SmtSolverOutput::is_sat)
+      .def("__str__", [](const SmtSolverOutput &self) { return (std::stringstream() << self).str(); });
 
   ContextClass.def(py::init<>()).def(py::init<const Config &>());
 

test/solver/TestMps.cpp

@@ -12,13 +12,13 @@
 #include <memory>
 #include <string_view>
 
-#include "dlinear/solver/Solver.h"
+#include "dlinear/solver/SmtSolver.h"
 #include "test/solver/TestSolverUtils.h"
 
 using dlinear::Config;
 using dlinear::get_files;
-using dlinear::Solver;
-using dlinear::SolverOutput;
+using dlinear::SmtSolver;
+using dlinear::SmtSolver;
 using dlinear::SolverResult;
 using std::unique_ptr;
 
@@ -36,7 +36,7 @@ TEST_P(TestMps, MpsInputAgainstExpectedOutput) {
   config_.m_filename() = filename;
   config_.m_lp_solver() = lp_solver;
   config_.m_precision() = precision;
-  Solver s{config_};
+  SmtSolver s{config_};
   const SolverResult result = s.CheckSat().result;
   EXPECT_THAT(expected_results(s.GetExpected()), ::testing::Contains(result));
 }