From 5253f3a12b36821a9c2a84bc604540689d80ddff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Jun 2016 13:56:01 -0700 Subject: [PATCH] internalize unsupported operations Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_prop_solver.h | 3 --- src/smt/theory_arith_core.h | 28 ++++++++++++++++++---------- 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h index 58bd611a9..ad7e1fd9a 100644 --- a/src/muz/pdr/pdr_prop_solver.h +++ b/src/muz/pdr/pdr_prop_solver.h @@ -87,9 +87,6 @@ namespace pdr { void set_subset_based_core(bool f) { m_subset_based_core = f; } void set_consequences(expr_ref_vector* consequences) { m_consequences = consequences; } - - void set_background_assumptions(expr_ref_vector const& assumptions); - bool assumes_level() const { return m_assumes_level; } void add_level(); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 95c7fdfad..8dfe8498f 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -747,17 +747,25 @@ namespace smt { enode * e = mk_enode(n); return mk_var(e); } - else { - TRACE("arith_internalize_detail", tout << "before:\n" << mk_pp(n, get_manager()) << "\n";); - if (!ctx.e_internalized(n)) - ctx.internalize(n, false); - TRACE("arith_internalize_detail", tout << "after:\n" << mk_pp(n, get_manager()) << "\n";); - enode * e = ctx.get_enode(n); - if (!is_attached_to_var(e)) - return mk_var(e); - else - return e->get_th_var(get_id()); + if (m_util.get_family_id() == n->get_family_id()) { + found_unsupported_op(n); + if (ctx.e_internalized(n)) + return expr2var(n); + for (unsigned i = 0; i < n->get_num_args(); ++i) { + ctx.internalize(n->get_arg(i), false); + } + return mk_var(mk_enode(n)); } + + TRACE("arith_internalize_detail", tout << "before:\n" << mk_pp(n, get_manager()) << "\n";); + if (!ctx.e_internalized(n)) + ctx.internalize(n, false); + TRACE("arith_internalize_detail", tout << "after:\n" << mk_pp(n, get_manager()) << "\n";); + enode * e = ctx.get_enode(n); + if (!is_attached_to_var(e)) + return mk_var(e); + else + return e->get_th_var(get_id()); } /**