Merge branch 'master' of https://github.com/z3prover/z3

src/math/lp/bound_analyzer_on_row.h

@@ -19,6 +19,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/vector.h"

src/math/lp/column_info.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"

src/math/lp/column_namer.h

@@ -18,6 +18,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <string>
 #include "math/lp/static_matrix.h"
 namespace lp {

src/math/lp/core_solver_pretty_printer.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include "math/lp/numeric_pair.h"
 #include "math/lp/core_solver_pretty_printer_def.h"
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);

src/math/lp/core_solver_pretty_printer.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include <limits>
 #include <string>

src/math/lp/core_solver_pretty_printer_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <limits>

src/math/lp/cross_nested.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include <functional>
 #include "math/lp/nex.h"

src/math/lp/dense_matrix.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include "math/lp/lp_settings.h"
 #include "math/lp/dense_matrix_def.h"
 #ifdef Z3DEBUG

src/math/lp/dense_matrix.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #ifdef Z3DEBUG
 #include "util/vector.h"

src/math/lp/dense_matrix_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/lp_settings.h"

src/math/lp/emonics.cpp

@@ -18,6 +18,7 @@
   replaced rooted_mons.h and rooted_mon, rooted_mon_tabled
 
 --*/
+// clang-format off
 
 #include "math/lp/emonics.h"
 #include "math/lp/nla_defs.h"

src/math/lp/emonics.h

@@ -18,6 +18,7 @@
     to replace rooted_mons.h and rooted_mon, rooted_mon_tabled
 
   --*/
+// clang-format off
 
 #pragma once
 #include "math/lp/lp_utils.h"

src/math/lp/explanation.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/lp_utils.h"
 #include "util/map.h"

src/math/lp/factorization.h

@@ -18,6 +18,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include "util/rational.h"
 #include "math/lp/monic.h"

src/math/lp/factorization_factory_imp.cpp

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #include "math/lp/factorization_factory_imp.h"
 #include "math/lp/nla_core.h"
 namespace nla {

src/math/lp/factorization_factory_imp.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include "math/lp/factorization.h"
 namespace nla {

src/math/lp/general_matrix.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include <functional>
 namespace lp {

src/math/lp/hnf.h

@@ -26,6 +26,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/numeric_pair.h"
 #include "util/ext_gcd.h"

src/math/lp/hnf_cutter.cpp

@@ -9,6 +9,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/hnf_cutter.h"

src/math/lp/hnf_cutter.h

@@ -14,6 +14,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 
 #pragma once
 #include "math/lp/lar_term.h"

src/math/lp/horner.cpp

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 
 #include "math/lp/horner.h"
 #include "math/lp/nla_core.h"

src/math/lp/horner.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/nla_common.h"

src/math/lp/implied_bound.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/lp_settings.h"
 #include "math/lp/lar_constraints.h"

src/math/lp/incremental_vector.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"

src/math/lp/indexed_value.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 namespace lp {

src/math/lp/indexed_vector.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include "util/vector.h"
 #include "math/lp/indexed_vector_def.h"
 namespace lp {

src/math/lp/indexed_vector.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"

src/math/lp/indexed_vector_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/vector.h"

src/math/lp/int_branch.h

@@ -15,6 +15,7 @@ Author:
 
 Revision History:
 --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/lar_solver.h"

src/math/lp/int_cube.cpp

@@ -15,6 +15,7 @@ Author:
 
 Revision History:
 --*/
+// clang-format off
 
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"

src/math/lp/int_cube.h

@@ -19,6 +19,7 @@ Author:
 
 Revision History:
 --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/lia_move.h"

src/math/lp/int_gcd_test.cpp

@@ -45,6 +45,7 @@ Accumulative:
  
 
 --*/
+// clang-format off
 
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"

src/math/lp/int_gcd_test.h

@@ -24,6 +24,7 @@ Author:
 
 Revision History:
 --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/lia_move.h"

src/math/lp/lar_constraints.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include <utility>

src/math/lp/lar_core_solver.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <utility>
 #include <memory>
 #include <string>

src/math/lp/lar_core_solver.h

@@ -5,6 +5,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <string>
@@ -16,7 +17,7 @@ Author:
 #include "math/lp/stacked_vector.h"
 #include "util/stacked_value.h"
 namespace lp {
-
+// clang-format off
 class lar_core_solver  {
     vector<std::pair<mpq, unsigned>> m_infeasible_linear_combination;
     int m_infeasible_sum_sign; // todo: get rid of this field

src/math/lp/lar_core_solver_def.h

@@ -9,6 +9,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <string>

src/math/lp/lar_solver.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include <algorithm>
 #include <functional>

src/math/lp/lar_term.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include "math/lp/indexed_vector.h"
 #include "util/map.h"

src/math/lp/lia_move.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 namespace lp {
 enum class lia_move {

src/math/lp/lp_api.h

@@ -7,6 +7,7 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/inf_rational.h"

src/math/lp/lp_core_solver_base.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <utility>
 #include <memory>
 #include <string>

src/math/lp/lp_core_solver_base.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include <set>
 #include "util/vector.h"

src/math/lp/lp_core_solver_base_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <set>

src/math/lp/lp_primal_core_solver.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <utility>
 #include <memory>
 #include <string>

src/math/lp/lp_primal_core_solver.h

@@ -159,7 +159,7 @@ namespace lp {
     }
     return r;
   }
-    // clang-format on
+    // clang-format off
     int find_beneficial_entering_in_row_tableau_rows_bland_mode(int i, T &a_ent) {
         int j = -1;
         unsigned bj = this->m_basis[i];

src/math/lp/lp_primal_core_solver_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <list>

src/math/lp/lp_primal_core_solver_tableau_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 // this is a part of lp_primal_core_solver that deals with the tableau

src/math/lp/lp_settings.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include "smt/params/smt_params_helper.hpp"

src/math/lp/lp_settings.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"

src/math/lp/lp_settings_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <cmath>

src/math/lp/lp_types.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <sstream>

src/math/lp/lp_utils.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include <string>
 #include "math/lp/numeric_pair.h"

src/math/lp/matrix.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include "math/lp/lp_settings.h"
 #include "math/lp/matrix_def.h"
 #include "math/lp/static_matrix.h"

src/math/lp/matrix.h

@@ -6,6 +6,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/numeric_pair.h"
 #include "util/vector.h"

src/math/lp/matrix_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <cmath>

src/math/lp/monomial_bounds.cpp

@@ -6,6 +6,7 @@
   Lev Nachmanson (levnach)
 
   --*/
+// clang-format off
 
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_core.h"

src/math/lp/monomial_bounds.h

@@ -6,6 +6,7 @@
   Lev Nachmanson (levnach)
 
   --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/nla_common.h"

src/math/lp/nex.h

@@ -4,6 +4,7 @@
   Author:
     Lev Nachmanson (levnach)
 --*/
+// clang-format off
 
 #pragma once
 #include <initializer_list>

src/math/lp/nex_creator.cpp

@@ -4,6 +4,7 @@
   Author:
    Lev Nachmanson (levnach)
   --*/
+// clang-format off
 #include "util/lbool.h"
 #include "math/lp/nex_creator.h"
 #include <map>

src/math/lp/nex_creator.h

@@ -5,6 +5,7 @@
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
   --*/
+// clang-format off
 #pragma once
 #include <map>
 #include <set>

src/math/lp/nla_basics_lemmas.cpp

@@ -6,6 +6,7 @@
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 
 #include "math/lp/nla_basics_lemmas.h"
 #include "math/lp/nla_core.h"

src/math/lp/nla_basics_lemmas.h

@@ -6,6 +6,7 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
+// clang-format off
 #pragma once
 #include "math/lp/monic.h"    
 #include "math/lp/factorization.h"    

src/math/lp/nla_common.cpp

@@ -6,6 +6,7 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
+// clang-format off
 #include "math/lp/nla_common.h"
 #include "math/lp/nla_core.h"
 

src/math/lp/nla_common.h

@@ -6,6 +6,7 @@
    Nikolaj Bjorner (nbjorner)
 
   --*/
+// clang-format off
 #pragma once
 #include "util/rational.h"
 #include "math/lp/nla_defs.h"

src/math/lp/nla_core.cpp

@@ -10,6 +10,7 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"

src/math/lp/nla_core.h

@@ -10,6 +10,7 @@
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/factorization.h"
 #include "math/lp/lp_types.h"

src/math/lp/nla_defs.h

@@ -8,6 +8,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include "math/lp/lp_types.h"
 #include "math/lp/column_info.h"

src/math/lp/nla_divisions.cpp

@@ -14,6 +14,7 @@ Description:
   Check divisions
 
 --*/
+// clang-format off
 #include "math/lp/nla_core.h"
 
 namespace nla {

src/math/lp/nla_divisions.h

@@ -13,6 +13,7 @@ Description:
   Check division constraints.
   
 --*/
+// clang-format off
 
 #include "math/lp/nla_types.h"
 

src/math/lp/nla_grobner.cpp

@@ -10,6 +10,7 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"

src/math/lp/nla_grobner.h

@@ -6,6 +6,7 @@
   Lev Nachmanson (levnach)
 
   --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/nla_common.h"

src/math/lp/nla_intervals.h

@@ -6,6 +6,7 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
+// clang-format off
 #pragma once
 #include "util/dependency.h"
 #include "util/region.h"

src/math/lp/nla_monotone_lemmas.cpp

@@ -5,6 +5,7 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
+// clang-format off
 #include "math/lp/nla_basics_lemmas.h"
 #include "math/lp/nla_core.h"
 namespace nla {

src/math/lp/nla_monotone_lemmas.h

@@ -5,6 +5,7 @@
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
   --*/
+// clang-format off
 #pragma once
 namespace nla {
 class core;

src/math/lp/nla_order_lemmas.cpp

@@ -5,6 +5,7 @@
     Nikolaj Bjorner (nbjorner)
     Lev Nachmanson (levnach)
   --*/
+// clang-format off
 
 #include "math/lp/nla_order_lemmas.h"
 #include "math/lp/nla_core.h"

src/math/lp/nla_order_lemmas.h

@@ -6,6 +6,7 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
+// clang-format off
 #pragma once
 #include "math/lp/factorization.h"
 #include "math/lp/nla_common.h"

src/math/lp/nla_powers.cpp

@@ -74,6 +74,7 @@ am().set(yval, am_value(y));
 am().set(rval, am_value(r));
 
 --*/
+// clang-format off
 #include "math/lp/nla_core.h"
 
 namespace nla {

src/math/lp/nla_powers.h

@@ -13,6 +13,7 @@ Description:
   Refines bounds on powers.
   
 --*/
+// clang-format off
 
 #include "math/lp/nla_types.h"
 

src/math/lp/nla_settings.h

@@ -6,6 +6,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 
 #pragma once
 namespace nla {

src/math/lp/nla_solver.cpp

@@ -5,6 +5,7 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
+// clang-format off
 #include "math/lp/nla_solver.h"
 #include <map>
 #include "math/lp/monic.h"

src/math/lp/nla_solver.h

@@ -6,6 +6,7 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 #pragma once
 #include "util/vector.h"
 #include "math/lp/lp_settings.h"

src/math/lp/nla_tangent_lemmas.cpp

@@ -6,6 +6,7 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
+// clang-format off
 #include "math/lp/nla_tangent_lemmas.h"
 #include "math/lp/nla_core.h"
 

src/math/lp/nla_tangent_lemmas.h

@@ -5,6 +5,7 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
+// clang-format off
 #pragma once
 #include "util/rational.h"
 #include "math/lp/factorization.h"

src/math/lp/nla_types.h

@@ -13,6 +13,7 @@ Description:
   Types used for nla solver.
   
 --*/
+// clang-format off
 
 #pragma once
 

src/math/lp/numeric_pair.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #define lp_for_z3
 #include <string>

src/math/lp/permutation_matrix.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include "math/lp/permutation_matrix_def.h"

src/math/lp/permutation_matrix.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <algorithm>

src/math/lp/permutation_matrix_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/vector.h"

src/math/lp/random_updater.cpp

@@ -17,5 +17,6 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include "math/lp/random_updater_def.h"
 

src/math/lp/random_updater.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include <set>

src/math/lp/random_updater_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/random_updater.h"

src/math/lp/stacked_vector.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"

src/math/lp/static_matrix.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include <set>
@@ -29,7 +30,6 @@ namespace lp {
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain();
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain();
 template void static_matrix<mpq, mpq>::add_column_to_vector(mpq const&, unsigned int, mpq*) const;
-template void static_matrix<mpq, mpq>::add_columns_at_the_end(unsigned int);
 template bool static_matrix<mpq, mpq>::is_correct() const;
 
 template mpq static_matrix<mpq, mpq>::get_balance() const;

src/math/lp/static_matrix.h

@@ -6,6 +6,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"
@@ -126,7 +127,6 @@ public:
 
     unsigned lowest_row_in_column(unsigned col);
 
-    void add_columns_at_the_end(unsigned delta);
     void add_new_element(unsigned i, unsigned j, const T & v);
 
     void add_row() {m_rows.push_back(row_strip<T>());}

src/math/lp/static_matrix_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/vector.h"
@@ -124,11 +125,6 @@ template <typename T, typename X> unsigned static_matrix<T, X>::lowest_row_in_co
     return ret;
 }
 
-template <typename T, typename X> void static_matrix<T, X>::add_columns_at_the_end(unsigned delta) {
-    for (unsigned i = 0; i < delta; i++)
-        add_column();
-}
-
 template <typename T, typename X> void static_matrix<T, X>::forget_last_columns(unsigned how_many_to_forget) {
     lp_assert(m_columns.size() >= how_many_to_forget);
     unsigned j = column_count() - 1;

src/math/lp/test_bound_analyzer.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #if 0
 #pragma once
 #include "util/vector.h"

src/math/lp/u_set.h

@@ -18,6 +18,7 @@ Revision History:
 TBD use indexed_uint_set from src/util/uint_set.h, 
 
 --*/
+// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <ostream>

src/math/lp/ul_pair.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"

src/math/lp/var_eqs.h

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 
 #pragma once
 #include "util/union_find.h"