From ffa53fee36d787d356b204db2ac40b0c0d687505 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Sep 2024 17:54:29 -0700 Subject: [PATCH] Refactor SLS engine and evaluator components for bit-vector specifics and adjust memory manager alignment --- src/ast/sls/CMakeLists.txt | 2 +- src/ast/sls/bvsls_opt_engine.h | 2 +- src/ast/sls/sls_bv_engine.cpp | 2 +- src/ast/sls/sls_bv_engine.h | 4 ++-- src/ast/sls/sls_bv_evaluator.h | 2 +- src/tactic/sls/sls_tactic.cpp | 2 +- src/util/memory_manager.cpp | 24 +++++++++++++----------- 7 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt index 3ee51a028..cdddc441c 100644 --- a/src/ast/sls/CMakeLists.txt +++ b/src/ast/sls/CMakeLists.txt @@ -5,13 +5,13 @@ z3_add_component(ast_sls sls_arith_base.cpp sls_arith_plugin.cpp sls_basic_plugin.cpp + sls_bv_engine.cpp sls_bv_eval.cpp sls_bv_fixed.cpp sls_bv_plugin.cpp sls_bv_terms.cpp sls_bv_valuation.cpp sls_context.cpp - sls_engine.cpp sls_euf_plugin.cpp sls_smt_solver.cpp COMPONENT_DEPENDENCIES diff --git a/src/ast/sls/bvsls_opt_engine.h b/src/ast/sls/bvsls_opt_engine.h index 435fa3af4..423dfd6a3 100644 --- a/src/ast/sls/bvsls_opt_engine.h +++ b/src/ast/sls/bvsls_opt_engine.h @@ -18,7 +18,7 @@ Notes: --*/ #pragma once -#include "ast/sls/sls_engine.h" +#include "ast/sls/sls_bv_engine.h" class bvsls_opt_engine : public sls_engine { sls_tracker & m_hard_tracker; diff --git a/src/ast/sls/sls_bv_engine.cpp b/src/ast/sls/sls_bv_engine.cpp index a2ab861c0..124a5ea77 100644 --- a/src/ast/sls/sls_bv_engine.cpp +++ b/src/ast/sls/sls_bv_engine.cpp @@ -26,7 +26,7 @@ Notes: #include "util/luby.h" #include "params/sls_params.hpp" -#include "ast/sls/sls_engine.h" +#include "ast/sls/sls_bv_engine.h" sls_engine::sls_engine(ast_manager & m, params_ref const & p) : diff --git a/src/ast/sls/sls_bv_engine.h b/src/ast/sls/sls_bv_engine.h index 3e67aa49c..f9d26ee70 100644 --- a/src/ast/sls/sls_bv_engine.h +++ b/src/ast/sls/sls_bv_engine.h @@ -23,8 +23,8 @@ Notes: #include "ast/converters/model_converter.h" #include "ast/sls/sls_stats.h" -#include "ast/sls/sls_tracker.h" -#include "ast/sls/sls_evaluator.h" +#include "ast/sls/sls_bv_tracker.h" +#include "ast/sls/sls_bv_evaluator.h" class sls_engine { diff --git a/src/ast/sls/sls_bv_evaluator.h b/src/ast/sls/sls_bv_evaluator.h index 2ee03c928..d0a71f158 100644 --- a/src/ast/sls/sls_bv_evaluator.h +++ b/src/ast/sls/sls_bv_evaluator.h @@ -22,7 +22,7 @@ Notes: #include "model/model_evaluator.h" #include "ast/sls/sls_powers.h" -#include "ast/sls/sls_tracker.h" +#include "ast/sls/sls_bv_tracker.h" class sls_evaluator { ast_manager & m_manager; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index fdb4620c8..e72c01af0 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -28,7 +28,7 @@ Notes: #include "util/stopwatch.h" #include "tactic/sls/sls_tactic.h" #include "params/sls_params.hpp" -#include "ast/sls/sls_engine.h" +#include "ast/sls/sls_bv_engine.h" #include "ast/sls/sls_smt_solver.h" class sls_smt_tactic : public tactic { diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 290881ba5..4ef1cac66 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -29,6 +29,8 @@ Copyright (c) 2015 Microsoft Corporation # define malloc_usable_size _msize #endif +#define SIZE_T_ALIGN 2 + // The following two function are automatically generated by the mk_make.py script. // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files. // For example, rational.h contains @@ -278,7 +280,7 @@ void memory::deallocate(void * p) { size_t sz = malloc_usable_size(p); void * real_p = p; #else - size_t * sz_p = reinterpret_cast(p) - 1; + size_t * sz_p = reinterpret_cast(p) - SIZE_T_ALIGN; size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); #endif @@ -291,7 +293,7 @@ void memory::deallocate(void * p) { void * memory::allocate(size_t s) { #ifndef HAS_MALLOC_USABLE_SIZE - s = s + sizeof(size_t); // we allocate an extra field! + s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! #endif g_memory_thread_alloc_size += s; g_memory_thread_alloc_count += 1; @@ -308,7 +310,7 @@ void * memory::allocate(size_t s) { return r; #else *(static_cast(r)) = s; - return static_cast(r) + 1; // we return a pointer to the location after the extra field + return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field #endif } @@ -323,7 +325,7 @@ void* memory::reallocate(void *p, size_t s) { size_t *sz_p = reinterpret_cast(p)-1; size_t sz = *sz_p; void *real_p = reinterpret_cast(sz_p); - s = s + sizeof(size_t); // we allocate an extra field! + s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! #endif g_memory_thread_alloc_size += s - sz; g_memory_thread_alloc_count += 1; @@ -341,7 +343,7 @@ void* memory::reallocate(void *p, size_t s) { return r; #else *(static_cast(r)) = s; - return static_cast(r) + 1; // we return a pointer to the location after the extra field + return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field #endif } @@ -358,7 +360,7 @@ void memory::deallocate(void * p) { size_t sz = malloc_usable_size(p); void * real_p = p; #else - size_t * sz_p = reinterpret_cast(p) - 1; + size_t * sz_p = reinterpret_cast(p) - SIZE_T_ALIGN; size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); #endif @@ -368,7 +370,7 @@ void memory::deallocate(void * p) { void * memory::allocate(size_t s) { #ifndef HAS_MALLOC_USABLE_SIZE - s = s + sizeof(size_t); // we allocate an extra field! + s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! #endif g_memory_alloc_size += s; g_memory_alloc_count += 1; @@ -389,7 +391,7 @@ void * memory::allocate(size_t s) { return r; #else *(static_cast(r)) = s; - return static_cast(r) + 1; // we return a pointer to the location after the extra field + return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field #endif } @@ -401,10 +403,10 @@ void* memory::reallocate(void *p, size_t s) { if (sz >= s) return p; #else - size_t * sz_p = reinterpret_cast(p) - 1; + size_t * sz_p = reinterpret_cast(p) - SIZE_T_ALIGN; size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); - s = s + sizeof(size_t); // we allocate an extra field! + s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! #endif g_memory_alloc_size += s - sz; g_memory_alloc_count += 1; @@ -425,7 +427,7 @@ void* memory::reallocate(void *p, size_t s) { return r; #else *(static_cast(r)) = s; - return static_cast(r) + 1; // we return a pointer to the location after the extra field + return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field #endif }