From e83a70f9ad2153d480118b7d384e9016fe00dc02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Aug 2022 06:57:31 -0700 Subject: [PATCH 01/16] add newlines for description Signed-off-by: Nikolaj Bjorner --- src/util/gparams.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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); } From ea8b118eb1c50a3ca1138af5d1b4c34d7d77fa85 Mon Sep 17 00:00:00 2001 From: Eric Kilmer Date: Fri, 19 Aug 2022 11:02:26 -0700 Subject: [PATCH 02/16] Android CI: Configure with CMAKE_ANDROID_API (#6284) CMAKE_ANDROID_API will set CMAKE_SYSTEM_VERSION if it's not defined. Also remove setting CMake variable values that don't affect the ability to successfully configure in CI. --- .github/workflows/android-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From b26420ed997a6a064b8fdb243e7d2d07541a321a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Aug 2022 18:15:54 -0700 Subject: [PATCH 03/16] #6285 --- src/api/js/src/high-level/high-level.ts | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 78012c502..797d3a0ce 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 BoolImpl(ast); + if (Z3.is_quantifier_exists(contextPtr, ast)) + return BoolImpl(ast); + if (Z3.is_quantifier_lambda(contextPtr, ast)) + return ExprImpl(ast); assert(false); } const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast))); From bb5d81195c124f74906da83c4a58e03c3624f14b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Aug 2022 18:17:07 -0700 Subject: [PATCH 04/16] use equalities --- src/sat/sat_solver.h | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e5b13af98..60aadf8a1 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(); From 665ef2c6bae91fb13e7cf4f9aab37b89d08c473a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Aug 2022 18:21:03 -0700 Subject: [PATCH 05/16] add missing new Signed-off-by: Nikolaj Bjorner --- src/api/js/src/high-level/high-level.ts | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 797d3a0ce..a2e3187ee 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -225,11 +225,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { 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 BoolImpl(ast); + return new BoolImpl(ast); if (Z3.is_quantifier_exists(contextPtr, ast)) - return BoolImpl(ast); + return new BoolImpl(ast); if (Z3.is_quantifier_lambda(contextPtr, ast)) - return ExprImpl(ast); + return new ExprImpl(ast); assert(false); } const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast))); From 08bf7a62933c787c5184b64727a849b551ecf2a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Aug 2022 18:22:42 -0700 Subject: [PATCH 06/16] fix name Signed-off-by: Nikolaj Bjorner --- src/api/js/src/high-level/high-level.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index a2e3187ee..574944b41 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -228,7 +228,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new BoolImpl(ast); if (Z3.is_quantifier_exists(contextPtr, ast)) return new BoolImpl(ast); - if (Z3.is_quantifier_lambda(contextPtr, ast)) + if (Z3.is_lambda(contextPtr, ast)) return new ExprImpl(ast); assert(false); } From d5d77dfe642181d61f033be508daba2fc88bb286 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 20 Aug 2022 12:56:45 +0100 Subject: [PATCH 07/16] minor code simplifications --- scripts/mk_genfile_common.py | 4 +--- src/util/mpq.cpp | 4 ---- src/util/mpq.h | 2 +- src/util/rational.h | 14 ++++---------- 4 files changed, 6 insertions(+), 18 deletions(-) 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/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; } From 706f7fbdc786509169abbb8483f055da9e1689e7 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 22 Aug 2022 02:39:30 +0700 Subject: [PATCH 08/16] Fix some warnings about unused stuff. (#6290) --- src/smt/theory_arith_eq.h | 1 - src/smt/theory_dense_diff_logic_def.h | 1 - src/tactic/bv/bv_size_reduction_tactic.cpp | 4 +++- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index fabdb6abd..fab67a801 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -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_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/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); From 6ba9ada1e2d4aefd6cbe0602b743124b40e11628 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 22 Aug 2022 02:40:07 +0700 Subject: [PATCH 09/16] Fix typos. (#6291) --- src/api/js/src/high-level/high-level.test.ts | 4 ++-- src/api/js/src/high-level/types.ts | 20 ++++++++++---------- src/api/ml/README.md | 4 ++-- src/math/interval/dep_intervals.cpp | 2 +- src/math/interval/dep_intervals.h | 2 +- src/math/lp/lar_solver.h | 2 +- src/muz/fp/dl_cmds.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 8 ++++---- src/smt/theory_arith_eq.h | 2 +- src/smt/theory_arith_int.h | 2 +- 10 files changed, 24 insertions(+), 24 deletions(-) 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/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 BitVecget_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/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index fab67a801..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; 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(); From 56fb1615327b75567bbf2b3c5c64806f7ba6d9ff Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Sun, 21 Aug 2022 21:40:38 +0200 Subject: [PATCH 10/16] ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287) --- src/api/dotnet/Context.cs | 2 +- src/api/java/Context.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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]); From 2181a0ff7464ab4c6a140d258d6f1ad36689b501 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 15:19:51 -0700 Subject: [PATCH 11/16] #6289 --- src/smt/theory_arith_core.h | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3be7e7b80..931b31de0 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,22 @@ 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. + qr1 = qr; + s(qr1); + if (qr != qr1) { + mk_axiom(m.mk_eq(qr, qr1), false); + 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)); From be0cd74c71eb3e6f9709fb05e5aba78ba13ec35f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 15:20:12 -0700 Subject: [PATCH 12/16] #6289 --- src/smt/theory_lra.cpp | 1 + 1 file changed, 1 insertion(+) 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))); From 17fc43847623bff8a0a3e2fb1ebfbd6719e6d23a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 15:24:30 -0700 Subject: [PATCH 13/16] don't have bv-ackerman influence simplification previous scheme has Ackmerman module instrument main solver to backjump and simplify when reaching a threshold. This destroys overall performance: simplification does many more things than invoking Ackerman axioms. Having a dependency between simplification (in-processing) and depleting a priority queue of auxiliary axioms therefore hurts overall performance. It has to be decoupled. The current approach is now to empty the axiom queue on occasion. It is still not ideal - it should be coupled with the search level - axioms don't survive higher levels where redundant clauses get garbage collected as they don't have a chance of being used. --- src/sat/sat_solver.h | 1 - src/sat/smt/bv_ackerman.cpp | 12 +++++++----- src/sat/smt/bv_ackerman.h | 12 ++++++------ 3 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 60aadf8a1..dc63c2943 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -714,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); From 409230259095bdc157321c5bdc2d8644f1157fda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 15:37:43 -0700 Subject: [PATCH 14/16] use interface for creating unary equalities Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 931b31de0..02a9f3c68 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -590,11 +590,16 @@ namespace smt { 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. + // 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) { - mk_axiom(m.mk_eq(qr, qr1), false); + 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)); } From a38308792efceb062fd1b9d5ad6c52ef9a47f552 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 15:47:19 -0700 Subject: [PATCH 15/16] #6288 floating points may also track bit-literals. Since the legacy solver doesn't handle dual tracking of literals we just let the floating point solver track. --- src/smt/theory_bv.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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(); From 9eb4237dfe23a70ec15b5e55b6ee2688d1ef46bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 16:32:01 -0700 Subject: [PATCH 16/16] fix #6292 this patches a case where macro-finder is used with arrays. It doesn't work so macro quantifiers have to be re-instated to ensure correctness --- src/ast/array_decl_plugin.h | 1 + src/ast/macros/macro_finder.cpp | 11 +++++++++++ src/ast/macros/macro_finder.h | 2 ++ src/ast/macros/macro_manager.cpp | 10 +++++++++- src/ast/macros/macro_manager.h | 3 ++- 5 files changed, 25 insertions(+), 2 deletions(-) diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 6fe2c7657..fdad692ac 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -178,6 +178,7 @@ public: bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); } bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); } bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); } + bool is_map(func_decl* f, func_decl*& g) const { return is_map(f) && (g = get_map_func_decl(f), true); } func_decl * get_as_array_func_decl(expr * n) const; func_decl * get_as_array_func_decl(func_decl* f) const; func_decl * get_map_func_decl(func_decl* f) const; diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp index ec2c166c9..e7452ee9c 100644 --- a/src/ast/macros/macro_finder.cpp +++ b/src/ast/macros/macro_finder.cpp @@ -376,7 +376,17 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect return found_new_macro; } +void macro_finder::revert_unsafe_macros(vector& 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; } };