mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

fix bug in factor_tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-04 11:02:53 -08:00
parent ff265c6c6c
commit 8b10e13251
1 changed files with 29 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/tactic/arith/factor_tactic.cpp
View file

@ -50,7 +50,7 @@ class factor_tactic : public tactic {
return args[0]; return args[0];
return m_util.mk_mul(sz, args); return m_util.mk_mul(sz, args);
} }
expr * mk_zero_for(expr * arg) { expr * mk_zero_for(expr * arg) {
return m_util.mk_numeral(rational(0), m_util.is_int(arg)); return m_util.mk_numeral(rational(0), m_util.is_int(arg));
} }
@ -92,10 +92,10 @@ class factor_tactic : public tactic {
return k; return k;
} }
} }
// p1^{2*k1} * p2^{2*k2 + 1} >=< 0 // p1^{2*k1} * p2^{2*k2 + 1} >=< 0
// --> // -->
// (p1^2)*p2 >=<0 // (p1^2)*p2 >=<0
void mk_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) { void mk_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) {
SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE);
expr_ref_buffer args(m); expr_ref_buffer args(m);
@ -127,7 +127,7 @@ class factor_tactic : public tactic {
} }
} }
} }
// Strict case // Strict case
// p1^{2*k1} * p2^{2*k2 + 1} >< 0 // p1^{2*k1} * p2^{2*k2 + 1} >< 0
// --> // -->
@ -158,11 +158,11 @@ class factor_tactic : public tactic {
args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.c_ptr()), mk_zero_for(odd_factors[0]))); args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.c_ptr()), mk_zero_for(odd_factors[0])));
} }
SASSERT(!args.empty()); SASSERT(!args.empty());
if (args.size() == 1) if (args.size() == 1)
result = args[0]; result = args[0];
else if (strict) else if (strict)
result = m.mk_and(args.size(), args.c_ptr()); result = m.mk_and(args.size(), args.c_ptr());
else else
result = m.mk_or(args.size(), args.c_ptr()); result = m.mk_or(args.size(), args.c_ptr());
} }
@ -173,7 +173,7 @@ class factor_tactic : public tactic {
scoped_mpz d2(m_qm); scoped_mpz d2(m_qm);
m_expr2poly.to_polynomial(lhs, p1, d1); m_expr2poly.to_polynomial(lhs, p1, d1);
m_expr2poly.to_polynomial(rhs, p2, d2); m_expr2poly.to_polynomial(rhs, p2, d2);
TRACE("factor_tactic_bug", TRACE("factor_tactic_bug",
tout << "lhs: " << mk_ismt2_pp(lhs, m) << "\n"; tout << "lhs: " << mk_ismt2_pp(lhs, m) << "\n";
tout << "p1: " << p1 << "\n"; tout << "p1: " << p1 << "\n";
tout << "d1: " << d1 << "\n"; tout << "d1: " << d1 << "\n";
@ -195,18 +195,18 @@ class factor_tactic : public tactic {
SASSERT(fs.distinct_factors() > 0); SASSERT(fs.distinct_factors() > 0);
TRACE("factor_tactic_bug", tout << "factors:\n"; fs.display(tout); tout << "\n";); TRACE("factor_tactic_bug", tout << "factors:\n"; fs.display(tout); tout << "\n";);
if (fs.distinct_factors() == 1 && fs.get_degree(0) == 1) if (fs.distinct_factors() == 1 && fs.get_degree(0) == 1)
return BR_FAILED; return BR_FAILED;
if (m.is_eq(f)) { if (m.is_eq(f)) {
if (m_split_factors) if (m_split_factors)
mk_split_eq(fs, result); mk_split_eq(fs, result);
else else
mk_eq(fs, result); mk_eq(fs, result);
} }
else { else {
decl_kind k = f->get_decl_kind(); decl_kind k = f->get_decl_kind();
if (m_qm.is_neg(fs.get_constant())) if (m_qm.is_neg(fs.get_constant()))
k = flip(k); k = flip(k);
if (m_split_factors) if (m_split_factors)
mk_split_comp(k, fs, result); mk_split_comp(k, fs, result);
else else
@ -215,10 +215,10 @@ class factor_tactic : public tactic {
return BR_DONE; return BR_DONE;
} }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (num != 2) if (num != 2)
return BR_FAILED; return BR_FAILED;
if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1]))) if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1])) && (!m.is_bool(args[0])))
return factor(f, args[0], args[1], result); return factor(f, args[0], args[1], result);
if (f->get_family_id() != m_util.get_family_id()) if (f->get_family_id() != m_util.get_family_id())
return BR_FAILED; return BR_FAILED;
@ -232,10 +232,10 @@ class factor_tactic : public tactic {
return BR_FAILED; return BR_FAILED;
} }
}; };
struct rw : public rewriter_tpl<rw_cfg> { struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg; rw_cfg m_cfg;
rw(ast_manager & m, params_ref const & p): rw(ast_manager & m, params_ref const & p):
rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, p) { m_cfg(m, p) {
@ -245,24 +245,24 @@ class factor_tactic : public tactic {
struct imp { struct imp {
ast_manager & m; ast_manager & m;
rw m_rw; rw m_rw;
imp(ast_manager & _m, params_ref const & p): imp(ast_manager & _m, params_ref const & p):
m(_m), m(_m),
m_rw(m, p) { m_rw(m, p) {
} }
void set_cancel(bool f) { void set_cancel(bool f) {
m_rw.set_cancel(f); m_rw.set_cancel(f);
m_rw.cfg().m_pm.set_cancel(f); m_rw.cfg().m_pm.set_cancel(f);
} }
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
m_rw.cfg().updt_params(p); m_rw.cfg().updt_params(p);
} }
void operator()(goal_ref const & g, void operator()(goal_ref const & g,
goal_ref_buffer & result, goal_ref_buffer & result,
model_converter_ref & mc, model_converter_ref & mc,
proof_converter_ref & pc, proof_converter_ref & pc,
expr_dependency_ref & core) { expr_dependency_ref & core) {
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
@ -288,7 +288,7 @@ class factor_tactic : public tactic {
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
} }
}; };
imp * m_imp; imp * m_imp;
params_ref m_params; params_ref m_params;
public: public:
@ -300,7 +300,7 @@ public:
virtual tactic * translate(ast_manager & m) { virtual tactic * translate(ast_manager & m) {
return alloc(factor_tactic, m, m_params); return alloc(factor_tactic, m, m_params);
} }
virtual ~factor_tactic() { virtual ~factor_tactic() {
dealloc(m_imp); dealloc(m_imp);
} }
@ -311,14 +311,14 @@ public:
} }
virtual void collect_param_descrs(param_descrs & r) { virtual void collect_param_descrs(param_descrs & r) {
r.insert("split_factors", CPK_BOOL, r.insert("split_factors", CPK_BOOL,
"(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0))."); "(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).");
polynomial::factor_params::get_param_descrs(r); polynomial::factor_params::get_param_descrs(r);
} }
virtual void operator()(goal_ref const & in, virtual void operator()(goal_ref const & in,
goal_ref_buffer & result, goal_ref_buffer & result,
model_converter_ref & mc, model_converter_ref & mc,
proof_converter_ref & pc, proof_converter_ref & pc,
expr_dependency_ref & core) { expr_dependency_ref & core) {
try { try {
@ -331,7 +331,7 @@ public:
throw tactic_exception(ex.msg()); throw tactic_exception(ex.msg());
} }
} }
virtual void cleanup() { virtual void cleanup() {
ast_manager & m = m_imp->m; ast_manager & m = m_imp->m;
imp * d = m_imp; imp * d = m_imp;