mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

#7667 - add API documentation

Browse source 
The scenario works as expected when disabling model compression:

```
from z3 import *
pre_processor = Tactic("bit-blast")
solver = Solver()

set_param("model.compact", False)

x = BitVec('x', 8)
pre_processed = pre_processor(x == 5)
print(pre_processed[0])
solver.add(pre_processed[0]) # add the sole assertion

if solver.check() == sat:
    print(solver.model())
    model = pre_processed[0].convert_model(solver.model())
    print(model)
    print(model[x].as_long())
```
This commit is contained in:
Nikolaj Bjorner 2025-05-30 11:05:51 +01:00
parent 2714dc2623
commit b4c2b455bd
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/z3_api.h
View file

@ -6284,6 +6284,11 @@ extern "C" {
The model may be null, in which case the returned model is valid if the goal was
established satisfiable.
When using this feature it is advisable to set the parameter \c model.compact to \c false.
It is by default true, which erases variables created by the solver from models.
Without access to model values for intermediary variables, values of other variables
may end up having the wrong values.
def_API('Z3_goal_convert_model', MODEL, (_in(CONTEXT), _in(GOAL), _in(MODEL)))
*/
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);