From ace6e8eea107e93c5400caff92963c73e9ad4526 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Apr 2023 13:49:06 -0700 Subject: [PATCH] add gcd-conflicts stats, formatting updates --- src/smt/theory_arith.h | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 34a76d955..a2a7617e5 100644 --- a/src/smt/theory_arith.h +++ b/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 m_var_pos; // temporary array used in add_rows atoms m_atoms; // set of theory atoms ptr_vector m_asserted_bounds; // set of asserted bounds - unsigned m_asserted_qhead; + unsigned m_asserted_qhead = 0; ptr_vector m_new_atoms; // new bound atoms that have yet to be internalized. svector m_nl_monomials; // non linear monomials svector m_nl_propagated; // non linear monomials that became linear v_dependency_manager m_dep_manager; // for tracking bounds during non-linear reasoning vector 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 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 > 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 > 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 var2num_occs; var2num_occs m_var2num_occs;