Skip to content

fix for support for eta constraints in spec file #152

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
zurabksmlp wants to merge 6 commits into
base: master
Choose a base branch
from
Open

fix for support for eta constraints in spec file #152

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ca430da
fix for support for eta constraints in spec file
May 31, 2026
446399f
update regression masters for more eta constraints tests
May 31, 2026
972c4a4
fixed typos and now using * for model exploration api functions; adde…
Jun 2, 2026
8bc18a2
undo unintended removal of True or in smlp_flows module
Jun 3, 2026
48cdadc
Update expected results after eta spec handling fix
mdmitry1 Jun 3, 2026
3d143b1
Fixed typos in comment
mdmitry1 Jun 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions regr_smlp/master/Test100_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : y1>7 and y2>6

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
2 changes: 2 additions & 0 deletions regr_smlp/master/Test101_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : None

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
2 changes: 2 additions & 0 deletions regr_smlp/master/Test103_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : None

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
2 changes: 2 additions & 0 deletions regr_smlp/master/Test104_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : None

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
2 changes: 2 additions & 0 deletions regr_smlp/master/Test105_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : None

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
2 changes: 2 additions & 0 deletions regr_smlp/master/Test106_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : None

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
2 changes: 2 additions & 0 deletions regr_smlp/master/Test107_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : None

smlp_logger - INFO - Global beta : y1>5

smlp_logger - INFO - Global eta : None

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down
6 changes: 4 additions & 2 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : p2<5 and x==10 and x<12

smlp_logger - INFO - Global beta : (y1+y2)>y1

smlp_logger - INFO - Global eta : p1==4 or p1==8

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.05}
Expand Down Expand Up @@ -237,9 +239,9 @@ smlp_logger - INFO - Eta ranges constraints: (and (and true (and (>= p1 0) (

smlp_logger - INFO - Eta grid constraints: (or (or (= p1 2) (= p1 4)) (= p1 7))

smlp_logger - INFO - Eta global constraints: true
smlp_logger - INFO - Eta global constraints: (or (= p1 4) (= p1 8))

smlp_logger - INFO - Eta combined constraints: (let ((|:0| true)) (and (and (and (and |:0| (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) |:0|))
smlp_logger - INFO - Eta combined constraints: (and (and (and (and true (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) (or (= p1 4) (= p1 8)))

smlp_logger - INFO - Creating model exploration base components: End

Expand Down
8 changes: 8 additions & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_dt_sklearn_y1_tree_rules.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#Forest semantics: majority vote
#Number of trees: 1

#TREE 0
if (p2 > 0.7000000178813934) and (x <= 0.6666666716337204) then (y1 = 1.0) | based on 3 samples
if (p2 <= 0.7000000178813934) and (x <= 0.8333333432674408) then (y1 = 0.0) | based on 3 samples
if (p2 > 0.7000000178813934) and (x > 0.6666666716337204) then (y1 = 0.0) | based on 1 samples
if (p2 <= 0.7000000178813934) and (x > 0.8333333432674408) then (y1 = 1.0) | based on 1 samples
7 changes: 7 additions & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_dt_sklearn_y2_tree_rules.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#Forest semantics: majority vote
#Number of trees: 1

#TREE 0
if (p2 > 0.4000000134110451) and (p1 <= 0.75) then (y2 = 0.0) | based on 5 samples
if (p2 <= 0.4000000134110451) then (y2 = 1.0) | based on 2 samples
if (p2 > 0.4000000134110451) and (p1 > 0.75) then (y2 = 1.0) | based on 1 samples
2 changes: 1 addition & 1 deletion regr_smlp/master/Test108_smlp_toy_num_resp_mult_synthesize_results.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
"configuration_stable": "true",
"synthesis_status": "PASS",
"synthesis_result": {
"p1": 2.0,
"p1": 4.0,
"p2": 4.0
}
}
6 changes: 6 additions & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_trace.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
stage,solver,p1,p2,x,y1,y2
interface_consistency,sat,4,3,10
model_consistency,sat,4,3,10,5,9
synthesis,synthesis_feasibility
ca,sat,4,4,10,5,9
ce,unsat
1 change: 1 addition & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_y1_smlp_full_model_term.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
"{'y1': <smlp.core.libsmlp.term2 (let ((|:0| (* (/ 1 5) (- p2 3)))) (let ((|:1| (* (/ 1 3) (- x 9)))) (+ (* (ite (and (<= |:0| (/ 23488103 33554432)) (> |:1| (/ 27962027 33554432))) 1 (ite (and (> |:0| (/ 23488103 33554432)) (> |:1| (/ 44739243 67108864))) 0 (ite (and (<= |:0| (/ 23488103 33554432)) (<= |:1| (/ 27962027 33554432))) 0 1))) 4) 5)))>}"
1 change: 1 addition & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_y1_smlp_model_term.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
"{'y1_scaled': <smlp.core.libsmlp.term2 (ite (and (<= p2_scaled (/ 23488103 33554432)) (> x_scaled (/ 27962027 33554432))) 1 (ite (and (> p2_scaled (/ 23488103 33554432)) (> x_scaled (/ 44739243 67108864))) 0 (ite (and (<= p2_scaled (/ 23488103 33554432)) (<= x_scaled (/ 27962027 33554432))) 0 1)))>}"
1 change: 1 addition & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_y2_smlp_full_model_term.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
"{'y2': <smlp.core.libsmlp.term2 (let ((|:0| (* (/ 1 5) (- p2 3)))) (+ (* (ite (and (> |:0| (/ 53687093 134217728)) (> (* (/ 1 2) (- p1 2)) (/ 3 4))) 1 (ite (<= |:0| (/ 53687093 134217728)) 1 0)) 4) 5))>}"
1 change: 1 addition & 0 deletions regr_smlp/master/Test108_smlp_toy_num_resp_mult_y2_smlp_model_term.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
"{'y2_scaled': <smlp.core.libsmlp.term2 (ite (and (> p2_scaled (/ 53687093 134217728)) (> p1_scaled (/ 3 4))) 1 (ite (<= p2_scaled (/ 53687093 134217728)) 1 0))>}"
6 changes: 4 additions & 2 deletions regr_smlp/master/Test109_smlp_toy_num_resp_mult.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : p2<5 and x==10 and x<12

smlp_logger - INFO - Global beta : (y1+y2)/4>y1

smlp_logger - INFO - Global eta : p1==4 or p1==8

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.05}
Expand Down Expand Up @@ -237,9 +239,9 @@ smlp_logger - INFO - Eta ranges constraints: (and (and true (and (>= p1 0) (

smlp_logger - INFO - Eta grid constraints: (or (or (= p1 2) (= p1 4)) (= p1 7))

smlp_logger - INFO - Eta global constraints: true
smlp_logger - INFO - Eta global constraints: (or (= p1 4) (= p1 8))

smlp_logger - INFO - Eta combined constraints: (let ((|:0| true)) (and (and (and (and |:0| (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) |:0|))
smlp_logger - INFO - Eta combined constraints: (and (and (and (and true (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) (or (= p1 4) (= p1 8)))

smlp_logger - INFO - Creating model exploration base components: End

Expand Down
6 changes: 4 additions & 2 deletions regr_smlp/master/Test113_smlp_toy_basic.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : p2<5 and x1==10 and x2<12

smlp_logger - INFO - Global beta : y1>=4 and y2>=8

smlp_logger - INFO - Global eta : p1==4 or (p1==8 and p2 > 3)

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down Expand Up @@ -218,9 +220,9 @@ smlp_logger - INFO - Eta ranges constraints: (and (and true (and (>= p1 0) (

smlp_logger - INFO - Eta grid constraints: (or (or (= p1 2) (= p1 4)) (= p1 7))

smlp_logger - INFO - Eta global constraints: true
smlp_logger - INFO - Eta global constraints: (or (= p1 4) (and (= p1 8) (> p2 3)))

smlp_logger - INFO - Eta combined constraints: (let ((|:0| true)) (and (and (and (and |:0| (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) |:0|))
smlp_logger - INFO - Eta combined constraints: (and (and (and (and true (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) (or (= p1 4) (and (= p1 8) (> p2 3))))

smlp_logger - INFO - Creating model exploration base components: End

Expand Down
37 changes: 37 additions & 0 deletions regr_smlp/master/Test113_smlp_toy_basic_trace.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
stage,solver,p1,p2,x1,x2,y1,y2
interface_consistency,sat,4,3,10,0
model_consistency,sat,4,3,10,0,499791472247068216593/720575940379279360000,601/50
synthesis_feasibility
synthesis,synthesis_feasibility
ca,sat,4,4,10,0,107007/10000,1077047109884722593/112589990684262400
ce,unsat
pareto_iteration,0,objective1__objective2,None__None
single_objective_u0_l0_u_l, objective1_scaled_objective2_scaled : 1 : 0 : inf : -inf
objective_thresholds_u0_l0_u_l_T, 2 : 0 : inf : -inf : 1
synthesis,objective1_scaled_objective2_scaled_1
ca,sat,4,4,10,0,107007/10000,1077047109884722593/112589990684262400
ce,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : inf : 1 : 2
synthesis,objective1_scaled_objective2_scaled_2
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 2 : 1 : 1.5
synthesis,objective1_scaled_objective2_scaled_1.5
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.5 : 1 : 1.25
synthesis,objective1_scaled_objective2_scaled_1.25
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.25 : 1 : 1.125
synthesis,objective1_scaled_objective2_scaled_1.125
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.125 : 1 : 1.0625
synthesis,objective1_scaled_objective2_scaled_1.0625
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.0625 : 1 : 1.03125
synthesis,objective1_scaled_objective2_scaled_1.03125
ca,unsat
activity check, objective objective1 threshold 1.0
synthesis,thresholds_1.05_1.0_check
ca,unsat
activity check, objective objective2 threshold 1.0
synthesis,thresholds_1.0_1.05_check
ca,unsat
6 changes: 4 additions & 2 deletions regr_smlp/master/Test114_smlp_toy_basic.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : p2<5 and x1==10 and x2<12

smlp_logger - INFO - Global beta : y1>=4 and y2>=8

smlp_logger - INFO - Global eta : p1==4 or (p1==8 and p2 > 3)

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': Fraction(1, 10)}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down Expand Up @@ -216,9 +218,9 @@ smlp_logger - INFO - Eta ranges constraints: (and (and true (and (>= p1 0) (

smlp_logger - INFO - Eta grid constraints: (or (or (= p1 2) (= p1 4)) (= p1 7))

smlp_logger - INFO - Eta global constraints: true
smlp_logger - INFO - Eta global constraints: (or (= p1 4) (and (= p1 8) (> p2 3)))

smlp_logger - INFO - Eta combined constraints: (let ((|:0| true)) (and (and (and (and |:0| (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) |:0|))
smlp_logger - INFO - Eta combined constraints: (and (and (and (and true (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) (or (= p1 4) (and (= p1 8) (> p2 3))))

smlp_logger - INFO - Creating model exploration base components: End

Expand Down
1 change: 1 addition & 0 deletions regr_smlp/master/Test114_smlp_toy_basic_smlp_full_model_term.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
"{'y1': <smlp.core.libsmlp.term2 (let ((|:0| (* (/ 1 4) (- p2 3)))) (let ((|:1| (* (/ 5000 51839) (- x1 (/ (- 4109) 5000))))) (let ((|:2| (* (/ 1 2) (- x2 (- 1))))) (+ (* (ite (and (and (<= |:0| (/ 1 8)) (<= |:1| (/ 11378887 16777216))) (<= |:1| (/ 7587435 33554432))) (/ 144656617128537 18014398509481984) (ite (and (and (<= |:0| (/ 1 8)) (<= |:1| (/ 11378887 16777216))) (> |:1| (/ 7587435 33554432))) 0 (ite (and (<= |:0| (/ 1 8)) (> |:1| (/ 11378887 16777216))) (/ 3124582929976399 72057594037927936) (ite (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (<= |:1| (/ 38562449 536870912))) (/ 7364743914427397 9007199254740992) (ite (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (<= |:1| (/ 63736525 268435456))) (/ 4615234927434275 72057594037927936) (ite (and (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (> |:1| (/ 63736525 268435456))) (<= |:2| (/ 1 4))) (/ 4118666647088875 9007199254740992) (ite (and (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (> |:1| (/ 63736525 268435456))) (> |:2| (/ 1 4))) (/ 155796468224373 281474976710656) 1))))))) (/ 104607 10000)) (/ 6 25)))))>, 'y2': <smlp.core.libsmlp.term2 (let ((|:0| (* (/ 1 4) (- p2 3)))) (let ((|:1| (* (/ 5000 51839) (- x1 (/ (- 4109) 5000))))) (let ((|:2| (* (/ 1 2) (- x2 (- 1))))) (+ (* (ite (and (and (<= |:0| (/ 1 8)) (<= |:1| (/ 11378887 16777216))) (<= |:1| (/ 7587435 33554432))) (/ 1421319515427019 2251799813685248) (ite (and (and (<= |:0| (/ 1 8)) (<= |:1| (/ 11378887 16777216))) (> |:1| (/ 7587435 33554432))) (/ 1421319515427019 2251799813685248) (ite (and (<= |:0| (/ 1 8)) (> |:1| (/ 11378887 16777216))) 1 (ite (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (<= |:1| (/ 38562449 536870912))) (/ 2182179947885989 4503599627370496) (ite (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (<= |:1| (/ 63736525 268435456))) (/ 7441268742104829 9007199254740992) (ite (and (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (> |:1| (/ 63736525 268435456))) (<= |:2| (/ 1 4))) (/ 1421319515427019 2251799813685248) (ite (and (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (> |:1| (/ 63736525 268435456))) (> |:2| (/ 1 4))) (/ 1421319515427019 2251799813685248) (/ 1744855633611649 2251799813685248)))))))) (/ 109 10)) (/ 28 25)))))>}"
37 changes: 37 additions & 0 deletions regr_smlp/master/Test114_smlp_toy_basic_trace.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
stage,solver,p1,p2,x1,x2,y1,y2
interface_consistency,sat,4,3,10,0
model_consistency,sat,4,3,10,0,499791472247068216593/720575940379279360000,601/50
synthesis_feasibility
synthesis,synthesis_feasibility
ca,sat,4,4,10,0,107007/10000,1077047109884722593/112589990684262400
ce,unsat
pareto_iteration,0,objective1__objective2,None__None
single_objective_u0_l0_u_l, objective1_scaled_objective2_scaled : 1 : 0 : inf : -inf
objective_thresholds_u0_l0_u_l_T, 2 : 0 : inf : -inf : 1
synthesis,objective1_scaled_objective2_scaled_1
ca,sat,4,4,10,0,107007/10000,1077047109884722593/112589990684262400
ce,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : inf : 1 : 2
synthesis,objective1_scaled_objective2_scaled_2
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 2 : 1 : 1.5
synthesis,objective1_scaled_objective2_scaled_1.5
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.5 : 1 : 1.25
synthesis,objective1_scaled_objective2_scaled_1.25
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.25 : 1 : 1.125
synthesis,objective1_scaled_objective2_scaled_1.125
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.125 : 1 : 1.0625
synthesis,objective1_scaled_objective2_scaled_1.0625
ca,unsat
objective_thresholds_u0_l0_u_l_T, 4 : 0 : 1.0625 : 1 : 1.03125
synthesis,objective1_scaled_objective2_scaled_1.03125
ca,unsat
activity check, objective objective1 threshold 1.0
synthesis,thresholds_1.05_1.0_check
ca,unsat
activity check, objective objective2 threshold 1.0
synthesis,thresholds_1.0_1.05_check
ca,unsat
6 changes: 4 additions & 2 deletions regr_smlp/master/Test115_smlp_toy_basic.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ smlp_logger - INFO - Global alpha : p2<5 and x1==10 and x2<12

smlp_logger - INFO - Global beta : y1>=4 and y2>=8

smlp_logger - INFO - Global eta : p1==4 or (p1==8 and p2 > 3)

smlp_logger - INFO - Radii theta : {'p1': {'rad-abs': None, 'rad-rel': 0}, 'p2': {'rad-abs': Fraction(1, 5), 'rad-rel': None}}

smlp_logger - INFO - Delta const : {'delta_abs': 0.0, 'delta_rel': 0.01}
Expand Down Expand Up @@ -248,9 +250,9 @@ smlp_logger - INFO - Eta ranges constraints: (and (and true (and (>= p1 0) (

smlp_logger - INFO - Eta grid constraints: (or (or (= p1 2) (= p1 4)) (= p1 7))

smlp_logger - INFO - Eta global constraints: true
smlp_logger - INFO - Eta global constraints: (or (= p1 4) (and (= p1 8) (> p2 3)))

smlp_logger - INFO - Eta combined constraints: (let ((|:0| true)) (and (and (and (and |:0| (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) |:0|))
smlp_logger - INFO - Eta combined constraints: (and (and (and (and true (and (>= p1 0) (<= p1 10))) (and (>= p2 3) (<= p2 7))) (or (or (= p1 2) (= p1 4)) (= p1 7))) (or (= p1 4) (and (= p1 8) (> p2 3))))

smlp_logger - INFO - Creating model exploration base components: End

Expand Down
12 changes: 12 additions & 0 deletions regr_smlp/master/Test115_smlp_toy_basic_dt_sklearn_y1_tree_rules.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#Forest semantics: majority vote
#Number of trees: 1

#TREE 0
if (p2 > 0.125) and (x1 > 0.7929165363311768) then (y1 = 1.0) | based on 1 samples
if (p2 > 0.125) and (x1 <= 0.7929165363311768) and (x1 > 0.07182815857231617) and (x1 > 0.23743705824017525) and (x2 > 0.25) then (y1 = 0.5535002437695375) | based on 1 samples
if (p2 > 0.125) and (x1 <= 0.7929165363311768) and (x1 > 0.07182815857231617) and (x1 > 0.23743705824017525) and (x2 <= 0.25) then (y1 = 0.4572638542353763) | based on 1 samples
if (p2 > 0.125) and (x1 <= 0.7929165363311768) and (x1 > 0.07182815857231617) and (x1 <= 0.23743705824017525) then (y1 = 0.06404925100614682) | based on 1 samples
if (p2 > 0.125) and (x1 <= 0.7929165363311768) and (x1 <= 0.07182815857231617) then (y1 = 0.81765082642653) | based on 1 samples
if (p2 <= 0.125) and (x1 > 0.6782345175743103) then (y1 = 0.04336229889013164) | based on 1 samples
if (p2 <= 0.125) and (x1 <= 0.6782345175743103) and (x1 > 0.22612318396568298) then (y1 = 0.0) | based on 1 samples
if (p2 <= 0.125) and (x1 <= 0.6782345175743103) and (x1 <= 0.22612318396568298) then (y1 = 0.008030055350024379) | based on 1 samples
9 changes: 9 additions & 0 deletions regr_smlp/master/Test115_smlp_toy_basic_dt_sklearn_y2_tree_rules.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#Forest semantics: majority vote
#Number of trees: 1

#TREE 0
if (x1 <= 0.7450278699398041) and (p1 <= 0.8535353541374207) and (p2 <= 0.625) then (y2 = 0.6311926605504588) | based on 4 samples
if (x1 > 0.7450278699398041) and (p2 > 0.375) then (y2 = 0.7748715596330276) | based on 1 samples
if (x1 > 0.7450278699398041) and (p2 <= 0.375) then (y2 = 1.0) | based on 1 samples
if (x1 <= 0.7450278699398041) and (p1 > 0.8535353541374207) then (y2 = 0.48454128440366984) | based on 1 samples
if (x1 <= 0.7450278699398041) and (p1 <= 0.8535353541374207) and (p2 > 0.625) then (y2 = 0.8261467889908257) | based on 1 samples
6 changes: 6 additions & 0 deletions regr_smlp/master/Test115_smlp_toy_basic_trace.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
stage,solver,p1,p2,x1,x2,y1,y2
interface_consistency,sat,4,3,10,0
model_consistency,sat,4,3,10,0,499791472247068216593/720575940379279360000,601/50
witness_consistency,sat,4,3,10,1,499791472247068216593/720575940379279360000,601/50
witness_consistency,unsat
ca,unsat
1 change: 1 addition & 0 deletions regr_smlp/master/Test115_smlp_toy_basic_y1_smlp_full_model_term.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
"{'y1': <smlp.core.libsmlp.term2 (let ((|:0| (* (/ 1 4) (- p2 3)))) (let ((|:1| (* (/ 5000 51839) (- x1 (/ (- 4109) 5000))))) (let ((|:2| (* (/ 1 2) (- x2 (- 1))))) (+ (* (ite (and (and (<= |:0| (/ 1 8)) (<= |:1| (/ 11378887 16777216))) (<= |:1| (/ 7587435 33554432))) (/ 144656617128537 18014398509481984) (ite (and (and (<= |:0| (/ 1 8)) (<= |:1| (/ 11378887 16777216))) (> |:1| (/ 7587435 33554432))) 0 (ite (and (<= |:0| (/ 1 8)) (> |:1| (/ 11378887 16777216))) (/ 3124582929976399 72057594037927936) (ite (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (<= |:1| (/ 38562449 536870912))) (/ 7364743914427397 9007199254740992) (ite (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (<= |:1| (/ 63736525 268435456))) (/ 4615234927434275 72057594037927936) (ite (and (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (> |:1| (/ 63736525 268435456))) (<= |:2| (/ 1 4))) (/ 4118666647088875 9007199254740992) (ite (and (and (and (and (> |:0| (/ 1 8)) (<= |:1| (/ 3325733 4194304))) (> |:1| (/ 38562449 536870912))) (> |:1| (/ 63736525 268435456))) (> |:2| (/ 1 4))) (/ 155796468224373 281474976710656) 1))))))) (/ 104607 10000)) (/ 6 25)))))>}"
Loading