From 391880b6fcef2e8cb7a7a8dc0deb7533525b1a2a Mon Sep 17 00:00:00 2001 From: Wael Boutglay Date: Thu, 25 Sep 2025 21:04:15 +0200 Subject: [PATCH 01/45] Add missing `::z3::sdiv` to z3++.h (#7947) --- src/api/c++/z3++.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 0a1e359da..9fb84236d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2173,7 +2173,15 @@ namespace z3 { inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); } inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); } inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); } + /** + \brief signed division operator for bitvectors. + */ + inline expr sdiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsdiv(a.ctx(), a, b)); } + inline expr sdiv(expr const & a, int b) { return sdiv(a, a.ctx().num_val(b, a.get_sort())); } + inline expr sdiv(int a, expr const & b) { return sdiv(b.ctx().num_val(a, b.get_sort()), b); } + +/** \brief unsigned division operator for bitvectors. */ inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); } From b7eb21efedfbf691cbd1928c5f06af689ba1ed65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Sep 2025 12:44:56 +0300 Subject: [PATCH 02/45] fix #7948 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 1 + src/math/polynomial/upolynomial.cpp | 3 +++ src/util/rlimit.cpp | 2 ++ 3 files changed, 6 insertions(+) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index fec10fe0e..a8b3abc8a 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -184,6 +184,7 @@ struct solver::imp { lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; try { + //verbose_stream() << m_limit. r = m_nlsat->check(); } catch (z3_exception&) { diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index a73d3e5fb..56d8524d4 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -3094,6 +3094,9 @@ namespace upolynomial { A.swap(D); // D is of the form P_{j+1} * P_{j+2} * ... * P_k j++; + if (j > 10000) { + display(verbose_stream(), A) << "\n"; + } } TRACE(factor_bug, tout << "A: "; display(tout, A); tout << "\n";); SASSERT(A.size() == 1 && m().is_one(A[0])); diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 28656bc63..3a3cdbc87 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -78,6 +78,8 @@ char const* reslimit::get_cancel_msg() const { void reslimit::push_child(reslimit* r) { lock_guard lock(*g_rlimit_mux); + r->m_limit = std::min(r->m_limit, m_limit - std::min(m_limit, m_count)); + r->m_count = 0; m_children.push_back(r); } From bda98d8da4453e6d6ccf9484879a636f0806cd63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Sep 2025 12:45:42 +0300 Subject: [PATCH 03/45] fix #7948 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 1 - src/math/polynomial/upolynomial.cpp | 3 --- 2 files changed, 4 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index a8b3abc8a..fec10fe0e 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -184,7 +184,6 @@ struct solver::imp { lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; try { - //verbose_stream() << m_limit. r = m_nlsat->check(); } catch (z3_exception&) { diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 56d8524d4..a73d3e5fb 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -3094,9 +3094,6 @@ namespace upolynomial { A.swap(D); // D is of the form P_{j+1} * P_{j+2} * ... * P_k j++; - if (j > 10000) { - display(verbose_stream(), A) << "\n"; - } } TRACE(factor_bug, tout << "A: "; display(tout, A); tout << "\n";); SASSERT(A.size() == 1 && m().is_one(A[0])); From ae55b6fa1efbdfadca9bb9251f8c710279b73429 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Sep 2025 13:02:05 +0300 Subject: [PATCH 04/45] add analysis Signed-off-by: Nikolaj Bjorner --- .github/workflows/codeql-analysis.yml | 41 ++++++++++ codeql/custom_queries/FindUnderspecified.ql | 87 +++++++++++++++++++++ 2 files changed, 128 insertions(+) create mode 100644 .github/workflows/codeql-analysis.yml create mode 100644 codeql/custom_queries/FindUnderspecified.ql diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml new file mode 100644 index 000000000..d53c5453c --- /dev/null +++ b/.github/workflows/codeql-analysis.yml @@ -0,0 +1,41 @@ +name: "CodeQL" + +on: + push: + branches: [ master ] + pull_request: + branches: [ master ] + schedule: + - cron: '0 0 * * 0' + +jobs: + analyze: + name: Analyze + runs-on: ubuntu-latest + permissions: + actions: read + contents: read + security-events: write + + strategy: + fail-fast: false + matrix: + language: [cpp] + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Initialize CodeQL + uses: github/codeql-action/init@v3 + with: + languages: ${{ matrix.language }} + + - name: Autobuild + uses: github/codeql-action/autobuild@v3 + + - name: Run CodeQL Query + uses: github/codeql-action/analyze@v3 + with: + category: 'custom' + queries: ./codeql/custom-queries \ No newline at end of file diff --git a/codeql/custom_queries/FindUnderspecified.ql b/codeql/custom_queries/FindUnderspecified.ql new file mode 100644 index 000000000..0d33dc4f8 --- /dev/null +++ b/codeql/custom_queries/FindUnderspecified.ql @@ -0,0 +1,87 @@ + /** + + * Finds function calls with arguments that have unspecified evaluation order. + + * + + * @name Unspecified argument evaluation order + + * @kind problem + + * @problem.severity warning + + * @id cpp/z3/unspecevalorder + + */ + + + + import cpp + + + + predicate isPureFunc(Function f) { + + f.getName() = "m" or + + not exists(Assignment a | a.getEnclosingFunction() = f) and + + forall(FunctionCall g | g.getEnclosingFunction() = f | isPureFunc(g.getTarget())) + + } + + + + predicate sideEffectfulArgument(Expr a) { + + exists(Function f | f = a.(FunctionCall).getTarget() | + + not f instanceof ConstMemberFunction and + + not isPureFunc(f) + + ) + + or + + exists(ArrayExpr b | b = a.(ArrayExpr) | + + sideEffectfulArgument(b.getArrayBase()) or sideEffectfulArgument(b.getArrayOffset()) + + ) + + or + + exists(Assignment b | b = a) + + or + + exists(BinaryOperation b | b = a | sideEffectfulArgument(b.getAnOperand())) + + or + + exists(UnaryOperation b | b = a | sideEffectfulArgument(b.getOperand())) + + } + + + + from FunctionCall f, Expr a, int i, Expr b, int j where + + i < j and + + f.getTarget().getName() != "operator&&" and + + f.getTarget().getName() != "operator||" and + + a = f.getArgument(i) and + + b = f.getArgument(j) and + + sideEffectfulArgument(a) and + + sideEffectfulArgument(b) + + select f, "potentially unspecified evaluation order of function arguments: $@ and $@", a, + + i.toString(), b, j.toString() \ No newline at end of file From b5f79da76a3f5c6606553e217bc351d31aeec604 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Sep 2025 13:03:31 +0300 Subject: [PATCH 05/45] add analysis Signed-off-by: Nikolaj Bjorner --- .github/workflows/codeql-analysis.yml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml index d53c5453c..5738a05b6 100644 --- a/.github/workflows/codeql-analysis.yml +++ b/.github/workflows/codeql-analysis.yml @@ -1,12 +1,9 @@ name: "CodeQL" on: - push: - branches: [ master ] - pull_request: - branches: [ master ] schedule: - - cron: '0 0 * * 0' + - cron: '0 0 */2 * *' + jobs: analyze: From 253a7245d0aeb129f5823fe3a62e1292ea4222af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Sep 2025 13:05:04 +0300 Subject: [PATCH 06/45] add analysis Signed-off-by: Nikolaj Bjorner --- .github/workflows/codeql-analysis.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml index 5738a05b6..397145536 100644 --- a/.github/workflows/codeql-analysis.yml +++ b/.github/workflows/codeql-analysis.yml @@ -1,8 +1,7 @@ name: "CodeQL" on: - schedule: - - cron: '0 0 */2 * *' + workflow_dispatch: jobs: From 339f0cd5f93c8d5c3ee5da7fee4cbe73ab914eb2 Mon Sep 17 00:00:00 2001 From: Ruijie Fang <57693513+ruijiefang@users.noreply.github.com> Date: Tue, 30 Sep 2025 11:55:14 -0500 Subject: [PATCH 07/45] Correctly distinguish between `Lambda` and `Quantifier` in Z3 Java API (#7955) * Distinguish between Quantifier and Lambda in AST.java * Distinguish betwee Lambda and Quantifier in Expr.java * Make things compile --- src/api/java/AST.java | 8 +++++++- src/api/java/Expr.java | 11 +++++++++-- src/api/java/Lambda.java | 2 +- 3 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 99cdde948..0257f5294 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable case Z3_FUNC_DECL_AST: return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: - return new Quantifier(ctx, obj); + // a quantifier AST is a lambda iff it is neither a forall nor an exists. + boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); + if (isLambda) { + return new Lambda(ctx, obj); + } else { + return new Quantifier(ctx, obj); + } case Z3_SORT_AST: return Sort.create(ctx, obj); case Z3_APP_AST: diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 60826665d..910869bcd 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2148,8 +2148,15 @@ public class Expr extends AST static Expr create(Context ctx, long obj) { Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); - if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) - return new Quantifier(ctx, obj); + if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) { + // a quantifier AST is a lambda iff it is neither a forall nor an exists. + boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); + if (isLambda) { + return new Lambda(ctx, obj); + } else { + return new Quantifier(ctx, obj); + } + } long s = Native.getSort(ctx.nCtx(), obj); Z3_sort_kind sk = Z3_sort_kind .fromInt(Native.getSortKind(ctx.nCtx(), s)); diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java index 780e543c8..a42dfbf45 100644 --- a/src/api/java/Lambda.java +++ b/src/api/java/Lambda.java @@ -126,7 +126,7 @@ public class Lambda extends ArrayExpr } - private Lambda(Context ctx, long obj) + Lambda(Context ctx, long obj) { super(ctx, obj); } From 65c9a18c3a5b71d382a4fec71b17708ff6a00f50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Sep 2025 15:41:40 -0700 Subject: [PATCH 08/45] fix #7956 Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 0841f73ee..3ce1ece4a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1621,7 +1621,7 @@ namespace smt2 { if (curr_id_is_underscore()) { has_as = false; return parse_indexed_identifier_core(); - } + } else { SASSERT(curr_id_is_as()); has_as = true; @@ -1638,8 +1638,10 @@ namespace smt2 { // '(' 'as' ')' // '(' '_' + ')' // '(' 'as' (|)+ ')' ')' - symbol parse_qualified_identifier(bool & has_as) { + // '(' lambda (...) ')' + symbol parse_qualified_identifier(bool & has_as, bool & is_lambda) { SASSERT(curr_is_lparen() || curr_is_identifier()); + is_lambda = false; if (curr_is_identifier()) { has_as = false; symbol r = curr_id(); @@ -1648,6 +1650,12 @@ namespace smt2 { } SASSERT(curr_is_lparen()); next(); + if (curr_id_is_lambda()) { + is_lambda = true; + has_as = false; + return symbol("select"); + } + if (!curr_is_identifier() || (!curr_id_is_underscore() && !curr_id_is_as())) throw parser_exception("invalid qualified/indexed identifier, '_' or 'as' expected"); return parse_qualified_identifier_core(has_as); @@ -1860,11 +1868,14 @@ namespace smt2 { SASSERT(curr_is_lparen() || curr_is_identifier()); unsigned param_spos = m_param_stack.size(); unsigned expr_spos = expr_stack().size(); - bool has_as; - symbol f = parse_qualified_identifier(has_as); - void * mem = m_stack.allocate(sizeof(quant_frame)); + bool has_as, is_lambda; + auto f = parse_qualified_identifier(has_as, is_lambda); + + void * mem = m_stack.allocate(sizeof(app_frame)); new (mem) app_frame(f, expr_spos, param_spos, has_as); m_num_expr_frames++; + if (is_lambda) + push_quant_frame(lambda_k); } void push_expr_frame(expr_frame * curr) { From 0881a71ed234f3da155a7d0967831a987035fa99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Sep 2025 15:42:01 -0700 Subject: [PATCH 09/45] update format Signed-off-by: Nikolaj Bjorner --- .clang-format | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.clang-format b/.clang-format index c4bbbf1e1..76669e19e 100644 --- a/.clang-format +++ b/.clang-format @@ -8,6 +8,7 @@ BasedOnStyle: LLVM IndentWidth: 4 TabWidth: 4 UseTab: Never +IndentCaseLabels: false # Column width ColumnLimit: 120 @@ -34,6 +35,7 @@ BraceWrapping: AfterControlStatement: false AfterNamespace: false AfterStruct: false + BeforeElse : true # Spacing SpaceAfterCStyleCast: false SpaceAfterLogicalNot: false @@ -42,7 +44,6 @@ SpaceInEmptyParentheses: false SpacesInCStyleCastParentheses: false SpacesInParentheses: false SpacesInSquareBrackets: false -IndentCaseLabels: false # Alignment AlignConsecutiveAssignments: false @@ -56,6 +57,7 @@ BinPackArguments: true BinPackParameters: true BreakBeforeBinaryOperators: None BreakBeforeTernaryOperators: true +# BreakBeforeElse: true # Includes SortIncludes: false # Z3 has specific include ordering conventions From 72c89e1a4e188c7bd07747853b526539ff307105 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Sep 2025 15:58:48 -0700 Subject: [PATCH 10/45] fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 9e154f9dc..f90768c0a 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -776,10 +776,26 @@ namespace datalog { array_util ar; DL_ENGINE m_engine_type; - bool is_large_bv(sort* s) { + bool is_large_bv(expr *e) { + sort *s = e->get_sort(); + if (bv.is_bv_sort(s)) { + unsigned sz = bv.get_bv_size(s); + if (sz > 24) + return true; + } + if (is_app(e)) { + unsigned sz = 0; + for (auto arg : *to_app(e)) { + if (bv.is_bv(arg)) + sz += bv.get_bv_size(arg->get_sort()); + } + if (sz > 24) + return true; + } return false; } + public: engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), ar(m), m_engine_type(DATALOG_ENGINE) {} @@ -795,7 +811,7 @@ namespace datalog { else if (dt.is_datatype(e->get_sort())) { m_engine_type = SPACER_ENGINE; } - else if (is_large_bv(e->get_sort())) { + else if (is_large_bv(e)) { m_engine_type = SPACER_ENGINE; } else if (!e->get_sort()->get_num_elements().is_finite()) { From 5d8fcaa3ee3d0d532a322c20f1fa99d9ef0e2bb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 10:39:37 -0700 Subject: [PATCH 11/45] update clang format --- .clang-format | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.clang-format b/.clang-format index 76669e19e..1d7d35dc5 100644 --- a/.clang-format +++ b/.clang-format @@ -8,7 +8,7 @@ BasedOnStyle: LLVM IndentWidth: 4 TabWidth: 4 UseTab: Never -IndentCaseLabels: false + # Column width ColumnLimit: 120 @@ -36,6 +36,7 @@ BraceWrapping: AfterNamespace: false AfterStruct: false BeforeElse : true + AfterCaseLabel: false # Spacing SpaceAfterCStyleCast: false SpaceAfterLogicalNot: false @@ -65,6 +66,11 @@ SortIncludes: false # Z3 has specific include ordering conventions # Namespaces NamespaceIndentation: All +# Switch statements +IndentCaseLabels: false +AllowShortCaseLabelsOnASingleLine: true +IndentCaseBlocks: false + # Comments and documentation ReflowComments: true SpacesBeforeTrailingComments: 2 From 0e6b3a922acc249e2c26c24b3e4b2bc130f325c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 10:47:10 -0700 Subject: [PATCH 12/45] Add commands for forcing preferences during search MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add commands: (prefer ) - will instruct case split queue to assign formula to true. - prefer commands added within a scope are forgotten after leaving the scope. (reset-preferences) - resets asserted preferences. Has to be invoked at base level. This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2 --- src/cmd_context/basic_cmds.cpp | 48 ++++++++++++++ src/cmd_context/cmd_context.cpp | 33 +++++++++- src/cmd_context/cmd_context.h | 4 ++ src/smt/theory_bv.cpp | 2 + src/smt/theory_user_propagator.cpp | 63 ++++++------------ src/solver/preferred_value_propagator.h | 85 +++++++++++++++++++++++++ 6 files changed, 190 insertions(+), 45 deletions(-) create mode 100644 src/solver/preferred_value_propagator.h diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index ff74e4614..ed7e14b20 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -334,6 +334,52 @@ public: } }; +class prefer_cmd : public cmd { + expr *m_formula = nullptr; + +public: + prefer_cmd() : cmd("prefer") {} + char const *get_usage() const override { + return ""; + } + char const *get_descr(cmd_context &ctx) const override { + return "set a preferred formula for the solver"; + } + unsigned get_arity() const override { + return 1; + } + void prepare(cmd_context &ctx) override { + m_formula = nullptr; + } + cmd_arg_kind next_arg_kind(cmd_context &ctx) const override { + return CPK_EXPR; + } + void set_next_arg(cmd_context &ctx, expr *e) override { + m_formula = e; + } + void execute(cmd_context &ctx) override { + SASSERT(m_formula); + ctx.set_preferred(m_formula); + } +}; + +class reset_preferences_cmd : public cmd { + public: + reset_preferences_cmd() : cmd("reset-preferences") {} + char const *get_usage() const override { + return ""; + } + char const *get_descr(cmd_context &ctx) const override { + return "reset all preferred formulas"; + } + unsigned get_arity() const override { + return 0; + } + void execute(cmd_context &ctx) override { + ctx.reset_preferred(); + } +}; + class set_get_option_cmd : public cmd { protected: symbol m_true; @@ -926,6 +972,8 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(get_info_cmd)); ctx.insert(alloc(set_info_cmd)); ctx.insert(alloc(set_initial_value_cmd)); + ctx.insert(alloc(prefer_cmd)); + ctx.insert(alloc(reset_preferences_cmd)); ctx.insert(alloc(get_consequences_cmd)); ctx.insert(alloc(builtin_cmd, "assert", "", "assert term.")); ctx.insert(alloc(builtin_cmd, "check-sat", "*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true.")); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4f093e749..4af0782e1 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -628,6 +628,7 @@ cmd_context::~cmd_context() { finalize_tactic_manager(); m_proof_cmds = nullptr; m_var2values.reset(); + m_preferred = nullptr; reset(true); m_mcs.reset(); m_solver = nullptr; @@ -1518,6 +1519,8 @@ void cmd_context::reset(bool finalize) { m_dt_eh = nullptr; m_std_subst = nullptr; m_rev_subst = nullptr; + m_preferred = nullptr; + m_var2values.reset(); if (m_manager) { dealloc(m_pmanager); m_pmanager = nullptr; @@ -1884,6 +1887,29 @@ void cmd_context::set_initial_value(expr* var, expr* value) { m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())}); } +void cmd_context::set_preferred(expr* fmla) { + if (!m_preferred) { + auto p = alloc(preferred_value_propagator, m()); + m_preferred = p; + if (get_solver()) { + get_solver()->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh); + get_solver()->user_propagate_register_decide(p->decide_eh); + } + } + m_preferred->set_preferred(fmla); + if (get_opt()) { + throw default_exception("setting preferred on optimization context is not supported yet"); + return; + } +} + +void cmd_context::reset_preferred() { + if (!m_scopes.empty()) + throw default_exception("reset-preferred can only be invoked at base level"); + if (m_preferred) + m_preferred->reset_preferred(); +} + void cmd_context::display_model(model_ref& mdl) { if (mdl) { @@ -2261,8 +2287,13 @@ void cmd_context::mk_solver() { m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); m_solver = mk_slice_solver(m_solver.get()); - if (m_simplifier_factory) + if (m_simplifier_factory) m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory); + if (m_preferred) { + auto p = m_preferred.get(); + m_solver->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh); + m_solver->user_propagate_register_decide(p->decide_eh); + } } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 83d0f06ee..ddc8b461a 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -39,6 +39,7 @@ Notes: #include "solver/check_logic.h" #include "solver/progress_callback.h" #include "solver/simplifier_solver.h" +#include "solver/preferred_value_propagator.h" #include "cmd_context/pdecl.h" #include "cmd_context/tactic_manager.h" #include "params/context_params.h" @@ -265,6 +266,7 @@ protected: dictionary m_object_refs; // anything that can be named. dictionary m_user_tactic_decls; vector> m_var2values; + scoped_ptr m_preferred; dictionary m_func_decls; obj_map m_func_decl2alias; @@ -429,6 +431,8 @@ public: void set_solver(solver* s) { m_solver = s; } void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; } void set_initial_value(expr* var, expr* value); + void set_preferred(expr *fmla); + void reset_preferred(); void set_solver_factory(solver_factory * s); void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 93f09f639..7b0afd7e1 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1890,6 +1890,8 @@ namespace smt { theory_bv::var_enode_pos theory_bv::get_bv_with_theory(bool_var v, theory_id id) const { atom* a = get_bv2a(v); + if (!a) + return var_enode_pos(nullptr, UINT32_MAX); svector vec; if (!a->is_bit()) return var_enode_pos(nullptr, UINT32_MAX); diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index f8c2a35b8..d8adbdb70 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -209,61 +209,36 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) { if (!m_decide_eh) return; - const bool_var_data& d = ctx.get_bdata(var); + expr *e = ctx.bool_var2expr(var); + if (!e) + e = m.mk_true(); // use a dummy case split atom. - if (!d.is_enode() && !d.is_theory_atom()) - return; - - enode* original_enode = nullptr; - unsigned original_bit = 0; - bv_util bv(m); - theory* th = nullptr; - theory_var v = null_theory_var; - - // get the associated theory - if (!d.is_enode()) { - // it might be a value that does not have an enode - th = ctx.get_theory(d.get_theory()); - } - else { - original_enode = ctx.bool_var2enode(var); - v = original_enode->get_th_var(get_family_id()); - if (v == null_theory_var) { - // it is not a registered boolean expression - th = ctx.get_theory(d.get_theory()); + unsigned bit = 0; + // determine if case split is a bit-position in a bit-vector + { + bv_util bv(m); + auto th = ctx.get_theory(bv.get_fid()); + if (th) { + // it is then n'th bit of a bit-vector n. + auto [n, nbit] = static_cast(th)->get_bv_with_theory(var, get_family_id()); + if (n) { + e = n->get_expr(); + bit = nbit; + } } } - if (v == null_theory_var && !th) - return; - - if (v == null_theory_var && th->get_family_id() != bv.get_fid()) - return; - - if (v == null_theory_var) { - // it is not a registered boolean value but it is a bitvector - auto registered_bv = ((theory_bv*) th)->get_bv_with_theory(var, get_family_id()); - if (!registered_bv.first) - // there is no registered bv associated with the bit - return; - original_enode = registered_bv.first; - original_bit = registered_bv.second; - v = original_enode->get_th_var(get_family_id()); - } - - // call the registered callback - unsigned new_bit = original_bit; - force_push(); - expr *e = var2expr(v); - m_decide_eh(m_user_context, this, e, new_bit, is_pos); + m_decide_eh(m_user_context, this, e, bit, is_pos); bool_var new_var; if (!get_case_split(new_var, is_pos) || new_var == var) // The user did not interfere return; + TRACE(user_propagate, + tout << "decide: " << ctx.bool_var2expr(var) << " -> " << ctx.bool_var2expr(new_var) << "\n"); var = new_var; - + // check if the new variable is unassigned if (ctx.get_assignment(var) != l_undef) throw default_exception("expression in \"decide\" is already assigned"); diff --git a/src/solver/preferred_value_propagator.h b/src/solver/preferred_value_propagator.h new file mode 100644 index 000000000..da83c1fa3 --- /dev/null +++ b/src/solver/preferred_value_propagator.h @@ -0,0 +1,85 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + preferred_value_propagator.h + +Abstract: + + Specialized propagator for preferred values + +Author: + + Nikolaj Bjorner (nbjorner) 10-2-2025 + +Notes: + +--*/ +#pragma once + +#include "tactic/user_propagator_base.h" +#include "util/trail.h" + + +class preferred_value_propagator { + ast_manager &m; + expr_ref_vector m_preferred; + unsigned m_qhead = 0; + trail_stack m_trail; + + bool decide(user_propagator::callback& cb) { + if (m_qhead >= m_preferred.size()) + return false; + m_trail.push(value_trail(m_qhead)); + while (m_qhead < m_preferred.size()) { + expr *e = m_preferred.get(m_qhead); + bool is_not = m.is_not(e, e); + m_qhead++; + if (cb.next_split_cb(e, 0, is_not ? l_false : l_true)) + return true; + } + return false; + } + +public: + preferred_value_propagator(ast_manager &m) : m(m), m_preferred(m) { + push_eh = [](void * ctx, user_propagator::callback* cb) { + auto &p = *static_cast(ctx); + p.m_trail.push_scope(); + }; + pop_eh = [](void * ctx, user_propagator::callback* cb, unsigned n) -> void { + auto &p = *static_cast(ctx); + p.m_trail.pop_scope(n); + }; + fresh_eh = [](void* ctx, ast_manager& dst, user_propagator::context_obj*& co) -> void* { + auto &p = *static_cast(ctx); + ast_translation tr(p.m, dst); + auto r = alloc(preferred_value_propagator, dst); + for (auto e : p.m_preferred) + r->set_preferred(tr(e)); + return r; + }; + + decide_eh = [](void * ctx, user_propagator::callback * cb, expr *, unsigned, bool) -> bool { + auto &p = *static_cast(ctx); + return p.decide(*cb); + }; + } + ~preferred_value_propagator() = default; + void set_preferred(expr *e) { + m_preferred.push_back(e); + if (m_trail.get_num_scopes() > 0) + m_trail.push(push_back_vector(m_preferred)); + } + void reset_preferred() { + if (m_trail.get_num_scopes() != 0) + throw default_exception("cannot reset preferred values in scoped context"); + m_preferred.reset(); + SASSERT(m_qhead == 0); + } + user_propagator::push_eh_t push_eh; + user_propagator::pop_eh_t pop_eh; + user_propagator::fresh_eh_t fresh_eh; + user_propagator::decide_eh_t decide_eh; +}; \ No newline at end of file From e137aaa24988b315874fedbfa0e512fcf89ef463 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 19:44:22 -0700 Subject: [PATCH 13/45] add user propagators to opt_solver --- src/cmd_context/cmd_context.cpp | 8 +++--- src/cmd_context/cmd_context.h | 5 +++- src/opt/opt_context.cpp | 5 ++++ src/opt/opt_context.h | 3 ++- src/opt/opt_solver.h | 43 +++++++++++++++++++++++++++++++++ 5 files changed, 58 insertions(+), 6 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4af0782e1..5513a86ef 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -657,6 +657,8 @@ void cmd_context::set_opt(opt_wrapper* opt) { for (auto const& [var, value] : m_var2values) m_opt->initialize_value(var, value); m_opt->set_logic(m_logic); + if (m_preferred) + m_opt->set_preferred(m_preferred.get()); } void cmd_context::global_params_updated() { @@ -1896,11 +1898,9 @@ void cmd_context::set_preferred(expr* fmla) { get_solver()->user_propagate_register_decide(p->decide_eh); } } + if (get_opt()) + get_opt()->set_preferred(m_preferred.get()); m_preferred->set_preferred(fmla); - if (get_opt()) { - throw default_exception("setting preferred on optimization context is not supported yet"); - return; - } } void cmd_context::reset_preferred() { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index ddc8b461a..b08944616 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -164,6 +164,9 @@ struct builtin_decl { }; class opt_wrapper : public check_sat_result { +protected: + preferred_value_propagator *m_preferred = nullptr; + public: opt_wrapper(ast_manager& m): check_sat_result(m) {} virtual bool empty() = 0; @@ -177,7 +180,7 @@ public: virtual void get_box_model(model_ref& mdl, unsigned index) = 0; virtual void updt_params(params_ref const& p) = 0; virtual void initialize_value(expr* var, expr* value) = 0; - + void set_preferred(preferred_value_propagator *p) { m_preferred = p; } }; class ast_context_params : public context_params { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6244533f0..388befe93 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -316,6 +316,11 @@ namespace opt { m_model_converter->convert_initialize_value(m_scoped_state.m_values); for (auto & [var, value] : m_scoped_state.m_values) s.user_propagate_initialize_value(var, value); + if (m_preferred) { + auto p = m_preferred; + s.user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh); + s.user_propagate_register_decide(p->decide_eh); + } opt_params optp(m_params); symbol pri = optp.priority(); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 123d3a44b..ed2377bab 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -22,6 +22,7 @@ Notes: #include "ast/bv_decl_plugin.h" #include "ast/converters/model_converter.h" #include "tactic/tactic.h" +#include "solver/preferred_value_propagator.h" #include "qe/qsat.h" #include "opt/opt_solver.h" #include "opt/opt_pareto.h" @@ -231,7 +232,7 @@ namespace opt { void get_labels(svector & r) override; void get_unsat_core(expr_ref_vector & r) override; std::string reason_unknown() const override; - void set_reason_unknown(char const* msg) override { m_unknown = msg; } + void set_reason_unknown(char const* msg) override { m_unknown = msg; } void display_assignment(std::ostream& out) override; bool is_pareto() override { return m_pareto.get() != nullptr; } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index e60bbfae6..a409e573a 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -117,6 +117,49 @@ namespace opt { void set_phase(phase* p) override { m_context.set_phase(p); } void move_to_front(expr* e) override { m_context.move_to_front(e); } void user_propagate_initialize_value(expr* var, expr* value) override { m_context.user_propagate_initialize_value(var, value); } + void user_propagate_init(void *ctx, user_propagator::push_eh_t &push_eh, user_propagator::pop_eh_t &pop_eh, user_propagator::fresh_eh_t &fresh_eh) override { + m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + m_first = false; + } + + void user_propagate_register_fixed(user_propagator::fixed_eh_t &fixed_eh) override { + m_context.user_propagate_register_fixed(fixed_eh); + } + + void user_propagate_register_final(user_propagator::final_eh_t &final_eh) override { + m_context.user_propagate_register_final(final_eh); + } + + void user_propagate_register_eq(user_propagator::eq_eh_t &eq_eh) override { + m_context.user_propagate_register_eq(eq_eh); + } + + void user_propagate_register_diseq(user_propagator::eq_eh_t &diseq_eh) override { + m_context.user_propagate_register_diseq(diseq_eh); + } + + void user_propagate_register_expr(expr *e) override { + m_context.user_propagate_register_expr(e); + } + + void user_propagate_register_created(user_propagator::created_eh_t &r) override { + m_context.user_propagate_register_created(r); + } + + void user_propagate_register_decide(user_propagator::decide_eh_t &r) override { + m_context.user_propagate_register_decide(r); + } + + void user_propagate_register_on_binding(user_propagator::binding_eh_t &r) override { + m_context.user_propagate_register_on_binding(r); + } + + void user_propagate_clear() override { + } + + void register_on_clause(void *, user_propagator::on_clause_eh_t &r) override { + m_context.register_on_clause(nullptr, r); + } void set_logic(symbol const& logic); From c8bdbd2dc4808bce28a075791a098808fc4758a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Oct 2025 11:58:57 -0700 Subject: [PATCH 14/45] remove directory Signed-off-by: Nikolaj Bjorner --- z3test | 1 - 1 file changed, 1 deletion(-) delete mode 160000 z3test diff --git a/z3test b/z3test deleted file mode 160000 index 4186a4bf4..000000000 --- a/z3test +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 4186a4bf47b920d50671c396f904fe69e3e5c41d From 3ce8aca41108063920d586f8c4693992c7981233 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Sat, 4 Oct 2025 01:22:52 -0700 Subject: [PATCH 15/45] Bump actions/checkout from 4 to 5 (#7954) Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](https://github.com/actions/checkout/compare/v4...v5) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '5' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/codeql-analysis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml index 397145536..75ec964bd 100644 --- a/.github/workflows/codeql-analysis.yml +++ b/.github/workflows/codeql-analysis.yml @@ -20,7 +20,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Initialize CodeQL uses: github/codeql-action/init@v3 From cd1ceb6efeb935963235788529bdd806cce4bceb Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 6 Oct 2025 13:38:18 -0700 Subject: [PATCH 16/45] [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) * Initial plan * Add mutex to warning.cpp for thread safety Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/util/warning.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/util/warning.cpp b/src/util/warning.cpp index 033c93780..c7becf49f 100644 --- a/src/util/warning.cpp +++ b/src/util/warning.cpp @@ -24,6 +24,10 @@ Revision History: #include "util/buffer.h" #include "util/vector.h" +#ifndef SINGLE_THREAD +#include +#endif + #ifdef _WINDOWS #if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) ) #include @@ -67,6 +71,10 @@ static bool g_use_std_stdout = false; static std::ostream* g_error_stream = nullptr; static std::ostream* g_warning_stream = nullptr; +#ifndef SINGLE_THREAD +static std::mutex g_warning_mutex; +#endif + void send_warnings_to_stdout(bool flag) { g_use_std_stdout = flag; } @@ -129,6 +137,9 @@ void print_msg(std::ostream * out, const char* prefix, const char* msg, va_list void warning_msg(const char * msg, ...) { if (g_warning_msgs) { +#ifndef SINGLE_THREAD + std::lock_guard lock(g_warning_mutex); +#endif va_list args; va_start(args, msg); print_msg(g_warning_stream, "WARNING: ", msg, args); From 542e01555081a0966bbd668db8a3582a493c35b4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Oct 2025 13:39:27 -0700 Subject: [PATCH 17/45] Remove unused variable 'first' in mpz.cpp Removed unused variable 'first' from the function. --- src/util/mpz.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 0d4df44a2..94d95d85c 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -2332,7 +2332,6 @@ bool mpz_manager::is_perfect_square(mpz const & a, mpz & root) { set(sq_lo, 1); bool result = false; - bool first = true; // lo*lo <= *this < hi*hi // first find small interval lo*lo <= a <<= hi*hi From aa5645b54bea707f16935ae8b87b849995ee29fd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 13:22:18 -0700 Subject: [PATCH 18/45] fixing the order Signed-off-by: Lev Nachmanson --- src/ast/normal_forms/nnf.cpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 4de3d7ba7..746d48fa2 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -566,7 +566,8 @@ struct nnf::imp { expr * _then = rs[2]; expr * _else = rs[3]; - app * r = m.mk_and(m.mk_or(_not_cond, _then), m.mk_or(_cond, _else)); + expr* a = m.mk_or(_not_cond, _then); + app * r = m.mk_and(a, m.mk_or(_cond, _else)); m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -612,11 +613,13 @@ struct nnf::imp { app * r; if (is_eq(t) == fr.m_pol) { - auto a = m.mk_or(not_lhs, rhs); + expr* a = m.mk_or(not_lhs, rhs); r = m.mk_and(a, m.mk_or(lhs, not_rhs)); } - else - r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs)); + else { + expr* a = m.mk_or(lhs, rhs); + r = m.mk_and(a, m.mk_or(not_lhs, not_rhs)); + } m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -688,8 +691,8 @@ struct nnf::imp { if (proofs_enabled()) { expr_ref aux(m); aux = m.mk_label(true, names.size(), names.data(), arg); - pr = m.mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)), - m.mk_iff_oeq(m.mk_rewrite(aux, r))); + auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)); + pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r))); } } else { From 5ae858f66bdba3c5b0a0dd2ce072067d2c49b06e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 13:35:37 -0700 Subject: [PATCH 19/45] fixing the order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/arith_rewriter.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 8851bc7fd..3da768df8 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -720,10 +720,11 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } expr* c = nullptr, *t = nullptr, *e = nullptr; if (m.is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) { + auto a = m.mk_not(c); switch (kind) { - case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2; - case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2; - case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2; + case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(a, m_util.mk_le(e, arg2)); return BR_REWRITE2; + case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(a, m_util.mk_ge(e, arg2)); return BR_REWRITE2; + case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2)) : m.mk_and(a, m_util.mk_eq(e, arg2)); return BR_REWRITE2; } } if (m.is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) { From 5a9663247b7887d09246bcd6de8c21e3ad86e0c9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 13:42:38 -0700 Subject: [PATCH 20/45] fix the order of parameter evaluation Signed-off-by: Lev Nachmanson --- src/ast/rewriter/arith_rewriter.cpp | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 3da768df8..c6fe0b8ad 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -728,17 +728,28 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } } if (m.is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) { + auto a = m.mk_not(c); switch (kind) { - case LE: result = a1 <= a2 ? m.mk_or(m.mk_not(c), m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2; - case GE: result = a1 >= a2 ? m.mk_or(m.mk_not(c), m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2; - case EQ: result = a1 == a2 ? m.mk_or(m.mk_not(c), m.mk_eq(t, arg2)) : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2; + case LE: result = a1 <= a2 ? m.mk_or(a, m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2; + case GE: result = a1 >= a2 ? m.mk_or(a, m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2; + case EQ: result = a1 == a2 ? m.mk_or(a, m.mk_eq(t, arg2)) : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2; } } if (m.is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) { switch (kind) { - case LE: result = m.mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2; - case GE: result = m.mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2; - case EQ: result = m.mk_ite(c, m.mk_eq(t, arg2), m.mk_eq(e, arg2)); return BR_REWRITE2; + case LE: + { + auto a = m_util.mk_le(t, arg2); + result = m.mk_ite(c, a, m_util.mk_le(e, arg2)); return BR_REWRITE2; + } + case GE: { + auto a = m_util.mk_ge(t, arg2); + result = m.mk_ite(c, a, m_util.mk_ge(e, arg2)); return BR_REWRITE2; + } + case EQ:{ + auto a = m.mk_eq(t, arg2); + result = m.mk_ite(c, a, m.mk_eq(e, arg2)); return BR_REWRITE2; + } } } if (m_util.is_to_int(arg2) && is_numeral(arg1)) { From e9a2766e6c680361062269322658d7a95e558ce2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Oct 2025 13:53:24 -0700 Subject: [PATCH 21/45] remove AI slop Signed-off-by: Nikolaj Bjorner --- a-tst.gcno | Bin 221 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 a-tst.gcno diff --git a/a-tst.gcno b/a-tst.gcno deleted file mode 100644 index 3b9127650ef76a04ccbdb11e05074f005850c6be..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 221 zcmd1LOHS7^Hg=l5(9MGZ2qb`5KO;XkRlle-FE6!7zdXMvTffQ}h!_|_3K$p|O@YMg zq5?LH*{?NTyo|lg3gqV|X6At;890Erq_{*cxuAf73CIRXf@qMz3=EEpEI<;385o=y odB8M89$5^eo*9TidSU87e2@bmj&NmE0J1^qKmgrNh$sUC09YU#%m4rY From 63bb367a10e54316ca2f5da89d7ec5c32f12fc63 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 15:44:41 -0700 Subject: [PATCH 22/45] param order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index c5ef8d9ed..bfcb8c36e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -55,7 +55,8 @@ expr_ref sym_expr::accept(expr* e) { result = m.mk_bool_val((r1 <= r2) && (r2 <= r3)); } else { - result = m.mk_and(u.mk_le(m_t, e), u.mk_le(e, m_s)); + auto a = u.mk_le(m_t, e); + result = m.mk_and(a, u.mk_le(e, m_s)); } break; } @@ -190,7 +191,9 @@ br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) { // sa in (ra n rb) u (C(ra) n C(rb)) if (is_not) rb = re().mk_complement(rb); - expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb))); + auto a_ = re().mk_inter(ra, rb); + auto b_ = re().mk_complement(ra); + expr* r = re().mk_union(a_, re().mk_inter(b_, re().mk_complement(rb))); result = re().mk_in_re(sa, r); return BR_REWRITE_FULL; } @@ -620,10 +623,14 @@ expr_ref seq_rewriter::mk_seq_rest(expr* t) { expr_ref result(m()); expr* s, * j, * k; rational jv; - if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv >= 0) - result = str().mk_substr(s, m_autil.mk_int(jv + 1), mk_sub(k, 1)); - else - result = str().mk_substr(t, one(), mk_sub(str().mk_length(t), 1)); + if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv >= 0) { + auto a = m_autil.mk_int(jv + 1); + result = str().mk_substr(s, a, mk_sub(k, 1)); + } + else { + auto a = one(); + result = str().mk_substr(t, a, mk_sub(str().mk_length(t), 1)); + } return result; } From 77c70bf81297b681254a5fde93ce58fb1c7ece92 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 15:51:53 -0700 Subject: [PATCH 23/45] param order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index bfcb8c36e..20af49fc8 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -661,7 +661,10 @@ expr_ref seq_rewriter::mk_seq_last(expr* t) { * No: if k > |s| then substring(s,0,k) = substring(s,0,k-1) */ expr_ref seq_rewriter::mk_seq_butlast(expr* t) { - return expr_ref(str().mk_substr(t, zero(), m_autil.mk_sub(str().mk_length(t), one())), m()); + auto b = zero(); + auto c = str().mk_length(t); + auto a = str().mk_substr(t, b, m_autil.mk_sub(c, one())); + return expr_ref(a, m()); } /* From c154b9df9090c8c49e806db74c13d925b8f45e52 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 08:34:56 -0700 Subject: [PATCH 24/45] param order evaluation --- src/ast/rewriter/seq_rewriter.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 20af49fc8..95e9c954a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2725,7 +2725,10 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_REWRITE2; } else if (re().is_union(r, r1, r2)) { - result = re().mk_union(re().mk_reverse(r1), re().mk_reverse(r2)); + // ensure deterministic evaluation order of parameters + auto a = re().mk_reverse(r1); + auto b = re().mk_reverse(r2); + result = re().mk_union(a, b); return BR_REWRITE2; } else if (re().is_intersection(r, r1, r2)) { @@ -4624,11 +4627,17 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { expr *e1 = nullptr, *e2 = nullptr; if (re().is_intersection(a, e1, e2)) { - result = re().mk_union(re().mk_complement(e1), re().mk_complement(e2)); + // enforce deterministic evaluation order for nested complement arguments + auto a1 = re().mk_complement(e1); + auto b1 = re().mk_complement(e2); + result = re().mk_union(a1, b1); return BR_REWRITE2; } if (re().is_union(a, e1, e2)) { - result = re().mk_inter(re().mk_complement(e1), re().mk_complement(e2)); + // enforce deterministic evaluation order for nested complement arguments + auto a1 = re().mk_complement(e1); + auto b1 = re().mk_complement(e2); + result = re().mk_inter(a1, b1); return BR_REWRITE2; } if (re().is_empty(a)) { From 00f1e6af7ecca97b81490c6c4595da55b9a865d1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 08:40:24 -0700 Subject: [PATCH 25/45] parameter eval order --- src/ast/rewriter/seq_rewriter.cpp | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 95e9c954a..de2584450 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3412,12 +3412,22 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) { result = mk_regex_concat(mk_regex_reverse(r2), mk_regex_reverse(r1)); else if (m().is_ite(r, c, r1, r2)) result = m().mk_ite(c, mk_regex_reverse(r1), mk_regex_reverse(r2)); - else if (re().is_union(r, r1, r2)) - result = re().mk_union(mk_regex_reverse(r1), mk_regex_reverse(r2)); - else if (re().is_intersection(r, r1, r2)) - result = re().mk_inter(mk_regex_reverse(r1), mk_regex_reverse(r2)); - else if (re().is_diff(r, r1, r2)) - result = re().mk_diff(mk_regex_reverse(r1), mk_regex_reverse(r2)); + else if (re().is_union(r, r1, r2)) { + // enforce deterministic evaluation order + auto a1 = mk_regex_reverse(r1); + auto b1 = mk_regex_reverse(r2); + result = re().mk_union(a1, b1); + } + else if (re().is_intersection(r, r1, r2)) { + auto a1 = mk_regex_reverse(r1); + auto b1 = mk_regex_reverse(r2); + result = re().mk_inter(a1, b1); + } + else if (re().is_diff(r, r1, r2)) { + auto a1 = mk_regex_reverse(r1); + auto b1 = mk_regex_reverse(r2); + result = re().mk_diff(a1, b1); + } else if (re().is_star(r, r1)) result = re().mk_star(mk_regex_reverse(r1)); else if (re().is_plus(r, r1)) @@ -5093,11 +5103,16 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) { } // Partial DNF expansion: else if (re().is_intersection(r, r1, r2) && re().is_union(r1, r3, r4)) { - result = eq_empty(re().mk_union(re().mk_inter(r3, r2), re().mk_inter(r4, r2))); + // enforce deterministic order for nested intersections inside union + auto a1 = re().mk_inter(r3, r2); + auto b1 = re().mk_inter(r4, r2); + result = eq_empty(re().mk_union(a1, b1)); return BR_REWRITE3; } else if (re().is_intersection(r, r1, r2) && re().is_union(r2, r3, r4)) { - result = eq_empty(re().mk_union(re().mk_inter(r3, r1), re().mk_inter(r4, r1))); + auto a1 = re().mk_inter(r3, r1); + auto b1 = re().mk_inter(r4, r1); + result = eq_empty(re().mk_union(a1, b1)); return BR_REWRITE3; } return BR_FAILED; From 93ff8c76db660cfc3cdcd82f9d29c18c7ef40ebb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 08:53:49 -0700 Subject: [PATCH 26/45] parameter evaluation order --- src/ast/rewriter/seq_rewriter.cpp | 40 ++++++++++++++++++++++--------- 1 file changed, 29 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index de2584450..23a799ef7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1557,17 +1557,20 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result } if (str().is_empty(b)) { - result = m().mk_ite(m().mk_and(m_autil.mk_le(zero(), c), - m_autil.mk_le(c, str().mk_length(a))), - c, - minus_one()); + // enforce deterministic evaluation order for bounds checks + auto a1 = m_autil.mk_le(zero(), c); + auto b1 = m_autil.mk_le(c, str().mk_length(a)); + auto cond = m().mk_and(a1, b1); + result = m().mk_ite(cond, c, minus_one()); return BR_REWRITE2; } if (str().is_empty(a)) { expr* emp = str().mk_is_empty(b); - result = m().mk_ite(m().mk_and(m().mk_eq(c, zero()), emp), zero(), minus_one()); + auto a1 = m().mk_eq(c, zero()); + auto cond = m().mk_and(a1, emp); + result = m().mk_ite(cond, zero(), minus_one()); return BR_REWRITE2; } @@ -2732,11 +2735,15 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_REWRITE2; } else if (re().is_intersection(r, r1, r2)) { - result = re().mk_inter(re().mk_reverse(r1), re().mk_reverse(r2)); + auto a = re().mk_reverse(r1); + auto b = re().mk_reverse(r2); + result = re().mk_inter(a, b); return BR_REWRITE2; } else if (re().is_diff(r, r1, r2)) { - result = re().mk_diff(re().mk_reverse(r1), re().mk_reverse(r2)); + auto a = re().mk_reverse(r1); + auto b = re().mk_reverse(r2); + result = re().mk_diff(a, b); return BR_REWRITE2; } else if (m().is_ite(r, p, r1, r2)) { @@ -3031,7 +3038,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref // SASSERT(u().is_char(c1)); // SASSERT(u().is_char(c2)); // case: c1 <= e <= c2 - range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2))); + // deterministic evaluation for range bounds + auto a_le = u().mk_le(c1, e); + auto b_le = u().mk_le(e, c2); + auto rng_cond = m().mk_and(a_le, b_le); + range = simplify_path(e, rng_cond); psi = simplify_path(e, m().mk_and(path, range)); } else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) { @@ -4005,8 +4016,13 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] // hd = mk_seq_first(r1); - m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), - m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result); + // isolate nested conjunction for deterministic evaluation + auto a0 = u().mk_le(m_util.mk_char('0'), ele); + auto a1 = u().mk_le(ele, m_util.mk_char('9')); + auto a2 = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))); + auto a3 = m().mk_eq(hd, ele); + auto inner = m().mk_and(a2, a3); + m_br.mk_and(a0, a1, inner, result); tl = re().mk_to_re(mk_seq_rest(r1)); return re_and(result, tl); } @@ -5040,7 +5056,9 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { rep.insert(elem, solution); rep(cond); if (!is_uninterp_const(elem)) { - cond = m().mk_and(m().mk_eq(elem, solution), cond); + // ensure deterministic evaluation order when augmenting condition + auto eq_sol = m().mk_eq(elem, solution); + cond = m().mk_and(eq_sol, cond); } } else if (all_ranges) { From 6e52b9584c031c6e6d139669152729da99f2939b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 09:04:24 -0700 Subject: [PATCH 27/45] param eval --- src/ast/rewriter/seq_rewriter.cpp | 34 +++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 23a799ef7..4c325f171 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1384,9 +1384,16 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) { } expr* la = str().mk_length(a); - result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, zero()), m().mk_not(m_autil.mk_le(la, b))), - str().mk_nth_i(a, b), - str().mk_nth_u(a, b)); + { + // deterministic evaluation order for guard components + auto ge0 = m_autil.mk_ge(b, zero()); + auto le_la = m_autil.mk_le(la, b); + auto not_le = m().mk_not(le_la); + auto guard = m().mk_and(ge0, not_le); + auto t1 = str().mk_nth_i(a, b); + auto e1 = str().mk_nth_u(a, b); + result = m().mk_ite(guard, t1, e1); + } return BR_REWRITE_FULL; } @@ -2716,7 +2723,10 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { zstring zs; unsigned lo = 0, hi = 0; if (re().is_concat(r, r1, r2)) { - result = re().mk_concat(re().mk_reverse(r2), re().mk_reverse(r1)); + // deterministic evaluation order for reverse operands + auto a_rev = re().mk_reverse(r2); + auto b_rev = re().mk_reverse(r1); + result = re().mk_concat(a_rev, b_rev); return BR_REWRITE2; } else if (re().is_star(r, r1)) { @@ -2787,8 +2797,9 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_DONE; } else if (re().is_to_re(r, s) && str().is_concat(s, s1, s2)) { - result = re().mk_concat(re().mk_reverse(re().mk_to_re(s2)), - re().mk_reverse(re().mk_to_re(s1))); + auto a_rev = re().mk_reverse(re().mk_to_re(s2)); + auto b_rev = re().mk_reverse(re().mk_to_re(s1)); + result = re().mk_concat(a_rev, b_rev); return BR_REWRITE3; } else { @@ -3022,8 +3033,15 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing())); } else if (m().is_ite(r, c, r1, r2)) { - c1 = simplify_path(e, m().mk_and(c, path)); - c2 = simplify_path(e, m().mk_and(m().mk_not(c), path)); + { + auto cp = m().mk_and(c, path); + c1 = simplify_path(e, cp); + } + { + auto notc = m().mk_not(c); + auto np = m().mk_and(notc, path); + c2 = simplify_path(e, np); + } if (m().is_false(c1)) result = mk_antimirov_deriv(e, r2, c2); else if (m().is_false(c2)) From 3a2bbf4802cf40b97c7340188dfac888c6702691 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 09:13:21 -0700 Subject: [PATCH 28/45] param eval order --- src/ast/rewriter/seq_rewriter.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4c325f171..129582daa 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4359,9 +4359,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { (re().is_union(b, b1, eps) && re().is_epsilon(eps)) || (re().is_union(b, eps, b1) && re().is_epsilon(eps))) { - result = m().mk_ite(m().mk_eq(str().mk_length(a), zero()), - m().mk_true(), - re().mk_in_re(a, b1)); + // deterministic evaluation order: build sub-expressions first + auto len_a = str().mk_length(a); + auto is_empty = m().mk_eq(len_a, zero()); + auto in_b1 = re().mk_in_re(a, b1); + result = m().mk_ite(is_empty, m().mk_true(), in_b1); return BR_REWRITE_FULL; } if (str().is_empty(a)) { From 2b3068d85fc7f23d249537f2dd91e2c0f31d48e3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 09:17:12 -0700 Subject: [PATCH 29/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 129582daa..44c29561d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4393,9 +4393,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m()); expr_ref len_a(str().mk_length(a), m()); expr_ref len_tl(m_autil.mk_sub(len_a, len_hd), m()); - result = m().mk_and(m_autil.mk_ge(len_a, len_hd), - re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd), - re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)); + auto ge_len = m_autil.mk_ge(len_a, len_hd); + auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd); + auto suffix = re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl); + result = m().mk_and(ge_len, prefix, suffix); return BR_REWRITE_FULL; } if (get_re_head_tail_reversed(b, hd, tl)) { @@ -4404,10 +4405,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { expr_ref len_a(str().mk_length(a), m()); expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m()); expr* s = nullptr; - result = m().mk_and(m_autil.mk_ge(len_a, len_tl), - re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd), - (re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) : - re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl))); + auto ge_len = m_autil.mk_ge(len_a, len_tl); + auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd); + auto tail_seq = str().mk_substr(a, len_hd, len_tl); + auto tail = (re().is_to_re(tl, s) ? m().mk_eq(s, tail_seq) : re().mk_in_re(tail_seq, tl)); + result = m().mk_and(ge_len, prefix, tail); return BR_REWRITE_FULL; } From a41549eee69986b3cede4408f4f416811879bae0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:06:43 -0700 Subject: [PATCH 30/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 44c29561d..351dde879 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2988,7 +2988,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref } else { // observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first - m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_first(r1), e), c1); + { + auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))); + auto eq_first = m().mk_eq(mk_seq_first(r1), e); + m_br.mk_and(is_non_empty, eq_first, c1); + } m_br.mk_and(path, c1, c2); if (m().is_false(c2)) result = nothing(); @@ -3001,7 +3005,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref if (re().is_to_re(r2, r1)) { // here r1 is a sequence // observe that the precondition |r1|>0 of mk_seq_last is implied by c1 - m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_last(r1), e), c1); + { + auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))); + auto eq_last = m().mk_eq(mk_seq_last(r1), e); + m_br.mk_and(is_non_empty, eq_last, c1); + } m_br.mk_and(path, c1, c2); if (m().is_false(c2)) result = nothing(); From 40b980079b6bb8351549a7f2c8557148aa9e54c3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:14:02 -0700 Subject: [PATCH 31/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 351dde879..0ea11248d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4082,7 +4082,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // tl = rest of reverse(r2) i.e. butlast of r2 //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one())); hd = mk_seq_last(r2); - m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); + // factor nested constructor calls to enforce deterministic argument evaluation order + auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))); + auto a_eq = m().mk_eq(hd, ele); + m_br.mk_and(a_non_empty, a_eq, result); tl = re().mk_to_re(mk_seq_butlast(r2)); return re_and(result, re().mk_reverse(tl)); } From 8ccf4cd8f77fe9145947613c33657f2b29bdf7f6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:19:24 -0700 Subject: [PATCH 32/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0ea11248d..4380504d5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2404,7 +2404,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { } expr* b; if (str().is_itos(a, b)) { - result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one()); + auto a = m_autil.mk_ge(b, zero()); + result = m().mk_ite(a, b, minus_one()); return BR_DONE; } if (str().is_ubv2s(a, b)) { @@ -2415,7 +2416,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { expr* c = nullptr, *t = nullptr, *e = nullptr; if (m().is_ite(a, c, t, e)) { - result = m().mk_ite(c, str().mk_stoi(t), str().mk_stoi(e)); + auto a = str().mk_stoi(t); + result = m().mk_ite(c, a, str().mk_stoi(e)); return BR_REWRITE_FULL; } From 6a9520bdc263f19171ab3df242b263039b57f077 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:21:09 -0700 Subject: [PATCH 33/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4380504d5..d7d9cb1f3 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1910,7 +1910,8 @@ br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& resu } if (str().is_concat(seqA, s1, s2)) { expr_ref j(m_autil.mk_add(i, str().mk_length(s1)), m()); - result = str().mk_concat(str().mk_mapi(f, i, s1), str().mk_mapi(f, j, s2)); + auto a = str().mk_mapi(f, i, s1); + result = str().mk_concat(a, str().mk_mapi(f, j, s2)); return BR_REWRITE2; } return BR_FAILED; From 8af9a20e01e92523a593cb71776a5fc476463f82 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:26:40 -0700 Subject: [PATCH 34/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d7d9cb1f3..c2649f20f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1890,7 +1890,10 @@ br_status seq_rewriter::mk_seq_map(expr* f, expr* seqA, expr_ref& result) { return BR_REWRITE2; } if (str().is_concat(seqA, s1, s2)) { - result = str().mk_concat(str().mk_map(f, s1), str().mk_map(f, s2)); + // introduce temporaries to ensure deterministic evaluation order of recursive map calls + auto m1 = str().mk_map(f, s1); + auto m2 = str().mk_map(f, s2); + result = str().mk_concat(m1, m2); return BR_REWRITE2; } return BR_FAILED; @@ -1910,8 +1913,9 @@ br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& resu } if (str().is_concat(seqA, s1, s2)) { expr_ref j(m_autil.mk_add(i, str().mk_length(s1)), m()); - auto a = str().mk_mapi(f, i, s1); - result = str().mk_concat(a, str().mk_mapi(f, j, s2)); + auto left = str().mk_mapi(f, i, s1); + auto right = str().mk_mapi(f, j, s2); + result = str().mk_concat(left, right); return BR_REWRITE2; } return BR_FAILED; From 641741f3a874130b28cf50a9a07e8bde19a0a855 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:30:58 -0700 Subject: [PATCH 35/45] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index c2649f20f..d708af9e0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2071,8 +2071,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { SASSERT(bs.size() > 1); s1 = s1.extract(s2.length(), s1.length() - s2.length()); as[0] = str().mk_string(s1); - result = str().mk_prefix(str().mk_concat(as.size(), as.data(), sort_a), - str().mk_concat(bs.size()-1, bs.data()+1, sort_a)); + auto a = str().mk_concat(as.size(), as.data(), sort_a); + result = str().mk_prefix(a, str().mk_concat(bs.size()-1, bs.data()+1, sort_a)); TRACE(seq, tout << s1 << " " << s2 << " " << result << "\n";); return BR_REWRITE_FULL; } From e669fbe55743517196361f52c16c6b3e002bf3fb Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 14 Oct 2025 18:08:27 +0200 Subject: [PATCH 36/45] Bump github/codeql-action from 3 to 4 (#7971) Bumps [github/codeql-action](https://github.com/github/codeql-action) from 3 to 4. - [Release notes](https://github.com/github/codeql-action/releases) - [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md) - [Commits](https://github.com/github/codeql-action/compare/v3...v4) --- updated-dependencies: - dependency-name: github/codeql-action dependency-version: '4' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/codeql-analysis.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml index 75ec964bd..279bd2b99 100644 --- a/.github/workflows/codeql-analysis.yml +++ b/.github/workflows/codeql-analysis.yml @@ -23,15 +23,15 @@ jobs: uses: actions/checkout@v5 - name: Initialize CodeQL - uses: github/codeql-action/init@v3 + uses: github/codeql-action/init@v4 with: languages: ${{ matrix.language }} - name: Autobuild - uses: github/codeql-action/autobuild@v3 + uses: github/codeql-action/autobuild@v4 - name: Run CodeQL Query - uses: github/codeql-action/analyze@v3 + uses: github/codeql-action/analyze@v4 with: category: 'custom' queries: ./codeql/custom-queries \ No newline at end of file From 5163411f9b90a339167a41fb3d46a4811420a4db Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 15 Oct 2025 20:51:21 +0200 Subject: [PATCH 37/45] Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) * Initial plan * Update Z3_mk_datatype_sort API to accept array of parameters Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update language bindings for parametric datatype sort API - Python: Updated DatatypeSort() to accept optional params list - OCaml: Added mk_sort_ref_p/mk_sort_ref_ps for parametric datatypes - .NET: Added MkDatatypeSortRef() methods with optional params - Java: Added mkDatatypeSortRef() methods with optional params - All changes maintain backward compatibility Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix .NET build error - rename params to parameters The 'params' keyword is reserved in C#, causing compilation errors. Renamed parameter from 'params' to 'parameters' in MkDatatypeSortRef methods. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add unit test for parametric datatypes Added test_parametric_datatype.cpp to demonstrate polymorphic datatypes. The test creates two concrete instantiations of a generic pair concept: - pair_int_real with fields (first:Int, second:Real) - pair_real_int with fields (first:Real, second:Int) Then verifies that accessors work correctly and type checking is enforced. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement polymorphic type variables support for parametric datatypes - Modified datatype_decl_plugin to allow type variables as parameters - Updated mk_datatype_decl to extract type variables from field sorts - Type variables are collected in order of first appearance - Revised unit test to use Z3_mk_type_variable for polymorphic datatypes - Test creates pair datatype with type variables alpha and beta - Successfully instantiates with concrete types (pair Int Real) and (pair Real Int) - Verifies accessor types match and equality terms are well-typed - All tests pass Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add Z3_mk_polymorphic_datatype API and refactor datatype creation - Added new API Z3_mk_polymorphic_datatype to z3_api.h - Renamed static mk_datatype_decl to api_datatype_decl in api_datatype.cpp - Modified api_datatype_decl to accept explicit type parameters - Updated all callers to use renamed function - Added test_polymorphic_datatype_api demonstrating new API usage - Both tests pass successfully Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove type variable collection logic from constructors Removed the logic for collecting type variables from field sorts based on constructors. * Update comments on parameter handling in api_datatype.cpp Clarify usage of parameters in API documentation. * Fix OCaml build error - use list instead of array for mk_datatype_sort Changed mk_sort_ref to pass empty list [] instead of empty array [||]. Changed mk_sort_ref_p to pass params list directly instead of converting to array. Z3native.mk_datatype_sort expects a list, not an array. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add polymorphic datatype example to C++ examples Added polymorphic_datatype_example() demonstrating: - Creating type variables alpha and beta with Z3_mk_type_variable - Defining parametric Pair datatype with fields of type alpha and beta - Instantiating with concrete types (Pair Int Real) and (Pair Real Int) - Getting constructors and accessors from instantiated datatypes - Creating constants and expressions using the polymorphic types - Verifying type correctness with equality (= (first p1) (second p2)) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- examples/c++/example.cpp | 90 ++++++++++++ src/api/api_datatype.cpp | 74 ++++++++-- src/api/c++/z3++.h | 17 ++- src/api/dotnet/Context.cs | 30 ++++ src/api/java/Context.java | 48 +++++++ src/api/ml/z3.ml | 8 +- src/api/ml/z3.mli | 6 + src/api/python/z3/z3.py | 26 +++- src/api/z3_api.h | 36 ++++- src/ast/datatype_decl_plugin.cpp | 6 + src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/parametric_datatype.cpp | 229 +++++++++++++++++++++++++++++++ 13 files changed, 554 insertions(+), 18 deletions(-) create mode 100644 src/test/parametric_datatype.cpp diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 06f3ffe3e..c3902dfff 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1006,6 +1006,95 @@ void datatype_example() { } +void polymorphic_datatype_example() { + std::cout << "polymorphic datatype example\n"; + context ctx; + + // Create type variables alpha and beta for polymorphic datatype using C API + Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); + Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); + sort alpha(ctx, Z3_mk_type_variable(ctx, alpha_sym)); + sort beta(ctx, Z3_mk_type_variable(ctx, beta_sym)); + + std::cout << "Type variables: " << alpha << ", " << beta << "\n"; + + // Define parametric Pair datatype with constructor mk-pair(first: alpha, second: beta) + symbol pair_name = ctx.str_symbol("Pair"); + symbol mk_pair_name = ctx.str_symbol("mk-pair"); + symbol is_pair_name = ctx.str_symbol("is-pair"); + symbol first_name = ctx.str_symbol("first"); + symbol second_name = ctx.str_symbol("second"); + + symbol field_names[2] = {first_name, second_name}; + sort field_sorts[2] = {alpha, beta}; // Use type variables + + constructors cs(ctx); + cs.add(mk_pair_name, is_pair_name, 2, field_names, field_sorts); + sort pair = ctx.datatype(pair_name, cs); + + std::cout << "Created parametric datatype: " << pair << "\n"; + + // Instantiate Pair with concrete types: (Pair Int Real) + sort_vector params_int_real(ctx); + params_int_real.push_back(ctx.int_sort()); + params_int_real.push_back(ctx.real_sort()); + sort pair_int_real = ctx.datatype_sort(pair_name, params_int_real); + + std::cout << "Instantiated with Int and Real: " << pair_int_real << "\n"; + + // Instantiate Pair with concrete types: (Pair Real Int) + sort_vector params_real_int(ctx); + params_real_int.push_back(ctx.real_sort()); + params_real_int.push_back(ctx.int_sort()); + sort pair_real_int = ctx.datatype_sort(pair_name, params_real_int); + + std::cout << "Instantiated with Real and Int: " << pair_real_int << "\n"; + + // Get constructors and accessors for (Pair Int Real) using C API + func_decl mk_pair_ir(ctx, Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0)); + func_decl first_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0)); + func_decl second_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1)); + + std::cout << "Constructors and accessors for (Pair Int Real):\n"; + std::cout << " Constructor: " << mk_pair_ir << "\n"; + std::cout << " first accessor: " << first_ir << "\n"; + std::cout << " second accessor: " << second_ir << "\n"; + + // Get constructors and accessors for (Pair Real Int) using C API + func_decl mk_pair_ri(ctx, Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0)); + func_decl first_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0)); + func_decl second_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1)); + + std::cout << "Constructors and accessors for (Pair Real Int):\n"; + std::cout << " Constructor: " << mk_pair_ri << "\n"; + std::cout << " first accessor: " << first_ri << "\n"; + std::cout << " second accessor: " << second_ri << "\n"; + + // Create constants of these types + expr p1 = ctx.constant("p1", pair_int_real); + expr p2 = ctx.constant("p2", pair_real_int); + + std::cout << "Created constants: " << p1 << " : " << p1.get_sort() << "\n"; + std::cout << " " << p2 << " : " << p2.get_sort() << "\n"; + + // Create expressions using accessors + expr first_p1 = first_ir(p1); // first(p1) has type Int + expr second_p2 = second_ri(p2); // second(p2) has type Int + + std::cout << "first(p1) = " << first_p1 << " : " << first_p1.get_sort() << "\n"; + std::cout << "second(p2) = " << second_p2 << " : " << second_p2.get_sort() << "\n"; + + // Create equality term: (= (first p1) (second p2)) + expr eq = first_p1 == second_p2; + std::cout << "Equality term: " << eq << "\n"; + + // Verify both sides have the same type (Int) + assert(first_p1.get_sort().id() == ctx.int_sort().id()); + assert(second_p2.get_sort().id() == ctx.int_sort().id()); + + std::cout << "Successfully created and verified polymorphic datatypes!\n"; +} + void expr_vector_example() { std::cout << "expr_vector example\n"; context c; @@ -1394,6 +1483,7 @@ int main() { enum_sort_example(); std::cout << "\n"; tuple_example(); std::cout << "\n"; datatype_example(); std::cout << "\n"; + polymorphic_datatype_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n"; substitute_example(); std::cout << "\n"; diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 2509434f8..886165455 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -306,12 +306,24 @@ extern "C" { Z3_CATCH; } - static datatype_decl* mk_datatype_decl(Z3_context c, - Z3_symbol name, - unsigned num_constructors, - Z3_constructor constructors[]) { + static datatype_decl* api_datatype_decl(Z3_context c, + Z3_symbol name, + unsigned num_parameters, + Z3_sort const parameters[], + unsigned num_constructors, + Z3_constructor constructors[]) { datatype_util& dt_util = mk_c(c)->dtutil(); ast_manager& m = mk_c(c)->m(); + + sort_ref_vector params(m); + + // A correct use of the API is to always provide parameters explicitly. + // implicit parameters through polymorphic type variables does not work + // because the order of polymorphic variables in the parameters is ambiguous. + if (num_parameters > 0 && parameters) + for (unsigned i = 0; i < num_parameters; ++i) + params.push_back(to_sort(parameters[i])); + ptr_vector constrs; for (unsigned i = 0; i < num_constructors; ++i) { constructor* cn = reinterpret_cast(constructors[i]); @@ -326,7 +338,7 @@ extern "C" { } constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.data())); } - return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.data()); + return mk_datatype_decl(dt_util, to_symbol(name), params.size(), params.data(), num_constructors, constrs.data()); } Z3_sort Z3_API Z3_mk_datatype(Z3_context c, @@ -341,7 +353,7 @@ extern "C" { sort_ref_vector sorts(m); { - datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors); + datatype_decl * data = api_datatype_decl(c, name, 0, nullptr, num_constructors, constructors); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts); del_datatype_decl(data); @@ -363,6 +375,42 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c, + Z3_symbol name, + unsigned num_parameters, + Z3_sort parameters[], + unsigned num_constructors, + Z3_constructor constructors[]) { + Z3_TRY; + LOG_Z3_mk_polymorphic_datatype(c, name, num_parameters, parameters, num_constructors, constructors); + RESET_ERROR_CODE(); + ast_manager& m = mk_c(c)->m(); + datatype_util data_util(m); + + sort_ref_vector sorts(m); + { + datatype_decl * data = api_datatype_decl(c, name, num_parameters, parameters, num_constructors, constructors); + bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts); + del_datatype_decl(data); + + if (!is_ok) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); + } + } + sort * s = sorts.get(0); + + mk_c(c)->save_ast_trail(s); + ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); + + for (unsigned i = 0; i < num_constructors; ++i) { + constructor* cn = reinterpret_cast(constructors[i]); + cn->m_constructor = cnstrs[i]; + } + RETURN_Z3_mk_polymorphic_datatype(of_sort(s)); + Z3_CATCH_RETURN(nullptr); + } + typedef ptr_vector constructor_list; Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, @@ -387,14 +435,18 @@ extern "C" { Z3_CATCH; } - Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name) { + Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]) { Z3_TRY; - LOG_Z3_mk_datatype_sort(c, name); + LOG_Z3_mk_datatype_sort(c, name, num_params, params); RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); datatype_util adt_util(m); - parameter p(to_symbol(name)); - sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p); + vector ps; + ps.push_back(parameter(to_symbol(name))); + for (unsigned i = 0; i < num_params; ++i) { + ps.push_back(parameter(to_sort(params[i]))); + } + sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, ps.size(), ps.data()); mk_c(c)->save_ast_trail(s); RETURN_Z3(of_sort(s)); Z3_CATCH_RETURN(nullptr); @@ -416,7 +468,7 @@ extern "C" { ptr_vector datas; for (unsigned i = 0; i < num_sorts; ++i) { constructor_list* cl = reinterpret_cast(constructor_lists[i]); - datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast(cl->data()))); + datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, cl->size(), reinterpret_cast(cl->data()))); } sort_ref_vector _sorts(m); bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.data(), 0, nullptr, _sorts); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9fb84236d..71f3ff79b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -343,6 +343,14 @@ namespace z3 { */ sort datatype_sort(symbol const& name); + /** + \brief a reference to a recursively defined parametric datatype. + Expect that it gets defined as a \ref datatype. + \param name name of the datatype + \param params sort parameters + */ + sort datatype_sort(symbol const& name, sort_vector const& params); + /** \brief create an uninterpreted sort with the name given by the string or symbol. @@ -3625,7 +3633,14 @@ namespace z3 { inline sort context::datatype_sort(symbol const& name) { - Z3_sort s = Z3_mk_datatype_sort(*this, name); + Z3_sort s = Z3_mk_datatype_sort(*this, name, 0, nullptr); + check_error(); + return sort(*this, s); + } + + inline sort context::datatype_sort(symbol const& name, sort_vector const& params) { + array _params(params); + Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr()); check_error(); return sort(*this, s); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 9293b1a31..49f183428 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -474,6 +474,36 @@ namespace Microsoft.Z3 return new DatatypeSort(this, symbol, constructors); } + /// + /// Create a forward reference to a datatype sort. + /// This is useful for creating recursive datatypes or parametric datatypes. + /// + /// name of the datatype sort + /// optional array of sort parameters for parametric datatypes + public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null) + { + Debug.Assert(name != null); + CheckContextMatch(name); + if (parameters != null) + CheckContextMatch(parameters); + + var numParams = (parameters == null) ? 0 : (uint)parameters.Length; + var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters); + return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative)); + } + + /// + /// Create a forward reference to a datatype sort. + /// This is useful for creating recursive datatypes or parametric datatypes. + /// + /// name of the datatype sort + /// optional array of sort parameters for parametric datatypes + public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null) + { + using var symbol = MkSymbol(name); + return MkDatatypeSortRef(symbol, parameters); + } + /// /// Create mutually recursive datatypes. /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 2350b52ae..691ecd737 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -388,6 +388,54 @@ public class Context implements AutoCloseable { return new DatatypeSort<>(this, mkSymbol(name), constructors); } + /** + * Create a forward reference to a datatype sort. + * This is useful for creating recursive datatypes or parametric datatypes. + * @param name name of the datatype sort + * @param params optional array of sort parameters for parametric datatypes + **/ + public DatatypeSort mkDatatypeSortRef(Symbol name, Sort[] params) + { + checkContextMatch(name); + if (params != null) + checkContextMatch(params); + + int numParams = (params == null) ? 0 : params.length; + long[] paramsNative = (params == null) ? new long[0] : AST.arrayToNative(params); + return new DatatypeSort<>(this, Native.mkDatatypeSort(nCtx(), name.getNativeObject(), numParams, paramsNative)); + } + + /** + * Create a forward reference to a datatype sort (non-parametric). + * This is useful for creating recursive datatypes. + * @param name name of the datatype sort + **/ + public DatatypeSort mkDatatypeSortRef(Symbol name) + { + return mkDatatypeSortRef(name, null); + } + + /** + * Create a forward reference to a datatype sort. + * This is useful for creating recursive datatypes or parametric datatypes. + * @param name name of the datatype sort + * @param params optional array of sort parameters for parametric datatypes + **/ + public DatatypeSort mkDatatypeSortRef(String name, Sort[] params) + { + return mkDatatypeSortRef(mkSymbol(name), params); + } + + /** + * Create a forward reference to a datatype sort (non-parametric). + * This is useful for creating recursive datatypes. + * @param name name of the datatype sort + **/ + public DatatypeSort mkDatatypeSortRef(String name) + { + return mkDatatypeSortRef(name, null); + } + /** * Create mutually recursive datatypes. * @param names names of datatype sorts diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 4d5238957..cc7294aba 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -909,11 +909,17 @@ struct mk_sort ctx (Symbol.mk_string ctx name) constructors let mk_sort_ref (ctx: context) (name:Symbol.symbol) = - Z3native.mk_datatype_sort ctx name + Z3native.mk_datatype_sort ctx name 0 [] let mk_sort_ref_s (ctx: context) (name: string) = mk_sort_ref ctx (Symbol.mk_string ctx name) + let mk_sort_ref_p (ctx: context) (name:Symbol.symbol) (params:Sort.sort list) = + Z3native.mk_datatype_sort ctx name (List.length params) params + + let mk_sort_ref_ps (ctx: context) (name: string) (params:Sort.sort list) = + mk_sort_ref_p ctx (Symbol.mk_string ctx name) params + let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) = let n = List.length names in let f e = ConstructorList.create ctx e in diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 7afc01918..6764b0e2d 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1087,6 +1087,12 @@ sig (* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *) val mk_sort_ref_s : context -> string -> Sort.sort + (** Create a forward reference to a parametric datatype sort. *) + val mk_sort_ref_p : context -> Symbol.symbol -> Sort.sort list -> Sort.sort + + (** Create a forward reference to a parametric datatype sort. *) + val mk_sort_ref_ps : context -> string -> Sort.sort list -> Sort.sort + (** Create a new datatype sort. *) val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 051265a78..128726dae 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -5474,10 +5474,30 @@ class DatatypeRef(ExprRef): """Return the datatype sort of the datatype expression `self`.""" return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) -def DatatypeSort(name, ctx = None): - """Create a reference to a sort that was declared, or will be declared, as a recursive datatype""" +def DatatypeSort(name, params=None, ctx=None): + """Create a reference to a sort that was declared, or will be declared, as a recursive datatype. + + Args: + name: name of the datatype sort + params: optional list/tuple of sort parameters for parametric datatypes + ctx: Z3 context (optional) + + Example: + >>> # Non-parametric datatype + >>> TreeRef = DatatypeSort('Tree') + >>> # Parametric datatype with one parameter + >>> ListIntRef = DatatypeSort('List', [IntSort()]) + >>> # Parametric datatype with multiple parameters + >>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()]) + """ ctx = _get_ctx(ctx) - return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx) + if params is None or len(params) == 0: + return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), 0, (Sort * 0)()), ctx) + else: + _params = (Sort * len(params))() + for i in range(len(params)): + _params[i] = params[i].ast + return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), len(params), _params), ctx) def TupleSort(name, sorts, ctx=None): """Create a named tuple sort base on a set of underlying sorts diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9de58e057..baa2fa34c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2127,6 +2127,33 @@ extern "C" { unsigned num_constructors, Z3_constructor constructors[]); + /** + \brief Create a parametric datatype with explicit type parameters. + + This function is similar to #Z3_mk_datatype, except it takes an explicit set of type parameters. + The parameters can be type variables created with #Z3_mk_type_variable, allowing the definition + of polymorphic datatypes that can be instantiated with different concrete types. + + \param c logical context + \param name name of the datatype + \param num_parameters number of type parameters (can be 0) + \param parameters array of type parameters (type variables or concrete sorts) + \param num_constructors number of constructors + \param constructors array of constructor specifications + + \sa Z3_mk_datatype + \sa Z3_mk_type_variable + \sa Z3_mk_datatype_sort + + def_API('Z3_mk_polymorphic_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(UINT), _inout_array(4, CONSTRUCTOR))) + */ + Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c, + Z3_symbol name, + unsigned num_parameters, + Z3_sort parameters[], + unsigned num_constructors, + Z3_constructor constructors[]); + /** \brief create a forward reference to a recursive datatype being declared. The forward reference can be used in a nested occurrence: the range of an array @@ -2136,9 +2163,14 @@ extern "C" { Forward references can replace the use sort references, that are unsigned integers in the \c Z3_mk_constructor call - def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL))) + \param c logical context + \param name name of the datatype + \param num_params number of sort parameters + \param params array of sort parameters + + def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT))) */ - Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name); + Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]); /** \brief Create list of constructors. diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index f91afc9ac..5bb918c5f 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -300,6 +300,12 @@ namespace datatype { TRACE(datatype, tout << "expected sort parameter at position " << i << " got: " << s << "\n";); throw invalid_datatype(); } + // Allow type variables as parameters for polymorphic datatypes + sort* param_sort = to_sort(s.get_ast()); + if (!m_manager->is_type_var(param_sort) && param_sort->get_family_id() == null_family_id) { + // Type variables and concrete sorts are allowed, but not other uninterpreted sorts + // Actually, all sorts should be allowed including uninterpreted ones + } } sort* s = m_manager->mk_sort(name.get_symbol(), diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 206dc0530..77cf2f6fd 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -21,6 +21,7 @@ add_executable(test-z3 api_polynomial.cpp api_pb.cpp api_datalog.cpp + parametric_datatype.cpp arith_rewriter.cpp arith_simplifier_plugin.cpp ast.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index c6bb23378..005b7ab59 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -179,6 +179,7 @@ int main(int argc, char ** argv) { TST(api_polynomial); TST(api_pb); TST(api_datalog); + TST(parametric_datatype); TST(cube_clause); TST(old_interval); TST(get_implied_equalities); diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp new file mode 100644 index 000000000..2958b934c --- /dev/null +++ b/src/test/parametric_datatype.cpp @@ -0,0 +1,229 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + parametric_datatype.cpp + +Abstract: + + Test parametric datatypes with type variables. + +Author: + + Copilot 2025-10-12 + +--*/ + +#include "api/z3.h" +#include "util/util.h" +#include + +/** + * Test polymorphic type variables with algebraic datatype definitions. + * + * This test uses Z3_mk_type_variable to create polymorphic type parameters alpha and beta, + * defines a generic pair datatype, then instantiates it with concrete types using + * Z3_mk_datatype_sort with parameters. + */ +static void test_parametric_pair() { + std::cout << "test_parametric_pair\n"; + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + // Create type variables alpha and beta for polymorphic datatype + Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); + Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); + Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym); + Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym); + + // Define parametric pair datatype with constructor mk-pair(first: alpha, second: beta) + Z3_symbol pair_name = Z3_mk_string_symbol(ctx, "pair"); + Z3_symbol mk_pair_name = Z3_mk_string_symbol(ctx, "mk-pair"); + Z3_symbol is_pair_name = Z3_mk_string_symbol(ctx, "is-pair"); + Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first"); + Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second"); + + Z3_symbol field_names[2] = {first_name, second_name}; + Z3_sort field_sorts[2] = {alpha, beta}; // Use type variables + unsigned sort_refs[2] = {0, 0}; // Not recursive references + + Z3_constructor mk_pair_con = Z3_mk_constructor( + ctx, mk_pair_name, is_pair_name, 2, field_names, field_sorts, sort_refs + ); + + // Create the parametric datatype + Z3_constructor constructors[1] = {mk_pair_con}; + Z3_sort pair = Z3_mk_datatype(ctx, pair_name, 1, constructors); + + Z3_del_constructor(ctx, mk_pair_con); + + std::cout << "Created parametric pair datatype\n"; + std::cout << "pair sort: " << Z3_sort_to_string(ctx, pair) << "\n"; + + // Now instantiate the datatype with concrete types + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort real_sort = Z3_mk_real_sort(ctx); + + // Create (pair Int Real) + Z3_sort params_int_real[2] = {int_sort, real_sort}; + Z3_sort pair_int_real = Z3_mk_datatype_sort(ctx, pair_name, 2, params_int_real); + + // Create (pair Real Int) + Z3_sort params_real_int[2] = {real_sort, int_sort}; + Z3_sort pair_real_int = Z3_mk_datatype_sort(ctx, pair_name, 2, params_real_int); + + std::cout << "Instantiated pair with Int and Real\n"; + std::cout << "pair_int_real: " << Z3_sort_to_string(ctx, pair_int_real) << "\n"; + std::cout << "pair_real_int: " << Z3_sort_to_string(ctx, pair_real_int) << "\n"; + + // Get constructors and accessors from the instantiated datatypes + Z3_func_decl mk_pair_int_real = Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0); + Z3_func_decl first_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0); + Z3_func_decl second_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1); + + Z3_func_decl mk_pair_real_int = Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0); + Z3_func_decl first_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0); + Z3_func_decl second_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1); + + std::cout << "Got constructors and accessors from instantiated datatypes\n"; + + // Create constants p1 : (pair Int Real) and p2 : (pair Real Int) + Z3_symbol p1_sym = Z3_mk_string_symbol(ctx, "p1"); + Z3_symbol p2_sym = Z3_mk_string_symbol(ctx, "p2"); + Z3_ast p1 = Z3_mk_const(ctx, p1_sym, pair_int_real); + Z3_ast p2 = Z3_mk_const(ctx, p2_sym, pair_real_int); + + // Create (first p1) - should be Int + Z3_ast first_p1 = Z3_mk_app(ctx, first_int_real, 1, &p1); + + // Create (second p2) - should be Int + Z3_ast second_p2 = Z3_mk_app(ctx, second_real_int, 1, &p2); + + // Create the equality (= (first p1) (second p2)) + Z3_ast eq = Z3_mk_eq(ctx, first_p1, second_p2); + + std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n"; + + // Verify the term was created successfully + ENSURE(eq != nullptr); + + // Check that first_p1 and second_p2 have the same sort (Int) + Z3_sort first_p1_sort = Z3_get_sort(ctx, first_p1); + Z3_sort second_p2_sort = Z3_get_sort(ctx, second_p2); + + std::cout << "Sort of (first p1): " << Z3_sort_to_string(ctx, first_p1_sort) << "\n"; + std::cout << "Sort of (second p2): " << Z3_sort_to_string(ctx, second_p2_sort) << "\n"; + + // Both should be Int + ENSURE(Z3_is_eq_sort(ctx, first_p1_sort, int_sort)); + ENSURE(Z3_is_eq_sort(ctx, second_p2_sort, int_sort)); + + std::cout << "test_parametric_pair passed!\n"; + + Z3_del_context(ctx); +} + +/** + * Test Z3_mk_polymorphic_datatype API with explicit parameters. + * + * This test demonstrates the new API that explicitly accepts type parameters. + */ +static void test_polymorphic_datatype_api() { + std::cout << "test_polymorphic_datatype_api\n"; + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + // Create type variables alpha and beta for polymorphic datatype + Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); + Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); + Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym); + Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym); + + // Define parametric triple datatype with constructor mk-triple(first: alpha, second: beta, third: alpha) + Z3_symbol triple_name = Z3_mk_string_symbol(ctx, "triple"); + Z3_symbol mk_triple_name = Z3_mk_string_symbol(ctx, "mk-triple"); + Z3_symbol is_triple_name = Z3_mk_string_symbol(ctx, "is-triple"); + Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first"); + Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second"); + Z3_symbol third_name = Z3_mk_string_symbol(ctx, "third"); + + Z3_symbol field_names[3] = {first_name, second_name, third_name}; + Z3_sort field_sorts[3] = {alpha, beta, alpha}; // Use type variables + unsigned sort_refs[3] = {0, 0, 0}; // Not recursive references + + Z3_constructor mk_triple_con = Z3_mk_constructor( + ctx, mk_triple_name, is_triple_name, 3, field_names, field_sorts, sort_refs + ); + + // Create the parametric datatype using Z3_mk_polymorphic_datatype + Z3_constructor constructors[1] = {mk_triple_con}; + Z3_sort type_params[2] = {alpha, beta}; + Z3_sort triple = Z3_mk_polymorphic_datatype(ctx, triple_name, 2, type_params, 1, constructors); + + Z3_del_constructor(ctx, mk_triple_con); + + std::cout << "Created parametric triple datatype using Z3_mk_polymorphic_datatype\n"; + std::cout << "triple sort: " << Z3_sort_to_string(ctx, triple) << "\n"; + + // Now instantiate the datatype with concrete types + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort bool_sort = Z3_mk_bool_sort(ctx); + + // Create (triple Int Bool) + Z3_sort params_int_bool[2] = {int_sort, bool_sort}; + Z3_sort triple_int_bool = Z3_mk_datatype_sort(ctx, triple_name, 2, params_int_bool); + + std::cout << "Instantiated triple with Int and Bool\n"; + std::cout << "triple_int_bool: " << Z3_sort_to_string(ctx, triple_int_bool) << "\n"; + + // Get constructors and accessors from the instantiated datatype + Z3_func_decl mk_triple_int_bool = Z3_get_datatype_sort_constructor(ctx, triple_int_bool, 0); + Z3_func_decl first_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 0); + Z3_func_decl second_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 1); + Z3_func_decl third_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 2); + + std::cout << "Got constructors and accessors from instantiated datatype\n"; + + // Create a constant t : (triple Int Bool) + Z3_symbol t_sym = Z3_mk_string_symbol(ctx, "t"); + Z3_ast t = Z3_mk_const(ctx, t_sym, triple_int_bool); + + // Create (first t) - should be Int + Z3_ast first_t = Z3_mk_app(ctx, first_int_bool, 1, &t); + + // Create (third t) - should also be Int + Z3_ast third_t = Z3_mk_app(ctx, third_int_bool, 1, &t); + + // Create the equality (= (first t) (third t)) + Z3_ast eq = Z3_mk_eq(ctx, first_t, third_t); + + std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n"; + + // Verify the term was created successfully + ENSURE(eq != nullptr); + + // Check that first_t and third_t have the same sort (Int) + Z3_sort first_t_sort = Z3_get_sort(ctx, first_t); + Z3_sort third_t_sort = Z3_get_sort(ctx, third_t); + + std::cout << "Sort of (first t): " << Z3_sort_to_string(ctx, first_t_sort) << "\n"; + std::cout << "Sort of (third t): " << Z3_sort_to_string(ctx, third_t_sort) << "\n"; + + // Both should be Int + ENSURE(Z3_is_eq_sort(ctx, first_t_sort, int_sort)); + ENSURE(Z3_is_eq_sort(ctx, third_t_sort, int_sort)); + + std::cout << "test_polymorphic_datatype_api passed!\n"; + + Z3_del_context(ctx); +} + +void tst_parametric_datatype() { + test_parametric_pair(); + test_polymorphic_datatype_api(); +} From 3b565bb2846f69bf1b3ae5eff297b0771d003892 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 21:39:39 +0200 Subject: [PATCH 38/45] trim parametric datatype test Signed-off-by: Nikolaj Bjorner --- src/test/parametric_datatype.cpp | 109 +------------------------------ 1 file changed, 1 insertion(+), 108 deletions(-) diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp index 2958b934c..2a31803aa 100644 --- a/src/test/parametric_datatype.cpp +++ b/src/test/parametric_datatype.cpp @@ -19,117 +19,11 @@ Author: #include "util/util.h" #include -/** - * Test polymorphic type variables with algebraic datatype definitions. - * - * This test uses Z3_mk_type_variable to create polymorphic type parameters alpha and beta, - * defines a generic pair datatype, then instantiates it with concrete types using - * Z3_mk_datatype_sort with parameters. - */ -static void test_parametric_pair() { - std::cout << "test_parametric_pair\n"; - - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_del_config(cfg); - - // Create type variables alpha and beta for polymorphic datatype - Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); - Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); - Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym); - Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym); - - // Define parametric pair datatype with constructor mk-pair(first: alpha, second: beta) - Z3_symbol pair_name = Z3_mk_string_symbol(ctx, "pair"); - Z3_symbol mk_pair_name = Z3_mk_string_symbol(ctx, "mk-pair"); - Z3_symbol is_pair_name = Z3_mk_string_symbol(ctx, "is-pair"); - Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first"); - Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second"); - - Z3_symbol field_names[2] = {first_name, second_name}; - Z3_sort field_sorts[2] = {alpha, beta}; // Use type variables - unsigned sort_refs[2] = {0, 0}; // Not recursive references - - Z3_constructor mk_pair_con = Z3_mk_constructor( - ctx, mk_pair_name, is_pair_name, 2, field_names, field_sorts, sort_refs - ); - - // Create the parametric datatype - Z3_constructor constructors[1] = {mk_pair_con}; - Z3_sort pair = Z3_mk_datatype(ctx, pair_name, 1, constructors); - - Z3_del_constructor(ctx, mk_pair_con); - - std::cout << "Created parametric pair datatype\n"; - std::cout << "pair sort: " << Z3_sort_to_string(ctx, pair) << "\n"; - - // Now instantiate the datatype with concrete types - Z3_sort int_sort = Z3_mk_int_sort(ctx); - Z3_sort real_sort = Z3_mk_real_sort(ctx); - - // Create (pair Int Real) - Z3_sort params_int_real[2] = {int_sort, real_sort}; - Z3_sort pair_int_real = Z3_mk_datatype_sort(ctx, pair_name, 2, params_int_real); - - // Create (pair Real Int) - Z3_sort params_real_int[2] = {real_sort, int_sort}; - Z3_sort pair_real_int = Z3_mk_datatype_sort(ctx, pair_name, 2, params_real_int); - - std::cout << "Instantiated pair with Int and Real\n"; - std::cout << "pair_int_real: " << Z3_sort_to_string(ctx, pair_int_real) << "\n"; - std::cout << "pair_real_int: " << Z3_sort_to_string(ctx, pair_real_int) << "\n"; - - // Get constructors and accessors from the instantiated datatypes - Z3_func_decl mk_pair_int_real = Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0); - Z3_func_decl first_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0); - Z3_func_decl second_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1); - - Z3_func_decl mk_pair_real_int = Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0); - Z3_func_decl first_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0); - Z3_func_decl second_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1); - - std::cout << "Got constructors and accessors from instantiated datatypes\n"; - - // Create constants p1 : (pair Int Real) and p2 : (pair Real Int) - Z3_symbol p1_sym = Z3_mk_string_symbol(ctx, "p1"); - Z3_symbol p2_sym = Z3_mk_string_symbol(ctx, "p2"); - Z3_ast p1 = Z3_mk_const(ctx, p1_sym, pair_int_real); - Z3_ast p2 = Z3_mk_const(ctx, p2_sym, pair_real_int); - - // Create (first p1) - should be Int - Z3_ast first_p1 = Z3_mk_app(ctx, first_int_real, 1, &p1); - - // Create (second p2) - should be Int - Z3_ast second_p2 = Z3_mk_app(ctx, second_real_int, 1, &p2); - - // Create the equality (= (first p1) (second p2)) - Z3_ast eq = Z3_mk_eq(ctx, first_p1, second_p2); - - std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n"; - - // Verify the term was created successfully - ENSURE(eq != nullptr); - - // Check that first_p1 and second_p2 have the same sort (Int) - Z3_sort first_p1_sort = Z3_get_sort(ctx, first_p1); - Z3_sort second_p2_sort = Z3_get_sort(ctx, second_p2); - - std::cout << "Sort of (first p1): " << Z3_sort_to_string(ctx, first_p1_sort) << "\n"; - std::cout << "Sort of (second p2): " << Z3_sort_to_string(ctx, second_p2_sort) << "\n"; - - // Both should be Int - ENSURE(Z3_is_eq_sort(ctx, first_p1_sort, int_sort)); - ENSURE(Z3_is_eq_sort(ctx, second_p2_sort, int_sort)); - - std::cout << "test_parametric_pair passed!\n"; - - Z3_del_context(ctx); -} /** * Test Z3_mk_polymorphic_datatype API with explicit parameters. * - * This test demonstrates the new API that explicitly accepts type parameters. + * This test demonstrates the API that explicitly accepts type parameters. */ static void test_polymorphic_datatype_api() { std::cout << "test_polymorphic_datatype_api\n"; @@ -224,6 +118,5 @@ static void test_polymorphic_datatype_api() { } void tst_parametric_datatype() { - test_parametric_pair(); test_polymorphic_datatype_api(); } From 1921260c424036b40f4fad1eb9a3f171590cdfd3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 14 Oct 2025 17:43:48 -0700 Subject: [PATCH 39/45] restore single cell Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 83c5f31b6..3d124864b 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1226,6 +1226,7 @@ namespace nlsat { * https://arxiv.org/abs/2003.00409 */ void project_cdcac(polynomial_ref_vector & ps, var max_x) { + bool first = true; if (ps.empty()) return; @@ -1256,9 +1257,17 @@ namespace nlsat { } TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; display(tout, ps); tout << "\n";); - add_lcs(ps, x); - psc_discriminant(ps, x); - psc_resultant(ps, x); + if (first) { + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant(ps, x); + first = false; + } + else { + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant_sample(ps, x, samples); + } if (m_todo.empty()) break; From a1792861831973e6cfed98b955f59742b1065be3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 15 Oct 2025 16:41:32 -0700 Subject: [PATCH 40/45] restore the method behavior Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 3d124864b..ff1ae6a07 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1245,8 +1245,6 @@ namespace nlsat { // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore polynomial_ref_vector samples(m_pm); - - if (x < max_x) cac_add_cell_lits(ps, x, samples); @@ -1257,7 +1255,8 @@ namespace nlsat { } TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; display(tout, ps); tout << "\n";); - if (first) { + if (first) { // The first run is special because x is not constrained by the sample, we cannot surround it by the root functions. + // we make the polynomials in ps delinable add_lcs(ps, x); psc_discriminant(ps, x); psc_resultant(ps, x); From 05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 16 Oct 2025 13:16:54 +0200 Subject: [PATCH 41/45] Add finite_set_value_factory for creating finite set values in model generation (#7981) * Initial plan * Add finite_set_value_factory implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove unused dl_decl_plugin variable and include Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update copyright and add TODOs in finite_set_value_factory Updated copyright information and added TODO comments for handling in finite_set_value_factory methods. * Update copyright information in finite_set_value_factory.h Updated copyright year from 2006 to 2025. * Implement finite_set_value_factory using array_util to create singleton sets Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Simplify empty set creation in finite_set_value_factory Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic. * Change family ID for finite_set_value_factory * Fix build error by restoring array_decl_plugin include and implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update finite_set_value_factory.h * Add SASSERT for finite set check in factory Added assertion to check if the sort is a finite set. * Rename member variable from m_util to u * Refactor finite_set_value_factory for value handling * Use register_value instead of direct set insertion Replaced direct insertion into set with register_value calls. * Update finite_set_value_factory.cpp --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/model/CMakeLists.txt | 1 + src/model/finite_set_value_factory.cpp | 58 ++++++++++++++++++++++++++ src/model/finite_set_value_factory.h | 30 +++++++++++++ src/model/model.cpp | 2 + 4 files changed, 91 insertions(+) create mode 100644 src/model/finite_set_value_factory.cpp create mode 100644 src/model/finite_set_value_factory.h diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt index 9ba93b8e1..436a3c69f 100644 --- a/src/model/CMakeLists.txt +++ b/src/model/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(model SOURCES array_factory.cpp datatype_factory.cpp + finite_set_value_factory.cpp func_interp.cpp model2expr.cpp model_core.cpp diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp new file mode 100644 index 000000000..df9ef46bc --- /dev/null +++ b/src/model/finite_set_value_factory.cpp @@ -0,0 +1,58 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_set_value_factory.cpp + +Abstract: + + Factory for creating finite set values + +--*/ +#include "model/finite_set_value_factory.h" +#include "model/model_core.h" + +finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md): + struct_factory(m, fid, md), + u(m) { +} + +expr * finite_set_value_factory::get_some_value(sort * s) { + // Check if we already have a value for this sort + value_set * set = nullptr; + SASSERT(u.is_finite_set(s)); + #if 0 + if (m_sort2value_set.find(s, set) && !set->empty()) + return *(set->begin()); + #endif + return u.mk_empty(s); +} + +expr * finite_set_value_factory::get_fresh_value(sort * s) { + sort* elem_sort = nullptr; + VERIFY(u.is_finite_set(s, elem_sort)); + // Get a fresh value for a finite set sort + + return nullptr; + #if 0 + value_set * set = get_value_set(s); + + // If no values have been generated yet, use get_some_value + if (set->empty()) { + auto r = u.mk_empty(s); + register_value(r); + return r; + } + auto e = md.get_fresh_value(elem_sort); + if (e) { + auto r = u.mk_singleton(e); + register_value(r); + return r; + } + + // For finite domains, we may not be able to generate fresh values + // if all values have been exhausted + return nullptr; + #endif +} diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_value_factory.h new file mode 100644 index 000000000..8dbbc7aae --- /dev/null +++ b/src/model/finite_set_value_factory.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_set_value_factory.h + +Abstract: + + Factory for creating finite set values + +--*/ +#pragma once + +#include "model/struct_factory.h" +#include "ast/finite_set_decl_plugin.h" + +/** + \brief Factory for finite set values. +*/ +class finite_set_value_factory : public struct_factory { + finite_set_util u; +public: + finite_set_value_factory(ast_manager & m, family_id fid, model_core & md); + + expr * get_some_value(sort * s) override; + + expr * get_fresh_value(sort * s) override; +}; + diff --git a/src/model/model.cpp b/src/model/model.cpp index fa4e50e54..02b495e72 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -40,6 +40,7 @@ Revision History: #include "model/numeral_factory.h" #include "model/fpa_factory.h" #include "model/char_factory.h" +#include "model/finite_set_value_factory.h" model::model(ast_manager & m): @@ -111,6 +112,7 @@ value_factory* model::get_factory(sort* s) { m_factories.register_plugin(alloc(arith_factory, m)); m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this)); m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id())); + m_factories.register_plugin(alloc(finite_set_value_factory, m, m.mk_family_id("finite_set"), *this)); //m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id()); } family_id fid = s->get_family_id(); From 62ee7ccf65d51c304553def478731aa17b848169 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Oct 2025 13:18:35 +0200 Subject: [PATCH 42/45] =?UTF-8?q?Revert=20"Add=20finite=5Fset=5Fvalue=5Ffa?= =?UTF-8?q?ctory=20for=20creating=20finite=20set=20values=20in=20model=20?= =?UTF-8?q?=E2=80=A6"=20(#7985)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This reverts commit 05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80. --- src/model/CMakeLists.txt | 1 - src/model/finite_set_value_factory.cpp | 58 -------------------------- src/model/finite_set_value_factory.h | 30 ------------- src/model/model.cpp | 2 - 4 files changed, 91 deletions(-) delete mode 100644 src/model/finite_set_value_factory.cpp delete mode 100644 src/model/finite_set_value_factory.h diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt index 436a3c69f..9ba93b8e1 100644 --- a/src/model/CMakeLists.txt +++ b/src/model/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(model SOURCES array_factory.cpp datatype_factory.cpp - finite_set_value_factory.cpp func_interp.cpp model2expr.cpp model_core.cpp diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp deleted file mode 100644 index df9ef46bc..000000000 --- a/src/model/finite_set_value_factory.cpp +++ /dev/null @@ -1,58 +0,0 @@ -/*++ -Copyright (c) 2025 Microsoft Corporation - -Module Name: - - finite_set_value_factory.cpp - -Abstract: - - Factory for creating finite set values - ---*/ -#include "model/finite_set_value_factory.h" -#include "model/model_core.h" - -finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md): - struct_factory(m, fid, md), - u(m) { -} - -expr * finite_set_value_factory::get_some_value(sort * s) { - // Check if we already have a value for this sort - value_set * set = nullptr; - SASSERT(u.is_finite_set(s)); - #if 0 - if (m_sort2value_set.find(s, set) && !set->empty()) - return *(set->begin()); - #endif - return u.mk_empty(s); -} - -expr * finite_set_value_factory::get_fresh_value(sort * s) { - sort* elem_sort = nullptr; - VERIFY(u.is_finite_set(s, elem_sort)); - // Get a fresh value for a finite set sort - - return nullptr; - #if 0 - value_set * set = get_value_set(s); - - // If no values have been generated yet, use get_some_value - if (set->empty()) { - auto r = u.mk_empty(s); - register_value(r); - return r; - } - auto e = md.get_fresh_value(elem_sort); - if (e) { - auto r = u.mk_singleton(e); - register_value(r); - return r; - } - - // For finite domains, we may not be able to generate fresh values - // if all values have been exhausted - return nullptr; - #endif -} diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_value_factory.h deleted file mode 100644 index 8dbbc7aae..000000000 --- a/src/model/finite_set_value_factory.h +++ /dev/null @@ -1,30 +0,0 @@ -/*++ -Copyright (c) 2025 Microsoft Corporation - -Module Name: - - finite_set_value_factory.h - -Abstract: - - Factory for creating finite set values - ---*/ -#pragma once - -#include "model/struct_factory.h" -#include "ast/finite_set_decl_plugin.h" - -/** - \brief Factory for finite set values. -*/ -class finite_set_value_factory : public struct_factory { - finite_set_util u; -public: - finite_set_value_factory(ast_manager & m, family_id fid, model_core & md); - - expr * get_some_value(sort * s) override; - - expr * get_fresh_value(sort * s) override; -}; - diff --git a/src/model/model.cpp b/src/model/model.cpp index 02b495e72..fa4e50e54 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -40,7 +40,6 @@ Revision History: #include "model/numeral_factory.h" #include "model/fpa_factory.h" #include "model/char_factory.h" -#include "model/finite_set_value_factory.h" model::model(ast_manager & m): @@ -112,7 +111,6 @@ value_factory* model::get_factory(sort* s) { m_factories.register_plugin(alloc(arith_factory, m)); m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this)); m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id())); - m_factories.register_plugin(alloc(finite_set_value_factory, m, m.mk_family_id("finite_set"), *this)); //m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id()); } family_id fid = s->get_family_id(); From fcc7e0216734bdac1a1f7f371c5d72343d95d08d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Oct 2025 13:32:49 +0200 Subject: [PATCH 43/45] Update arith_rewriter.cpp fix memory leak introduced by update to ensure determinism --- src/ast/rewriter/arith_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index c6fe0b8ad..d5ad70a1f 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -720,7 +720,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } expr* c = nullptr, *t = nullptr, *e = nullptr; if (m.is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) { - auto a = m.mk_not(c); + expr_ref a(m.mk_not(c), m); switch (kind) { case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(a, m_util.mk_le(e, arg2)); return BR_REWRITE2; case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(a, m_util.mk_ge(e, arg2)); return BR_REWRITE2; @@ -728,7 +728,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } } if (m.is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) { - auto a = m.mk_not(c); + expr_ref a(m.mk_not(c), m); switch (kind) { case LE: result = a1 <= a2 ? m.mk_or(a, m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2; case GE: result = a1 >= a2 ? m.mk_or(a, m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2; From d65c0fbcd650903b7a13cf7dd8a7fd92b8998410 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Oct 2025 20:14:20 +0200 Subject: [PATCH 44/45] add explicit constructors for nightly mac build failure Signed-off-by: Nikolaj Bjorner --- src/util/obj_hashtable.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 36715facf..c59f87696 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -58,6 +58,9 @@ public: struct key_data { Key * m_key = nullptr; Value m_value; + key_data() {} + key_data(Key *key) : m_key(key) {} + key_data(Key *k, Value const &v) : m_key(k), m_value(v) {} Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } From aaaa32b4a0644e6febf6336d1ae4a187ae28a911 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Oct 2025 20:55:45 +0200 Subject: [PATCH 45/45] build fixes Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_tracker.h | 29 +++++++++++++++++++++++++++++ src/util/obj_hashtable.h | 4 ++++ 2 files changed, 33 insertions(+) diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index 7c9b02a46..37ef91480 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/src/ast/sls/sls_bv_tracker.h @@ -42,8 +42,37 @@ class sls_tracker { struct value_score { value_score() : value(unsynch_mpz_manager::mk_z(0)) {}; value_score(value_score&&) noexcept = default; + value_score(const value_score &other) { + m = other.m; + if (other.m && !unsynch_mpz_manager::is_zero(other.value)) { + m->set(value, other.value); + } + score = other.score; + score_prune = other.score_prune; + has_pos_occ = other.has_pos_occ; + has_neg_occ = other.has_neg_occ; + distance = other.distance; + touched = other.touched; + } ~value_score() { if (m) m->del(value); } value_score& operator=(value_score&&) = default; + value_score &operator=(const value_score &other) { + if (this != &other) { + if (m) + m->del(value); + m = other.m; + if (other.m && !unsynch_mpz_manager::is_zero(other.value)) { + m->set(value, other.value); + } + score = other.score; + score_prune = other.score_prune; + has_pos_occ = other.has_pos_occ; + has_neg_occ = other.has_neg_occ; + distance = other.distance; + touched = other.touched; + } + return *this; + } unsynch_mpz_manager * m = nullptr; mpz value; double score = 0.0; diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index c59f87696..cf7cdff05 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -61,6 +61,10 @@ public: key_data() {} key_data(Key *key) : m_key(key) {} key_data(Key *k, Value const &v) : m_key(k), m_value(v) {} + key_data(key_data &&kd) noexcept = default; + key_data(key_data const &kd) noexcept = default; + key_data &operator=(key_data const &kd) = default; + key_data &operator=(key_data &&kd) = default; Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); }