diff --git a/.github/workflows/android-build.yml b/.github/workflows/android-build.yml index 8bbfd5ab0..eec9032df 100644 --- a/.github/workflows/android-build.yml +++ b/.github/workflows/android-build.yml @@ -13,7 +13,7 @@ permissions: jobs: build: runs-on: ubuntu-latest - + strategy: fail-fast: false matrix: @@ -27,10 +27,10 @@ jobs: run: | mkdir build cd build - cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_SYSTEM_VERSION=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} -DCMAKE_ANDROID_NDK=$ANDROID_NDK_HOME -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" -DJAVA_AWT_LIBRARY=NotNeeded -DJAVA_JVM_LIBRARY=NotNeeded -DJAVA_INCLUDE_PATH2=NotNeeded -DJAVA_AWT_INCLUDE_PATH=NotNeeded ../ + cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_SYSTEM_VERSION=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} "-DCMAKE_ANDROID_NDK=$ANDROID_NDK_LATEST_HOME" -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" -DJAVA_AWT_LIBRARY=NotNeeded -DJAVA_JVM_LIBRARY=NotNeeded -DJAVA_INCLUDE_PATH2=NotNeeded -DJAVA_AWT_INCLUDE_PATH=NotNeeded ../ make -j $(nproc) tar -cvf z3-build-${{ matrix.android-abi }}.tar *.jar *.so - + - name: Archive production artifacts uses: actions/upload-artifact@v3 with: diff --git a/CMakeLists.txt b/CMakeLists.txt index 4b232f32d..14bc1bfc2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.9.2.0 LANGUAGES CXX C) +project(Z3 VERSION 4.11.0.0 LANGUAGES CXX C) ################################################################################ # Project version diff --git a/README.md b/README.md index 4849c33d8..2d75c73d6 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ Pre-built binaries for stable and nightly releases are available from [here](htt Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides [bindings for several programming languages][4]. -See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. +See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3. ## Build status diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 4b2834640..6b03a2576 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,19 @@ Version 4.next - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. +Version 4.11.0 +============== +- remove Z3_bool from API + +Version 4.10.2 +============== +- fix regression #6194. It broke mod/rem/div reasoning. +- fix user propagator scope management for equality callbacks. + +Version 4.10.1 +============== +- fix implementation of mk_fresh in user propagator for Python API + Version 4.10.0 ============== - Added API Z3_enable_concurrent_dec_ref to be set by interfaces that @@ -39,6 +52,7 @@ Version 4.10.0 of the form x = 0 - After (partial) completion, perform factorization for factors of the form x*y*p = 0 where x, are variables, p is linear. +- Added support for declaring algebraic datatypes from the C++ interface. Version 4.9.1 diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 41624b255..1c367e141 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -2171,7 +2171,6 @@ INCLUDE_FILE_PATTERNS = # This tag requires that the tag ENABLE_PREPROCESSING is set to YES. PREDEFINED = Z3_ast_opt:=Z3_ast \ - Z3_bool_opt:=Z3_bool \ Z3_func_interp_opt:=Z3_func_interp \ Z3_model_opt:=Z3_model \ __out_opt:=__out diff --git a/doc/z3code.dox b/doc/z3code.dox index b6a7fb088..f69fe2bed 100644 --- a/doc/z3code.dox +++ b/doc/z3code.dox @@ -816,7 +816,7 @@ INCLUDE_FILE_PATTERNS = # undefined via #undef or recursively expanded use the := operator # instead of the = operator. -PREDEFINED =Z3_ast_opt:=Z3_ast Z3_bool_opt:=Z3_bool Z3_func_interp_opt:=Z3_func_interp Z3_model_opt:=Z3_model __out_opt:=__out +PREDEFINED =Z3_ast_opt:=Z3_ast Z3_func_interp_opt:=Z3_func_interp Z3_model_opt:=Z3_model __out_opt:=__out # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then # this tag can be used to specify a list of macro names that should be expanded. @@ -825,7 +825,7 @@ PREDEFINED =Z3_ast_opt:=Z3_ast Z3_bool_opt:=Z3_bool Z3_func_interp_o EXPAND_AS_DEFINED = -# Z3_ast_opt Z3_bool_opt Z3_func_interp_opt Z3_model_opt __out_opt +# Z3_ast_opt Z3_func_interp_opt Z3_model_opt __out_opt # If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then # doxygen's preprocessor will remove all function-like macros that are alone diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 919e18a4a..dff6fc644 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 9, 2, 0) + set_version(4, 11, 0, 0) # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index fd93d4236..33bed5b55 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,8 +1,8 @@ variables: Major: '4' - Minor: '9' - Patch: '2' + Minor: '11' + Patch: '0' NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName) stages: diff --git a/scripts/release.yml b/scripts/release.yml index 419d4bc4b..f305e7c74 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.9.2' + ReleaseVersion: '4.11.0' stages: @@ -516,8 +516,9 @@ stages: inputs: command: push nuGetFeedType: External - publishFeedCredentials: Z3Nuget + publishFeedCredentials: $(NugetZ3) packagesToPush: $(Agent.TempDirectory)/*.nupkg + # Enable on release: - job: PyPIPublish diff --git a/scripts/update_api.py b/scripts/update_api.py index 8c6275c56..a468a6885 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1854,6 +1854,7 @@ _lib.Z3_solver_propagate_final.restype = None _lib.Z3_solver_propagate_fixed.restype = None _lib.Z3_solver_propagate_eq.restype = None _lib.Z3_solver_propagate_diseq.restype = None +_lib.Z3_solver_propagate_decide.restype = None on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p) _lib.Z3_optimize_register_model_eh.restype = None diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 79cad2fb2..5ef783c93 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -29,8 +29,6 @@ public: updt_params(p); } - ~ackermannize_bv_tactic() override { } - char const* name() const override { return "ackermannize_bv"; } void operator()(goal_ref const & g, goal_ref_buffer & result) override { diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 78fe6bef0..a38455e03 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -40,8 +40,6 @@ public: fixed_model(false) { } - ~ackr_model_converter() override { } - void get_units(obj_map& units) override { units.reset(); } void operator()(model_ref & md) override { diff --git a/src/ackermannization/lackr_model_converter_lazy.cpp b/src/ackermannization/lackr_model_converter_lazy.cpp index ec54b1d19..991fbed8e 100644 --- a/src/ackermannization/lackr_model_converter_lazy.cpp +++ b/src/ackermannization/lackr_model_converter_lazy.cpp @@ -28,8 +28,6 @@ public: , model_constructor(lmc) { } - ~lackr_model_converter_lazy() override { } - void operator()(model_ref & md) override { SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions())); SASSERT(model_constructor.get()); diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index d24a4a624..8416b0636 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -344,7 +344,6 @@ extern "C" { scoped_anum_vector const & m_as; public: vector_var2anum(scoped_anum_vector & as):m_as(as) {} - virtual ~vector_var2anum() {} algebraic_numbers::manager & m() const override { return m_as.m(); } bool contains(polynomial::var x) const override { return static_cast(x) < m_as.size(); } algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); } diff --git a/src/api/api_ast_vector.h b/src/api/api_ast_vector.h index fe6203cb9..dc1fcb8e6 100644 --- a/src/api/api_ast_vector.h +++ b/src/api/api_ast_vector.h @@ -26,7 +26,6 @@ namespace api { struct Z3_ast_vector_ref : public api::object { ast_ref_vector m_ast_vector; Z3_ast_vector_ref(api::context& c, ast_manager & m): api::object(c), m_ast_vector(m) {} - ~Z3_ast_vector_ref() override {} }; inline Z3_ast_vector_ref * to_ast_vector(Z3_ast_vector v) { return reinterpret_cast(v); } diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index cbe89e9fb..93d4e27e1 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -47,7 +47,7 @@ extern "C" { env_params::updt_params(); } - Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { + bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { memory::initialize(UINT_MAX); LOG_Z3_global_param_get(param_id, param_value); *param_value = nullptr; diff --git a/src/api/api_context.h b/src/api/api_context.h index 182958b1e..3bc0d4403 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,7 +58,7 @@ namespace api { solver_ref s; public: seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {} - lbool check_sat(expr* e) { + lbool check_sat(expr* e) override { if (!s) { s = mk_smt_solver(m, p, symbol("ALL")); } diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 8c6227d7d..19b488239 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -52,7 +52,6 @@ namespace api { m_context(m, m_register_engine, p), m_trail(m) {} - ~fixedpoint_context() override {} family_id get_family_id() const override { return const_cast(m_context).get_decl_util().get_family_id(); } void set_state(void* state) { SASSERT(!m_state); diff --git a/src/api/api_goal.h b/src/api/api_goal.h index 86f6a4331..56f48df91 100644 --- a/src/api/api_goal.h +++ b/src/api/api_goal.h @@ -23,7 +23,6 @@ Revision History: struct Z3_goal_ref : public api::object { goal_ref m_goal; Z3_goal_ref(api::context& c) : api::object(c) {} - ~Z3_goal_ref() override {} }; inline Z3_goal_ref * to_goal(Z3_goal g) { return reinterpret_cast(g); } diff --git a/src/api/api_model.h b/src/api/api_model.h index c05c86ceb..c04fc088d 100644 --- a/src/api/api_model.h +++ b/src/api/api_model.h @@ -23,7 +23,6 @@ Revision History: struct Z3_model_ref : public api::object { model_ref m_model; Z3_model_ref(api::context& c): api::object(c) {} - ~Z3_model_ref() override {} }; inline Z3_model_ref * to_model(Z3_model s) { return reinterpret_cast(s); } @@ -34,7 +33,6 @@ struct Z3_func_interp_ref : public api::object { model_ref m_model; // must have it to prevent reference to m_func_interp to be killed. func_interp * m_func_interp; Z3_func_interp_ref(api::context& c, model * m): api::object(c), m_model(m), m_func_interp(nullptr) {} - ~Z3_func_interp_ref() override {} }; inline Z3_func_interp_ref * to_func_interp(Z3_func_interp s) { return reinterpret_cast(s); } @@ -46,7 +44,6 @@ struct Z3_func_entry_ref : public api::object { func_interp * m_func_interp; func_entry const * m_func_entry; Z3_func_entry_ref(api::context& c, model * m):api::object(c), m_model(m), m_func_interp(nullptr), m_func_entry(nullptr) {} - ~Z3_func_entry_ref() override {} }; inline Z3_func_entry_ref * to_func_entry(Z3_func_entry s) { return reinterpret_cast(s); } diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 60d663638..7d8c00fbe 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -459,4 +459,33 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } +#if 0 + Z3_ast Z3_API Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort* srt) { + LOG_TRY; + LOG_Z3_mk_mpz_numeral(c, sign, n, nums, srt); + RESET_ERROR_CODE(); + rational z; + + // todo fill in z + if (!z.size()) + z.neg(); + arith_util & a = mk_c(c)->autil(); + auto* a = mk_c(c)->mk_numeral_core(r, a.mk_int_sort()); + Z3_CATCH_RETURN(nullptr); + + } + + Z3_ast Z3_API Z3_mk_mpq_numeral1(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]) { + LOG_TRY; + LOG_Z3_mk_mpq_numeral(c, sign, n, nums, d, dens); + RESET_ERROR_CODE(); + rational q; + + if (!sign) + q.neg(); + + Z3_CATCH_RETURN(nullptr); + } +#endif + }; diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 6355642fc..3a1fe7af1 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -47,8 +47,6 @@ extern "C" { ctx->register_plist(); ctx->set_ignore_check(true); } - - ~Z3_parser_context_ref() override {} }; inline Z3_parser_context_ref * to_parser_context(Z3_parser_context pc) { return reinterpret_cast(pc); } diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 5214d274c..71b7f9a46 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -51,7 +51,6 @@ struct Z3_solver_ref : public api::object { Z3_solver_ref(api::context& c, solver_factory * f): api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null), m_eh(nullptr) {} - ~Z3_solver_ref() override {} void assert_expr(expr* e); void assert_expr(expr* e, expr* t); diff --git a/src/api/api_stats.h b/src/api/api_stats.h index 209daafdd..ff6eeeea2 100644 --- a/src/api/api_stats.h +++ b/src/api/api_stats.h @@ -23,7 +23,6 @@ Revision History: struct Z3_stats_ref : public api::object { statistics m_stats; Z3_stats_ref(api::context& c): api::object(c) {} - ~Z3_stats_ref() override {} }; inline Z3_stats_ref * to_stats(Z3_stats s) { return reinterpret_cast(s); } diff --git a/src/api/api_tactic.h b/src/api/api_tactic.h index a4d0f263e..91e2d76ab 100644 --- a/src/api/api_tactic.h +++ b/src/api/api_tactic.h @@ -28,13 +28,11 @@ namespace api { struct Z3_tactic_ref : public api::object { tactic_ref m_tactic; Z3_tactic_ref(api::context& c): api::object(c) {} - ~Z3_tactic_ref() override {} }; struct Z3_probe_ref : public api::object { probe_ref m_probe; Z3_probe_ref(api::context& c):api::object(c) {} - ~Z3_probe_ref() override {} }; inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast(g); } @@ -50,7 +48,6 @@ struct Z3_apply_result_ref : public api::object { model_converter_ref m_mc; proof_converter_ref m_pc; Z3_apply_result_ref(api::context& c, ast_manager & m); - ~Z3_apply_result_ref() override {} }; inline Z3_apply_result_ref * to_apply_result(Z3_apply_result g) { return reinterpret_cast(g); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5f630d814..2731d6d27 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3414,7 +3414,7 @@ namespace z3 { } }; - constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) { + inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) { array cons(cs.size()); for (unsigned i = 0; i < cs.size(); ++i) cons[i] = cs[i]; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 764beb470..8896904dd 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -938,6 +938,15 @@ namespace Microsoft.Z3 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } + /// + /// Creates a distinct term. + /// + public BoolExpr MkDistinct(IEnumerable args) + { + Debug.Assert(args != null); + return MkDistinct(args.ToArray()); + } + /// /// Mk an expression representing not(a). /// diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md index e4c385680..42d58a916 100644 --- a/src/api/js/PUBLISHED_README.md +++ b/src/api/js/PUBLISHED_README.md @@ -103,7 +103,7 @@ function rcf_get_numerator_denominator(c: Z3_context, a: Z3_rcf_num): { n: Z3_rc When there is only a single out parameter, and the return value is not otherwise of interest, the parameter is not wrapped. For example, the C declaration ```c -Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); +bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); ``` is represented in the TS bindings as diff --git a/src/api/js/scripts/parse-api.ts b/src/api/js/scripts/parse-api.ts index 3c8b37be0..cee61ca29 100644 --- a/src/api/js/scripts/parse-api.ts +++ b/src/api/js/scripts/parse-api.ts @@ -16,7 +16,6 @@ const files = [ const aliases = { __proto__: null, - Z3_bool: 'boolean', Z3_string: 'string', bool: 'boolean', signed: 'int', diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 489d4acdb..a5e27429b 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -498,6 +498,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return result; } + /////////////////////////////// + // expression simplification // + /////////////////////////////// + + async function simplify(e : Expr) { + const result = await Z3.simplify(contextPtr, e.ast) + return _toExpr(check(result)); + } + ///////////// // Objects // ///////////// @@ -1050,6 +1059,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return check(Z3.model_to_string(contextPtr, this.ptr)); } + toString() { + return this.sexpr(); + } + eval(expr: Bool, modelCompletion?: boolean): Bool; eval(expr: Arith, modelCompletion?: boolean): Arith; eval(expr: Expr, modelCompletion: boolean = false) { diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 7d1f43629..f78963344 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -133,7 +133,7 @@ def _configure_z3(): # Allow command-line arguments to add and override Z3_ options for i in range(len(sys.argv) - 1): key = sys.argv[i] - if key.starts_with("Z3_"): + if key.startswith("Z3_"): val = sys.argv[i + 1].upper() if val == "TRUE" or val == "FALSE": cmake_options[key] = val diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 11dcedbe8..8f227649c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -204,12 +204,13 @@ class Context: Z3_set_param_value(conf, str(prev), _to_param_value(a)) prev = None self.ctx = Z3_mk_context_rc(conf) + self.owner = True self.eh = Z3_set_error_handler(self.ctx, z3_error_handler) Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT) Z3_del_config(conf) def __del__(self): - if Z3_del_context is not None: + if Z3_del_context is not None and self.owner: Z3_del_context(self.ctx) self.ctx = None self.eh = None @@ -11363,16 +11364,18 @@ def to_ContextObj(ptr,): return ctx -def user_prop_fresh(ctx, new_ctx): +def user_prop_fresh(ctx, _new_ctx): _prop_closures.set_threaded() prop = _prop_closures.get(ctx) nctx = Context() - new_ctx = to_ContextObj(new_ctx) + Z3_del_context(nctx.ctx) + new_ctx = to_ContextObj(_new_ctx) nctx.ctx = new_ctx nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler) + nctx.owner = False new_prop = prop.fresh(nctx) _prop_closures.set(new_prop.id, new_prop) - return ctypes.c_void_p(new_prop.id) + return new_prop.id def to_Ast(ptr,): ast = Ast(ptr) @@ -11387,6 +11390,13 @@ def user_prop_fixed(ctx, cb, id, value): prop.fixed(id, value) prop.cb = None +def user_prop_created(ctx, cb, id): + prop = _prop_closures.get(ctx) + prop.cb = cb + id = _to_expr_ref(to_Ast(id), prop.ctx()) + prop.created(id) + prop.cb = None + def user_prop_final(ctx, cb): prop = _prop_closures.get(ctx) prop.cb = cb @@ -11409,15 +11419,50 @@ def user_prop_diseq(ctx, cb, x, y): prop.diseq(x, y) prop.cb = None +# TODO The decision callback is not fully implemented. +# It needs to handle the ast*, unsigned* idx, and Z3_lbool* +def user_prop_decide(ctx, cb, t_ref, idx_ref, phase_ref): + prop = _prop_closures.get(ctx) + prop.cb = cb + t = _to_expr_ref(to_Ast(t_ref), prop.ctx()) + t, idx, phase = prop.decide(t, idx, phase) + t_ref = t + idx_ref = idx + phase_ref = phase + prop.cb = None + _user_prop_push = Z3_push_eh(user_prop_push) _user_prop_pop = Z3_pop_eh(user_prop_pop) _user_prop_fresh = Z3_fresh_eh(user_prop_fresh) _user_prop_fixed = Z3_fixed_eh(user_prop_fixed) +_user_prop_created = Z3_created_eh(user_prop_created) _user_prop_final = Z3_final_eh(user_prop_final) _user_prop_eq = Z3_eq_eh(user_prop_eq) _user_prop_diseq = Z3_eq_eh(user_prop_diseq) +_user_prop_decide = Z3_decide_eh(user_prop_decide) +def PropagateFunction(name, *sig): + """Create a function that gets tracked by user propagator. + Every term headed by this function symbol is tracked. + If a term is fixed and the fixed callback is registered a + callback is invoked that the term headed by this function is fixed. + """ + sig = _get_args(sig) + if z3_debug(): + _z3_assert(len(sig) > 0, "At least two arguments expected") + arity = len(sig) - 1 + rng = sig[arity] + if z3_debug(): + _z3_assert(is_sort(rng), "Z3 sort expected") + dom = (Sort * arity)() + for i in range(arity): + if z3_debug(): + _z3_assert(is_sort(sig[i]), "Z3 sort expected") + dom[i] = sig[i].ast + ctx = rng.ctx + return FuncDeclRef(Z3_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx) + class UserPropagateBase: @@ -11440,6 +11485,7 @@ class UserPropagateBase: self.final = None self.eq = None self.diseq = None + self.created = None if ctx: self.fresh_ctx = ctx if s: @@ -11470,6 +11516,13 @@ class UserPropagateBase: Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed) self.fixed = fixed + def add_created(self, created): + assert not self.created + assert not self._ctx + if self.solver: + Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created) + self.created = created + def add_final(self, final): assert not self.final assert not self._ctx @@ -11491,6 +11544,13 @@ class UserPropagateBase: Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq) self.diseq = diseq + def add_decide(self, decide): + assert not self.decide + assert not self._ctx + if self.solver: + Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide) + self.decide = decide + def push(self): raise Z3Exception("push needs to be overwritten") @@ -11501,10 +11561,20 @@ class UserPropagateBase: raise Z3Exception("fresh needs to be overwritten") def add(self, e): - assert self.solver assert not self._ctx - Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast) - + if self.solver: + Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast) + else: + Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast) + + # + # Tell the solver to perform the next split on a given term + # If the term is a bit-vector the index idx specifies the index of the Boolean variable being + # split on. A phase of true = 1/false = -1/undef = 0 = let solver decide is the last argument. + # + def next_split(self, t, idx, phase): + Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase) + # # Propagation can only be invoked as during a fixed or final callback. # @@ -11516,5 +11586,5 @@ class UserPropagateBase: Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p( self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast) - def conflict(self, deps): - self.propagate(BoolVal(False, self.ctx()), deps, eqs=[]) + def conflict(self, deps = [], eqs = []): + self.propagate(BoolVal(False, self.ctx()), deps, eqs) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2820205b9..6beee6d90 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1528,7 +1528,7 @@ extern "C" { def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING))) */ - Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value); + bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value); /**@}*/ @@ -3387,6 +3387,39 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty); +#if 0 + /** + \brief Create an integer numeral from a vector of unsigned numerals. + + \param c - context + \param sign - true if positive, false if negative + \param n - length of array of numerals + \param nums - array of numerals + \param s - sort of numeral (int, real, bit-vector). + + future_('Z3_mk_mpz_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(SORT))) + */ + + Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s); + + /** + \brief Create a rational numeral from a vector of unsigned numerals. + + \param c - context + \param sign - true if positive, false if negative + \param n - length of array of nominator numerals + \param nums - array of numerator numerals + \param d - length of array of denominator numerals + \param dens - array of denominator numerals + + The sort of returned numeral is Real. + + future_('Z3_mk_mpq_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT))) + */ + + Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]); +#endif + /** \brief Create a real from a fraction. @@ -4407,7 +4440,7 @@ extern "C" { def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64))) */ - Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r); + bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r); /** \brief Return the domain of the given array sort. @@ -4822,6 +4855,8 @@ extern "C" { \brief Return the number of argument of an application. If \c t is an constant, then the number of arguments is 0. + \sa Z3_get_app_arg + def_API('Z3_get_app_num_args', UINT, (_in(CONTEXT), _in(APP))) */ unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a); @@ -4831,6 +4866,8 @@ extern "C" { \pre i < Z3_get_app_num_args(c, a) + \sa Z3_get_app_num_args + def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT))) */ Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i); @@ -5376,7 +5413,7 @@ extern "C" { def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST))) */ - Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); + bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); /** \brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m. @@ -5425,6 +5462,7 @@ extern "C" { \pre i < Z3_model_get_num_consts(c, m) \sa Z3_model_eval + \sa Z3_model_get_num_consts def_API('Z3_model_get_const_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) */ @@ -5436,6 +5474,8 @@ extern "C" { A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. + \sa Z3_model_get_func_decl + def_API('Z3_model_get_num_funcs', UINT, (_in(CONTEXT), _in(MODEL))) */ unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m); @@ -5561,6 +5601,8 @@ extern "C" { Each entry in the finite map represents the value of a function given a set of arguments. This procedure return the number of element in the finite map of \c f. + \sa Z3_func_interp_get_entry + def_API('Z3_func_interp_get_num_entries', UINT, (_in(CONTEXT), _in(FUNC_INTERP))) */ unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f); @@ -5649,6 +5691,7 @@ extern "C" { /** \brief Return the number of arguments in a \c Z3_func_entry object. + \sa Z3_func_entry_get_arg \sa Z3_func_interp_get_entry def_API('Z3_func_entry_get_num_args', UINT, (_in(CONTEXT), _in(FUNC_ENTRY))) @@ -5660,6 +5703,7 @@ extern "C" { \pre i < Z3_func_entry_get_num_args(c, e) + \sa Z3_func_entry_get_num_args \sa Z3_func_interp_get_entry def_API('Z3_func_entry_get_arg', AST, (_in(CONTEXT), _in(FUNC_ENTRY), _in(UINT))) @@ -5672,6 +5716,9 @@ extern "C" { /** \brief Log interaction to a file. + \sa Z3_append_log + \sa Z3_close_log + extra_API('Z3_open_log', INT, (_in(STRING),)) */ bool Z3_API Z3_open_log(Z3_string filename); @@ -5679,10 +5726,13 @@ extern "C" { /** \brief Append user-defined string to interaction log. - The interaction log is opened using Z3_open_log. + The interaction log is opened using #Z3_open_log. It contains the formulas that are checked using Z3. You can use this command to append comments, for instance. + \sa Z3_open_log + \sa Z3_close_log + extra_API('Z3_append_log', VOID, (_in(STRING),)) */ void Z3_API Z3_append_log(Z3_string string); @@ -5690,6 +5740,9 @@ extern "C" { /** \brief Close interaction log. + \sa Z3_open_log + \sa Z3_append_log + extra_API('Z3_close_log', VOID, ()) */ void Z3_API Z3_close_log(void); @@ -6388,6 +6441,8 @@ extern "C" { /** \brief Return the number of builtin tactics available in Z3. + \sa Z3_get_tactic_name + def_API('Z3_get_num_tactics', UINT, (_in(CONTEXT),)) */ unsigned Z3_API Z3_get_num_tactics(Z3_context c); @@ -6397,6 +6452,8 @@ extern "C" { \pre i < Z3_get_num_tactics(c) + \sa Z3_get_num_tactics + def_API('Z3_get_tactic_name', STRING, (_in(CONTEXT), _in(UINT))) */ Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i); @@ -6404,6 +6461,8 @@ extern "C" { /** \brief Return the number of builtin probes available in Z3. + \sa Z3_get_probe_name + def_API('Z3_get_num_probes', UINT, (_in(CONTEXT),)) */ unsigned Z3_API Z3_get_num_probes(Z3_context c); @@ -6413,6 +6472,8 @@ extern "C" { \pre i < Z3_get_num_probes(c) + \sa Z3_get_num_probes + def_API('Z3_get_probe_name', STRING, (_in(CONTEXT), _in(UINT))) */ Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i); @@ -6456,6 +6517,8 @@ extern "C" { /** \brief Apply tactic \c t to the goal \c g. + \sa Z3_tactic_apply_ex + def_API('Z3_tactic_apply', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL))) */ Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g); @@ -6463,6 +6526,8 @@ extern "C" { /** \brief Apply tactic \c t to the goal \c g using the parameter set \c p. + \sa Z3_tactic_apply + def_API('Z3_tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS))) */ Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p); @@ -6491,6 +6556,8 @@ extern "C" { /** \brief Return the number of subgoals in the \c Z3_apply_result object returned by #Z3_tactic_apply. + \sa Z3_apply_result_get_subgoal + def_API('Z3_apply_result_get_num_subgoals', UINT, (_in(CONTEXT), _in(APPLY_RESULT))) */ unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r); @@ -6500,6 +6567,8 @@ extern "C" { \pre i < Z3_apply_result_get_num_subgoals(c, r) + \sa Z3_apply_result_get_num_subgoals + def_API('Z3_apply_result_get_subgoal', GOAL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT))) */ Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i); @@ -6542,6 +6611,10 @@ extern "C" { \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + \sa Z3_mk_simple_solver + \sa Z3_mk_solver_for_logic + \sa Z3_mk_solver_from_tactic + def_API('Z3_mk_solver', SOLVER, (_in(CONTEXT),)) */ Z3_solver Z3_API Z3_mk_solver(Z3_context c); @@ -6569,6 +6642,10 @@ extern "C" { \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + \sa Z3_mk_solver + \sa Z3_mk_solver_for_logic + \sa Z3_mk_solver_from_tactic + def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),)) */ Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c); @@ -6580,6 +6657,10 @@ extern "C" { \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + \sa Z3_mk_solver + \sa Z3_mk_simple_solver + \sa Z3_mk_solver_from_tactic + def_API('Z3_mk_solver_for_logic', SOLVER, (_in(CONTEXT), _in(SYMBOL))) */ Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic); @@ -6592,6 +6673,10 @@ extern "C" { \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + \sa Z3_mk_solver + \sa Z3_mk_simple_solver + \sa Z3_mk_solver_for_logic + def_API('Z3_mk_solver_from_tactic', SOLVER, (_in(CONTEXT), _in(TACTIC))) */ Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t); @@ -6899,7 +6984,7 @@ extern "C" { /** Create uninterpreted function declaration for the user propagator. When expressions using the function are created by the solver invoke a callback - to \ref \Z3_solver_propagate_created with arguments + to \ref Z3_solver_propagate_created with arguments 1. context and callback solve 2. declared_expr: expression using function that was used as the top-level symbol 3. declared_id: a unique identifier (unique within the current scope) to track the expression. diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 646209575..2c95e18ca 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -16,6 +16,8 @@ Author: Notes: --*/ +#pragma once + #include "util/symbol.h" void R(); diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h index 08756cf15..5f8659379 100644 --- a/src/api/z3_macros.h +++ b/src/api/z3_macros.h @@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ - +#pragma once #ifndef Z3_API # ifdef __GNUC__ diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 51f380243..6fe2c7657 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -107,7 +107,6 @@ class array_decl_plugin : public decl_plugin { bool is_array_sort(sort* s) const; public: array_decl_plugin(); - ~array_decl_plugin() override {} decl_plugin * mk_fresh() override { return alloc(array_decl_plugin); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 473bd82b5..c51ea4e32 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1429,7 +1429,7 @@ ast_manager::~ast_manager() { } m_plugins.reset(); while (!m_ast_table.empty()) { - DEBUG_CODE(IF_VERBOSE(0, verbose_stream() << "ast_manager LEAKED: " << m_ast_table.size() << std::endl);); + DEBUG_CODE(IF_VERBOSE(1, verbose_stream() << "ast_manager LEAKED: " << m_ast_table.size() << std::endl);); ptr_vector roots; ast_mark mark; for (ast * n : m_ast_table) { @@ -1465,22 +1465,21 @@ ast_manager::~ast_manager() { break; } } - for (ast * n : m_ast_table) { - if (!mark.is_marked(n)) { + for (ast * n : m_ast_table) + if (!mark.is_marked(n)) roots.push_back(n); - } - } + SASSERT(!roots.empty()); for (unsigned i = 0; i < roots.size(); ++i) { ast* a = roots[i]; DEBUG_CODE( - std::cout << "Leaked: "; - if (is_sort(a)) { - std::cout << to_sort(a)->get_name() << "\n"; - } - else { - std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n"; - }); + IF_VERBOSE(1, + verbose_stream() << "Leaked: "; + if (is_sort(a)) + verbose_stream() << to_sort(a)->get_name() << "\n"; + else + verbose_stream() << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n"; + );); a->m_ref_count = 0; delete_node(a); } diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp index 7f717df96..46f39ffde 100644 --- a/src/ast/ast_printer.cpp +++ b/src/ast/ast_printer.cpp @@ -26,7 +26,6 @@ class simple_ast_printer_context : public ast_printer_context { smt2_pp_environment_dbg & env() const { return *(m_env.get()); } public: simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); } - ~simple_ast_printer_context() override {} ast_manager & m() const { return m_manager; } ast_manager & get_ast_manager() override { return m_manager; } void display(std::ostream & out, sort * s, unsigned indent = 0) const override { out << mk_ismt2_pp(s, m(), indent); } diff --git a/src/ast/ast_printer.h b/src/ast/ast_printer.h index d57a9b845..37023393f 100644 --- a/src/ast/ast_printer.h +++ b/src/ast/ast_printer.h @@ -45,7 +45,6 @@ public: class ast_printer_context : public ast_printer { public: - ~ast_printer_context() override {} virtual ast_manager & get_ast_manager() = 0; virtual std::ostream & regular_stream(); virtual std::ostream & diagnostic_stream(); diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 598124c5c..60efc73a9 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -241,7 +241,6 @@ protected: public: bv_decl_plugin(); - ~bv_decl_plugin() override {} void finalize() override; decl_plugin * mk_fresh() override { return alloc(bv_decl_plugin); } diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 39cdbf835..c1cf08719 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -101,7 +101,6 @@ namespace datalog { public: dl_decl_plugin(); - ~dl_decl_plugin() override {} decl_plugin * mk_fresh() override { return alloc(dl_decl_plugin); } diff --git a/src/ast/format.cpp b/src/ast/format.cpp index 4aeaf183d..a14d4b758 100644 --- a/src/ast/format.cpp +++ b/src/ast/format.cpp @@ -52,8 +52,6 @@ namespace format_ns { m_line_break_ext("cr++") { } - ~format_decl_plugin() override {} - void finalize() override { if (m_format_sort) m_manager->dec_ref(m_format_sort); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index d663fda95..19315129a 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -239,7 +239,6 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter { fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) : fpa2bv_converter(m), m_rw(rw) {} - virtual ~fpa2bv_converter_wrapped() {} void mk_const(func_decl * f, expr_ref & result) override; void mk_rm_const(func_decl * f, expr_ref & result) override; app_ref wrap(expr * e); diff --git a/src/ast/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp index bb2543b3e..c500d92bd 100644 --- a/src/ast/normal_forms/name_exprs.cpp +++ b/src/ast/normal_forms/name_exprs.cpp @@ -77,9 +77,6 @@ public: m_rw(m, m.proofs_enabled(), m_cfg) { } - ~name_exprs_core() override { - } - void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override { m_cfg.m_def_exprs = &new_defs; m_cfg.m_def_proofs = &new_def_proofs; @@ -113,9 +110,6 @@ public: name_exprs_core(m, n, m_pred), m_pred(m) { } - - ~name_quantifier_labels() override { - } }; name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n) { @@ -145,9 +139,6 @@ public: m_pred(m) { } - ~name_nested_formulas() override { - } - void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override { m_pred.m_root = n; TRACE("name_exprs", tout << "operator()\n";); diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index 372e7b06f..89f566263 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -52,7 +52,6 @@ class pb_decl_plugin : public decl_plugin { func_decl * mk_eq(unsigned arity, rational const* coeffs, int k); public: pb_decl_plugin(); - ~pb_decl_plugin() override {} sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { UNREACHABLE(); diff --git a/src/ast/proofs/proof_checker.h b/src/ast/proofs/proof_checker.h index 27f872d25..591fb1157 100644 --- a/src/ast/proofs/proof_checker.h +++ b/src/ast/proofs/proof_checker.h @@ -52,8 +52,6 @@ class proof_checker { public: hyp_decl_plugin(); - ~hyp_decl_plugin() override {} - void finalize() override; decl_plugin * mk_fresh() override { return alloc(hyp_decl_plugin); } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index ae125a0ad..dc1df22a3 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -16,6 +16,8 @@ Author: Revision History: --*/ +#pragma once + #include "util/rational.h" #include "util/common_msgs.h" #include "ast/rewriter/bit_blaster/bit_blaster_tpl.h" diff --git a/src/ast/rewriter/elim_bounds.h b/src/ast/rewriter/elim_bounds.h index 378ac20cc..99d002f98 100644 --- a/src/ast/rewriter/elim_bounds.h +++ b/src/ast/rewriter/elim_bounds.h @@ -68,8 +68,6 @@ public: rewriter_tpl(m, m.proofs_enabled(), m_cfg), m_cfg(m) {} - - ~elim_bounds_rw() override {} }; diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index e822c1775..4fa83bed0 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -129,8 +129,6 @@ public: m_r(m, p) { } - ~th_rewriter2expr_replacer() override {} - ast_manager & m() const override { return m_r.m(); } void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); } diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index eb72ddd67..0a17fc375 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -16,6 +16,7 @@ Author: Notes: --*/ +#pragma once #include "util/container_util.h" #include "ast/rewriter/poly_rewriter.h" diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h index a2e18dd25..67c48c7ae 100644 --- a/src/ast/rewriter/push_app_ite.h +++ b/src/ast/rewriter/push_app_ite.h @@ -49,7 +49,6 @@ protected: bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override; public: ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {} - virtual ~ng_push_app_ite_cfg() {} }; struct push_app_ite_rw : public rewriter_tpl { diff --git a/src/ast/rewriter/recfun_replace.h b/src/ast/rewriter/recfun_replace.h index 09ee3c60d..edc0283a8 100644 --- a/src/ast/rewriter/recfun_replace.h +++ b/src/ast/rewriter/recfun_replace.h @@ -32,7 +32,6 @@ class recfun_replace : public recfun::replace { expr_safe_replace m_replace; public: recfun_replace(ast_manager& m): m(m), m_replace(m) {} - ~recfun_replace() override {} void reset() override { m_replace.reset(); } void insert(expr* s, expr* t) override { m_replace.insert(s, t); } expr_ref operator()(expr* e) override { expr_ref r(m); m_replace(e, r); return r; } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 4bf829be6..e9b9c316a 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -16,6 +16,8 @@ Author: Notes: --*/ +#pragma once + #include "ast/rewriter/rewriter.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index bf377df43..54ef58e32 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1107,6 +1107,31 @@ unsigned seq_util::rex::max_length(expr* r) const { return UINT_MAX; } +/** + \brief determine if \c n is a range regular expression where the lower and upper bounds + are given by single characters. + Range expressions where lower and upper bounds are not single characters are either + the empty language (when a bound is a string but not a single character) or symbolic + (when both bounds are not ground strings). The general is_range can be used to process + range expressions for these cases, but they don't correspond to mainstream regex usage. + */ +bool seq_util::rex::is_range(expr const* n, unsigned& lo, unsigned& hi) const { + expr* _lo, *_hi; + zstring los, his; + if (!is_range(n, _lo, _hi)) + return false; + if (!u.str.is_string(_lo, los)) + return false; + if (!u.str.is_string(_hi, his)) + return false; + if (los.length() != 1 || his.length() != 1) + return false; + lo = los[0]; + hi = his[0]; + return true; +} + + sort* seq_util::rex::to_seq(sort* re) { (void)u; SASSERT(u.is_re(re)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index b0c3ab3c6..d5c6da187 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -545,6 +545,7 @@ public: bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); } bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); } + bool is_range(expr const* n, unsigned& lo, unsigned& hi) const; bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); } bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); } bool is_full_char(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_CHAR_SET); } diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index d804fa179..daff802e7 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -40,8 +40,6 @@ class special_relations_decl_plugin : public decl_plugin { public: special_relations_decl_plugin(); - ~special_relations_decl_plugin() override {} - decl_plugin * mk_fresh() override { return alloc(special_relations_decl_plugin); } diff --git a/src/ast/value_generator.cpp b/src/ast/value_generator.cpp index ef21f2444..6e52afba3 100644 --- a/src/ast/value_generator.cpp +++ b/src/ast/value_generator.cpp @@ -99,7 +99,7 @@ public: datatype_value_generator(value_generator& g, ast_manager& m): m(m), g(g), dt(m), m_sorts(m) {} - ~datatype_value_generator() { + ~datatype_value_generator() override { for (auto& kv : m_values) dealloc(kv.m_value); } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index dc8836138..b17bc3641 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -379,8 +379,6 @@ public: m_int_real_coercions(":int-real-coercions"), m_reproducible_resource_limit(":reproducible-resource-limit") { } - ~set_get_option_cmd() override {} - }; class set_option_cmd : public set_get_option_cmd { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 32dd6aee5..644bf5c7b 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -493,7 +493,6 @@ protected: public: pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dtutil(o.m()), m_dlutil(o.m()) {} - ~pp_env() override {} ast_manager & get_manager() const override { return m_owner.m(); } arith_util & get_autil() override { return m_autil; } bv_util & get_bvutil() override { return m_bvutil; } diff --git a/src/cmd_context/extra_cmds/subpaving_cmds.h b/src/cmd_context/extra_cmds/subpaving_cmds.h index 33ed347b7..651d5b161 100644 --- a/src/cmd_context/extra_cmds/subpaving_cmds.h +++ b/src/cmd_context/extra_cmds/subpaving_cmds.h @@ -15,6 +15,7 @@ Author: Notes: --*/ +#pragma once class cmd_context; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 1545487c7..5c7058bb5 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -147,7 +147,6 @@ class psort_sort : public psort { sort * get_sort() const { return m_sort; } sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override { return m_sort; } public: - ~psort_sort() override {} bool is_sort_wrapper() const override { return true; } char const * hcons_kind() const override { return "psort_sort"; } unsigned hcons_hash() const override { return m_sort->get_id(); } @@ -171,7 +170,6 @@ class psort_var : public psort { } size_t obj_size() const override { return sizeof(psort_var); } public: - ~psort_var() override {} char const * hcons_kind() const override { return "psort_var"; } unsigned hcons_hash() const override { return hash_u_u(m_num_params, m_idx); } bool hcons_eq(psort const * other) const override { @@ -233,7 +231,6 @@ class psort_app : public psort { } public: - ~psort_app() override {} char const * hcons_kind() const override { return "psort_app"; } unsigned hcons_hash() const override { return get_composite_hash(const_cast(this), m_args.size()); @@ -800,8 +797,6 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { m.m().inc_array_ref(n, s); } - ~app_sort_info() override {} - unsigned obj_size() const override { return sizeof(app_sort_info); } void finalize(pdecl_manager & m) override { @@ -843,8 +838,6 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { m_indices(n, s) { } - ~indexed_sort_info() override {} - unsigned obj_size() const override { return sizeof(indexed_sort_info); } void display(std::ostream & out, pdecl_manager const & m) const override { diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 4f9c56825..66e1e5e81 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -66,7 +66,6 @@ protected: psort(unsigned id, unsigned num_params):pdecl(id, num_params), m_inst_cache(nullptr) {} bool is_psort() const override { return true; } void finalize(pdecl_manager & m) override; - ~psort() override {} virtual void cache(pdecl_manager & m, sort * const * s, sort * r); virtual sort * find(sort * const * s) const; public: @@ -98,7 +97,6 @@ protected: sort * find(sort * const * s); psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n); void finalize(pdecl_manager & m) override; - ~psort_decl() override {} public: virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) = 0; virtual sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) { return nullptr; } @@ -120,7 +118,6 @@ protected: psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p); size_t obj_size() const override { return sizeof(psort_user_decl); } void finalize(pdecl_manager & m) override; - ~psort_user_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; std::ostream& display(std::ostream & out) const override; @@ -133,7 +130,6 @@ protected: decl_kind m_kind; psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k); size_t obj_size() const override { return sizeof(psort_builtin_decl); } - ~psort_builtin_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override; @@ -145,7 +141,6 @@ protected: friend class pdecl_manager; psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n); size_t obj_size() const override { return sizeof(psort_dt_decl); } - ~psort_dt_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; std::ostream& display(std::ostream & out) const override; @@ -196,7 +191,6 @@ class paccessor_decl : public pdecl { accessor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s); symbol const & get_name() const { return m_name; } ptype const & get_type() const { return m_type; } - ~paccessor_decl() override {} public: std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; @@ -217,7 +211,6 @@ class pconstructor_decl : public pdecl { symbol const & get_name() const { return m_name; } symbol const & get_recognizer_name() const { return m_recogniser_name; } constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s); - ~pconstructor_decl() override {} public: std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; @@ -234,7 +227,6 @@ class pdatatype_decl : public psort_decl { size_t obj_size() const override { return sizeof(pdatatype_decl); } bool fix_missing_refs(dictionary const & symbol2idx, symbol & missing); datatype_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s); - ~pdatatype_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; std::ostream& display(std::ostream & out) const override; @@ -255,7 +247,6 @@ class pdatatypes_decl : public pdecl { size_t obj_size() const override { return sizeof(pdatatypes_decl); } bool fix_missing_refs(symbol & missing); bool instantiate(pdecl_manager & m, sort * const * s); - ~pdatatypes_decl() override {} public: pdatatype_decl const * const * children() const { return m_datatypes.data(); } pdatatype_decl * const * begin() const { return m_datatypes.begin(); } diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp index 0c389a78a..d5200374c 100644 --- a/src/cmd_context/simplify_cmd.cpp +++ b/src/cmd_context/simplify_cmd.cpp @@ -46,10 +46,7 @@ public: p.insert("print_proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one."); p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } - - ~simplify_cmd() override { - } - + void prepare(cmd_context & ctx) override { parametric_cmd::prepare(ctx); m_target = nullptr; diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h index 4bd80af4b..8c1ca55e6 100644 --- a/src/math/automata/boolean_algebra.h +++ b/src/math/automata/boolean_algebra.h @@ -38,7 +38,6 @@ public: template class boolean_algebra : public positive_boolean_algebra { public: - ~boolean_algebra() override {} virtual T mk_not(T x) = 0; }; diff --git a/src/math/dd/pdd_eval.h b/src/math/dd/pdd_eval.h index f7682927f..9872935cf 100644 --- a/src/math/dd/pdd_eval.h +++ b/src/math/dd/pdd_eval.h @@ -17,6 +17,8 @@ Author: Revision History: --*/ +#pragma once + #include "math/dd/dd_pdd.h" namespace dd { diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index d8e2b8db1..c5b4c9e1c 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -17,6 +17,8 @@ Author: Revision History: --*/ +#pragma once + #include "math/dd/dd_pdd.h" #include "math/interval/dep_intervals.h" diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h index 7d4179de8..fcdce7311 100644 --- a/src/math/hilbert/heap_trie.h +++ b/src/math/hilbert/heap_trie.h @@ -80,7 +80,6 @@ class heap_trie { Value m_value; public: leaf(): node(leaf_t) {} - ~leaf() override {} Value const& get_value() const { return m_value; } void set_value(Value const& v) { m_value = v; } void display(std::ostream& out, unsigned indent) const override { @@ -98,9 +97,6 @@ class heap_trie { public: trie(): node(trie_t) {} - ~trie() override { - } - node* find_or_insert(Key k, node* n) { for (unsigned i = 0; i < m_nodes.size(); ++i) { if (m_nodes[i].first == k) { diff --git a/src/math/lp/binary_heap_priority_queue_def.h b/src/math/lp/binary_heap_priority_queue_def.h index c17d70fb2..0e640d949 100644 --- a/src/math/lp/binary_heap_priority_queue_def.h +++ b/src/math/lp/binary_heap_priority_queue_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "util/vector.h" #include "math/lp/binary_heap_priority_queue.h" namespace lp { diff --git a/src/math/lp/binary_heap_upair_queue_def.h b/src/math/lp/binary_heap_upair_queue_def.h index a74f9e46a..65485a6eb 100644 --- a/src/math/lp/binary_heap_upair_queue_def.h +++ b/src/math/lp/binary_heap_upair_queue_def.h @@ -17,6 +17,7 @@ Revision History: --*/ +#pragma once #include #include "math/lp/lp_utils.h" diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index 2f54b175a..23417b691 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include #include diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h index f781dbf8f..8eb9ad5dd 100644 --- a/src/math/lp/dense_matrix_def.h +++ b/src/math/lp/dense_matrix_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "math/lp/lp_settings.h" #ifdef Z3DEBUG #include "util/vector.h" diff --git a/src/math/lp/factorization_factory_imp.h b/src/math/lp/factorization_factory_imp.h index b404d5f14..599039094 100644 --- a/src/math/lp/factorization_factory_imp.h +++ b/src/math/lp/factorization_factory_imp.h @@ -28,8 +28,8 @@ namespace nla { const monic& m_rm; factorization_factory_imp(const monic& rm, const core& s); - bool find_canonical_monic_of_vars(const svector& vars, unsigned & i) const; - virtual bool canonize_sign(const monic& m) const; - virtual bool canonize_sign(const factorization& m) const; + bool find_canonical_monic_of_vars(const svector& vars, unsigned & i) const override; + bool canonize_sign(const monic& m) const override; + bool canonize_sign(const factorization& m) const override; }; } diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h index 443ca160e..0e25ee271 100644 --- a/src/math/lp/indexed_vector_def.h +++ b/src/math/lp/indexed_vector_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "util/vector.h" #include "math/lp/indexed_vector.h" #include "math/lp/lp_settings.h" diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index f20aa7e6b..939a05114 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -9,6 +9,8 @@ Revision History: --*/ +#pragma once + #include #include "util/vector.h" #include "math/lp/lar_core_solver.h" diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index f1cbd3370..cce63855d 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -543,7 +543,7 @@ public: void get_model(std::unordered_map & variable_values) const; void get_rid_of_inf_eps(); void get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const; - std::string get_variable_name(var_index vi) const; + std::string get_variable_name(var_index vi) const override; void set_variable_name(var_index vi, std::string); inline unsigned number_of_vars() const { return m_var_register.size(); } inline bool is_base(unsigned j) const { return m_mpq_lar_core_solver.m_r_heading[j] >= 0; } @@ -651,7 +651,7 @@ public: lar_solver(); void set_track_pivoted_rows(bool v); bool get_track_pivoted_rows() const; - virtual ~lar_solver(); + ~lar_solver() override; const vector& r_x() const { return m_mpq_lar_core_solver.m_r_x; } bool column_is_int(unsigned j) const; inline bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 42c2ddcf7..c1b64492b 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include #include "util/vector.h" diff --git a/src/math/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h index 4a847fe85..b42d644af 100644 --- a/src/math/lp/lp_dual_core_solver_def.h +++ b/src/math/lp/lp_dual_core_solver_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include #include "util/vector.h" diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h index c21429c88..8af9d87c1 100644 --- a/src/math/lp/lp_dual_simplex_def.h +++ b/src/math/lp/lp_dual_simplex_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "math/lp/lp_dual_simplex.h" namespace lp{ diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index 75eff208a..7b5dec945 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include "util/vector.h" #include diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index 03f07115b..46297a63e 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + // this is a part of lp_primal_core_solver that deals with the tableau #include "math/lp/lp_primal_core_solver.h" namespace lp { diff --git a/src/math/lp/lp_primal_simplex_def.h b/src/math/lp/lp_primal_simplex_def.h index e805ecc88..7ffe819b2 100644 --- a/src/math/lp/lp_primal_simplex_def.h +++ b/src/math/lp/lp_primal_simplex_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include "util/vector.h" #include "math/lp/lp_primal_simplex.h" diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h index 4c783049c..2aba35946 100644 --- a/src/math/lp/lp_settings_def.h +++ b/src/math/lp/lp_settings_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include #include "util/vector.h" diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h index 68beca06f..ab16a686f 100644 --- a/src/math/lp/lp_solver.h +++ b/src/math/lp/lp_solver.h @@ -149,7 +149,7 @@ public: } - virtual ~lp_solver(); + ~lp_solver() override; void flip_costs(); diff --git a/src/math/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h index 4b5bc6db7..191832a24 100644 --- a/src/math/lp/lp_solver_def.h +++ b/src/math/lp/lp_solver_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include #include "util/vector.h" diff --git a/src/math/lp/lu_def.h b/src/math/lp/lu_def.h index df0f53730..80c9cdf0e 100644 --- a/src/math/lp/lu_def.h +++ b/src/math/lp/lu_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include #include diff --git a/src/math/lp/matrix_def.h b/src/math/lp/matrix_def.h index 8dba9d0b8..95810bd5a 100644 --- a/src/math/lp/matrix_def.h +++ b/src/math/lp/matrix_def.h @@ -17,6 +17,7 @@ Revision History: --*/ +#pragma once #include #include diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h index c6ad20a39..703830ffc 100644 --- a/src/math/lp/permutation_matrix_def.h +++ b/src/math/lp/permutation_matrix_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "util/vector.h" #include "math/lp/permutation_matrix.h" namespace lp { diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h index 25ef6f82f..7d167a4a0 100644 --- a/src/math/lp/random_updater_def.h +++ b/src/math/lp/random_updater_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "math/lp/random_updater.h" #include "math/lp/static_matrix.h" #include "math/lp/lar_solver.h" diff --git a/src/math/lp/row_eta_matrix_def.h b/src/math/lp/row_eta_matrix_def.h index 817d39481..faac5c6fe 100644 --- a/src/math/lp/row_eta_matrix_def.h +++ b/src/math/lp/row_eta_matrix_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "util/vector.h" #include "math/lp/row_eta_matrix.h" namespace lp { diff --git a/src/math/lp/scaler_def.h b/src/math/lp/scaler_def.h index c05b25a16..8604a67a1 100644 --- a/src/math/lp/scaler_def.h +++ b/src/math/lp/scaler_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include #include "math/lp/scaler.h" #include "math/lp/numeric_pair.h" diff --git a/src/math/lp/square_dense_submatrix_def.h b/src/math/lp/square_dense_submatrix_def.h index 8b565f92e..3a9006b4d 100644 --- a/src/math/lp/square_dense_submatrix_def.h +++ b/src/math/lp/square_dense_submatrix_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "util/vector.h" #include "math/lp/square_dense_submatrix.h" namespace lp { diff --git a/src/math/lp/square_sparse_matrix_def.h b/src/math/lp/square_sparse_matrix_def.h index 0a2cffd61..3533ba066 100644 --- a/src/math/lp/square_sparse_matrix_def.h +++ b/src/math/lp/square_sparse_matrix_def.h @@ -17,6 +17,7 @@ Revision History: --*/ +#pragma once #include "util/vector.h" #include "math/lp/square_sparse_matrix.h" diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index 45d5d6d89..af2eac360 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -17,6 +17,8 @@ Revision History: --*/ +#pragma once + #include "util/vector.h" #include #include diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp index 19dd661c6..e9c72e2d7 100644 --- a/src/math/subpaving/subpaving.cpp +++ b/src/math/subpaving/subpaving.cpp @@ -38,7 +38,6 @@ namespace subpaving { CTX m_ctx; public: context_wrapper(reslimit& lim, typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(lim, m, p, a) {} - ~context_wrapper() override {} unsigned num_vars() const override { return m_ctx.num_vars(); } var mk_var(bool is_int) override { return m_ctx.mk_var(is_int); } bool is_int(var x) const override { return m_ctx.is_int(x); } @@ -66,8 +65,6 @@ namespace subpaving { m_as(m) {} - ~context_mpq_wrapper() override {} - unsynch_mpq_manager & qm() const override { return m_ctx.nm(); } var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { @@ -108,8 +105,6 @@ namespace subpaving { m_q2(m_qm) { } - ~context_mpf_wrapper() override {} - unsynch_mpq_manager & qm() const override { return m_qm; } var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { @@ -165,8 +160,6 @@ namespace subpaving { m_qm(qm) { } - ~context_hwf_wrapper() override {} - unsynch_mpq_manager & qm() const override { return m_qm; } var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { @@ -223,8 +216,6 @@ namespace subpaving { m_z2(m_qm) { } - ~context_fpoint_wrapper() override {} - unsynch_mpq_manager & qm() const override { return m_qm; } var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index c31e920ab..89f6dad0f 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -16,6 +16,8 @@ Author: Revision History: --*/ +#pragma once + #include "math/subpaving/subpaving_t.h" #include "math/interval/interval_def.h" #include "util/buffer.h" diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index cdd8bac0a..639528a7f 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -37,8 +37,6 @@ class subpaving_tactic : public tactic { e2v.mk_inv(m_inv); } - virtual ~display_var_proc() {} - ast_manager & m() const { return m_inv.get_manager(); } void operator()(std::ostream & out, subpaving::var x) const override { diff --git a/src/model/array_factory.h b/src/model/array_factory.h index c4bfc05df..c77e619c9 100644 --- a/src/model/array_factory.h +++ b/src/model/array_factory.h @@ -32,8 +32,6 @@ class array_factory : public struct_factory { public: array_factory(ast_manager & m, model_core & md); - ~array_factory() override {} - expr * get_some_value(sort * s) override; bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override; diff --git a/src/model/datatype_factory.h b/src/model/datatype_factory.h index 8ee4170e3..b2a6b75d3 100644 --- a/src/model/datatype_factory.h +++ b/src/model/datatype_factory.h @@ -32,7 +32,6 @@ class datatype_factory : public struct_factory { public: datatype_factory(ast_manager & m, model_core & md); - ~datatype_factory() override {} expr * get_some_value(sort * s) override; expr * get_fresh_value(sort * s) override; }; diff --git a/src/model/fpa_factory.h b/src/model/fpa_factory.h index ff2f18e35..1c2c98b25 100644 --- a/src/model/fpa_factory.h +++ b/src/model/fpa_factory.h @@ -34,8 +34,6 @@ class fpa_value_factory : public value_factory { value_factory(m, fid), m_util(m) {} - ~fpa_value_factory() override {} - expr * get_some_value(sort * s) override { mpf_manager & mpfm = m_util.fm(); diff --git a/src/model/numeral_factory.h b/src/model/numeral_factory.h index 6d805dd90..174ea8757 100644 --- a/src/model/numeral_factory.h +++ b/src/model/numeral_factory.h @@ -25,7 +25,6 @@ Revision History: class numeral_factory : public simple_factory { public: numeral_factory(ast_manager & m, family_id fid):simple_factory(m, fid) {} - ~numeral_factory() override {} }; class arith_factory : public numeral_factory { diff --git a/src/model/value_factory.h b/src/model/value_factory.h index 8df61c181..cf56439d9 100644 --- a/src/model/value_factory.h +++ b/src/model/value_factory.h @@ -230,7 +230,6 @@ class user_sort_factory : public simple_factory { app * mk_value_core(unsigned const & val, sort * s) override; public: user_sort_factory(ast_manager & m); - ~user_sort_factory() override {} /** \brief Make the universe of \c s finite, by preventing new diff --git a/src/muz/base/dl_boogie_proof.h b/src/muz/base/dl_boogie_proof.h index ed2f5a801..5107d9529 100644 --- a/src/muz/base/dl_boogie_proof.h +++ b/src/muz/base/dl_boogie_proof.h @@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ +#pragma once /** diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 01523e8d2..f6ce39518 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -159,8 +159,6 @@ namespace datalog { public: restore_rules(context& ctx, rule_set& r): ctx(ctx), m_old_rules(alloc(rule_set, r)) {} - ~restore_rules() override {} - void undo() override { ctx.replace_rules(*m_old_rules); reset(); @@ -173,7 +171,6 @@ namespace datalog { unsigned m_old_size; public: restore_vec_size_trail(Vec& v): m_vector(v), m_old_size(v.size()) {} - ~restore_vec_size_trail() override {} void undo() override { m_vector.shrink(m_old_size); } }; diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index c35cfd58a..e9ee4c690 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -105,7 +105,6 @@ namespace datalog { class rel_context_base : public engine_base { public: rel_context_base(ast_manager& m, char const* name): engine_base(m, name) {} - ~rel_context_base() override {} virtual relation_manager & get_rmanager() = 0; virtual const relation_manager & get_rmanager() const = 0; virtual relation_base & get_relation(func_decl * pred) = 0; @@ -141,7 +140,6 @@ namespace datalog { context const& ctx; public: contains_pred(context& ctx): ctx(ctx) {} - ~contains_pred() override {} bool operator()(expr* e) override { return ctx.is_predicate(e); diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index ff2210610..24b109f35 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -190,7 +190,6 @@ namespace datalog { const unsigned * cols1, const unsigned * cols2) : convenient_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2), m_join(j) {} - ~join_fn() override {} relation_base * operator()(const relation_base & r1, const relation_base & r2) override { check_relation const& t1 = get(r1); check_relation const& t2 = get(r2); @@ -219,7 +218,6 @@ namespace datalog { : convenient_join_project_fn(o1_sig, o2_sig, col_cnt, cols1, cols2, removed_col_cnt, removed_cols), m_join(j) {} - ~join_project_fn() override {} relation_base * operator()(const relation_base & r1, const relation_base & r2) override { check_relation const& t1 = get(r1); check_relation const& t2 = get(r2); @@ -527,8 +525,6 @@ namespace datalog { m_filter(f) { } - ~filter_identical_fn() override {} - void operator()(relation_base & _r) override { check_relation& r = get(_r); check_relation_plugin& p = r.get_plugin(); @@ -563,8 +559,6 @@ namespace datalog { m_condition(condition) { } - ~filter_interpreted_fn() override {} - void operator()(relation_base & tb) override { check_relation& r = get(tb); check_relation_plugin& p = r.get_plugin(); @@ -590,8 +584,6 @@ namespace datalog { m_project(p) { } - ~project_fn() override {} - relation_base * operator()(const relation_base & tb) override { check_relation const& t = get(tb); check_relation_plugin& p = t.get_plugin(); @@ -618,8 +610,6 @@ namespace datalog { m_permute(permute) { } - ~rename_fn() override {} - relation_base * operator()(const relation_base & _t) override { check_relation const& t = get(_t); check_relation_plugin& p = t.get_plugin(); @@ -647,7 +637,6 @@ namespace datalog { m_val(val), m_col(col) {} - ~filter_equal_fn() override { } void operator()(relation_base & tb) override { check_relation & t = get(tb); check_relation_plugin& p = t.get_plugin(); @@ -760,8 +749,6 @@ namespace datalog { m_cond(cond), m_xform(xform) {} - - ~filter_proj_fn() override {} relation_base* operator()(const relation_base & tb) override { check_relation const & t = get(tb); diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 909539a85..f0634f0d5 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -799,7 +799,6 @@ namespace datalog { protected: relation_base(relation_plugin & plugin, const relation_signature & s) : base_ancestor(plugin, s) {} - ~relation_base() override {} public: virtual relation_base * complement(func_decl* p) const = 0; @@ -1040,7 +1039,6 @@ namespace datalog { protected: table_base(table_plugin & plugin, const table_signature & s) : base_ancestor(plugin, s) {} - ~table_base() override {} public: table_base * clone() const override; virtual table_base * complement(func_decl* p, const table_element * func_columns = nullptr) const; diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 07921a3be..a991c9e6c 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -794,8 +794,6 @@ namespace datalog { m_delta_indexes(delta_indexes), m_delta_rels(delta_rels) {} - ~union_mapper() override {} - bool operator()(table_element * func_columns) override { relation_base & otgt_orig = m_tgt.get_inner_rel(func_columns[0]); const relation_base & osrc = m_src.get_inner_rel(func_columns[1]); diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h index f9a846c3a..56bfc961f 100644 --- a/src/muz/rel/dl_lazy_table.h +++ b/src/muz/rel/dl_lazy_table.h @@ -128,8 +128,6 @@ namespace datalog { m_ref(t) {} - ~lazy_table() override {} - lazy_table_plugin& get_lplugin() const { return dynamic_cast(table_base::get_plugin()); } @@ -164,7 +162,6 @@ namespace datalog { m_table = table; // SASSERT(&p.m_plugin == &table->get_lplugin()); } - ~lazy_table_base() override {} lazy_table_kind kind() const override { return LAZY_TABLE_BASE; } table_base* force() override { return m_table.get(); } }; @@ -183,7 +180,6 @@ namespace datalog { m_cols2(col_cnt, cols2), m_t1(t1.get_ref()), m_t2(t2.get_ref()) { } - ~lazy_table_join() override {} lazy_table_kind kind() const override { return LAZY_TABLE_JOIN; } unsigned_vector const& cols1() const { return m_cols1; } unsigned_vector const& cols2() const { return m_cols2; } @@ -201,7 +197,6 @@ namespace datalog { : lazy_table_ref(src.get_lplugin(), sig), m_cols(col_cnt, cols), m_src(src.get_ref()) {} - ~lazy_table_project() override {} lazy_table_kind kind() const override { return LAZY_TABLE_PROJECT; } unsigned_vector const& cols() const { return m_cols; } @@ -217,8 +212,7 @@ namespace datalog { : lazy_table_ref(src.get_lplugin(), sig), m_cols(col_cnt, cols), m_src(src.get_ref()) {} - ~lazy_table_rename() override {} - + lazy_table_kind kind() const override { return LAZY_TABLE_RENAME; } unsigned_vector const& cols() const { return m_cols; } lazy_table_ref* src() const { return m_src.get(); } @@ -231,8 +225,7 @@ namespace datalog { public: lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src) : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.get_ref()) {} - ~lazy_table_filter_identical() override {} - + lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_IDENTICAL; } unsigned_vector const& cols() const { return m_cols; } lazy_table_ref* src() const { return m_src.get(); } @@ -249,8 +242,7 @@ namespace datalog { m_col(col), m_value(value), m_src(src.get_ref()) {} - ~lazy_table_filter_equal() override {} - + lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_EQUAL; } unsigned col() const { return m_col; } table_element value() const { return m_value; } @@ -265,8 +257,7 @@ namespace datalog { lazy_table_filter_interpreted(lazy_table const& src, app* condition) : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.get_ref()) {} - ~lazy_table_filter_interpreted() override {} - + lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_INTERPRETED; } app* condition() const { return m_condition; } lazy_table_ref* src() const { return m_src.get(); } @@ -287,7 +278,6 @@ namespace datalog { m_src(src.get_ref()), m_cols1(c1), m_cols2(c2) {} - ~lazy_table_filter_by_negation() override {} lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_BY_NEGATION; } lazy_table_ref* tgt() const { return m_tgt.get(); } lazy_table_ref* src() const { return m_src.get(); } diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 3b32a1532..51e7f4ac6 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1589,8 +1589,6 @@ namespace datalog { m_union_fn = plugin.mk_union_fn(t, *m_aux_table, static_cast(nullptr)); } - ~default_table_map_fn() override {} - void operator()(table_base & t) override { SASSERT(t.get_signature()==m_aux_table->get_signature()); if(!m_aux_table->empty()) { @@ -1644,8 +1642,6 @@ namespace datalog { m_former_row.resize(get_result_signature().size()); } - ~default_table_project_with_reduce_fn() override {} - virtual void modify_fact(table_fact & f) const { unsigned ofs=1; unsigned r_i=1; diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index 1481b5184..9f3304e7a 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -406,8 +406,6 @@ namespace datalog { m_key_fact.resize(t.get_signature().size()); } - ~full_signature_key_indexer() override {} - query_result get_matching_offsets(const key_value & key) const override { unsigned key_len = m_key_cols.size(); for (unsigned i=0; i const& cores) override { i.relax_cores(cores); } rational cost(model& mdl) override { return i.cost(mdl); } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 2f8992e01..72195467f 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -85,7 +85,6 @@ namespace opt { public: maxsmt_solver_base(maxsat_context& c, vector& soft, unsigned index); - ~maxsmt_solver_base() override {} rational get_lower() const override { return m_lower; } rational get_upper() const override { return m_upper; } bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); } diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 41f7bedb3..1daed0e3b 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -56,9 +56,6 @@ public: m_opt(opt) {} - ~assert_soft_cmd() override { - } - void reset(cmd_context & ctx) override { m_idx = 0; m_formula = nullptr; diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h index a814ac0f8..ab5a90237 100644 --- a/src/opt/opt_pareto.h +++ b/src/opt/opt_pareto.h @@ -87,7 +87,6 @@ namespace opt { params_ref & p): pareto_base(m, cb, s, p) { } - ~gia_pareto() override {} lbool operator()() override; }; @@ -101,7 +100,6 @@ namespace opt { params_ref & p): pareto_base(m, cb, s, p) { } - ~oia_pareto() override {} lbool operator()() override; }; diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 962369bf2..da25e2285 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -39,8 +39,6 @@ namespace opt { sortmax(maxsat_context& c, vector& s, unsigned index): maxsmt_solver_base(c, s, index), m_sort(*this), m_trail(m), m_fresh(m) {} - ~sortmax() override {} - lbool operator()() override { if (!init()) return l_undef; diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 1fbd26cb8..1fb6c05dd 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -49,8 +49,6 @@ namespace opt { m_trail(m), m_defs(m) {} - ~wmax() override {} - lbool operator()() override { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index 4a4997de6..e86e42091 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -1616,7 +1616,6 @@ namespace nlarith { public: simple_branch(ast_manager& m, app* cnstr): m_cnstr(cnstr, m), m_atoms(m) {} - ~simple_branch() override {} app* get_constraint() override { return m_cnstr.get(); } void get_updates(ptr_vector& atoms, svector& updates) override { for (unsigned i = 0; i < m_atoms.size(); ++i) { @@ -1636,7 +1635,6 @@ namespace nlarith { public: ins_rem_branch(ast_manager& m, app* a, app* r, app* cnstr): simple_branch(m, cnstr) { insert(a); remove(r); } - ~ins_rem_branch() override {} }; /** diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 37924496a..3a1fa19c6 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -835,9 +835,6 @@ namespace qe { m_nftactic = mk_tseitin_cnf_tactic(m); } - ~nlqsat() override { - } - char const* name() const override { return "nlqsat"; } void updt_params(params_ref const & p) override { diff --git a/src/qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp index 43d2f9686..ce0e61d02 100644 --- a/src/qe/qe_array_plugin.cpp +++ b/src/qe/qe_array_plugin.cpp @@ -27,9 +27,6 @@ namespace qe { { } - ~array_plugin() override {} - - void assign(contains_app& x, expr* fml, rational const& vl) override { UNREACHABLE(); } diff --git a/src/qe/qe_cmd.cpp b/src/qe/qe_cmd.cpp index f708d5223..12605defd 100644 --- a/src/qe/qe_cmd.cpp +++ b/src/qe/qe_cmd.cpp @@ -26,9 +26,6 @@ public: p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } - ~qe_cmd() override { - } - void prepare(cmd_context & ctx) override { parametric_cmd::prepare(ctx); m_target = nullptr; diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index d7b825fcd..e35822813 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -106,7 +106,6 @@ namespace qe { solver_ref m_solver; public: prop_mbi_plugin(solver* s); - ~prop_mbi_plugin() override {} mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; void block(expr_ref_vector const& lits) override; }; @@ -134,7 +133,6 @@ namespace qe { expr_ref_vector& uflits); public: uflia_mbi(solver* s, solver* emptySolver); - ~uflia_mbi() override {} mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; void project(model_ref& mdl, expr_ref_vector& lits); void block(expr_ref_vector const& lits) override; diff --git a/src/sat/sat_cutset_compute_shift.h b/src/sat/sat_cutset_compute_shift.h index 7a9aff612..45d2e1de8 100644 --- a/src/sat/sat_cutset_compute_shift.h +++ b/src/sat/sat_cutset_compute_shift.h @@ -18,6 +18,7 @@ The truth table covers up to 6 inputs, which fits in 64 bits. --*/ +#pragma once static uint64_t compute_shift(uint64_t x, unsigned code) { switch (code) { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 409d03652..97405fb32 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1812,9 +1812,9 @@ namespace sat { CTRACE("resolve_bug", !c1.contains(l) || !c2.contains(~l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";); if (m_visited.size() <= 2*s.num_vars()) m_visited.resize(2*s.num_vars(), false); - if (c1.was_removed()) + if (c1.was_removed() && !c1.contains(l)) return false; - if (c2.was_removed()) + if (c2.was_removed() && !c2.contains(~l)) return false; SASSERT(c1.contains(l)); SASSERT(c2.contains(~l)); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 3d46ec643..a83cb6a45 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -115,8 +115,6 @@ public: return m_solver.get_config().m_incremental; } - ~inc_sat_solver() override {} - solver* translate(ast_manager& dst_m, params_ref const& p) override { if (m_num_scopes > 0) { throw default_exception("Cannot translate sat solver at non-base level"); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 345f3421a..4e616a64c 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -351,7 +351,6 @@ namespace bv { public: solver(euf::solver& ctx, theory_id id); - ~solver() override {} void set_lookahead(sat::lookahead* s) override { } void init_search() override {} double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override; diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index dc2bb71dd..13d3e02e4 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -1823,7 +1823,7 @@ namespace pb { } bool solver::validate_watch(pbc const& p, literal alit) const { - if (value(p.lit()) != l_true) + if (p.lit() == sat::null_literal || value(p.lit()) != l_true) return true; for (unsigned i = 0; i < p.size(); ++i) { literal l = p[i].second; diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 4be554633..fa8b2bc26 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -3744,9 +3744,6 @@ namespace q { reset_pp_pc(); } - ~mam_impl() override { - } - void add_pattern(quantifier * qa, app * mp) override { SASSERT(m.is_pattern(mp)); TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m) << "\n" << mk_ismt2_pp(mp, m) << "\n";); diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 52d1a064c..37e2424ce 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -45,7 +45,6 @@ namespace q { arith_util a; public: arith_projection(ast_manager& m) : projection_function(m), a(m) {} - ~arith_projection() override {} bool operator()(expr* e1, expr* e2) const override { return lt(a, e1, e2); } expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); } }; @@ -54,7 +53,6 @@ namespace q { bv_util bvu; public: ubv_projection(ast_manager& m) : projection_function(m), bvu(m) {} - ~ubv_projection() override {} bool operator()(expr* e1, expr* e2) const override { return lt(bvu, e1, e2); } expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); } }; diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h index a843d3825..9653268e6 100644 --- a/src/sat/smt/q_model_fixer.h +++ b/src/sat/smt/q_model_fixer.h @@ -95,7 +95,6 @@ namespace q { public: model_fixer(euf::solver& ctx, solver& qs); - ~model_fixer() override {} /** * Update model in order to best satisfy quantifiers. diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 5d6a52c8f..32025888b 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -65,7 +65,6 @@ namespace q { public: solver(euf::solver& ctx, family_id fid); - ~solver() override {} bool is_external(sat::bool_var v) override { return false; } void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override; void asserted(sat::literal l) override; diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 4484a7717..7209fa051 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -189,7 +189,6 @@ namespace euf { public: th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id); - virtual ~th_euf_solver() {} virtual theory_var mk_var(enode* n); unsigned get_num_vars() const { return m_var2enode.size(); } euf::enode* e_internalize(expr* e); diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 9e2ea3eab..494e69e55 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -131,6 +131,21 @@ namespace user_solver { m_id2justification.setx(v, lits, sat::literal_vector()); m_fixed_eh(m_user_context, this, var2expr(v), lit.sign() ? m.mk_false() : m.mk_true()); } + + void solver::new_eq_eh(euf::th_eq const& eq) { + if (!m_eq_eh) + return; + force_push(); + m_eq_eh(m_user_context, this, var2expr(eq.v1()), var2expr(eq.v2())); + } + + void solver::new_diseq_eh(euf::th_eq const& de) { + if (!m_diseq_eh) + return; + force_push(); + m_diseq_eh(m_user_context, this, var2expr(de.v1()), var2expr(de.v2())); + } + void solver::push_core() { th_euf_solver::push_core(); diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index 951b97fb6..28528b9a1 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -144,6 +144,10 @@ namespace user_solver { bool get_case_split(sat::bool_var& var, lbool &phase) override; void asserted(sat::literal lit) override; + bool use_diseqs() const override { return (bool)m_diseq_eh; } + void new_eq_eh(euf::th_eq const& eq) override; + void new_diseq_eh(euf::th_eq const& de) override; + sat::check_result check() override; void push_core() override; void pop_core(unsigned n) override; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 73d8561df..a5d9dec4e 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -93,10 +93,6 @@ struct goal2sat::imp : public sat::sat_internalizer { updt_params(p); } - ~imp() override { - } - - sat::cut_simplifier* aig() { return m_solver.get_cut_simplifier(); } diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h index b911f7b47..1e1dfcd5e 100644 --- a/src/sat/tactic/sat2goal.h +++ b/src/sat/tactic/sat2goal.h @@ -51,7 +51,6 @@ public: public: mc(ast_manager& m); - ~mc() override {} // flush model converter from SAT solver to this structure. void flush_smc(sat::solver& s, atom2bool_var const& map); void operator()(sat::model& m); diff --git a/src/shell/options.h b/src/shell/options.h index ee1de00fb..39fe2fe8f 100644 --- a/src/shell/options.h +++ b/src/shell/options.h @@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ +#pragma once /** diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index f251d01ae..b77a38927 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -67,8 +67,6 @@ namespace smt { m_ge(ge) { } - ~arith_eq_relevancy_eh() override {} - void operator()(relevancy_propagator & rp) override { if (!rp.is_relevant(m_n1)) return; diff --git a/src/smt/database.h b/src/smt/database.h index 3edb87f1f..f1ce25f26 100644 --- a/src/smt/database.h +++ b/src/smt/database.h @@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ +#pragma once static char const g_pattern_database[] = "(benchmark patterns \n" diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 42844f575..978f1fbe3 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -346,7 +346,6 @@ namespace smt { dyn_ack_clause_del_eh(dyn_ack_manager & m): m(m) { } - ~dyn_ack_clause_del_eh() override {} void operator()(ast_manager & _m, clause * cls) override { m.del_clause_eh(cls); dealloc(this); diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index d0c1b97f2..f069e0a60 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -59,7 +59,6 @@ class proto_model : public model_core { public: proto_model(ast_manager & m, params_ref const & p = params_ref()); - ~proto_model() override {} void register_factory(value_factory * f) { m_factories.register_plugin(f); } diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 2189b64e0..9f5bdb0d4 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -150,8 +150,6 @@ namespace { if (!first) out << "\n"; } - - ~act_case_split_queue() override {}; }; /** @@ -1244,8 +1242,6 @@ namespace { out << "\n"; } - - ~theory_aware_branching_queue() override {}; }; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6652804ea..420147256 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -821,6 +821,8 @@ namespace smt { SASSERT(t2 != null_theory_id); theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t2) : r1->get_th_var(t2); + TRACE("merge_theory_vars", tout << get_theory(t2)->get_name() << ": " << v2 << " == " << v1 << "\n"); + if (v1 != null_theory_var) { // only send the equality to the theory, if the equality was not propagated by it. if (t2 != from_th) @@ -839,6 +841,7 @@ namespace smt { SASSERT(v1 != null_theory_var); SASSERT(t1 != null_theory_id); theory_var v2 = r2->get_th_var(t1); + TRACE("merge_theory_vars", tout << get_theory(t1)->get_name() << ": " << v2 << " == " << v1 << "\n"); if (v2 == null_theory_var) { r2->add_th_var(v1, t1, m_region); push_new_th_diseqs(r2, v1, get_theory(t1)); diff --git a/src/smt/smt_for_each_relevant_expr.h b/src/smt/smt_for_each_relevant_expr.h index ef687ae01..4b4492b7f 100644 --- a/src/smt/smt_for_each_relevant_expr.h +++ b/src/smt/smt_for_each_relevant_expr.h @@ -92,7 +92,6 @@ namespace smt { for_each_relevant_expr(ctx), m_buffer(b) { } - ~collect_relevant_label_lits() override {} void operator()(expr * n) override; }; @@ -103,7 +102,6 @@ namespace smt { for_each_relevant_expr(ctx), m_buffer(b) { } - ~collect_relevant_labels() override {} void operator()(expr * n) override; }; diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index 48987e746..b90233792 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -239,7 +239,6 @@ namespace smt { unsigned num_params, parameter* params): simple_justification(r, num_lits, lits), m_th_id(fid), m_params(num_params, params) {} - ~simple_theory_justification() override {} bool has_del_eh() const override { return !m_params.empty(); } @@ -323,8 +322,6 @@ namespace smt { unsigned num_eqs, enode_pair const * eqs, unsigned num_params = 0, parameter* params = nullptr): ext_simple_justification(r, num_lits, lits, num_eqs, eqs), m_th_id(fid), m_params(num_params, params) {} - - ~ext_theory_simple_justification() override {} bool has_del_eh() const override { return !m_params.empty(); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 34f323695..24ec4d5b9 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -464,7 +464,7 @@ namespace smt { m.limit().inc(); } - virtual ~auf_solver() { + ~auf_solver() override { flush_nodes(); reset_eval_cache(); } @@ -1180,7 +1180,6 @@ namespace smt { unsigned m_var_j; public: f_var(ast_manager& m, func_decl* f, unsigned i, unsigned j) : qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {} - ~f_var() override {} char const* get_kind() const override { return "f_var"; @@ -1261,7 +1260,6 @@ namespace smt { f_var(m, f, i, j), m_offset(offset, m) { } - ~f_var_plus_offset() override {} char const* get_kind() const override { return "f_var_plus_offset"; @@ -1427,7 +1425,6 @@ namespace smt { public: select_var(ast_manager& m, app* s, unsigned i, unsigned j) :qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {} - ~select_var() override {} char const* get_kind() const override { return "select_var"; @@ -1497,8 +1494,6 @@ namespace smt { std::swap(m_var_i, m_var_j); } - ~var_pair() override {} - bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) return false; @@ -1577,7 +1572,6 @@ namespace smt { var_expr_pair(ast_manager& m, unsigned i, expr* t) : qinfo(m), m_var_i(i), m_t(t, m) {} - ~var_expr_pair() override {} bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index b67599a99..b0696049b 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -606,9 +606,6 @@ namespace smt { m_active(false) { } - ~default_qm_plugin() override { - } - void set_manager(quantifier_manager & qm) override { SASSERT(m_qm == nullptr); m_qm = &qm; diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 4b787561d..649d75737 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -52,7 +52,6 @@ namespace smt { app * m_parent; public: and_relevancy_eh(app * p):m_parent(p) {} - ~and_relevancy_eh() override {} void operator()(relevancy_propagator & rp) override; }; @@ -60,7 +59,6 @@ namespace smt { app * m_parent; public: or_relevancy_eh(app * p):m_parent(p) {} - ~or_relevancy_eh() override {} void operator()(relevancy_propagator & rp) override; }; @@ -68,7 +66,6 @@ namespace smt { app * m_parent; public: ite_relevancy_eh(app * p):m_parent(p) {} - ~ite_relevancy_eh() override {} void operator()(relevancy_propagator & rp) override; }; @@ -78,7 +75,6 @@ namespace smt { app * m_else_eq; public: ite_term_relevancy_eh(app * p, app * then_eq, app * else_eq):m_parent(p), m_then_eq(then_eq), m_else_eq(else_eq) {} - ~ite_term_relevancy_eh() override {} void operator()(relevancy_propagator & rp) override; }; diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index a1054423a..af7b97c72 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -319,7 +319,6 @@ namespace smt { public: atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind); atom_kind get_atom_kind() const { return static_cast(m_atom_kind); } - ~atom() override {} inline inf_numeral const & get_k() const { return m_k; } bool_var get_bool_var() const { return m_bvar; } bool is_true() const { return m_is_true; } @@ -341,7 +340,6 @@ namespace smt { m_rhs(rhs) { SASSERT(m_lhs->get_root() == m_rhs->get_root()); } - ~eq_bound() override {} bool has_justification() const override { return true; } void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override { SASSERT(m_lhs->get_root() == m_rhs->get_root()); @@ -357,7 +355,6 @@ namespace smt { friend class theory_arith; public: derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {} - ~derived_bound() override {} literal_vector const& lits() const { return m_lits; } eq_vector const& eqs() const { return m_eqs; } bool has_justification() const override { return true; } @@ -374,7 +371,6 @@ namespace smt { friend class theory_arith; public: justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {} - ~justified_derived_bound() override {} bool has_justification() const override { return true; } void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override; void push_lit(literal l, numeral const& coeff) override; diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 9379c939f..988f3fdad 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -450,7 +450,6 @@ namespace smt { app* m_obj; public: remove_sz(ast_manager& m, obj_map& tab, app* t): m(m), m_table(tab), m_obj(t) { } - ~remove_sz() override {} void undo() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); } }; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index d1a01c807..1be88a6de 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -890,8 +890,6 @@ namespace smt { m_unspecified_else(true) { } - ~array_value_proc() override {} - void add_entry(unsigned num_args, enode * const * args, enode * value) { SASSERT(num_args > 0); SASSERT(m_dim == 0 || m_dim == num_args); diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index d73b7a008..e26db51d0 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -56,7 +56,6 @@ namespace smt { struct bit_atom : public atom { var_pos_occ * m_occs; bit_atom():m_occs(nullptr) {} - ~bit_atom() override {} bool is_bit() const override { return true; } }; @@ -64,7 +63,6 @@ namespace smt { literal m_var; literal m_def; le_atom(literal v, literal d):m_var(v), m_def(d) {} - ~le_atom() override {} bool is_bit() const override { return false; } }; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d11172691..febd2763c 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -823,7 +823,6 @@ namespace smt { public: datatype_value_proc(func_decl * d):m_constructor(d) {} void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); } - ~datatype_value_proc() override {} void get_dependencies(buffer & result) override { result.append(m_dependencies.size(), m_dependencies.data()); } diff --git a/src/smt/theory_dummy.h b/src/smt/theory_dummy.h index 6f2e641fd..817d1fda1 100644 --- a/src/smt/theory_dummy.h +++ b/src/smt/theory_dummy.h @@ -46,7 +46,6 @@ namespace smt { public: theory_dummy(context& ctx, family_id fid, char const * name); - ~theory_dummy() override {} theory * mk_fresh(context * new_ctx) override { return alloc(theory_dummy, *new_ctx, get_family_id(), m_name); } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 9d5df855e..9aa70d9bf 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -47,8 +47,6 @@ namespace smt { m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m_ebits(ebits), m_sbits(sbits) {} - ~fpa_value_proc() override {} - void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); } void get_dependencies(buffer & result) override { @@ -75,7 +73,6 @@ namespace smt { result.append(m_deps); } - ~fpa_rm_value_proc() override {} app * mk_value(model_generator & mg, expr_ref_vector const & values) override; }; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 75f9cb997..0b9f4c072 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1113,7 +1113,7 @@ public: } { scoped_trace_stream ts(th, dgez, neg); - mk_axiom( dgez, neg); + mk_axiom( dgez, neg); } } @@ -1224,7 +1224,6 @@ public: return; } expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m); - ctx().get_rewriter()(mod_r); expr_ref eq_r(th.mk_eq_atom(mod_r, p), m); ctx().internalize(eq_r, false); literal eq = ctx().get_literal(eq_r); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 2d62bb7ac..f713877b3 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -19,6 +19,7 @@ Notes: It performs unit propagation and switches to creating sorting circuits if it keeps having to propagate (create new clauses). --*/ +#pragma once #include "smt/smt_theory.h" #include "ast/pb_decl_plugin.h" diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 9dc0b8740..6d8cbc6de 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1923,7 +1923,6 @@ public: seq_value_proc(theory_seq& th, enode* n, sort* s): th(th), m_node(n), m_sort(s) { (void)m_node; } - ~seq_value_proc() override {} void add_unit(enode* n) { m_dependencies.push_back(model_value_dependency(n)); m_source.push_back(unit_source); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index cf7e9da23..fb5a821d5 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -230,7 +230,6 @@ namespace smt { expr_ref m_e; public: replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {} - ~replay_length_coherence() override {} void operator()(theory_seq& th) override { th.check_length_coherence(m_e); m_e.reset(); @@ -241,7 +240,6 @@ namespace smt { expr_ref m_e; public: replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {} - ~replay_fixed_length() override {} void operator()(theory_seq& th) override { th.fixed_length(m_e, false, false); m_e.reset(); @@ -252,7 +250,6 @@ namespace smt { expr_ref m_e; public: replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {} - ~replay_axiom() override {} void operator()(theory_seq& th) override { th.enque_axiom(m_e); m_e.reset(); @@ -264,7 +261,6 @@ namespace smt { bool m_sign; public: replay_unit_literal(ast_manager& m, expr* e, bool sign) : m_e(e, m), m_sign(sign) {} - ~replay_unit_literal() override {} void operator()(theory_seq& th) override { literal lit = th.mk_literal(m_e); if (m_sign) lit.neg(); @@ -278,7 +274,6 @@ namespace smt { expr_ref m_e; public: replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {} - ~replay_is_axiom() override {} void operator()(theory_seq& th) override { th.check_int_string(m_e); m_e.reset(); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 090a5fe36..27ee97c97 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -51,7 +51,6 @@ public: str_value_factory(ast_manager & m, family_id fid) : value_factory(m, fid), u(m), delim("!"), m_next(0) {} - ~str_value_factory() override {} expr * get_some_value(sort * s) override { return u.str.mk_string("some value"); } @@ -93,7 +92,6 @@ class binary_search_trail : public trail { public: binary_search_trail(obj_map > & target, expr * entry) : target(target), entry(entry) {} - ~binary_search_trail() override {} void undo() override { TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;); if (target.contains(entry)) { diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index 57ed89588..0fb5f92df 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -724,8 +724,7 @@ namespace smt { unsigned cx = estimate_regex_complexity(sub1); return _qadd(lo, cx); } else if (u.re.is_range(re, sub1, sub2)) { - SASSERT(u.str.is_string(sub1)); - SASSERT(u.str.is_string(sub2)); + if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals"); zstring str1, str2; u.str.is_string(sub1, str1); u.str.is_string(sub2, str2); @@ -767,8 +766,7 @@ namespace smt { unsigned cx = estimate_regex_complexity_under_complement(sub1); return _qmul(2, cx); } else if (u.re.is_range(re, sub1, sub2)) { - SASSERT(u.str.is_string(sub1)); - SASSERT(u.str.is_string(sub2)); + if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals"); zstring str1, str2; u.str.is_string(sub1, str1); u.str.is_string(sub2, str2); @@ -874,8 +872,7 @@ namespace smt { // this is bad -- term generation requires this not to appear lens.reset(); } else if (u.re.is_range(re, sub1, sub2)) { - SASSERT(u.str.is_string(sub1)); - SASSERT(u.str.is_string(sub2)); + if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals"); zstring str1, str2; u.str.is_string(sub1, str1); u.str.is_string(sub2, str2); @@ -1006,8 +1003,7 @@ namespace smt { SASSERT(retval); return retval; } else if (u.re.is_range(re, sub1, sub2)) { - SASSERT(u.str.is_string(sub1)); - SASSERT(u.str.is_string(sub2)); + if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals"); zstring str1, str2; u.str.is_string(sub1, str1); u.str.is_string(sub2, str2); diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 911d1715e..ec0acd903 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -146,7 +146,9 @@ final_check_status theory_user_propagator::final_check_eh() { catch (...) { throw default_exception("Exception thrown in \"final\"-callback"); } + CTRACE("user_propagate", can_propagate(), tout << "can propagate\n"); propagate(); + CTRACE("user_propagate", ctx.inconsistent(), tout << "inconsistent\n"); // check if it became inconsistent or something new was propagated/registered bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent(); return done ? FC_DONE : FC_CONTINUE; @@ -298,13 +300,17 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) { m_eqs.reset(); for (expr* id : prop.m_ids) m_lits.append(m_id2justification[expr2var(id)]); - for (auto const& p : prop.m_eqs) - m_eqs.push_back(enode_pair(get_enode(expr2var(p.first)), get_enode(expr2var(p.second)))); - DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); + for (auto const& [a,b] : prop.m_eqs) + if (a != b) + m_eqs.push_back(enode_pair(get_enode(expr2var(a)), get_enode(expr2var(b)))); + DEBUG_CODE(for (auto const& [a, b] : m_eqs) VERIFY(a->get_root() == b->get_root());); DEBUG_CODE(for (expr* e : prop.m_ids) VERIFY(m_fixed.contains(expr2var(e)));); DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); - TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n"); + TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n"; + for (auto const& [a,b] : m_eqs) tout << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n"; + for (expr* e : prop.m_ids) tout << mk_pp(e, m) << "\n"; + for (literal lit : m_lits) tout << lit << "\n"); if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification( @@ -341,9 +347,9 @@ void theory_user_propagator::propagate_new_fixed(prop_info const& prop) { void theory_user_propagator::propagate() { - TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n"); if (m_qhead == m_prop.size() && m_to_add_qhead == m_to_add.size()) return; + TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n"); force_push(); unsigned qhead = m_to_add_qhead; diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index ba9900848..73fc5bb45 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -140,10 +140,11 @@ namespace smt { bool get_case_split(bool_var& var, bool& is_pos); theory * mk_fresh(context * new_ctx) override; + char const* get_name() const override { return "user_propagate"; } bool internalize_atom(app* atom, bool gate_ctx) override; bool internalize_term(app* term) override; - void new_eq_eh(theory_var v1, theory_var v2) override { if (m_eq_eh) m_eq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } - void new_diseq_eh(theory_var v1, theory_var v2) override { if (m_diseq_eh) m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } + void new_eq_eh(theory_var v1, theory_var v2) override { force_push(); if (m_eq_eh) m_eq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } + void new_diseq_eh(theory_var v1, theory_var v2) override { force_push(); if (m_diseq_eh) m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } bool use_diseqs() const override { return ((bool)m_diseq_eh); } bool build_models() const override { return false; } final_check_status final_check_eh() override; diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index 236f56bee..03a205ca6 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -74,10 +74,7 @@ namespace smt { m_old_values(old) { old.push_back(value); } - - ~numeral_trail() override { - } - + void undo() override { m_value = m_old_values.back(); m_old_values.shrink(m_old_values.size() - 1); diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 29a5c0a8f..6e414816f 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -398,7 +398,6 @@ class combined_solver_factory : public solver_factory { scoped_ptr m_f2; public: combined_solver_factory(solver_factory * f1, solver_factory * f2):m_f1(f1), m_f2(f2) {} - ~combined_solver_factory() override {} solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), diff --git a/src/solver/solver.h b/src/solver/solver.h index dde4ccbe0..09daf3b29 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -53,7 +53,6 @@ class solver : public check_sat_result, public user_propagator::core { symbol m_cancel_backup_file; public: solver() {} - ~solver() override {} /** \brief Creates a clone of the solver. diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 09ede0c35..b178929bd 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -357,9 +357,7 @@ class tactic2solver_factory : public solver_factory { public: tactic2solver_factory(tactic * t):m_tactic(t) { } - - ~tactic2solver_factory() override {} - + solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic); } diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index 33ffbf282..a544c6810 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -51,7 +51,6 @@ public: result operator()(goal const & g) override { return is_unbounded(g); } - ~is_unbounded_probe() override {} }; probe * mk_is_unbounded_probe() { diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 3cc7436d1..25c5620c2 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -39,9 +39,6 @@ public: return alloc(card2bv_tactic, m, m_params); } - ~card2bv_tactic() override { - } - char const* name() const override { return "card2bv"; } void updt_params(params_ref const & p) override { diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index a1a1a56cc..1711a34ac 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -165,10 +165,6 @@ public: m_bounds(m) { } - ~eq2bv_tactic() override { - } - - void updt_params(params_ref const & p) override { } diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 569dbff21..d0564139a 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -61,7 +61,8 @@ class fm_tactic : public tactic { return m.is_false(val); } - r_kind process(func_decl * x, expr * cls, arith_util & u, model& ev, rational & r) { + r_kind process(func_decl * x, expr * cls, arith_util & u, model& ev, rational & r, expr_ref& r_e) { + r_e = nullptr; unsigned num_lits; expr * const * lits; if (m.is_or(cls)) { @@ -93,6 +94,7 @@ class fm_tactic : public tactic { expr * lhs = to_app(l)->get_arg(0); expr * rhs = to_app(l)->get_arg(1); rational c; + expr_ref c_e(m); if (!u.is_numeral(rhs, c)) return NONE; if (neg) @@ -133,27 +135,41 @@ class fm_tactic : public tactic { expr_ref val(m); val = ev(monomial); rational tmp; - if (!u.is_numeral(val, tmp)) - return NONE; - if (neg) - tmp.neg(); - c -= tmp; + if (u.is_numeral(val, tmp)) { + if (neg) + tmp.neg(); + c -= tmp; + } + else { + // this happens for algebraic numerals + if (neg) + val = u.mk_uminus(val); + if (!c_e) + c_e = u.mk_uminus(val); + else + c_e = u.mk_sub(c_e, val); + } } } if (u.is_int(x->get_range()) && strict) { // a*x < c --> a*x <= c-1 SASSERT(c.is_int()); c--; + SASSERT(!c_e); } is_lower = a_val.is_neg(); c /= a_val; + if (c_e) + c_e = u.mk_div(c_e, u.mk_numeral(a_val, false)); if (u.is_int(x->get_range())) { + SASSERT(!c_e); if (is_lower) c = ceil(c); else c = floor(c); } r = c; + r_e = c_e; } } (void)found; @@ -187,6 +203,12 @@ class fm_tactic : public tactic { //model_evaluator ev(*(md.get())); //ev.set_model_completion(true); arith_util u(m); + auto mk_max = [&](expr* a, expr* b) { + return expr_ref(m.mk_ite(u.mk_ge(a, b), a, b), m); + }; + auto mk_min = [&](expr* a, expr* b) { + return expr_ref(m.mk_ite(u.mk_ge(a, b), b, a), m); + }; unsigned i = m_xs.size(); while (i > 0) { --i; @@ -194,44 +216,67 @@ class fm_tactic : public tactic { rational lower; rational upper; rational val; - bool has_lower = false; - bool has_upper = false; + expr_ref val_e(m), val_upper_e(m), val_lower_e(m); + bool has_lower = false, has_upper = false; TRACE("fm_mc", tout << "processing " << x->get_name() << "\n";); - clauses::iterator it = m_clauses[i].begin(); - clauses::iterator end = m_clauses[i].end(); - for (; it != end; ++it) { + for (expr* cl : m_clauses[i]) { if (!m.inc()) throw tactic_exception(m.limit().get_cancel_msg()); - switch (process(x, *it, u, *md, val)) { + switch (process(x, cl, u, *md, val, val_e)) { case NONE: - TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";); + TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(cl, m) << "\n";); break; case LOWER: - TRACE("fm_mc", tout << "lower bound: " << val << " for:\n" << mk_ismt2_pp(*it, m) << "\n";); - if (!has_lower || val > lower) - lower = val; - has_lower = true; + TRACE("fm_mc", tout << "lower bound: " << val << " for:\n" << mk_ismt2_pp(cl, m) << "\n";); + if (val_e) + val_lower_e = val_lower_e != nullptr ? mk_max(val_lower_e, val_e) : val_e; + else if (!has_lower || val > lower) + lower = val, has_lower = true; break; case UPPER: - TRACE("fm_mc", tout << "upper bound: " << val << " for:\n" << mk_ismt2_pp(*it, m) << "\n";); - if (!has_upper || val < upper) - upper = val; - has_upper = true; + TRACE("fm_mc", tout << "upper bound: " << val << " for:\n" << mk_ismt2_pp(cl, m) << "\n";); + if (val_e) + val_upper_e = val_upper_e != nullptr ? mk_min(val_upper_e, val_e) : val_e; + else if (!has_upper || val < upper) + upper = val, has_upper = true; break; } } expr * x_val; + if (u.is_int(x->get_range())) { - if (has_lower) + if (val_lower_e) { + x_val = val_lower_e; + if (has_lower) + x_val = mk_max(x_val, u.mk_numeral(lower, true)); + } + else if (val_upper_e) { + x_val = val_upper_e; + if (has_upper) + x_val = mk_min(x_val, u.mk_numeral(upper, true)); + } + else if (has_lower) x_val = u.mk_numeral(lower, true); else if (has_upper) x_val = u.mk_numeral(upper, true); else x_val = u.mk_numeral(rational(0), true); + } else { - if (has_lower && has_upper) + if (val_lower_e && has_lower) + val_lower_e = mk_max(val_lower_e, u.mk_numeral(lower, false)); + if (val_upper_e && has_upper) + val_upper_e = mk_min(val_upper_e, u.mk_numeral(upper, false)); + + if (val_lower_e && val_upper_e) + x_val = u.mk_div(u.mk_add(val_lower_e, val_upper_e), u.mk_real(2)); + else if (val_lower_e) + x_val = u.mk_add(val_lower_e, u.mk_real(1)); + else if (val_upper_e) + x_val = u.mk_sub(val_upper_e, u.mk_real(1)); + else if (has_lower && has_upper) x_val = u.mk_numeral((upper + lower)/rational(2), false); else if (has_lower) x_val = u.mk_numeral(lower + rational(1), false); @@ -1168,18 +1213,12 @@ class fm_tactic : public tactic { } // x_cost_lt is not a total order on variables std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int)); - TRACE("fm", - svector::iterator it2 = x_cost_vector.begin(); - svector::iterator end2 = x_cost_vector.end(); - for (; it2 != end2; ++it2) { - tout << "(" << mk_ismt2_pp(m_var2expr.get(it2->first), m) << " " << it2->second << ") "; - } + TRACE("fm", + for (auto const& [v,c] : x_cost_vector) + tout << "(" << mk_ismt2_pp(m_var2expr.get(v), m) << " " << c << ") "; tout << "\n";); - svector::iterator it2 = x_cost_vector.begin(); - svector::iterator end2 = x_cost_vector.end(); - for (; it2 != end2; ++it2) { - xs.push_back(it2->first); - } + for (auto const& [v, c] : x_cost_vector) + xs.push_back(v); } void cleanup_constraints(constraints & cs) { @@ -1215,11 +1254,9 @@ class fm_tactic : public tactic { void analyze(constraints const & cs, var x, bool & all_int, bool & unit_coeff) const { all_int = true; unit_coeff = true; - constraints::const_iterator it = cs.begin(); - constraints::const_iterator end = cs.end(); - for (; it != end; ++it) { + for (auto const * c : cs) { bool curr_unit_coeff; - analyze(*(*it), x, all_int, curr_unit_coeff); + analyze(*c, x, all_int, curr_unit_coeff); if (!all_int) return; if (!curr_unit_coeff) @@ -1243,12 +1280,8 @@ class fm_tactic : public tactic { } void copy_constraints(constraints const & s, clauses & t) { - constraints::const_iterator it = s.begin(); - constraints::const_iterator end = s.end(); - for (; it != end; ++it) { - app * c = to_expr(*(*it)); - t.push_back(c); - } + for (auto const* cp : s) + t.push_back(to_expr(*cp)); } clauses tmp_clauses; @@ -1262,10 +1295,8 @@ class fm_tactic : public tactic { } void mark_constraints_dead(constraints const & cs) { - constraints::const_iterator it = cs.begin(); - constraints::const_iterator end = cs.end(); - for (; it != end; ++it) - (*it)->m_dead = true; + for (auto* cp : cs) + cp->m_dead = true; } void mark_constraints_dead(var x) { @@ -1514,14 +1545,8 @@ class fm_tactic : public tactic { } void copy_remaining(vector & v2cs) { - vector::iterator it = v2cs.begin(); - vector::iterator end = v2cs.end(); - for (; it != end; ++it) { - constraints & cs = *it; - constraints::iterator it2 = cs.begin(); - constraints::iterator end2 = cs.end(); - for (; it2 != end2; ++it2) { - constraint * c = *it2; + for (constraints& cs : v2cs) { + for (constraint* c : cs) { if (!c->m_dead) { c->m_dead = true; expr * new_f = to_expr(*c); @@ -1604,11 +1629,9 @@ class fm_tactic : public tactic { } void display_constraints(std::ostream & out, constraints const & cs) const { - constraints::const_iterator it = cs.begin(); - constraints::const_iterator end = cs.end(); - for (; it != end; ++it) { + for (auto const* cp : cs) { out << " "; - display(out, *(*it)); + display(out, *cp); out << "\n"; } } diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 560b7b265..36df89da5 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -434,9 +434,6 @@ public: return alloc(nla2bv_tactic, m_params); } - ~nla2bv_tactic() override { - } - char const* name() const override { return "nla2bv"; } void updt_params(params_ref const & p) override { diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 843d32828..afcecd7d3 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -902,9 +902,6 @@ public: tactic * translate(ast_manager & m) override { return alloc(purify_arith_tactic, m, m_params); } - - ~purify_arith_tactic() override { - } char const* name() const override { return "purify_arith"; } diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index fe3294e4c..5c26fb2b5 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -50,10 +50,7 @@ struct bit_blaster_model_converter : public model_converter { for (func_decl* f : newbits) m_newbits.push_back(f); } - - ~bit_blaster_model_converter() override { - } - + void collect_bits(obj_hashtable & bits) { unsigned sz = m_bits.size(); for (unsigned i = 0; i < sz; i++) { diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index 7ea7c0a69..b0e6be1bd 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -109,8 +109,6 @@ struct bv_bound_chk_rewriter : public rewriter_tpl { updt_params(p); } - ~bv_bound_chk_rewriter() override {} - void updt_params(params_ref const & _p) { m_cfg.updt_params(_p); } diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 4f9ae6e9d..650095207 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -93,7 +93,6 @@ class dt2bv_tactic : public tactic { struct sort_pred : public i_sort_pred { dt2bv_tactic& m_t; sort_pred(dt2bv_tactic& t): m_t(t) {} - ~sort_pred() override {} bool operator()(sort* s) override { return m_t.m_fd_sorts.contains(s); } diff --git a/src/tactic/converter.h b/src/tactic/converter.h index 3146058bb..60602557e 100644 --- a/src/tactic/converter.h +++ b/src/tactic/converter.h @@ -57,8 +57,6 @@ protected: public: concat_converter(T * c1, T * c2):m_c1(c1), m_c2(c2) {} - - ~concat_converter() override {} void cancel() override { m_c2->cancel(); diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 234b7262c..b65fd8353 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -50,7 +50,6 @@ public: return alloc(cofactor_term_ite_tactic, m, m_params); } - ~cofactor_term_ite_tactic() override {} char const* name() const override { return "cofactor"; } void updt_params(params_ref const & p) override { m_params.append(p); m_elim_ite.updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); } diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 04750a7c3..b02adad6e 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -52,8 +52,6 @@ public: m_params(p) { } - ~collect_statistics_tactic() override {} - char const* name() const override { return "collect_statistics"; } tactic * translate(ast_manager & m_) override { diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 47b2fa389..9ef1cf224 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -32,7 +32,6 @@ class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier { void assert_eq_core(expr * t, app * val); public: ctx_propagate_assertions(ast_manager& m); - ~ctx_propagate_assertions() override {} bool assert_expr(expr * t, bool sign) override; bool simplify(expr* t, expr_ref& result) override; void push(); diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 1dda062c8..9bf70ab16 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -541,7 +541,6 @@ class expr_substitution_simplifier : public dom_simplifier { public: expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {} - ~expr_substitution_simplifier() override {} bool assert_expr(expr * t, bool sign) override { expr* tt; diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index fccfdf53e..959a1fc18 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -47,8 +47,6 @@ public: return alloc(nnf_tactic, m_params); } - ~nnf_tactic() override {} - char const* name() const override { return "nnf"; } void updt_params(params_ref const & p) override { m_params.append(p); } diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 0313899ac..2c4b80b93 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -102,8 +102,6 @@ public: pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): m(m), m_trail(m), pb(m), m_r(m) {} - ~pb_preprocess_tactic() override {} - tactic * translate(ast_manager & m) override { return alloc(pb_preprocess_tactic, m); } diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index cfcc42482..df3de8219 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -45,8 +45,6 @@ public: m_arith(m) {} - ~reduce_invertible_tactic() override { } - char const* name() const override { return "reduce_invertible"; } tactic * translate(ast_manager & m) override { diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h index dae38304a..85fa8ed24 100644 --- a/src/tactic/core/special_relations_tactic.h +++ b/src/tactic/core/special_relations_tactic.h @@ -47,8 +47,6 @@ public: special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()): m(m), m_params(ref), m_pm(m) {} - ~special_relations_tactic() override {} - void updt_params(params_ref const & p) override { m_params.append(p); } void collect_param_descrs(param_descrs & r) override { } diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index 12b76b638..99a69395b 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -52,8 +52,6 @@ class split_clause_tactic : public tactic { split_pc(ast_manager & m, app * cls, proof * pr):m_clause(cls, m), m_clause_pr(pr, m) { } - ~split_pc() override { } - proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { // Let m_clause be of the form (l_0 or ... or l_{num_source - 1}) // Each source[i] proof is a proof for "false" using l_i as a hypothesis @@ -87,9 +85,6 @@ public: t->m_largest_clause = m_largest_clause; return t; } - - ~split_clause_tactic() override { - } char const* name() const override { return "split_clause"; } diff --git a/src/tactic/equiv_proof_converter.h b/src/tactic/equiv_proof_converter.h index 4a479a7ae..87a8f7131 100644 --- a/src/tactic/equiv_proof_converter.h +++ b/src/tactic/equiv_proof_converter.h @@ -32,8 +32,6 @@ public: equiv_proof_converter(ast_manager& m): m(m), m_replace(m) {} - ~equiv_proof_converter() override {} - proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { return m_replace(m, num_source, source); } diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index cb136ad9f..5322b523d 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -46,8 +46,6 @@ public: solver::updt_params(p); } - ~enum2bv_solver() override {} - solver* translate(ast_manager& dst_m, params_ref const& p) override { solver* result = alloc(enum2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); model_converter_ref mc = external_model_converter(); diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp index cd19b0dca..ee4a03d31 100644 --- a/src/tactic/fd_solver/pb2bv_solver.cpp +++ b/src/tactic/fd_solver/pb2bv_solver.cpp @@ -46,8 +46,6 @@ public: solver::updt_params(p); } - ~pb2bv_solver() override {} - solver* translate(ast_manager& dst_m, params_ref const& p) override { flush_assertions(); solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 18b97d116..f653e22e2 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -1867,9 +1867,7 @@ namespace smtfd { updt_params(p); add_toggle(m.mk_true()); } - - ~solver() override {} - + ::solver* translate(ast_manager& dst_m, params_ref const& p) override { solver* result = alloc(solver, m_indent, dst_m, p); if (m_fd_sat_solver) result->m_fd_sat_solver = m_fd_sat_solver->translate(dst_m, p); diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index a9294471e..9595cc606 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -70,7 +70,6 @@ public: result operator()(goal const & g) override { return !test(g); } - ~is_fp_qfnra_probe() override {} }; probe * mk_is_fp_qfnra_probe() { @@ -145,8 +144,6 @@ public: result operator()(goal const & g) override { return !test(g); } - - ~is_qffp_probe() override {} }; probe * mk_is_qffp_probe() { diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp index 0fdad5943..711eadc8f 100644 --- a/src/tactic/fpa/qffplra_tactic.cpp +++ b/src/tactic/fpa/qffplra_tactic.cpp @@ -82,8 +82,6 @@ public: test(g) && !test(g); } - - ~is_qffplra_probe() override {} }; probe * mk_is_qffplra_probe() { diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 55b7b27b4..5c08da76f 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -136,8 +136,6 @@ public: model2mc(model * m, labels_vec const & r):m_model(m), m_labels(r) {} - ~model2mc() override {} - void operator()(model_ref & m) override { if (!m || !m_model) { m = m_model; diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 073262edd..60041e434 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -130,8 +130,7 @@ class smt_strategic_solver_factory : public solver_factory { symbol m_logic; public: smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {} - - ~smt_strategic_solver_factory() override {} + solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { symbol l; if (m_logic != symbol::null) diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index c92968c8c..96458c711 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -131,8 +131,6 @@ public: return alloc(solver_subsumption_tactic, other_m, m_params); } - ~solver_subsumption_tactic() override {} - char const* name() const override { return "solver_subsumption"; } void updt_params(params_ref const& p) override { diff --git a/src/tactic/proof_converter.cpp b/src/tactic/proof_converter.cpp index b876f1216..d1905b383 100644 --- a/src/tactic/proof_converter.cpp +++ b/src/tactic/proof_converter.cpp @@ -86,7 +86,6 @@ class proof2pc : public proof_converter { proof_ref m_pr; public: proof2pc(ast_manager & m, proof * pr):m_pr(pr, m) {} - ~proof2pc() override {} proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 0); diff --git a/src/tactic/proof_converter.h b/src/tactic/proof_converter.h index fd4df7311..88152ce5b 100644 --- a/src/tactic/proof_converter.h +++ b/src/tactic/proof_converter.h @@ -25,7 +25,6 @@ class goal; class proof_converter : public converter { public: - ~proof_converter() override { } virtual proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) = 0; virtual proof_converter * translate(ast_translation & translator) = 0; }; diff --git a/src/tactic/replace_proof_converter.h b/src/tactic/replace_proof_converter.h index cc9a9c6c2..37bbf55b3 100644 --- a/src/tactic/replace_proof_converter.h +++ b/src/tactic/replace_proof_converter.h @@ -31,8 +31,6 @@ public: replace_proof_converter(ast_manager& _m): m(_m), m_proofs(m) {} - ~replace_proof_converter() override {} - proof_ref operator()(ast_manager & _m, unsigned num_source, proof * const * source) override; proof_converter * translate(ast_translation & translator) override; diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 57c6ae99a..d93a17ce1 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -51,8 +51,6 @@ public: , m_inc_use_sat(false) {} - ~qfufbv_ackr_tactic() override { } - char const* name() const override { return "qfufbv_ackr"; } void operator()(goal_ref const & g, goal_ref_buffer & result) override { diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index af8b24b2f..d919f51ee 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -35,7 +35,6 @@ class tactic : public user_propagator::core { unsigned m_ref_count; public: tactic():m_ref_count(0) {} - virtual ~tactic() {} void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h index f230d417b..c6be82daa 100644 --- a/src/tactic/tactic_exception.h +++ b/src/tactic/tactic_exception.h @@ -26,7 +26,6 @@ protected: std::string m_msg; public: tactic_exception(std::string && msg) : m_msg(std::move(msg)) {} - ~tactic_exception() override {} char const * msg() const override { return m_msg.c_str(); } }; diff --git a/src/test/api.cpp b/src/test/api.cpp index 2b6cda0ea..ccbbef6ea 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifdef _WINDOWS #include "api/z3.h" #include "api/z3_private.h" #include @@ -112,7 +111,3 @@ void tst_api() { test_bvneg(); test_mk_distinct(); } -#else -void tst_api() { -} -#endif diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index e418d5ea0..942714560 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifdef _WINDOWS #include "ast/reg_decl_plugins.h" #include "muz/base/dl_context.h" #include "muz/fp/dl_register_engine.h" @@ -23,7 +22,7 @@ namespace datalog { public: collector_of_reduced(idx_set & accumulator) : m_acc(accumulator) {} - virtual void operator()(table_element * func_columns, const table_element * merged_func_columns) { + void operator()(table_element * func_columns, const table_element * merged_func_columns) override { m_acc.insert(static_cast(merged_func_columns[0])); } }; @@ -352,6 +351,7 @@ namespace datalog { using namespace datalog; +#ifdef _WINDOWS void tst_dl_product_relation() { smt_params fparams; params_ref params; @@ -363,6 +363,6 @@ void tst_dl_product_relation() { } #else -void tst_dl_product_relation() { -} +void tst_dl_product_relation() {} + #endif diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp index a69e44cd2..412139eb8 100644 --- a/src/test/dl_relation.cpp +++ b/src/test/dl_relation.cpp @@ -4,8 +4,6 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifdef _WINDOWS - #include "ast/reg_decl_plugins.h" #include "muz/base/dl_context.h" #include "muz/fp/dl_register_engine.h" @@ -296,8 +294,3 @@ void tst_dl_relation() { datalog::test_interval_relation(); datalog::test_bound_relation(); } - -#else -void tst_dl_relation() { -} -#endif diff --git a/src/test/lp/argument_parser.h b/src/test/lp/argument_parser.h index f2a74f122..12ab02831 100644 --- a/src/test/lp/argument_parser.h +++ b/src/test/lp/argument_parser.h @@ -17,6 +17,7 @@ Revision History: --*/ +#pragma once #include #include diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index c7b0002cd..890ff90e3 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -1,3 +1,5 @@ +#pragma once + namespace lp { #include "math/lp/lp_utils.h" struct gomory_test { diff --git a/src/test/matcher.cpp b/src/test/matcher.cpp index 6d5576714..1d1c517fe 100644 --- a/src/test/matcher.cpp +++ b/src/test/matcher.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ -#ifdef _WINDOWS #include "ast/substitution/matcher.h" #include "ast/ast_pp.h" #include "ast/reg_decl_plugins.h" @@ -110,7 +109,3 @@ void tst1() { void tst_matcher() { tst1(); } -#else -void tst_matcher() { -} -#endif diff --git a/src/test/memory.cpp b/src/test/memory.cpp index 48ba35b78..9a8d12b5d 100644 --- a/src/test/memory.cpp +++ b/src/test/memory.cpp @@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifdef _WINDOWS #include "api/z3.h" #include "api/z3_private.h" #include @@ -59,8 +58,3 @@ void tst_memory() { Z3_reset_memory(); } - -#else -void tst_memory() { -} -#endif diff --git a/src/test/no_overflow.cpp b/src/test/no_overflow.cpp index eb26866a5..c1ba48ea7 100644 --- a/src/test/no_overflow.cpp +++ b/src/test/no_overflow.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ -#ifdef _WINDOWS #include "api/z3.h" #include "util/trace.h" @@ -724,7 +723,3 @@ void tst_no_overflow() { } } } -#else -void tst_no_overflow() { -} -#endif diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index a42ed86b1..944f64026 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifdef _WINDOWS #include "api/z3.h" #include "api/z3_private.h" #include @@ -214,8 +213,3 @@ void tst_simplifier() { test_bool(); test_skolemize_bug(); } - -#else -void tst_simplifier() { -} -#endif diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 30ef36d3e..b1f0c3cbe 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -312,13 +312,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o } void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) { -#if defined(_WINDOWS) && _MSC_VER <= 1700 - o.value = fmod(x.value, y.value); - if (o.value >= (y.value/2.0)) - o.value -= y.value; -#else o.value = remainder(x.value, y.value); -#endif } void hwf_manager::maximum(hwf const & x, hwf const & y, hwf & o) { diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h index 2841db609..de68b6b10 100644 --- a/src/util/max_cliques.h +++ b/src/util/max_cliques.h @@ -17,6 +17,7 @@ Notes: --*/ +#pragma once #include "util/vector.h" #include "util/uint_set.h" diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index ebbf235fb..6841031c3 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1630,11 +1630,7 @@ std::string mpf_manager::to_string_hexfloat(mpf const & x) { std::ios_base::showpoint | std::ios_base::showpos); ss.setf(ff); ss.precision(13); -#if defined(_WIN32) && _MSC_VER >= 1800 ss << std::hexfloat << to_double(x); -#else - ss << std::hex << (*reinterpret_cast(&(x))); -#endif return ss.str(); } diff --git a/src/util/trail.h b/src/util/trail.h index 969c4a746..9a7ec4303 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -243,7 +243,7 @@ public: m_value(m_vector.back()) { } - virtual void undo() { + void undo() override { m_vector.push_back(m_value); } }; diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h index cb0a58e37..1d54fb7b5 100644 --- a/src/util/z3_exception.h +++ b/src/util/z3_exception.h @@ -42,7 +42,6 @@ public: struct fmt {}; default_exception(std::string && msg) : m_msg(std::move(msg)) {} default_exception(fmt, char const* msg, ...); - ~default_exception() override {} char const * msg() const override; };