mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

fixup model construction on undef results for arithmetic. Fixes issue #161

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-07-13 12:44:07 -07:00
parent e13bf2424e
commit 96c8b1e7ff
4 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/arith_decl_plugin.cpp
View file

@ -417,6 +417,7 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
if (is_int && !val.is_int()) { if (is_int && !val.is_int()) {
SASSERT(false);
m_manager->raise_exception("invalid rational value passed as an integer"); m_manager->raise_exception("invalid rational value passed as an integer");
} }
if (val.is_unsigned()) { if (val.is_unsigned()) {

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

@ -125,7 +125,7 @@ protected:
m_solver.assert_expr(fml1); m_solver.assert_expr(fml1);
lbool is_sat = m_solver.check(); lbool is_sat = m_solver.check();
TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";); TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
if (is_sat != l_false) { if (is_sat == l_true) {
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
tout << "result is not equivalent to input\n"; tout << "result is not equivalent to input\n";
tout << mk_pp(fml1, m) << "\n";); tout << mk_pp(fml1, m) << "\n";);

6
src/smt/theory_arith_aux.h
View file

@ -1479,9 +1479,9 @@ namespace smt {
SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
SASSERT(min_gain.is_minus_one() || !min_gain.is_neg()); SASSERT(min_gain.is_minus_one() || !min_gain.is_neg());
SASSERT(!is_int(x_i) || min_gain.is_pos()); //SASSERT(!is_int(x_i) || min_gain.is_pos());
SASSERT(!is_int(x_i) || min_gain.is_int()); //SASSERT(!is_int(x_i) || min_gain.is_int());
SASSERT(!is_int(x_i) || max_gain.is_int()); //SASSERT(!is_int(x_i) || max_gain.is_int());
return is_tighter; return is_tighter;
} }

4
src/smt/theory_arith_core.h
View file

@ -3065,6 +3065,10 @@ namespace smt {
SASSERT(v != null_theory_var); SASSERT(v != null_theory_var);
inf_numeral const & val = get_value(v); inf_numeral const & val = get_value(v);
rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
if (is_int(v) && !num.is_int()) {
TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
num = floor(num);
}
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
} }