Difference in results between eager and lazy strategies for Test125

[mdmitry1]

Reproduction:

pip install smlptech
cd $(git rev-parse --show-toplevel)/regr_smlp/code
for s in lazy eager; do smlp -data "../data/smlp_toy_basic.csv" -out_dir ./ -pref Test125 -mode optsyn -pareto t -opt_strategy $s -model system -resp y1,y2 -feat p1,p2 -save_model f -use_model f -mrmr_pred 0 -model_per_response t -spec ../specs/smlp_toy_system_stable_constant_synth_feasible.spec -epsilon 0.00000001 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f &> /dev/null && echo $s && jq .y1 Test125_smlp_toy_basic_optimization_results.json; done

lazy
{
  "value_in_config": 0.0,
  "value_in_system": 0
}
eager
{
  "value_in_config": 0.125,
  "value_in_system": 0.125
}

There is no difference for y2:

for s in lazy eager; do smlp -data "../data/smlp_toy_basic.csv" -out_dir ./ -pref Test125 -mode optsyn -pareto t -opt_strategy $s -model system -resp y1,y2 -feat p1,p2 -save_model f -use_model f -mrmr_pred 0 -model_per_response t -spec ../specs/smlp_toy_system_stable_constant_synth_feasible.spec -epsilon 0.00000001 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f &> /dev/null && echo $s && jq .y2 Test125_smlp_toy_basic_optimization_results.json; done

lazy
{
  "value_in_config": 0.0,
  "value_in_system": 0
}
eager
{
  "value_in_config": 0.0,
  "value_in_system": 0
}

Difference starts from initial condition:

for s in lazy eager; do echo $s && grep ^single_objective $s/*trace*; done

lazy
single_objective_u0_l0_u_l, objv1_scaled_objv2_scaled : 1 : 0 : inf : -inf
single_objective_u0_l0_u_l, objv2_scaled : 1 : -0.022943009866943358 : inf : -0.022943009866943358
eager
single_objective_u0_l0, 1 : 0
single_objective_u0_l0, 1 : -0.022943009866943358

[konstantin-korovin]

On MacOS with Z3 4.16.0, eager and lazy results coincide. The issue is probably connected to Z3 version 4.8.12, (or difference in MacOS setup).

for s in lazy eager; do smlp -data "../data/smlp_toy_basic.csv" -out_dir ./ -pref Test125 -mode optsyn -pareto t -opt_strategy $s -model system -resp y1,y2 -feat p1,p2 -save_model f -use_model f -mrmr_pred 0 -model_per_response t -spec ../specs/smlp_toy_system_stable_constant_synth_feasible.spec -epsilon 0.00000001 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f &> /dev/null && echo $s && jq .y1 Test125_smlp_toy_basic_optimization_results.json; done
lazy
{
  "value_in_config": 0.0,
  "value_in_system": 0
}
eager
{
  "value_in_config": 0.0,
  "value_in_system": 0
}

[mdmitry1]

CONFIRMED on Ubuntu 24.04

• Used version build from commit f29f963 .
• Script for checking Z3 version

#!/usr/bin/env python3.11
from ctypes import cdll, c_char_p
from smlp import core
libz3=cdll.LoadLibrary(core.libsmlp.__file__)
z3_version=libz3.Z3_get_full_version
z3_version.restype=c_char_p
print(z3_version().decode())

cd $(git rev-parse --show-toplevel)/scripts/github
./download_artifact.sh smlptech-1.2.3rc16.dev3+gf29f96344-cp311-cp311-manylinux_2_26_x86_64.manylinux_2_28_x86_64.whl 25987636509
pip install smlptech-1.2.3rc16.dev3+gf29f96344-cp311-cp311-manylinux_2_26_x86_64.manylinux_2_28_x86_64.whl 
z3_version.py 

Z3 4.16.0.0

cd $(git rev-parse --show-toplevel)/regr_smlp/code
for s in lazy eager; do smlp -data "../data/smlp_toy_basic.csv" -out_dir ./ -pref Test125 -mode optsyn -pareto t -opt_strategy $s -model system -resp y1,y2 -feat p1,p2 -save_model f -use_model f -mrmr_pred 0 -model_per_response t -spec ../specs/smlp_toy_system_stable_constant_synth_feasible.spec -epsilon 0.00000001 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f &> /dev/null && echo $s && jq .y1 Test125_smlp_toy_basic_optimization_results.json; done

lazy
{
  "value_in_config": 0.0,
  "value_in_system": 0
}
eager
{
  "value_in_config": 0.0,
  "value_in_system": 0
}