Skip to content

Commit

Permalink
Add initial value setting API for solver and optimize contexts and up…
Browse files Browse the repository at this point in the history
…date related function signatures
  • Loading branch information
NikolajBjorner committed Sep 18, 2024
1 parent 48712b4 commit 0f89650
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 3 deletions.
5 changes: 4 additions & 1 deletion RELEASE_NOTES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
==============
Expand Down
2 changes: 1 addition & 1 deletion src/api/z3_api.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);


/**
Expand Down
2 changes: 1 addition & 1 deletion src/api/z3_optimization.h
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 0f89650

Please sign in to comment.