From 31e75d1401b13e2ac782c325144ef3d50883638a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 31 May 2020 13:26:27 +0100 Subject: [PATCH] minor simplifications --- src/smt/smt_context.h | 8 ++++---- src/smt/smt_internalizer.cpp | 32 ++++++++++++++++---------------- src/smt/theory_fpa.cpp | 8 +++----- 3 files changed, 23 insertions(+), 25 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 1a6cbd446..99aa8785b 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -731,13 +731,13 @@ namespace smt { typedef std::pair expr_bool_pair; - void ts_visit_child(expr * n, bool gate_ctx, svector & tcolors, svector & fcolors, svector & todo, bool & visited); + void ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited); - bool ts_visit_children(expr * n, bool gate_ctx, svector & tcolors, svector & fcolors, svector & todo); + bool ts_visit_children(expr * n, bool gate_ctx, svector & todo); svector ts_todo; - svector tcolors; - svector fcolors; + char_vector tcolors; + char_vector fcolors; void top_sort_expr(expr * n, svector & sorted_exprs); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 18fc25555..4c04778e8 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -29,7 +29,7 @@ namespace smt { /** \brief Return true if the expression is viewed as a logical gate. */ - inline bool is_gate(ast_manager const & m, expr * n) { + static bool is_gate(ast_manager const & m, expr * n) { if (is_app(n) && to_app(n)->get_family_id() == m.get_basic_family_id()) { switch (to_app(n)->get_decl_kind()) { case OP_AND: @@ -45,19 +45,19 @@ namespace smt { return false; } -#define White 0 +#define White 0 #define Grey 1 #define Black 2 - static int get_color(svector & tcolors, svector & fcolors, expr * n, bool gate_ctx) { - svector & colors = gate_ctx ? tcolors : fcolors; - if (colors.size() > n->get_id()) + static char get_color(char_vector & tcolors, char_vector & fcolors, expr * n, bool gate_ctx) { + char_vector & colors = gate_ctx ? tcolors : fcolors; + if (colors.size() > n->get_id()) return colors[n->get_id()]; return White; } - static void set_color(svector & tcolors, svector & fcolors, expr * n, bool gate_ctx, int color) { - svector & colors = gate_ctx ? tcolors : fcolors; + static void set_color(char_vector & tcolors, char_vector & fcolors, expr * n, bool gate_ctx, char color) { + char_vector & colors = gate_ctx ? tcolors : fcolors; if (colors.size() <= n->get_id()) { colors.resize(n->get_id()+1, White); } @@ -99,14 +99,14 @@ namespace smt { } } - void context::ts_visit_child(expr * n, bool gate_ctx, svector & tcolors, svector< int> & fcolors, svector & todo, bool & visited) { + void context::ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited) { if (get_color(tcolors, fcolors, n, gate_ctx) == White) { todo.push_back(expr_bool_pair(n, gate_ctx)); visited = false; } } - bool context::ts_visit_children(expr * n, bool gate_ctx, svector & tcolors, svector & fcolors, svector & todo) { + bool context::ts_visit_children(expr * n, bool gate_ctx, svector & todo) { if (is_quantifier(n)) return true; SASSERT(is_app(n)); @@ -127,7 +127,7 @@ namespace smt { ptr_buffer descendants; get_foreign_descendants(to_app(n), fid, descendants); for (expr * arg : descendants) { - ts_visit_child(arg, false, tcolors, fcolors, todo, visited); + ts_visit_child(arg, false, todo, visited); } return visited; } @@ -135,9 +135,9 @@ namespace smt { SASSERT(def_int); if (m.is_term_ite(n)) { - ts_visit_child(to_app(n)->get_arg(0), true, tcolors, fcolors, todo, visited); - ts_visit_child(to_app(n)->get_arg(1), false, tcolors, fcolors, todo, visited); - ts_visit_child(to_app(n)->get_arg(2), false, tcolors, fcolors, todo, visited); + ts_visit_child(to_app(n)->get_arg(0), true, todo, visited); + ts_visit_child(to_app(n)->get_arg(1), false, todo, visited); + ts_visit_child(to_app(n)->get_arg(2), false, todo, visited); return visited; } bool new_gate_ctx = m.is_bool(n) && (is_gate(m, n) || m.is_not(n)); @@ -145,7 +145,7 @@ namespace smt { while (j > 0) { --j; expr * arg = to_app(n)->get_arg(j); - ts_visit_child(arg, new_gate_ctx, tcolors, fcolors, todo, visited); + ts_visit_child(arg, new_gate_ctx, todo, visited); } return visited; } @@ -162,10 +162,10 @@ namespace smt { switch (get_color(tcolors, fcolors, curr, gate_ctx)) { case White: set_color(tcolors, fcolors, curr, gate_ctx, Grey); - ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo); + ts_visit_children(curr, gate_ctx, ts_todo); break; case Grey: - SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo)); + SASSERT(ts_visit_children(curr, gate_ctx, ts_todo)); set_color(tcolors, fcolors, curr, gate_ctx, Black); if (n != curr && !m.is_not(curr)) sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx)); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 4da4b3350..7c97dbc52 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -380,7 +380,7 @@ namespace smt { for (expr* arg : m_converter.m_extra_assertions) { ctx.get_rewriter()(arg, t, t_pr); - fmls.push_back(t); + fmls.push_back(std::move(t)); } m_converter.m_extra_assertions.reset(); res = m.mk_and(fmls); @@ -440,8 +440,7 @@ namespace smt { for (unsigned i = 0; i < num_args; i++) ctx.internalize(term->get_arg(i), false); - enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : - ctx.mk_enode(term, false, false, true); + enode * e = ctx.mk_enode(term, false, false, true); if (!is_attached_to_var(e)) { attach_new_th_var(e); @@ -457,8 +456,7 @@ namespace smt { case OP_FPA_TO_SBV: case OP_FPA_TO_REAL: case OP_FPA_TO_IEEE_BV: { - expr_ref conv(m); - conv = convert(term); + expr_ref conv = convert(term); expr_ref eq(m.mk_eq(term, conv), m); assert_cnstr(eq); assert_cnstr(mk_side_conditions());