mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

tabs and indentation

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-17 13:25:22 +01:00
parent d2c9b69eb3
commit f3441c6a9b
7 changed files with 86 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/math/polynomial/polynomial.cpp
View file

@ -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) {

90
src/math/polynomial/polynomial_factorization.cpp
View file

@ -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<typename manager_to_check, typename manager_1, typename manager_2>
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<manager>(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<zp_manager, manager, zp_manager>(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<manager>(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

2
src/muz/base/proof_utils.cpp
View file

@ -525,7 +525,7 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>
cache.insert(pr, prNew);
refs.push_back(prNew);
pr = prNew;
}
}
// permute unit resolution over Theory lemmas to track premises.

2
src/muz/pdr/pdr_context.cpp
View file

@ -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();

20
src/opt/mus.cpp
View file

@ -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<expr> 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";
}

4
src/smt/smt_case_split_queue.cpp
View file

@ -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";
}

44
src/util/scoped_timer.cpp
View file

@ -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<unsigned long long>(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<unsigned long long>(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
}