From 0f896503a9ffe875936ec4f80094ea0e587e833a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Sep 2024 16:18:47 +0300 Subject: [PATCH] Add initial value setting API for solver and optimize contexts and update related function signatures --- RELEASE_NOTES.md | 5 ++++- src/api/z3_api.h | 2 +- src/api/z3_optimization.h | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index b69772dcd..cc961a760 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -15,7 +15,10 @@ Version 4.13.1 - single-sample cell projection in nlsat was designed by Haokun Li and Bican Xia. - using simple-checker together with and variable ordering supported by qfnra_tactic was developed by Mengyu Zhao (Linxi) and Shaowei Cai. - The projection is described in paper by Haokun Li and Bican Xia, [Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection](https://arxiv.org/abs/2003.00409). The code ported from https://github.com/hybridSMT/hybridSMT.git + The projection is described in paper by Haokun Li and Bican Xia, [Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection](https://arxiv.org/abs/2003.00409). The code ported from https://github.com/hybridSMT/hybridSMT.git + +- Add API for providing hints for the solver/optimize contexts for which initial values to attempt to use for variables. + The new API function are Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively. Supply these functions with a Boolean or numeric variable, and a value. The solver will then attempt to use these values in the initial phase of search. The feature is aimed at resolving nearly similar problems, or problems with a predicted model and the intent is that restarting the solver based on a near solution can avoid prune the space of constraints that are initially infeasible. Version 4.13.0 ============== diff --git a/src/api/z3_api.h b/src/api/z3_api.h index fdc25ef46..6c3efe7fc 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7250,7 +7250,7 @@ extern "C" { def_API('Z3_solver_set_initial_value', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(AST))) */ - void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast var, Z3_ast value); + void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val); /** diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index ad55cab1d..4e585efb2 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -149,7 +149,7 @@ extern "C" { def_API('Z3_optimize_set_initial_value', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(AST))) */ - void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast var, Z3_ast value); + void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val); /** \brief Check consistency and produce optimal values.