From 81f1f7690df331065f775aa15b9abea6441fa5be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Dec 2013 15:59:56 -0800 Subject: [PATCH 1/3] fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/lia2pb_tactic.cpp | 1 + src/util/rational.h | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 6fee55e4b..9ee8f6728 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic { if (m_bm.has_lower(n, l, s) && m_bm.has_upper(n, u, s) && l.is_zero() && + !u.is_neg() && u.get_num_bits() <= m_max_bits) { return true; diff --git a/src/util/rational.h b/src/util/rational.h index fc03228bf..c02a5a2c3 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -104,7 +104,7 @@ public: } bool is_int32() const { - if (is_small()) return true; + if (is_small() && is_int()) return true; // we don't assume that if it is small, then it is int32. if (!is_int64()) return false; int64 v = get_int64(); From 084a6f35eb2f1ad7db7b6c89bf580e36f4052a75 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jan 2014 17:37:35 -0800 Subject: [PATCH 2/3] fix bug reported by Nuno Lopes: inlining is unsound for negated predicates Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_rule_inliner.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 3e933b099..d9dad5c56 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -527,6 +527,9 @@ namespace datalog { bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) { + if (r->has_negation()) { + return false; + } SASSERT(rules.is_closed()); const rule_stratifier& strat = rules.get_stratifier(); From da4793de76a5e0a34bb00c333f8c2902d1c96ec3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Jan 2014 21:14:30 -0800 Subject: [PATCH 3/3] fix type checking bug reported by Nate Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b000201b7..68f7596ee 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const { ast_manager& m = const_cast(*this); + if (decl->is_associative()) { sort * expected = decl->get_domain(0); for (unsigned i = 0; i < num_args; i++) { @@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const { if (n->get_kind() != AST_APP) return; // nothing else to check... app const * a = to_app(n); - check_sort(a->get_decl(), a->get_num_args(), a->get_args()); + func_decl* d = a->get_decl(); + check_sort(d, a->get_num_args(), a->get_args()); + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_right_associative()) { + check_sorts_core(a->get_arg(1)); + } + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_left_associative()) { + check_sorts_core(a->get_arg(0)); + } } bool ast_manager::check_sorts(ast const * n) const {