add gcd-conflicts stats, formatting updates

src/smt/theory_arith.h

@@ -41,7 +41,7 @@ Revision History:
 namespace smt {
 
     struct theory_arith_stats {
-        unsigned m_conflicts, m_add_rows, m_pivots, m_diseq_cs, m_gomory_cuts, m_branches, m_gcd_tests, m_patches, m_patches_succ;
+        unsigned m_conflicts, m_add_rows, m_pivots, m_diseq_cs, m_gomory_cuts, m_branches, m_gcd_tests, m_gcd_conflicts, m_patches, m_patches_succ;
         unsigned m_assert_lower, m_assert_upper, m_assert_diseq, m_core2th_eqs, m_core2th_diseqs;
         unsigned m_th2core_eqs, m_th2core_diseqs, m_bound_props, m_offset_eqs, m_fixed_eqs, m_offline_eqs;
         unsigned m_max_min; 
@@ -452,18 +452,18 @@ namespace smt {
         svector<int>            m_var_pos;          // temporary array used in add_rows
         atoms                   m_atoms;            // set of theory atoms
         ptr_vector<bound>       m_asserted_bounds;  // set of asserted bounds
-        unsigned                m_asserted_qhead;   
+        unsigned                m_asserted_qhead = 0;   
         ptr_vector<atom>        m_new_atoms;        // new bound atoms that have yet to be internalized.
         svector<theory_var>     m_nl_monomials;     // non linear monomials
         svector<theory_var>     m_nl_propagated;    // non linear monomials that became linear
         v_dependency_manager    m_dep_manager;      // for tracking bounds during non-linear reasoning
 
         vector<uint_set>        m_row_vars;         // variables in a given row. Used during internalization to detect repeated variables.
-        unsigned                m_row_vars_top;
+        unsigned                m_row_vars_top = 0;
 
         var_heap                m_to_patch;         // heap containing all variables v s.t. m_value[v] does not satisfy bounds of v.
         nat_set                 m_left_basis;       // temporary: set of variables that already left the basis in make_feasible
-        bool                    m_blands_rule;
+        bool                    m_blands_rule = false;
 
         svector<unsigned>       m_update_trail_stack;    // temporary trail stack used to restore the last feasible assignment.
         nat_set                 m_in_update_trail_stack; // set of variables in m_update_trail_stack
@@ -473,11 +473,11 @@ namespace smt {
 
         inf_numeral             m_tmp;
         random_gen              m_random;
-        unsigned                m_num_conflicts;
+        unsigned                m_num_conflicts = 0;
 
-        unsigned                m_branch_cut_counter;
+        unsigned                m_branch_cut_counter = 0;
         bool                    m_eager_gcd; // true if gcd should be applied at every add_row
-        unsigned                m_final_check_idx;
+        unsigned                m_final_check_idx = 0;
 
 
         // backtracking
@@ -676,7 +676,7 @@ namespace smt {
 
            See also m_changed_assignment flag.
         */
-        bool    m_liberal_final_check; 
+        bool    m_liberal_final_check = true; 
         final_check_status final_check_core();
         final_check_status final_check_eh() override;
 
@@ -734,7 +734,7 @@ namespace smt {
         // Assignment management
         //
         // -----------------------------------
-        bool m_changed_assignment; //!< auxiliary variable set to true when the assignment is changed.
+        bool m_changed_assignment = false; //!< auxiliary variable set to true when the assignment is changed.
         void save_value(theory_var v);
         void discard_update_trail();
         void restore_assignment();
@@ -790,11 +790,12 @@ namespace smt {
         void mark_row_for_bound_prop(unsigned r1);
         void mark_rows_for_bound_prop(theory_var v);
         void is_row_useful_for_bound_prop(row const & r, int & lower_idx, int & upper_idx) const;
-        void imply_bound_for_monomial(row const & r, int idx, bool lower);
-        void imply_bound_for_all_monomials(row const & r, bool lower);
+        unsigned imply_bound_for_monomial(row const & r, int idx, bool lower);
+        unsigned imply_bound_for_all_monomials(row const & r, bool lower);
         void explain_bound(row const & r, int idx, bool lower, inf_numeral & delta, 
                            antecedents & antecedents);
-        void mk_implied_bound(row const & r, unsigned idx, bool lower, theory_var v, bound_kind kind, inf_numeral const & k);
+        bool m_validating = false;
+        unsigned mk_implied_bound(row const & r, unsigned idx, bool lower, theory_var v, bound_kind kind, inf_numeral const & k);
         void assign_bound_literal(literal l, row const & r, unsigned idx, bool lower, inf_numeral & delta);
         void propagate_bounds();
 
@@ -821,7 +822,7 @@ namespace smt {
         var_set         m_tmp_var_set;
         var_set         m_tmp_var_set2;
         svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates;
-        unsigned                                          m_assume_eq_head;
+        unsigned                                          m_assume_eq_head = 0;
         bool random_update(theory_var v);
         void mutate_assignment();
         bool assume_eqs_core();
@@ -953,10 +954,10 @@ namespace smt {
         //
         // -----------------------------------
         typedef int_hashtable<int_hash, default_eq<int> > row_set;
-        bool            m_model_depends_on_computed_epsilon;
-        unsigned        m_nl_rounds;
-        bool            m_nl_gb_exhausted;
-        unsigned        m_nl_strategy_idx; // for fairness
+        bool            m_model_depends_on_computed_epsilon = false;
+        unsigned        m_nl_rounds = 0;
+        bool            m_nl_gb_exhausted = false;
+        unsigned        m_nl_strategy_idx = 0; // for fairness
         expr_ref_vector m_nl_new_exprs;
         typedef obj_map<expr, unsigned> var2num_occs;
         var2num_occs m_var2num_occs;