regression tests: use relative -solver_path to mathsat

regr_smlp/code/smlp_regr.csv

@@ -170,8 +170,8 @@ d,data,new_data,switches,description
 169,smlp_toy_num_resp_mult,,"-mode optimize -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model et_sklearn -et_sklearn_max_depth 2 -rf_sklearn_n_estimators 3 -et_sklearn_bootstrap f -tree_encoding flat -model_per_response t -compress_rules t -save_model f -use_model f -mrmr_pred 2 -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -solver_path mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic test for et_sklearn with flat tree_encoding and model_per_response t in model exploration mode optimize
 170,smlp_toy_num_resp_mult,,"-mode optimize -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model et_sklearn -et_sklearn_max_depth 2 -rf_sklearn_n_estimators 3 -et_sklearn_bootstrap f -tree_encoding flat -model_per_response f -compress_rules t -save_model f -use_model f -mrmr_pred 2 -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -solver_path mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic test for et_sklearn with flat tree_encoding and model_per_response f in model exploration mode optimize
 171,smlp_toy_num_resp_mult,,"-mode optimize -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model et_caret -tree_encoding flat -model_per_response t -compress_rules t -save_model f -use_model f -mrmr_pred 2 -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic test for et_caret with flat tree_encoding in model exploration mode optimize
-172,smlp_toy_num_resp_mult,,"-mode verify -resp y2 -feat x,p1,p2 -model nn_keras -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -nn_keras_epochs 20 -nn_keras_seq_api f -nnet_encoding layered -nn_keras_tuner hyperband -nn_keras_layers_grid ""2,2;3,3,3"" -save_model_config f -spec smlp_toy_num_resp_mult_y2_verify.spec -asrt_names asrt1 -asrt_exprs ""2*y2>1"" -sw_coef 4 -sw_exp 5 -sw_int 0.5 -solver_path "/nfs/iil/proj/dt/eva/smlp/external/mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic test for nn_keras flat encoding for functional api, i, one response variable, adapts test 154
-173,smlp_toy_num_resp_mult,,"-mode verify -resp y2 -feat x,p1,p2 -model nn_keras -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -nn_keras_epochs 20 -nn_keras_seq_api t -nnet_encoding layered -nn_keras_tuner hyperband -nn_keras_layers_grid ""2,2;3,3,3"" -save_model_config f -spec smlp_toy_num_resp_mult_y2_verify.spec -asrt_names asrt1 -asrt_exprs ""2*y2>1"" -sw_coef 4 -sw_exp 5 -sw_int 0.5 -nn_keras_metrics mae -solver_path "/nfs/iil/proj/dt/eva/smlp/external/mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic test for nn_keras flat encoding for sequential api, one response variable, adapts test 155
+172,smlp_toy_num_resp_mult,,"-mode verify -resp y2 -feat x,p1,p2 -model nn_keras -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -nn_keras_epochs 20 -nn_keras_seq_api f -nnet_encoding layered -nn_keras_tuner hyperband -nn_keras_layers_grid ""2,2;3,3,3"" -save_model_config f -spec smlp_toy_num_resp_mult_y2_verify.spec -asrt_names asrt1 -asrt_exprs ""2*y2>1"" -sw_coef 4 -sw_exp 5 -sw_int 0.5 -solver_path "mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic test for nn_keras flat encoding for functional api, i, one response variable, adapts test 154
+173,smlp_toy_num_resp_mult,,"-mode verify -resp y2 -feat x,p1,p2 -model nn_keras -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -nn_keras_epochs 20 -nn_keras_seq_api t -nnet_encoding layered -nn_keras_tuner hyperband -nn_keras_layers_grid ""2,2;3,3,3"" -save_model_config f -spec smlp_toy_num_resp_mult_y2_verify.spec -asrt_names asrt1 -asrt_exprs ""2*y2>1"" -sw_coef 4 -sw_exp 5 -sw_int 0.5 -nn_keras_metrics mae -solver_path "mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic test for nn_keras flat encoding for sequential api, one response variable, adapts test 155
 174,smlp_toy_num_resp_mult,,"-mode optsyn -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model nn_keras -nn_keras_epochs 20 -nn_keras_seq_api f -nnet_encoding layered -save_model f -use_model f -mrmr_pred 2 -model_per_response f -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic layered nn_keras encoding test with model_per_response f nn_keras_seq_api f for nn_keras in model exploration mode optsyn
 175,smlp_toy_num_resp_mult,,"-mode optsyn -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model nn_keras -nn_keras_epochs 20 -nn_keras_seq_api t -nnet_encoding layered -save_model f -use_model f -mrmr_pred 2 -model_per_response f -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic layered nn_keras encoding test with model_per_response f nn_keras_seq_api t for nn_keras in model exploration mode optsyn
 176,smlp_toy_num_resp_mult,,"-mode optsyn -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model nn_keras -nn_keras_epochs 20 -nn_keras_seq_api f -nnet_encoding layered -save_model f -use_model f -mrmr_pred 2 -model_per_response t -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic layered nn_keras encoding test with model_per_response t nn_keras_seq_api f for nn_keras in model exploration mode optsyn
@@ -180,7 +180,7 @@ d,data,new_data,switches,description
 179,smlp_toy_num_resp_mult,,"-mode optsyn -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model nn_keras -nn_keras_epochs 20 -nn_keras_seq_api f -nnet_encoding layered -save_model f -use_model f -mrmr_pred 2 -model_per_response f -scale_resp f -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic layered nn_keras encoding test with model_per_response f nn_keras_seq_api f for nn_keras in model exploration mode optsyn when resposes are not scaled adapts test 174
 180,smlp_toy_num_resp_mult,,"-mode optsyn -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model nn_keras -nn_keras_epochs 20 -nn_keras_seq_api t -nnet_encoding layered -save_model f -use_model f -mrmr_pred 2 -model_per_response f -scale_feat f -scale_resp f -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic layered nn_keras encoding test with model_per_response f nn_keras_seq_api t for nn_keras in model exploration mode optsyn when features and responses are not scaled adapts test 175
 181,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding flat -scale_feat f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic flat tree encoding test for dt_sklearn multi objective pareto optimization when features are not scaled modifies test 164
-182,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding flat -scale_resp f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -solver_path "/nfs/iil/proj/dt/eva/smlp/external/mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic flat tree encoding test for dt_sklearn multi objective pareto optimization when responses are not scaled modifies test 164
+182,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding flat -scale_resp f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -solver_path "mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic flat tree encoding test for dt_sklearn multi objective pareto optimization when responses are not scaled modifies test 164
 183,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding flat -scale_resp f -scale_feat f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic flat tree encoding test for dt_sklearn multi objective pareto optimization when features and responses are not scaled modifies test 164
 184,smlp_toy_num_resp_noknobs,smlp_toy_num_resp_noknobs_pred_labeled,"-mode verify -resp y1,y2 -feat x0,x1,x2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding branched -mrmr_pred 2 -model_per_response t -spec smlp_toy_num_resp_noknobs_verify.spec -asrt_names asrt1,asrt2,asrt3 -asrt_exprs ""(y2**3+x2)/2<6;y1>=9;y2<0"" -trace_anonym t -trace_prec 3 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",tests model term formation when mrmr_pred is activated and not all features are selected for training the model adapts test 139
 185,smlp_toy_num_resp_noknobs,smlp_toy_num_resp_noknobs_pred_labeled,"-mode verify -resp y1,y2 -feat x0,x1,x2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding branched -mrmr_pred 2 -model_per_response t -spec smlp_toy_num_resp_noknobs_verify.spec -asrt_names asrt1,asrt2,asrt3 -asrt_exprs ""(y2**3+x2)/2<6;y1>=9;y2<0"" -trace_anonym t -trace_prec 3 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",tests model term construction with branched_encoding of tress and model per reponse when mrmr_pred is activated and not all features are selected for training the model, adapts test 162
@@ -195,7 +195,7 @@ d,data,new_data,switches,description
 194,smlp_toy_num_resp_mult,,"-mode optsyn -resp y1,y2 -feat x,p1,p2 -model rf_sklearn -rf_sklearn_max_depth 4 -rf_sklearn_n_estimators 3 -tree_encoding branched -compress_rules t -save_model f -use_model f  -mrmr_pred 2 -model_per_response t -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic branched tree encoding test with model_per_response t for rf_sklearn in model exploration mode optsyn, adapts test 94 and test 167
 195,smlp_toy_num_resp_mult,,"-mode optimize -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model et_sklearn -et_sklearn_max_depth 2 -et_sklearn_n_estimators 3 -et_sklearn_bootstrap f -tree_encoding branched -model_per_response f -compress_rules t -save_model f -use_model f -mrmr_pred 2 -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -solver_path mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic test for et_sklearn with branched tree_encoding and model_per_response f in model exploration mode optimize adapts test 192 by setting n_estimators 3 and then discrepancy between z3, mathsat and yices results disappear
 196,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding branched -scale_feat f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic branched tree encoding test for dt_sklearn multi objective pareto optimization when features are not scaled modifies test 164 and test 181
-197,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding branched -scale_resp f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -solver_path "/nfs/iil/proj/dt/eva/smlp/external/mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic branched tree encoding test for dt_sklearn multi objective pareto optimization when responses are not scaled modifies test 164 and test 182
+197,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding branched -scale_resp f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -solver_path "mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"",basic branched tree encoding test for dt_sklearn multi objective pareto optimization when responses are not scaled modifies test 164 and test 182
 198,smlp_toy_num_resp_mult,,"-mode optimize -pareto t -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model dt_sklearn -dt_sklearn_max_depth 15 -compress_rules f -tree_encoding branched -scale_resp f -scale_feat f -spec smlp_toy_num_resp_mult_free_inps_beta_objv.spec -data_scaler min_max -epsilon 0.05 -delta_rel 0.01 -save_model_config f -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -solver_path mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat",basic branched tree encoding test for dt_sklearn multi objective pareto optimization when features and responses are not scaled modifies test 164 and test 183
 199,smlp_toy_num_resp_mult,,"-mode optimize -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model et_sklearn -et_sklearn_max_depth 2 -et_sklearn_n_estimators 100 -et_sklearn_bootstrap f -tree_encoding branched -model_per_response f -compress_rules t -save_model f -use_model f -mrmr_pred 2 -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0.05 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",test to demonstrate that in pareto optimization and optsyn modes with multiple objectives when beta constraints are not present SMLP results are not consistent when different solvers are used; this is due to fact that when a subset of objectoves are exemined in pareto algo, outputs not covered by the active objectives become don't cares (there are no contraints on then except model constraints) and this situation is likely not modeled in SMLP accurately; modifies test 192 to use z3 instead of mathsat
 200,smlp_toy_num_resp_mult,,"-mode optimize -opt_strategy lazy -resp y1,y2 -feat x,p1,p2 -model et_sklearn -et_sklearn_max_depth 2 -et_sklearn_n_estimators 100 -et_sklearn_bootstrap f -tree_encoding branched -model_per_response f -compress_rules t -save_model f -use_model f -mrmr_pred 2 -spec smlp_toy_num_resp_mult_optsyn.spec -epsilon 0.1 -delta_rel 0 -solver_path mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat -plots f -pred_plots f -resp_plots f -seed 10 -log_time f",basic test for et_sklearn with branched tree_encoding and model_per_response f in model exploration mode optimize adapts test 170 !!!!!!!!! in this test z3 result differs from mathsat and yices results (the latter two give sma results, cvc5 faild with incomparable ite tipes for if and else branches)