mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fix #2921

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-02 10:35:06 -08:00
parent 805ac745e9
commit b0a28160f7
5 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/arith_decl_plugin.h
View file

@ -172,6 +172,8 @@ public:
return alloc(arith_decl_plugin);
}
bool convert_int_numerals_to_real() const { return m_convert_int_numerals_to_real; }
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -363,6 +365,7 @@ public:
return plugin().am();
}
bool convert_int_numerals_to_real() const { return plugin().convert_int_numerals_to_real(); }
bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val);
algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);

3
src/ast/rewriter/arith_rewriter.cpp
View file

@ -1228,6 +1228,9 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
numeral a;
expr* x = nullptr;
if (m_util.convert_int_numerals_to_real())
return BR_FAILED;
if (m_util.is_numeral(arg, a)) {
result = m_util.mk_numeral(floor(a), true);
return BR_DONE;

4
src/ast/rewriter/rewriter_def.h
View file

@ -288,13 +288,13 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
m_pr = m().mk_congruence(t, new_t, num_prs, result_pr_stack().c_ptr() + fr.m_spos);
}
}
br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);
CTRACE("reduce_app", st != BR_FAILED,
tout << mk_bounded_pp(t, m()) << "\n";
tout << "st: " << st;
if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
tout << "\n";);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
if (st != BR_FAILED) {
result_stack().shrink(fr.m_spos);
SASSERT(m().get_sort(m_r) == m().get_sort(t));

2
src/math/lp/lar_solver.cpp
View file

@ -1237,7 +1237,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
}
}
// (x, y) != (x', y') => (x + delty*y) != (x' + delty*y')
// (x, y) != (x', y') => (x + delta*y) != (x' + delta*y')
void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
variable_values.clear();

9
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -48,10 +48,8 @@ public:
}
~ctx_solver_simplify_tactic() override {
obj_map<sort, func_decl*>::iterator it = m_fns.begin(), end = m_fns.end();
for (; it != end; ++it) {
m.dec_ref(it->m_value);
}
for (auto & kv : m_fns)
m.dec_ref(kv.m_value);
m_fns.reset();
}
@ -86,6 +84,7 @@ protected:
void reduce(goal& g) {
SASSERT(g.is_well_sorted());
TRACE("ctx_solver_simplify_tactic", g.display(tout););
expr_ref fml(m);
tactic_report report("ctx-solver-simplify", g);
if (g.inconsistent())
@ -277,7 +276,7 @@ protected:
m.inc_ref(fn);
m_fns.insert(s, fn);
}
return expr_ref(m.mk_app(fn, m_arith.mk_numeral(rational(id++), true)), m);
return expr_ref(m.mk_app(fn, m_arith.mk_int(id++)), m);
}
};