From 49906a5a58d699b1f8f0a5d6a4bd8906d5245970 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 13 Apr 2021 17:42:42 +0100 Subject: [PATCH] api_context: remove basic&arith fids fields these are now constant,s o we can save some space the remaining ones need to be made constant as well.. --- src/api/api_context.cpp | 4 +--- src/api/api_context.h | 6 ++---- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 05c128cd6..b5437a358 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -91,8 +91,6 @@ namespace api { m_interruptable = nullptr; m_error_handler = &default_error_handler; - m_basic_fid = m().get_basic_family_id(); - m_arith_fid = m().mk_family_id("arith"); m_bv_fid = m().mk_family_id("bv"); m_pb_fid = m().mk_family_id("pb"); m_array_fid = m().mk_family_id("array"); @@ -174,7 +172,7 @@ namespace api { expr * context::mk_numeral_core(rational const & n, sort * s) { expr* e = nullptr; family_id fid = s->get_family_id(); - if (fid == m_arith_fid) { + if (fid == arith_family_id) { e = m_arith_util.mk_numeral(n, s); } else if (fid == m_bv_fid) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 6a0ac588e..c2e2a4da2 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -97,9 +97,7 @@ namespace api { u_map m_allocated_objects; // !< table containing current set of allocated API objects unsigned_vector m_free_object_ids; // !< free list of identifiers available for allocated objects. - family_id m_basic_fid; family_id m_array_fid; - family_id m_arith_fid; family_id m_bv_fid; family_id m_dt_fid; family_id m_datalog_fid; @@ -152,9 +150,9 @@ namespace api { datatype_util& dtutil() { return m_dt_plugin->u(); } seq_util& sutil() { return m_sutil; } recfun::util& recfun() { return m_recfun; } - family_id get_basic_fid() const { return m_basic_fid; } + family_id get_basic_fid() const { return basic_family_id; } family_id get_array_fid() const { return m_array_fid; } - family_id get_arith_fid() const { return m_arith_fid; } + family_id get_arith_fid() const { return arith_family_id; } family_id get_bv_fid() const { return m_bv_fid; } family_id get_dt_fid() const { return m_dt_fid; } family_id get_datalog_fid() const { return m_datalog_fid; }