diff --git a/.github/workflows/android-build.yml b/.github/workflows/android-build.yml index eec9032df..019eb18b1 100644 --- a/.github/workflows/android-build.yml +++ b/.github/workflows/android-build.yml @@ -27,7 +27,7 @@ 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_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 ../ + cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_ANDROID_API=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} "-DCMAKE_ANDROID_NDK=$ANDROID_NDK_LATEST_HOME" -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" ../ make -j $(nproc) tar -cvf z3-build-${{ matrix.android-abi }}.tar *.jar *.so diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index f4b54cba0..3b19b8c25 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -886,8 +886,7 @@ def mk_hpp_from_pyg(pyg_file, output_dir): hpp = os.path.join(dirname, '%s.hpp' % class_name) out = open(hpp, 'w') out.write('// Automatically generated file\n') - out.write('#ifndef __%s_HPP_\n' % class_name.upper()) - out.write('#define __%s_HPP_\n' % class_name.upper()) + out.write('#pragma once\n') out.write('#include "util/params.h"\n') if export: out.write('#include "util/gparams.h"\n') @@ -919,7 +918,6 @@ def mk_hpp_from_pyg(pyg_file, output_dir): out.write(' %s %s() const { return p.%s("%s", %s); }\n' % (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) out.write('};\n') - out.write('#endif\n') out.close() OUTPUT_HPP_FILE.append(hpp) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 8896904dd..af982b2d4 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -124,7 +124,7 @@ namespace Microsoft.Z3 /// internal Symbol[] MkSymbols(string[] names) { - if (names == null) return null; + if (names == null) return new Symbol[0]; Symbol[] result = new Symbol[names.Length]; for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]); return result; diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 4582439ec..bb3f6fe8e 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -110,7 +110,7 @@ public class Context implements AutoCloseable { Symbol[] mkSymbols(String[] names) { if (names == null) - return null; + return new Symbol[0]; Symbol[] result = new Symbol[names.length]; for (int i = 0; i < names.length; ++i) result[i] = mkSymbol(names[i]); diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index aeb0939a0..7fb20e627 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -8,7 +8,7 @@ import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types'; * * **NOTE**: The set of solutions might be infinite. * Always ensure to limit amount generated, either by knowing that the - * solution space is constrainted, or by taking only a specified + * solution space is constrained, or by taking only a specified * amount of solutions * ```typescript * import { sliceAsync } from 'iter-tools'; @@ -46,7 +46,7 @@ async function* allSolutions(...assertions: Bool[]): .filter(decl => decl.arity() === 0) .map(decl => { const term = decl.call(); - // TODO(ritave): Assert not an array / uinterpeted sort + // TODO(ritave): Assert not an array / uninterpreted sort const value = model.eval(term, true); return term.neq(value); }), diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 662192bdd..e1a2b35ab 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -224,6 +224,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { function _toExpr(ast: Z3_ast): Bool | IntNum | RatNum | Arith | Expr { const kind = check(Z3.get_ast_kind(contextPtr, ast)); if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) { + if (Z3.is_quantifier_forall(contextPtr, ast)) + return new BoolImpl(ast); + if (Z3.is_quantifier_exists(contextPtr, ast)) + return new BoolImpl(ast); + if (Z3.is_lambda(contextPtr, ast)) + return new ExprImpl(ast); assert(false); } const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast))); diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index c27395d21..57e5c37f8 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -617,7 +617,7 @@ export interface Arith extends Expr | number | bigint | string): Arith; /** - * Substract second number from the first one + * Subtract second number from the first one */ sub(other: Arith | number | bigint | string): Arith; /** @@ -709,7 +709,7 @@ export interface RatNum extends Arith { } /** - * A Sort represting Bit Vector numbers of specified {@link BitVecSort.size size} + * A Sort representing Bit Vector numbers of specified {@link BitVecSort.size size} * * @typeParam Bits - A number representing amount of bits for this sort * @category Bit Vectors @@ -878,42 +878,42 @@ export interface BitVec& new_fmls) { + auto& unsafe_macros = m_macro_manager.unsafe_macros(); + for (auto* f : unsafe_macros) { + quantifier* q = m_macro_manager.get_macro_quantifier(f); + new_fmls.push_back(justified_expr(m, q, nullptr)); + } + unsafe_macros.reset(); +} + void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector& new_fmls) { + m_macro_manager.unsafe_macros().reset(); TRACE("macro_finder", tout << "processing macros...\n";); vector _new_fmls; if (expand_macros(n, fmls, _new_fmls)) { @@ -388,6 +398,7 @@ void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); + public: macro_finder(ast_manager & m, macro_manager & mm); ~macro_finder(); diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index 254663c66..032c724e1 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -241,12 +241,14 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { ast_manager& m; macro_manager& mm; + array_util a; expr_dependency_ref m_used_macro_dependencies; expr_ref_vector m_trail; macro_expander_cfg(ast_manager& m, macro_manager& mm): m(m), mm(mm), + a(m), m_used_macro_dependencies(m), m_trail(m) {} @@ -296,7 +298,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { return false; app * n = to_app(_n); quantifier * q = nullptr; - func_decl * d = n->get_decl(); + func_decl * d = n->get_decl(), *d2 = nullptr; TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";); if (mm.m_decl2macro.find(d, q)) { app * head = nullptr; @@ -343,6 +345,12 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed); return true; } + else if (a.is_as_array(d, d2) && mm.m_decl2macro.find(d2, q)) { + mm.unsafe_macros().insert(d2); + } + else if (a.is_map(d, d2) && mm.m_decl2macro.find(d2, q)) { + mm.unsafe_macros().insert(d2); + } return false; } }; diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h index 6aac12114..8f7d0c4b1 100644 --- a/src/ast/macros/macro_manager.h +++ b/src/ast/macros/macro_manager.h @@ -47,6 +47,7 @@ class macro_manager { expr_dependency_ref_vector m_macro_deps; obj_hashtable m_forbidden_set; func_decl_ref_vector m_forbidden; + obj_hashtable m_unsafe_macros; struct scope { unsigned m_decls_lim; unsigned m_forbidden_lim; @@ -86,7 +87,7 @@ public: quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; } void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const; void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep); - + obj_hashtable& unsafe_macros() { return m_unsafe_macros; } }; diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp index 7d543b0fb..b1d18092c 100644 --- a/src/math/interval/dep_intervals.cpp +++ b/src/math/interval/dep_intervals.cpp @@ -7,7 +7,7 @@ Abstract: - intervals with depedency tracking. + intervals with dependency tracking. Author: Nikolaj Bjorner (nbjorner) diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index 990816696..d14a0fc53 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -7,7 +7,7 @@ Abstract: - intervals with depedency tracking. + intervals with dependency tracking. Author: Nikolaj Bjorner (nbjorner) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index cce63855d..e7f8d0ea4 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -93,7 +93,7 @@ class lar_solver : public column_namer { unsigned_vector m_row_bounds_to_replay; u_set m_basic_columns_with_changed_cost; - // these are basic columns with the value changed, so the the corresponding row in the tableau + // these are basic columns with the value changed, so the corresponding row in the tableau // does not sum to zero anymore u_set m_incorrect_columns; // copy of m_r_solver.inf_set() diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 62455b625..f40400167 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -226,7 +226,7 @@ public: void set_next_arg(cmd_context & ctx, func_decl* t) override { m_target = t; if (t->get_family_id() != null_family_id) { - throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted"); + throw cmd_exception("Invalid query argument, expected uninterpreted function name, but argument is interpreted"); } datalog::context& dlctx = m_dl_ctx->dlctx(); if (!dlctx.get_predicates().contains(t)) { diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index eda00b64d..834bb41ef 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -25,7 +25,7 @@ Revision History: Let x_i, y_i, z_i be indices into the vectors x, y, z. Suppose that positions in P and R are annotated with what is - slicable. + sliceable. Sufficient conditions for sliceability: @@ -43,9 +43,9 @@ Revision History: and the positions where z_i is used in P and R are sliceable - A more refined approach may be using Gaussean elimination based + A more refined approach may be using Gaussian elimination based on x,z and eliminating variables from x,y (expressing them in terms - of a disjoint subeset of x,z). + of a disjoint subset of x,z). --*/ @@ -441,7 +441,7 @@ namespace datalog { void mk_slice::filter_unique_vars(rule& r) { // - // Variables that occur in multiple uinterpreted predicates are not sliceable. + // Variables that occur in multiple uninterpreted predicates are not sliceable. // uint_set used_vars; for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e5b13af98..dc63c2943 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -527,20 +527,21 @@ namespace sat { unsigned m_conflicts_since_init { 0 }; unsigned m_restarts { 0 }; - unsigned m_restart_next_out { 0 }; - unsigned m_conflicts_since_restart { 0 }; - bool m_force_conflict_analysis { false }; - unsigned m_simplifications { 0 }; - unsigned m_restart_threshold { 0 }; - unsigned m_luby_idx { 0 }; - unsigned m_conflicts_since_gc { 0 }; - unsigned m_gc_threshold { 0 }; - unsigned m_defrag_threshold { 0 }; - unsigned m_num_checkpoints { 0 }; - double m_min_d_tk { 0 } ; - unsigned m_next_simplify { 0 }; - bool m_simplify_enabled { true }; - bool m_restart_enabled { true }; + unsigned m_restart_next_out = 0; + unsigned m_conflicts_since_restart = 0; + bool m_force_conflict_analysis = false; + unsigned m_simplifications = 0; + unsigned m_restart_threshold = 0; + unsigned m_luby_idx = 0; + unsigned m_conflicts_since_gc = 0; + unsigned m_gc_threshold = 0; + unsigned m_defrag_threshold = 0; + unsigned m_num_checkpoints = 0; + double m_min_d_tk = 0.0 ; + unsigned m_next_simplify = 0; + double m_simplify_mult = 1.5; + bool m_simplify_enabled = true; + bool m_restart_enabled = true; bool guess(bool_var next); bool decide(); bool_var next_var(); @@ -713,7 +714,6 @@ namespace sat { // // ----------------------- public: - void set_should_simplify() { m_next_simplify = m_conflicts_since_init; } bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; } bool is_probing() const { return m_is_probing; } bool is_free(bool_var v) const { return m_free_vars.contains(v); } diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index 18f0bd951..88cca5257 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -57,8 +57,8 @@ namespace bv { remove(other); add_cc(v1, v2); } - else if (other->m_count > m_propagate_high_watermark) - s.s().set_should_simplify(); + else if (other->m_count > 2*m_propagate_high_watermark) + propagate(); } void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) { @@ -76,8 +76,8 @@ namespace bv { new_tmp(); gc(); } - if (other->m_count > m_propagate_high_watermark) - s.s().set_should_simplify(); + if (other->m_count > 2*m_propagate_high_watermark) + propagate(); } void ackerman::update_glue(vv& v) { @@ -137,6 +137,9 @@ namespace bv { if (m_num_propagations_since_last_gc <= s.get_config().m_dack_gc) return; m_num_propagations_since_last_gc = 0; + + if (m_table.size() > m_gc_threshold) + propagate(); while (m_table.size() > m_gc_threshold) remove(m_queue->prev()); @@ -147,7 +150,6 @@ namespace bv { } void ackerman::propagate() { - SASSERT(s.s().at_base_lvl()); auto* n = m_queue; vv* k = nullptr; unsigned num_prop = static_cast(s.s().get_stats().m_conflict * s.get_config().m_dack_factor); diff --git a/src/sat/smt/bv_ackerman.h b/src/sat/smt/bv_ackerman.h index f6465abc7..aab4053a2 100644 --- a/src/sat/smt/bv_ackerman.h +++ b/src/sat/smt/bv_ackerman.h @@ -51,13 +51,13 @@ namespace bv { solver& s; table_t m_table; - vv* m_queue { nullptr }; - vv* m_tmp_vv { nullptr }; + vv* m_queue = nullptr; + vv* m_tmp_vv = nullptr; - unsigned m_gc_threshold { 100 }; - unsigned m_propagate_high_watermark { 10000 }; - unsigned m_propagate_low_watermark { 10 }; - unsigned m_num_propagations_since_last_gc { 0 }; + unsigned m_gc_threshold = 100; + unsigned m_propagate_high_watermark = 10000; + unsigned m_propagate_low_watermark = 10; + unsigned m_num_propagations_since_last_gc = 0; bool_vector m_diff_levels; void update_glue(vv& v); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3be7e7b80..02a9f3c68 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -561,17 +561,9 @@ namespace smt { void theory_arith::mk_idiv_mod_axioms(expr * dividend, expr * divisor) { th_rewriter & s = ctx.get_rewriter(); if (!m_util.is_zero(divisor)) { - auto mk_mul = [&](expr* a, expr* b) { - if (m_util.is_mul(a)) { - ptr_vector args(to_app(a)->get_num_args(), to_app(a)->get_args()); - args.push_back(b); - return m_util.mk_mul(args.size(), args.data()); - } - return m_util.mk_mul(a, b); - }; // if divisor is zero, then idiv and mod are uninterpreted functions. expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m); - expr_ref eqz(m), eq(m), lower(m), upper(m), qr(m), le(m), ge(m); + expr_ref eqz(m), eq(m), lower(m), upper(m), qr(m), qr1(m), le(m), ge(m); div = m_util.mk_idiv(dividend, divisor); mod = m_util.mk_mod(dividend, divisor); zero = m_util.mk_int(0); @@ -579,7 +571,7 @@ namespace smt { abs_divisor = m_util.mk_sub(m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor), one); s(abs_divisor); eqz = m.mk_eq(divisor, zero); - qr = m_util.mk_add(mk_mul(divisor, div), mod); + qr = m_util.mk_add(m_util.mk_mul(divisor, div), mod); eq = m.mk_eq(qr, dividend); lower = m_util.mk_ge(mod, zero); upper = m_util.mk_le(mod, abs_divisor); @@ -589,16 +581,27 @@ namespace smt { tout << "lower: " << lower << "\n"; tout << "upper: " << upper << "\n";); - le = m_util.mk_le(m_util.mk_sub(qr, dividend), zero); - ge = m_util.mk_ge(m_util.mk_sub(qr, dividend), zero); - mk_axiom(eqz, le, false); - mk_axiom(eqz, ge, false); mk_axiom(eqz, eq, false); mk_axiom(eqz, lower, false); mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor)); + rational k; - // m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(dividend)); + m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(dividend)); + + // non-linear divisors/mod have to be flattened for the non-linear solver to understand the terms. + // to ensure this use the rewriter. This is a hack required to fix a latent bug that affects the + // legacy arithmetic solver broadly. It is not something that the newer arithmetic solver suffers from. + qr1 = qr; + s(qr1); + if (qr != qr1) { + expr_ref eq(m.mk_eq(qr, qr1), m); + ctx.internalize(eq, false); + literal qeq = ctx.get_literal(eq); + ctx.mark_as_relevant(qeq); + ctx.mk_th_axiom(get_id(), 1, &qeq); + m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(qr1)); + } if (m_util.is_zero(dividend)) { mk_axiom(eqz, m.mk_eq(div, zero)); diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index fabdb6abd..cffac2459 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -37,7 +37,7 @@ namespace smt { return; SASSERT(is_fixed(v)); - // WARNINING: it is not safe to use get_value(v) here, since + // WARNING: it is not safe to use get_value(v) here, since // get_value(v) may not satisfy v bounds at this point. if (!lower_bound(v).is_rational()) return; @@ -328,7 +328,6 @@ namespace smt { return; } context & ctx = get_context(); - region & r = ctx.get_region(); enode * _x = get_enode(x); enode * _y = get_enode(y); eq_vector const& eqs = antecedents.eqs(); diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 56fbd4ecf..699ebd5d2 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -711,7 +711,7 @@ namespace smt { for (; it != end; ++it) { if (!it->is_dead()) { if (is_fixed(it->m_var)) { - // WARNINING: it is not safe to use get_value(it->m_var) here, since + // WARNING: it is not safe to use get_value(it->m_var) here, since // get_value(it->m_var) may not satisfy it->m_var bounds at this point. numeral aux = lcm_den * it->m_coeff; consts += aux * lower_bound(it->m_var).get_rational(); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 556391250..6c4e1b3a7 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -294,8 +294,7 @@ namespace smt { m_trail_stack.push(add_var_pos_trail(b)); b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs); } - else { - SASSERT(th_id == null_theory_id); + else if (th_id == null_theory_id) { ctx.set_var_theory(l.var(), get_id()); SASSERT(ctx.get_var_theory(l.var()) == get_id()); bit_atom * b = new (get_region()) bit_atom(); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 46d2b0119..8f69c9489 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -591,7 +591,6 @@ namespace smt { get_antecedents(target, source, antecedents); if (l != null_literal) antecedents.push_back(l); - region & r = ctx.get_region(); ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), ctx, antecedents.size(), antecedents.data()))); return; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 7a46e1a1e..642103f73 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1241,6 +1241,7 @@ public: context& c = ctx(); if (!k.is_zero()) { mk_axiom(eq); + m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p)); mk_axiom(mk_literal(a.mk_ge(mod, zero))); mk_axiom(mk_literal(a.mk_le(mod, upper))); diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 18083452b..788f562d3 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -112,6 +112,7 @@ public: unsigned bv_sz; expr * f, * lhs, * rhs; +#if 0 auto match_bitmask = [&](expr* lhs, expr* rhs) { unsigned lo, hi; expr* arg; @@ -131,7 +132,8 @@ public: update_unsigned_upper(to_app(arg), val); return true; }; - +#endif + for (unsigned i = 0; i < sz; i++) { bool negated = false; f = g.form(i); diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 23099e0b5..22babb9cc 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -541,11 +541,10 @@ public: strm << "unknown module '" << module_name << "'"; throw exception(std::move(strm).str()); } - out << "## Module " << module_name << "\n\n"; + out << "\n## Module " << module_name << "\n\n"; char const * descr = nullptr; - if (get_module_descrs().find(module_name, descr)) { - out << "Description: " << descr; - } + if (get_module_descrs().find(module_name, descr)) + out << "Description: " << descr << "\n"; out << "\n"; d->display_markdown(out); } diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index ed73e21f0..324750cfa 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -20,10 +20,6 @@ Revision History: #include "util/warning.h" #include "util/z3_exception.h" -template -mpq_manager::mpq_manager() { -} - template mpq_manager::~mpq_manager() { del(m_tmp1); diff --git a/src/util/mpq.h b/src/util/mpq.h index 1b97b6ece..f1afcbe50 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -115,7 +115,7 @@ public: static bool precise() { return true; } static bool field() { return true; } - mpq_manager(); + mpq_manager() = default; ~mpq_manager(); diff --git a/src/util/rational.h b/src/util/rational.h index cffd0083c..4203a54ea 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -138,21 +138,15 @@ public: m().set(m_val, r.m_val); return *this; } -private: - rational & operator=(bool) { - UNREACHABLE(); return *this; - } - inline rational operator*(bool r1) const { - UNREACHABLE(); - return *this; - } -public: + rational & operator=(bool) = delete; + rational operator*(bool r1) const = delete; + rational & operator=(int v) { m().set(m_val, v); return *this; } - rational & operator=(double v) { UNREACHABLE(); return *this; } + rational & operator=(double v) = delete; friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }