dreal · mrdomino · Jun 1, 2024 · Jun 1, 2024
diff --git a/dreal/api/test/api_test.cc b/dreal/api/test/api_test.cc
@@ -16,6 +16,7 @@
 #include "dreal/api/api.h"
 
 #include <cmath>
+
 #include <gtest/gtest.h>
 
 #include "dreal/solver/formula_evaluator.h"

diff --git a/dreal/contractor/contractor_fixpoint.cc b/dreal/contractor/contractor_fixpoint.cc
@@ -31,8 +31,7 @@ ContractorFixpoint::ContractorFixpoint(TerminationCondition term_cond,
                                        vector<Contractor> contractors,
                                        const Config& config)
     : ContractorCell{Contractor::Kind::FIXPOINT,
-                     DynamicBitset(ComputeInputSize(contractors)),
-                     config},
+                     DynamicBitset(ComputeInputSize(contractors)), config},
       term_cond_{std::move(term_cond)},
       contractors_{std::move(contractors)} {
   DREAL_ASSERT(!contractors_.empty());

diff --git a/dreal/contractor/contractor_forall.h b/dreal/contractor/contractor_forall.h
@@ -74,8 +74,8 @@ class ContractorForall : public ContractorCell {
   /// @pre 0.0 < inner_delta < epsilon < config.precision().
   ContractorForall(Formula f, const Box& box, double epsilon,
                    double inner_delta, const Config& config)
-      : ContractorCell{Contractor::Kind::FORALL,
-                       DynamicBitset(box.size()), config},
+      : ContractorCell{Contractor::Kind::FORALL, DynamicBitset(box.size()),
+                       config},
         f_{std::move(f)},
         quantified_variables_{get_quantified_variables(f_)},
         strengthend_negated_nested_f_{Nnfizer{}.Convert(
@@ -264,8 +264,8 @@ class ContractorForallMt : public ContractorCell {
   /// Constructs ForallMt contractor using @p f and @p box.
   ContractorForallMt(Formula f, const Box& box, double epsilon,
                      double inner_delta, const Config& config)
-      : ContractorCell{Contractor::Kind::FORALL,
-                       DynamicBitset(box.size()), config},
+      : ContractorCell{Contractor::Kind::FORALL, DynamicBitset(box.size()),
+                       config},
         f_{std::move(f)},
         epsilon_{epsilon},
         inner_delta_{inner_delta},

diff --git a/dreal/contractor/contractor_ibex_fwdbwd_mt.cc b/dreal/contractor/contractor_ibex_fwdbwd_mt.cc
@@ -29,8 +29,8 @@ namespace dreal {
 
 ContractorIbexFwdbwdMt::ContractorIbexFwdbwdMt(Formula f, const Box& box,
                                                const Config& config)
-    : ContractorCell{Contractor::Kind::IBEX_FWDBWD,
-                     DynamicBitset(box.size()), config},
+    : ContractorCell{Contractor::Kind::IBEX_FWDBWD, DynamicBitset(box.size()),
+                     config},
       f_{std::move(f)},
       config_{config},
       ctc_ready_(config_.number_of_jobs(), 0),

diff --git a/dreal/contractor/contractor_ibex_polytope.cc b/dreal/contractor/contractor_ibex_polytope.cc
@@ -36,8 +36,8 @@ namespace dreal {
 ContractorIbexPolytope::ContractorIbexPolytope(vector<Formula> formulas,
                                                const Box& box,
                                                const Config& config)
-    : ContractorCell{Contractor::Kind::IBEX_POLYTOPE,
-                     DynamicBitset(box.size()), config},
+    : ContractorCell{Contractor::Kind::IBEX_POLYTOPE, DynamicBitset(box.size()),
+                     config},
       formulas_{std::move(formulas)},
       ibex_converter_{box} {
   DREAL_LOG_DEBUG("ContractorIbexPolytope::ContractorIbexPolytope");

diff --git a/dreal/contractor/contractor_ibex_polytope_mt.cc b/dreal/contractor/contractor_ibex_polytope_mt.cc
@@ -32,8 +32,8 @@ namespace dreal {
 ContractorIbexPolytopeMt::ContractorIbexPolytopeMt(vector<Formula> formulas,
                                                    const Box& box,
                                                    const Config& config)
-    : ContractorCell{Contractor::Kind::IBEX_POLYTOPE,
-                     DynamicBitset(box.size()), config},
+    : ContractorCell{Contractor::Kind::IBEX_POLYTOPE, DynamicBitset(box.size()),
+                     config},
       formulas_{std::move(formulas)},
       config_{config},
       ctc_ready_(config_.number_of_jobs(), 0),

diff --git a/dreal/contractor/contractor_join.cc b/dreal/contractor/contractor_join.cc
@@ -27,8 +27,7 @@ namespace dreal {
 ContractorJoin::ContractorJoin(vector<Contractor> contractors,
                                const Config& config)
     : ContractorCell{Contractor::Kind::JOIN,
-                     DynamicBitset(ComputeInputSize(contractors)),
-                     config},
+                     DynamicBitset(ComputeInputSize(contractors)), config},
       contractors_{std::move(contractors)} {
   DREAL_ASSERT(!contractors_.empty());
   DynamicBitset& input{mutable_input()};

diff --git a/dreal/contractor/contractor_seq.cc b/dreal/contractor/contractor_seq.cc
@@ -27,8 +27,7 @@ namespace dreal {
 ContractorSeq::ContractorSeq(vector<Contractor> contractors,
                              const Config& config)
     : ContractorCell{Contractor::Kind::SEQ,
-                     DynamicBitset(ComputeInputSize(contractors)),
-                     config},
+                     DynamicBitset(ComputeInputSize(contractors)), config},
       contractors_{std::move(contractors)} {
   DREAL_ASSERT(!contractors_.empty());
   DynamicBitset& input{mutable_input()};

diff --git a/dreal/dr/scanner.h b/dreal/dr/scanner.h
@@ -34,9 +34,8 @@
 
 // The following include should come first before parser.yy.hh.
 // Do not alpha-sort them.
-#include "dreal/symbolic/symbolic.h"
-
 #include "dreal/dr/parser.yy.hh"
+#include "dreal/symbolic/symbolic.h"
 
 namespace dreal {
 

diff --git a/dreal/examples/synthesize_lyapunov_damped_mathieu.cc b/dreal/examples/synthesize_lyapunov_damped_mathieu.cc
@@ -13,11 +13,10 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/examples/control.h"
-
 #include <iostream>
 #include <vector>
 
+#include "dreal/examples/control.h"
 #include "dreal/util/logging.h"
 
 namespace dreal {

diff --git a/dreal/examples/synthesize_lyapunov_moore_greitzer.cc b/dreal/examples/synthesize_lyapunov_moore_greitzer.cc
@@ -13,11 +13,11 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/examples/control.h"
-
 #include <iostream>
 #include <vector>
 
+#include "dreal/examples/control.h"
+
 namespace dreal {
 namespace {
 

diff --git a/dreal/examples/synthesize_lyapunov_normalized_pendulum.cc b/dreal/examples/synthesize_lyapunov_normalized_pendulum.cc
@@ -13,10 +13,10 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/examples/control.h"
-
 #include <iostream>
 
+#include "dreal/examples/control.h"
+
 namespace dreal {
 namespace {
 

diff --git a/dreal/examples/synthesize_lyapunov_power_train.cc b/dreal/examples/synthesize_lyapunov_power_train.cc
@@ -13,11 +13,11 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/examples/control.h"
-
 #include <iostream>
 #include <vector>
 
+#include "dreal/examples/control.h"
+
 namespace dreal {
 namespace {
 

diff --git a/dreal/examples/synthesize_lyapunov_simple.cc b/dreal/examples/synthesize_lyapunov_simple.cc
@@ -13,10 +13,10 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/examples/control.h"
-
 #include <iostream>
 
+#include "dreal/examples/control.h"
+
 namespace dreal {
 namespace {
 

diff --git a/dreal/examples/verify_nn.cc b/dreal/examples/verify_nn.cc
@@ -13,14 +13,14 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/api/api.h"
-
 #include <cassert>
 #include <ostream>
 #include <random>
 #include <string>
 #include <vector>
 
+#include "dreal/api/api.h"
+
 using dreal::Config;
 using dreal::Expression;
 using dreal::Formula;

diff --git a/dreal/odr_test_module_py.cc b/dreal/odr_test_module_py.cc
@@ -13,10 +13,10 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "pybind11/pybind11.h"
-
 #include <string>
 
+#include "pybind11/pybind11.h"
+
 #include "dreal/symbolic/symbolic.h"
 
 namespace dreal {

diff --git a/dreal/smt2/scanner.h b/dreal/smt2/scanner.h
@@ -34,14 +34,13 @@
 
 // The following include should come first before parser.yy.hh.
 // Do not alpha-sort them.
+#include "dreal/smt2/parser.yy.hh"
 #include "dreal/smt2/sort.h"
 #include "dreal/smt2/term.h"
 #include "dreal/symbolic/symbolic.h"
 #include "dreal/util/box.h"
 #include "dreal/util/string_to_interval.h"
 
-#include "dreal/smt2/parser.yy.hh"
-
 namespace dreal {
 
 /** Smt2Scanner is a derived class to add some extra function to the scanner

diff --git a/dreal/solver/test/jorge_test.cc b/dreal/solver/test/jorge_test.cc
@@ -13,13 +13,12 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "dreal/solver/context.h"
-
 #include <iostream>
 #include <vector>
 
 #include <gtest/gtest.h>
 
+#include "dreal/solver/context.h"
 #include "dreal/symbolic/symbolic.h"
 
 namespace dreal {

diff --git a/dreal/util/exception.h b/dreal/util/exception.h
@@ -15,10 +15,10 @@
 */
 #pragma once
 
-#include <fmt/format.h>
-
 #include <stdexcept>
 
+#include <fmt/format.h>
+
 namespace dreal {
 
 #define DREAL_RUNTIME_ERROR(...)                                 \

diff --git a/dreal/util/test/if_then_else_eliminator_test.cc b/dreal/util/test/if_then_else_eliminator_test.cc
@@ -94,8 +94,7 @@ TEST_F(IfThenElseEliminatorTest, ITEs) {
   ASSERT_FALSE(ite_elim.variables().empty());
   ASSERT_EQ(ite_elim.variables().size(), 1);
   const Variable& ite_var{*(ite_elim.variables().begin())};
-  const Formula expected{ite_var == z_ &&
-                         (!(x_ > y_) || ite_var == x_ + 1.0) &&
+  const Formula expected{ite_var == z_ && (!(x_ > y_) || ite_var == x_ + 1.0) &&
                          (x_ > y_ || ite_var == y_ + 1.0)};
   EXPECT_PRED2(FormulaNotEqual, f, converted);
   EXPECT_PRED2(FormulaEqual, converted, expected);

diff --git a/dreal/util/timer.h b/dreal/util/timer.h
@@ -79,7 +79,6 @@ class TimerGuard {
   TimerGuard& operator=(const TimerGuard&) = delete;
   TimerGuard& operator=(TimerGuard&&) = delete;
 
-
   /// Destructs the timer guard object. It pauses the embedded timer object.
   ~TimerGuard();
 

diff --git a/test/cds_test.cc b/test/cds_test.cc
@@ -18,11 +18,10 @@
 #include <thread>
 #include <vector>
 
-#include <gtest/gtest.h>
-
 #include <cds/container/treiber_stack.h>
 #include <cds/gc/hp.h>  // for cds::HP (Hazard Pointer) SMR
 #include <cds/init.h>   // for cds::Initialize and cds::Terminate
+#include <gtest/gtest.h>
 
 using std::for_each;
 using std::mem_fn;

diff --git a/test/ibex_bitset_test.cc b/test/ibex_bitset_test.cc
@@ -13,12 +13,12 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 */
-#include "./ibex.h"
-
 #include <iostream>
 
 #include <gtest/gtest.h>
 
+#include "./ibex.h"
+
 namespace {
 
 GTEST_TEST(IbexBitsetTest, Add) {

diff --git a/test/spdlog_test.cc b/test/spdlog_test.cc
@@ -15,7 +15,9 @@
 */
 // From https://github.com/gabime/spdlog/wiki/1.-QuickStart
 #include "spdlog/spdlog.h"
+
 #include <iostream>
+
 #include "spdlog/sinks/basic_file_sink.h"
 #include "spdlog/sinks/rotating_file_sink.h"
 #include "spdlog/sinks/stdout_color_sinks.h"

diff --git a/third_party/.clang-format b/third_party/.clang-format
@@ -0,0 +1,2 @@
+DisableFormat: true
+SortIncludes: Never