mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

Add initial value setting API for solver and optimize contexts and update related function signatures

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-18 16:18:47 +03:00
parent 48712b4f60
commit 0f896503a9
3 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
RELEASE_NOTES.md
View file

@ -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
==============

2
src/api/z3_api.h
View file

@ -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);
/**

2
src/api/z3_optimization.h
View file

@ -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.