Source file regression_model_default.ml

open Smtzilla_utils.Regression_model

let default_models = [("z3", DTModel (Node { feature = "Lt"; threshold = (score_of_float 13.5); left = Node { feature = "ConvertSI32"; threshold = (score_of_float 0.5); left = Node { feature = "Eq"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_bitv"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_fp"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Div"; threshold = (score_of_float 1.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } }; right = Node { feature = "Lt"; threshold = (score_of_float 10.5); left = Node { feature = "And"; threshold = (score_of_float 3450.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Mul"; threshold = (score_of_float 3.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } } }; right = Node { feature = "Unop"; threshold = (score_of_float 0.5); left = Node { feature = "Xor"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Eq"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } } }; right = Node { feature = "Mul"; threshold = (score_of_float 3.5); left = Node { feature = "Mul"; threshold = (score_of_float 0.5); left = Node { feature = "Extract"; threshold = (score_of_float 35.5); left = Node { feature = "nb_queries"; threshold = (score_of_float 85.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Eq"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } }; right = Node { feature = "Lt"; threshold = (score_of_float 19.5); left = Node { feature = "Lt"; threshold = (score_of_float 14.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Zero_extend"; threshold = (score_of_float 3.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } } }; right = Node { feature = "Sign_extend"; threshold = (score_of_float 84.); left = Node { feature = "Shl"; threshold = (score_of_float 0.5); left = Node { feature = "Eq"; threshold = (score_of_float 1.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Binop"; threshold = (score_of_float 10.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } }; right = Node { feature = "Symbol"; threshold = (score_of_float 99.5); left = Node { feature = "Ty_bitv"; threshold = (score_of_float 185.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } }; right = Node { feature = "Val"; threshold = (score_of_float 504.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 36768502.5)); right = Leaf ((score_of_float 36768502.5)) } } } } } })); ("bitwuzla", DTModel (Node { feature = "Zero_extend"; threshold = (score_of_float 29.5); left = Node { feature = "ShrA"; threshold = (score_of_float 11.); left = Node { feature = "Binop"; threshold = (score_of_float 4.5); left = Node { feature = "ConvertSI32"; threshold = (score_of_float 0.5); left = Node { feature = "Eq"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "Ty_bool"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } }; right = Node { feature = "Ty_bitv"; threshold = (score_of_float 4.5); left = Node { feature = "Binop"; threshold = (score_of_float 10.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "And"; threshold = (score_of_float 4452.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } } }; right = Node { feature = "Eq"; threshold = (score_of_float 5.5); left = Node { feature = "Val"; threshold = (score_of_float 40.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "Ne"; threshold = (score_of_float 49.5); left = Node { feature = "Xor"; threshold = (score_of_float 6.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } } }; right = Node { feature = "Add"; threshold = (score_of_float 2.5); left = Node { feature = "Or"; threshold = (score_of_float 1.); left = Node { feature = "Unop"; threshold = (score_of_float 1.5); left = Node { feature = "nb_queries"; threshold = (score_of_float 51.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "Eq"; threshold = (score_of_float 7.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } }; right = Node { feature = "Extract"; threshold = (score_of_float 59.5); left = Node { feature = "Sign_extend"; threshold = (score_of_float 26.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "Not"; threshold = (score_of_float 0.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } } }; right = Node { feature = "Extract"; threshold = (score_of_float 249.); left = Node { feature = "Eq"; threshold = (score_of_float 7.); left = Node { feature = "LtU"; threshold = (score_of_float 2.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } }; right = Node { feature = "Eq"; threshold = (score_of_float 17.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } }; right = Node { feature = "Ne"; threshold = (score_of_float 1.5); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Binop"; threshold = (score_of_float 236.); left = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) }; right = Node { feature = "Ty_regexp"; threshold = (score_of_float (-2.)); left = Leaf ((score_of_float 61403449.333333336)); right = Leaf ((score_of_float 61403449.333333336)) } } } } } }))]