diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 638c83642..93dc419d8 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -1653,12 +1653,12 @@ namespace polynomial { } void manager::factors::display(std::ostream & out) const { - out << m().m().to_string(get_constant()); - for (unsigned i = 0; i < m_factors.size(); ++ i) { - out << " * ("; - m_manager.display(out, m_factors[i]); - out << ")^" << m_degrees[i]; - } + out << m().m().to_string(get_constant()); + for (unsigned i = 0; i < m_factors.size(); ++ i) { + out << " * ("; + m_manager.display(out, m_factors[i]); + out << ")^" << m_degrees[i]; + } } void manager::factors::set_constant(numeral const & constant) { diff --git a/src/math/polynomial/polynomial_factorization.cpp b/src/math/polynomial/polynomial_factorization.cpp index 220048a9a..4bf227d44 100644 --- a/src/math/polynomial/polynomial_factorization.cpp +++ b/src/math/polynomial/polynomial_factorization.cpp @@ -172,8 +172,8 @@ void multivariate_factor_coefficient_bound(polynomial_ref const & f, var x, nume // check that A*S+B*T=C in zp mod ideal bool check_solve(zp_manager & zp_pm, var2degree const & ideal, - zp_polynomial_ref const & A, zp_polynomial_ref const & B, zp_polynomial_ref const & C, - zp_polynomial_ref const & S, zp_polynomial_ref const & T) { + zp_polynomial_ref const & A, zp_polynomial_ref const & B, zp_polynomial_ref const & C, + zp_polynomial_ref const & S, zp_polynomial_ref const & T) { zp_polynomial_ref AS(zp_pm), BT(zp_pm), sum(zp_pm); AS = zp_pm.mul(A, S); AS = zp_pm.mod_d(AS, ideal); BT = zp_pm.mul(B, T); BT = zp_pm.mod_d(BT, ideal); @@ -266,7 +266,7 @@ void solve(zp_manager & zp_pm, var x, var2degree const & ideal, * all polynomials in Z_p[x, ..., y] mod (..., y^d) */ void multivariate_hansel_lift_ideal( - zp_manager & zp_pm, var x, + zp_manager & zp_pm, var x, zp_polynomial_ref const & C, zp_polynomial_ref & A, zp_polynomial_ref & U, zp_polynomial_ref & B, zp_polynomial_ref & V, var2degree & ideal, var y, unsigned d) { @@ -333,7 +333,7 @@ void multivariate_hansel_lift_ideal( tout << "A = " << A << endl; tout << "B = " << B << endl; ); - + // get the S, T, solution to A*S+B*T = f, with d(T, x) < d(A, x) // but we know that S = U*f + Bt, T = V*f - At, so we do division zp_polynomial_ref S(zp_pm), T(zp_pm); @@ -415,9 +415,9 @@ void multivariate_hansel_lift_ideal( template bool are_equal_in( - manager_to_check pm, - typename manager_1::polynomial_ref const & A, - typename manager_2::polynomial_ref const & B) { + manager_to_check pm, + typename manager_1::polynomial_ref const & A, + typename manager_2::polynomial_ref const & B) { typename manager_to_check::polynomial_ref A_pm(pm), B_pm(pm); A_pm = convert(A.m(), A, pm); @@ -436,16 +436,16 @@ bool are_equal_in( A_lifted*B_lifted = f mod x_i^d_i, p^e */ void multivariate_hansel_lift_zp( - manager & pm, zp_manager & zp_pm, zp_manager & zpe_pm, - zp_polynomial_ref const & C_pe, var x, unsigned e, + manager & pm, zp_manager & zp_pm, zp_manager & zpe_pm, + zp_polynomial_ref const & C_pe, var x, unsigned e, zp_polynomial_ref const & A_p, zp_polynomial_ref const & U_p, zp_polynomial_ref const & B_p, zp_polynomial_ref const & V_p, - var2degree const & ideal, - zp_polynomial_ref & A_lifted, zp_polynomial_ref & B_lifted) { + var2degree const & ideal, + zp_polynomial_ref & A_lifted, zp_polynomial_ref & B_lifted) { TRACE("polynomial::factorization::multivariate", tout << "polynomial::multiratiate_hensel_lift_zp:" << endl; tout << "zp_pm = Z_" << zp_pm.m().m().to_string(zp_pm.m().p()) << endl; - tout << "zpe_pm = Z_" << zpe_pm.m().m().to_string(zpe_pm.m().p()) << endl; + tout << "zpe_pm = Z_" << zpe_pm.m().m().to_string(zpe_pm.m().p()) << endl; tout << "x = x" << x << endl; tout << "ideal = " << ideal << endl; tout << "C_pe = " << C_pe << "," << endl; @@ -483,8 +483,8 @@ void multivariate_hansel_lift_zp( U_pk = convert(zp_pm, U_p, zpk_pm); V_pk = convert(zp_pm, V_p, zpk_pm); - TRACE("polynomial::factorization::multivariate", - tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; + TRACE("polynomial::factorization::multivariate", + tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; tout << "A_pk = " << A_pk << endl; tout << "B_pk = " << B_pk << endl; tout << "U_pk = " << U_pk << endl; @@ -509,8 +509,8 @@ void multivariate_hansel_lift_zp( f_in_Z = pm.mod_d(f_in_Z, ideal); f_pk = convert(pm, f_in_Z, zpk_pm); - TRACE("polynomial::factorization::multivariate", - tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; + TRACE("polynomial::factorization::multivariate", + tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; tout << "f_pk = " << f_pk << endl; ); @@ -523,8 +523,8 @@ void multivariate_hansel_lift_zp( polynomial_ref S_in_Z(pm), T_in_Z(pm); solve(zpk_pm, x, ideal, A_pk, U_pk, B_pk, V_pk, f_pk, pm, T_in_Z, S_in_Z); - TRACE("polynomial::factorization::multivariate", - tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; + TRACE("polynomial::factorization::multivariate", + tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; tout << "S_in_Z = " << S_in_Z << endl; tout << "T_in_Z = " << T_in_Z << endl; ); @@ -540,15 +540,15 @@ void multivariate_hansel_lift_zp( B_next_in_Z = convert(zpk_pm, B_pk, pm); B_next_in_Z = pm.add(B_next_in_Z, T_in_Z); - TRACE("polynomial::factorization::multivariate", - tout << "pk = " << nm.to_string(pk) << endl; - tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; - tout << "S_in_Z = " << S_in_Z << endl; - tout << "T_in_Z = " << T_in_Z << endl; - tout << "A_pk = " << A_pk << endl; - tout << "B_pk = " << B_pk << endl; - tout << "A_next_in_Z = " << A_next_in_Z << endl; - tout << "B_next_in_Z = " << B_next_in_Z << endl; + TRACE("polynomial::factorization::multivariate", + tout << "pk = " << nm.to_string(pk) << endl; + tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; + tout << "S_in_Z = " << S_in_Z << endl; + tout << "T_in_Z = " << T_in_Z << endl; + tout << "A_pk = " << A_pk << endl; + tout << "B_pk = " << B_pk << endl; + tout << "A_next_in_Z = " << A_next_in_Z << endl; + tout << "B_next_in_Z = " << B_next_in_Z << endl; ); bool eq1 = are_equal_in(zpk_pm, A_next_in_Z, A_pk); @@ -574,9 +574,9 @@ void multivariate_hansel_lift_zp( f_in_Z = pm.sub(f_in_Z, UA_in_Z); f_in_Z = pm.sub(f_in_Z, BV_in_Z); - TRACE("polynomial::factorization::multivariate", - tout << "pk = " << nm.to_string(pk) << endl; - tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; + TRACE("polynomial::factorization::multivariate", + tout << "pk = " << nm.to_string(pk) << endl; + tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; tout << "U_pk_in_Z = " << U_pk_in_Z << endl; tout << "V_pk_in_Z = " << V_pk_in_Z << endl; tout << "UA_in_Z = " << UA_in_Z << endl; @@ -589,10 +589,10 @@ void multivariate_hansel_lift_zp( // get the S, T, solution to A*S+B*T = f, with d(T, x) < d(A, x) solve(zpk_pm, x, ideal, A_pk, U_pk, B_pk, V_pk, f_pk, pm, S_in_Z, T_in_Z); - - TRACE("polynomial::factorization::multivariate", - tout << "pk = " << nm.to_string(pk) << endl; - tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; + + TRACE("polynomial::factorization::multivariate", + tout << "pk = " << nm.to_string(pk) << endl; + tout << "zpk_pm = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; tout << "S_in_Z = " << S_in_Z << endl; tout << "T_in_Z = " << T_in_Z << endl; ); @@ -601,7 +601,7 @@ void multivariate_hansel_lift_zp( scoped_numeral next_pk(nm); nm.mul(pk, pk, next_pk); zpk_nm.set_p(next_pk); - + TRACE("polynomial::factorization::multivariate", tout << "zp_pk = Z_" << zpk_pm.m().m().to_string(zpk_pm.m().p()) << endl; ); @@ -618,7 +618,7 @@ void multivariate_hansel_lift_zp( U_pk = zpk_pm.add(U_pk, S_pk); // lift V zp_polynomial_ref T_pk(zpk_pm); - T_in_Z = pm.mul(pk, T_in_Z); + T_in_Z = pm.mul(pk, T_in_Z); T_pk = convert(pm, T_in_Z, zpk_pm); TRACE("polynomial::factorization::multivariate", @@ -667,7 +667,7 @@ void multivariate_hansel_lift_zp( A_lifted*B_lifted = f mod x_i^d_i, p^e */ void multivariate_hensel_lift( - manager & pm, zp_manager & zp_pm, zp_manager & zpe_pm, + manager & pm, zp_manager & zp_pm, zp_manager & zpe_pm, zp_polynomial_ref const & f, var x, unsigned e, var_vector const & all_vars, upolynomial::zp_manager & zp_upm, upolynomial::numeral_vector const & U, upolynomial::numeral_vector const & A, @@ -746,7 +746,7 @@ void multivariate_hensel_lift( i.e. such that f congruent to the new factors. output goes to f_zpe factors. */ void multivariate_hensel_lift( - manager & pm, zp_manager & zp_pm, zp_manager & zpe_pm, + manager & pm, zp_manager & zp_pm, zp_manager & zpe_pm, polynomial_ref const & f, var x, unsigned e, var_vector const & all_vars, upolynomial::manager & upm, upolynomial::numeral_vector const & f_u, upolynomial::zp_factors const & f_u_zp_factors, @@ -777,9 +777,9 @@ void multivariate_hensel_lift( f_target_zpe = convert(pm, f, zpe_pm); f_target_zpe = zpe_pm.mod_d(f_target_zpe, target_ideal); - TRACE("polynomial::factorization::multivariate", - tout << "target_ideal = " << target_ideal << endl; - tout << "f_target_zpe = " << f_target_zpe << endl; + TRACE("polynomial::factorization::multivariate", + tout << "target_ideal = " << target_ideal << endl; + tout << "f_target_zpe = " << f_target_zpe << endl; ); // we do the product by doing individual lifting like in the univarate case @@ -807,7 +807,7 @@ void multivariate_hensel_lift( // and get the U, V, such that A*U+B*V = 1 zp_upm.ext_gcd(A_u, B_u, U, V, tmp_u); - TRACE("polynomial::factorization::multivariate", + TRACE("polynomial::factorization::multivariate", tout << "U = "; upm.display(tout, U); tout << endl; tout << "V = "; upm.display(tout, V); tout << endl; tout << "gcd = "; upm.display(tout, tmp_u); tout << endl; @@ -943,7 +943,7 @@ bool factor_square_free_primitive(polynomial_ref const & f, factors & f_factors) // to start with, maybe this should be part of input var x = pm.max_var(f); // get all the variables - var_vector vars, vars_no_x; + var_vector vars, vars_no_x; pm.vars(f, vars); for(unsigned i = 0; i < vars.size(); ++ i) { if (vars[i] != x) { @@ -969,7 +969,7 @@ bool factor_square_free_primitive(polynomial_ref const & f, factors & f_factors) unsigned size = 1; a.resize(vars_no_x.size()); for (unsigned i = 0; i < a.size(); ++ i) { nm.reset(a[i]); } - generate_substitution_values(f, x, f_lc, vars_no_x, size, a, upm, f_u); + generate_substitution_values(f, x, f_lc, vars_no_x, size, a, upm, f_u); TRACE("polynomial::factorization::multivariate", tout << "f_u = "; upm.display(tout, f_u); tout << endl; @@ -1068,7 +1068,7 @@ bool factor_square_free_primitive(polynomial_ref const & f, factors & f_factors) multivariate_hensel_lift(pm, zp_pm, zpe_pm, f_t, x, e, vars, upm, f_u_pp_zp, factors_u_zp, target_ideal, factors_zpe); TRACE("polynomial::factorization::multivariate", - tout << "factors_zpe = " << factors_zpe << endl; + tout << "factors_zpe = " << factors_zpe << endl; ); // try the factors from the lifted combinations diff --git a/src/muz/base/proof_utils.cpp b/src/muz/base/proof_utils.cpp index 4bfbf3365..59856c160 100644 --- a/src/muz/base/proof_utils.cpp +++ b/src/muz/base/proof_utils.cpp @@ -525,7 +525,7 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map cache.insert(pr, prNew); refs.push_back(prNew); pr = prNew; -} +} // permute unit resolution over Theory lemmas to track premises. diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index ddf2a9820..d349da4ec 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1874,7 +1874,7 @@ namespace pdr { decl2rel::iterator it = m_rels.begin (), end = m_rels.end (); for (; m_inductive_lvl > 0 && it != end; ++it) { if (it->m_value->head() != m_query_pred) { - it->m_value->propagate_to_infinity (m_inductive_lvl); + it->m_value->propagate_to_infinity (m_inductive_lvl); } } validate(); diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 566f4ec0b..27361a4f9 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -60,7 +60,7 @@ struct mus::imp { m_expr2cls.insert(cls, idx); m_cls2expr.push_back(cls); TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n"; - display_vec(tout, m_cls2expr);); + display_vec(tout, m_cls2expr);); return idx; } @@ -115,10 +115,10 @@ struct mus::imp { core.push_back(cls_id); } } - TRACE("opt", display_vec(tout << "core exprs:", core_exprs); - display_vec(tout << "core:", core); - display_vec(tout << "mus:", mus); - ); + TRACE("opt", display_vec(tout << "core exprs:", core_exprs); + display_vec(tout << "core:", core); + display_vec(tout << "mus:", mus); + ); } break; @@ -152,17 +152,15 @@ struct mus::imp { } void display_vec(std::ostream& out, expr_ref_vector const& v) const { - for (unsigned i = 0; i < v.size(); ++i) { - out << mk_pp(v[i], m) << " "; - } + for (unsigned i = 0; i < v.size(); ++i) + out << mk_pp(v[i], m) << " "; out << "\n"; } void display_vec(std::ostream& out, ptr_vector const& v) const { - for (unsigned i = 0; i < v.size(); ++i) { - out << mk_pp(v[i], m) << " "; - } + for (unsigned i = 0; i < v.size(); ++i) + out << mk_pp(v[i], m) << " "; out << "\n"; } diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 5a4a6ff25..06004e3b8 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -394,7 +394,7 @@ namespace smt { } if ((is_or && val == l_true) || (is_and && val == l_false)) { expr * undef_child = 0; - if (!has_child_assigned_to(m_context, to_app(curr), val, undef_child, m_params.m_rel_case_split_order)) { + if (!has_child_assigned_to(m_context, to_app(curr), val, undef_child, m_params.m_rel_case_split_order)) { if (m_manager.has_trace_stream()) { m_manager.trace_stream() << "[decide-and-or] #" << curr->get_id() << " #" << undef_child->get_id() << "\n"; } @@ -850,7 +850,7 @@ namespace smt { } if ((is_or && val == l_true) || (is_and && val == l_false)) { expr * undef_child = 0; - if (!has_child_assigned_to(m_context, to_app(curr), val, undef_child, m_params.m_rel_case_split_order)) { + if (!has_child_assigned_to(m_context, to_app(curr), val, undef_child, m_params.m_rel_case_split_order)) { if (m_manager.has_trace_stream()) { m_manager.trace_stream() << "[decide-and-or] #" << curr->get_id() << " #" << undef_child->get_id() << "\n"; } diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 15891168c..5c36a2d82 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -120,13 +120,13 @@ struct scoped_timer::imp { m_eh(eh) { #if defined(_WINDOWS) || defined(_CYGWIN) m_first = true; - CreateTimerQueueTimer(&m_timer, - NULL, + CreateTimerQueueTimer(&m_timer, + NULL, abort_proc, this, - 0, - ms, - WT_EXECUTEINTIMERTHREAD); + 0, + ms, + WT_EXECUTEINTIMERTHREAD); #elif defined(__APPLE__) && defined(__MACH__) // Mac OS X m_interval = ms?ms:0xFFFFFFFF; @@ -151,26 +151,26 @@ struct scoped_timer::imp { if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0) throw default_exception("failed to start timer thread"); #elif defined(_LINUX_) || defined(_FREEBSD_) - // Linux & FreeBSD - struct sigevent sev; + // Linux & FreeBSD + struct sigevent sev; memset(&sev, 0, sizeof(sigevent)); - sev.sigev_notify = SIGEV_THREAD; + sev.sigev_notify = SIGEV_THREAD; sev.sigev_value.sival_ptr = this; sev.sigev_notify_function = sig_handler; - if (timer_create(CLOCKID, &sev, &m_timerid) == -1) - throw default_exception("failed to create timer"); + if (timer_create(CLOCKID, &sev, &m_timerid) == -1) + throw default_exception("failed to create timer"); - unsigned long long nano = static_cast(ms) * 1000000ull; - struct itimerspec its; - its.it_value.tv_sec = nano / 1000000000ull; - its.it_value.tv_nsec = nano % 1000000000ull; - its.it_interval.tv_sec = 0; // timer experies once - its.it_interval.tv_nsec = 0; + unsigned long long nano = static_cast(ms) * 1000000ull; + struct itimerspec its; + its.it_value.tv_sec = nano / 1000000000ull; + its.it_value.tv_nsec = nano % 1000000000ull; + its.it_interval.tv_sec = 0; // timer experies once + its.it_interval.tv_nsec = 0; - if (timer_settime(m_timerid, 0, &its, NULL) == -1) - throw default_exception("failed to set timer"); + if (timer_settime(m_timerid, 0, &its, NULL) == -1) + throw default_exception("failed to set timer"); #else - // Other platforms + // Other platforms #endif } @@ -203,10 +203,10 @@ struct scoped_timer::imp { if (pthread_attr_destroy(&m_attributes) != 0) throw default_exception("failed to destroy pthread attributes object"); #elif defined(_LINUX_) || defined(_FREEBSD_) - // Linux & FreeBSD - timer_delete(m_timerid); + // Linux & FreeBSD + timer_delete(m_timerid); #else - // Other Platforms + // Other Platforms #endif }