From e13bf2424e9641fb9e0c38ed626ebad8239a1723 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 08:29:24 -0700 Subject: [PATCH 1/3] fix type checking for non-associative basic operations, fixes issue #160 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 59efb2a89..2881f1b62 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2046,8 +2046,14 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2 } app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) { - if (decl->get_arity() != num_args && !decl->is_right_associative() && - !decl->is_left_associative() && !decl->is_chainable()) { + bool type_error = + decl->get_arity() != num_args && !decl->is_right_associative() && + !decl->is_left_associative() && !decl->is_chainable(); + + type_error |= (decl->get_arity() != num_args && num_args < 2 && + decl->get_family_id() == m_basic_family_id && !decl->is_associative()); + + if (type_error) { std::ostringstream buffer; buffer << "Wrong number of arguments (" << num_args << ") passed to function " << mk_pp(decl, *this); From 96c8b1e7ffc4b9d55f6ac20fa0e117c2d636366d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 12:44:07 -0700 Subject: [PATCH 2/3] fixup model construction on undef results for arithmetic. Fixes issue #161 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 1 + src/smt/tactic/ctx_solver_simplify_tactic.cpp | 2 +- src/smt/theory_arith_aux.h | 6 +++--- src/smt/theory_arith_core.h | 4 ++++ 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 9d1f4343f..5245b9685 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -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) { if (is_int && !val.is_int()) { + SASSERT(false); m_manager->raise_exception("invalid rational value passed as an integer"); } if (val.is_unsigned()) { diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 98b7592c8..622d67a34 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -125,7 +125,7 @@ protected: m_solver.assert_expr(fml1); lbool is_sat = m_solver.check(); 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", tout << "result is not equivalent to input\n"; tout << mk_pp(fml1, m) << "\n";); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 397f6683b..ebdd1386c 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1479,9 +1479,9 @@ namespace smt { SASSERT(max_gain.is_minus_one() || !max_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_int()); - SASSERT(!is_int(x_i) || max_gain.is_int()); + //SASSERT(!is_int(x_i) || min_gain.is_pos()); + //SASSERT(!is_int(x_i) || min_gain.is_int()); + //SASSERT(!is_int(x_i) || max_gain.is_int()); return is_tighter; } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 2b91452a9..c47585606 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3065,6 +3065,10 @@ namespace smt { SASSERT(v != null_theory_var); inf_numeral const & val = get_value(v); 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))); } From 6e22250d1a3486d760bb539b4b77710d8901a9f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 12:44:55 -0700 Subject: [PATCH 3/3] fixup model construction on undef results for arithmetic. Fixes issue #161 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 5245b9685..9d1f4343f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -417,7 +417,6 @@ 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) { if (is_int && !val.is_int()) { - SASSERT(false); m_manager->raise_exception("invalid rational value passed as an integer"); } if (val.is_unsigned()) {