diff --git a/dreal/api/test/api_test.cc b/dreal/api/test/api_test.cc index 611a34d9..8a1bdeaf 100644 --- a/dreal/api/test/api_test.cc +++ b/dreal/api/test/api_test.cc @@ -16,6 +16,7 @@ #include "dreal/api/api.h" #include + #include #include "dreal/solver/formula_evaluator.h" diff --git a/dreal/contractor/contractor_fixpoint.cc b/dreal/contractor/contractor_fixpoint.cc index 795f18c9..e4e5f35c 100644 --- a/dreal/contractor/contractor_fixpoint.cc +++ b/dreal/contractor/contractor_fixpoint.cc @@ -31,8 +31,7 @@ ContractorFixpoint::ContractorFixpoint(TerminationCondition term_cond, vector 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 index 683d8ee4..6e703d8d 100644 --- 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 index c16652cf..d9c990aa 100644 --- 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 index e2b12fbe..321ad128 100644 --- a/dreal/contractor/contractor_ibex_polytope.cc +++ b/dreal/contractor/contractor_ibex_polytope.cc @@ -36,8 +36,8 @@ namespace dreal { ContractorIbexPolytope::ContractorIbexPolytope(vector 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 index 59ac44f6..4ab66a83 100644 --- 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 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 index b40349e5..bb7927c3 100644 --- a/dreal/contractor/contractor_join.cc +++ b/dreal/contractor/contractor_join.cc @@ -27,8 +27,7 @@ namespace dreal { ContractorJoin::ContractorJoin(vector 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 index acae3e31..1e84e4eb 100644 --- a/dreal/contractor/contractor_seq.cc +++ b/dreal/contractor/contractor_seq.cc @@ -27,8 +27,7 @@ namespace dreal { ContractorSeq::ContractorSeq(vector 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 index 2328d29d..23509adb 100644 --- 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 index 0df443ae..9a30f894 100644 --- 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 #include +#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 index 0184bf34..8b7d183a 100644 --- 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 #include +#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 index dd9dba41..55cb057e 100644 --- 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 +#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 index 28f4ea29..31957870 100644 --- 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 #include +#include "dreal/examples/control.h" + namespace dreal { namespace { diff --git a/dreal/examples/synthesize_lyapunov_simple.cc b/dreal/examples/synthesize_lyapunov_simple.cc index b855d21a..b07be4be 100644 --- 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 +#include "dreal/examples/control.h" + namespace dreal { namespace { diff --git a/dreal/examples/verify_nn.cc b/dreal/examples/verify_nn.cc index dc3da9cb..2cae8e78 100644 --- 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 #include #include #include #include +#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 index fc668a08..263c03af 100644 --- 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 +#include "pybind11/pybind11.h" + #include "dreal/symbolic/symbolic.h" namespace dreal { diff --git a/dreal/smt2/scanner.h b/dreal/smt2/scanner.h index 99cb54ba..944494f2 100644 --- 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 index 3ab799d1..eb154738 100644 --- 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 #include #include +#include "dreal/solver/context.h" #include "dreal/symbolic/symbolic.h" namespace dreal { diff --git a/dreal/util/exception.h b/dreal/util/exception.h index 3f010de7..4070ccfe 100644 --- a/dreal/util/exception.h +++ b/dreal/util/exception.h @@ -15,10 +15,10 @@ */ #pragma once -#include - #include +#include + 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 index bff0d8f9..a3f2f324 100644 --- 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 index 1fbde6c5..18f7b255 100644 --- 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 index d1973a24..48ac28b6 100644 --- a/test/cds_test.cc +++ b/test/cds_test.cc @@ -18,11 +18,10 @@ #include #include -#include - #include #include // for cds::HP (Hazard Pointer) SMR #include // for cds::Initialize and cds::Terminate +#include using std::for_each; using std::mem_fn; diff --git a/test/ibex_bitset_test.cc b/test/ibex_bitset_test.cc index c9747c12..4f86ce43 100644 --- 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 #include +#include "./ibex.h" + namespace { GTEST_TEST(IbexBitsetTest, Add) { diff --git a/test/spdlog_test.cc b/test/spdlog_test.cc index b7ec525e..10be0fd7 100644 --- 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 + #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 new file mode 100644 index 00000000..47a38a93 --- /dev/null +++ b/third_party/.clang-format @@ -0,0 +1,2 @@ +DisableFormat: true +SortIncludes: Never