Given's Rotation SVD example, simplified

Time bar (total: 27.7s)

analyze1.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%100%0%0%0%0%0
100%100%0%0%0%0%0%1
Compiler

Compiled 14 to 10 computations (28.6% saved)

sample27.3s (98.7%)

Results
2.0s4158×0valid
502.0ms4104×0valid-sollya
4.5s4098×1valid
875.0ms4030×1valid-sollya
33.0ms68×1exit-sollya
45.0ms54×0exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(3.963227483252121e-133)1.9633965105006178e-266(0.0 5.421010862427522e-20)+nan.0validexit10.215809#f
(4.9587776526132955e-113)3.073684476007128e-226(0.0 5.421010862427522e-20)+nan.0validexit10.23272099999999998#f
(3.4254004067462683e-40)1.4666709933171876e-80(0.0 5.421010862427522e-20)+nan.0validexit10.208182#f
(8.275495183057839e-107)8.560477565601686e-214(0.0 5.421010862427522e-20)+nan.0validexit10.173331#f
(-2.721360902709262e-140)9.257256453493212e-281(0.0 5.421010862427522e-20)+nan.0validexit10.217052#f
(4.0811366243868555e-61)2.0819595183639673e-122(0.0 5.421010862427522e-20)+nan.0validexit10.237047#f
(-2.5221231199428513e+129)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.224126#f
(1.650341540630745e+277)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.190665#f
(2.4024060875035996e+302)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.26271#f
(-2.615766484621159e+224)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.211562#f
(-4.414876115196412e+231)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.111587#f
(-7.516072917601343e-274)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.20597000000000001#f
(-1.068950749912924e+285)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.221654#f
(-1.7770338221870913e-303)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.217831#f
(-3.7824373347307535e-57)1.788354023895636e-114(0.0 5.421010862427522e-20)+nan.0validexit10.321004#f
(4.7339387509635365e-283)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.244925#f
(-1.078471236741995e+26)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.213358#f
(-4.929306626907673e-137)3.0372579777594875e-274(0.0 5.421010862427522e-20)+nan.0validexit10.122679#f
(1.6408105117334488e-178)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13636900000000002#f
(1.831311518715137e-304)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.24660300000000002#f
(-2.7739388157508404e-217)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.231303#f
(-5.476472935293311e+29)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.209878#f
(4.357507757993547e+205)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.22995900000000002#f
(4.482715501095871e+83)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.236259#f
(-7.658235156918579e-261)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.22992600000000002#f
(-6.1062764645543794e-124)4.660826532696341e-248(0.0 5.421010862427522e-20)+nan.0validexit10.224997#f
(-6.455146865526693e-240)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.267253#f
(7.319188007766597e+149)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.219948#f
(7.981629997213683e-124)7.963302176552663e-248(0.0 5.421010862427522e-20)+nan.0validexit10.119381#f
(-1.3690951342805385e-157)2.34302686e-315(0.0 5.421010862427522e-20)+nan.0validexit10.238981#f
(-2.2956264073749795e+73)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.11172599999999999#f
(3.623624342955e-102)1.641331672357007e-204(0.0 5.421010862427522e-20)+nan.0validexit10.120477#f
(-3.6924737645007255e-146)1.70429531269077e-292(0.0 5.421010862427522e-20)+nan.0validexit10.24241900000000002#f
(2.3077721065694454e-144)6.6572651198249695e-289(0.0 5.421010862427522e-20)+nan.0validexit10.12323100000000001#f
(9.680298340636827e-153)1.1713521995467015e-305(0.0 5.421010862427522e-20)+nan.0validexit10.243883#f
(-7.299424516064266e-242)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.198194#f
(5.203006039684116e-187)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.142175#f
(-5.693342604242261e+88)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.201409#f
(-4.9690026553919895e+177)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.210901#f
(3.5790723757606626e+111)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.21978699999999998#f
(-2.852683272033409e-303)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.238793#f
(-5.693705777670083e-175)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.11665#f
(-1.551919451420782e-125)3.010567479622726e-251(0.0 5.421010862427522e-20)+nan.0validexit10.247268#f
(-5.604356419530156e-65)3.926101359641109e-130(0.0 5.421010862427522e-20)+nan.0validexit10.258862#f
(-1.6146511019587933e-176)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.230226#f
(-1750825654.8976178)0.29289321861151724(0.29289321861151724 0.29289321861151724)+nan.0validexit00.227035#f
(1.3964707182809222e-186)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.231369#f
(-1.9571559766329084e+281)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.1096604432262118e+301)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.24052300000000001#f
(2.5830037615982462e+191)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.26884#f
(1.4310250282166868e-104)2.5597907892282114e-209(0.0 5.421010862427522e-20)+nan.0validexit10.131901#f
(-3.921745545420122e-257)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.122853#f
(3.0010669216577304e-101)1.1258003335335258e-202(0.0 5.421010862427522e-20)+nan.0validexit10.24680699999999997#f
(-8.485036474207696e+110)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.24896800000000002#f
(-8.963183995462762e-60)1.0042333417064976e-119(0.0 5.421010862427522e-20)+nan.0validexit10.120573#f
(-8.501106521809911e-290)-0.0(+nan.0 +nan.0)+nan.0validexit15.0#f
(-1.1087468632888853e-121)1.5366495085661776e-243(0.0 5.421010862427522e-20)+nan.0validexit10.28133800000000003#f
(-1.5884218546552932e+52)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(-1.830002580768506e-106)4.18613680702424e-213(0.0 5.421010862427522e-20)+nan.0validexit10.203316#f
(-3.7223277787337614e-128)1.7319655115416272e-256(+nan.0 +nan.0)+nan.0validexit15.0#f
(-1.6554937992164205e-97)3.425824649055022e-195(0.0 5.421010862427522e-20)+nan.0validexit10.238753#f
(-1.1823606954983015e+181)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.212673#f
(-1.3280836710259863e-127)2.204757796557325e-255(0.0 5.421010862427522e-20)+nan.0validexit10.117556#f
(-2.0962735987573295e-224)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.242174#f
(1.011206884275921e-116)1.2781742035087699e-233(0.0 5.421010862427522e-20)+nan.0validexit10.240017#f
(2.7638397152050935e-284)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.162877#f
(-5.991827904828387e+287)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.221278#f
(-5.598751439874995e-130)3.918252210687791e-260(0.0 5.421010862427522e-20)+nan.0validexit10.244093#f
(-4.606687511113949e-72)2.6526962281316535e-144(0.0 5.421010862427522e-20)+nan.0validexit10.11700400000000001#f
(-4.092576726378703e-282)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.235174#f
(-163706579831119550.0)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.24110700000000002#f
(-8.7703431374612e+236)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.22089599999999998#f
(-1.9176327434423624e+266)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(-1.4444230383201652e+242)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.23414900000000002#f
(-1.326181171180229e-85)2.1984456234912047e-171(0.0 5.421010862427522e-20)+nan.0validexit10.273775#f
(-1.4992335869046365e+149)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.221663#f
(-2.276668178369782e+232)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(8.657505033093292e+233)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.23623#f
(-1.9865062595607946e+217)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.249049#f
(-3.7916907860936705e+218)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.114354#f
(5.904369148011426e-100)4.3576968794986465e-200(0.0 5.421010862427522e-20)+nan.0validexit10.283141#f
(3.392267846885325e+39)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.235293#f
(6.824712857595244e+82)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.247417#f
(-1.3574383672854873e-26)2.303298651223362e-53(0.0 5.421010862427522e-20)+nan.0validexit10.11638#f
(-1.3362976679272611e-66)2.232114321634796e-133(+nan.0 +nan.0)+nan.0validexit15.0#f
(-2.272166060352717e-75)6.453423257273484e-151(0.0 5.421010862427522e-20)+nan.0validexit10.260611#f
(-9.488733400711638e-297)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.12273899999999999#f
(3.9803869953152543e+217)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.247433#f
(-2.2975473245469167e-114)6.598404635665869e-229(0.0 5.421010862427522e-20)+nan.0validexit10.227818#f
(-6.550237100424727e-97)5.363200758972567e-194(0.0 5.421010862427522e-20)+nan.0validexit10.17022700000000002#f
(3.535584247144028e+182)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.125747#f
(-7.965467681767583e-191)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.290761#f
(-3.3783504842853624e+218)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.25086200000000003#f
(-2.160895044334607e+189)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.23368799999999998#f
(-8.435160716918041e+61)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.212948#f
(6.89483666993259e-63)5.942346588130891e-126(0.0 5.421010862427522e-20)+nan.0validexit10.280773#f
(-4.855089015100535e+263)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(-3.6022265560856157e+124)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.230106#f
(-2.3190412004407377e-14)6.722440111677022e-29(+nan.0 +nan.0)+nan.0validexit15.0#f
(1.2351390526190079e+82)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.11144799999999999#f
(-1.3859935843804217e+219)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.176115#f
(3.4769458969974423e+186)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.227324#f
(8.223218737145057e-35)8.452665799866693e-70(0.0 5.421010862427522e-20)+nan.0validexit10.228941#f
(6.105389836987882e+193)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.2613145904105508e+81)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.206926#f
(4.895087095301784e-179)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.21792799999999998#f
(-4.8450833502954796e-194)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.272462#f
(6.709815333262279e-38)5.627702725810199e-76(0.0 5.421010862427522e-20)+nan.0validexit10.277631#f
(1.056758938804455e+139)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.224922#f
(-4.652635590046614e-277)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.255621#f
(-2.246441308145464e+221)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.177896#f
(2.799268230171088e-273)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.23769300000000002#f
(1.294950736406972e+217)0.2928932188134525(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.9066528220264405e+178)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.10076600000000001#f
(-3.2149111656062637e-198)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.24447599999999997#f
(2.660507463088568e+72)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.23491#f
(-2.9556442416599125e-245)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.147735#f
(-3.449136471945975e+203)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.115221#f
(7.839552694950336e-27)7.682323307112883e-54(0.0 5.421010862427522e-20)+nan.0validexit10.175408#f
(3.558788625239762e-108)1.5831220598919897e-216(0.0 5.421010862427522e-20)+nan.0validexit10.12249099999999999#f
(1.2558796873448282e+175)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.25096199999999996#f
(-4.598856323255119e+195)0.2928932188134525(0.2928932188134525 0.2928932188134525)+nan.0validexit00.227584#f
Sollya timings
Total time spent in Sollya 1.5s
Bogosity

preprocess260.0ms (0.9%)

Algorithm
egg-herbie
Rules
43×fma-define
34×fma-neg
13×neg-mul-1
12×associate--r+
12×associate-+l-
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
022160
157128
295128
3158128
4242128
5300128
6328128
7338128
8342128
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) (neg.f64 x)))))))
(neg.f64 (-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) (neg.f64 x))))))))
Outputs
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (*.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1/2 binary64) (hypot.f64 #s(literal 1 binary64) x)))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (*.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1/2 binary64) (hypot.f64 #s(literal 1 binary64) x)))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) (neg.f64 x)))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (*.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
(-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1/2 binary64) (hypot.f64 #s(literal 1 binary64) x)))))
(neg.f64 (-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) (neg.f64 x))))))))
(neg.f64 (-.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (*.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) (neg.f64 x))))))))
(+.f64 #s(literal -1 binary64) (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1/2 binary64) (hypot.f64 #s(literal 1 binary64) x)))))
(+.f64 (sqrt.f64 (+.f64 #s(literal 1/2 binary64) (/.f64 #s(literal 1/2 binary64) (hypot.f64 #s(literal 1 binary64) x)))) #s(literal -1 binary64))
Symmetry

(abs x)

Compiler

Compiled 13 to 9 computations (30.8% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
75.4%
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
Compiler

Compiled 26 to 18 computations (30.8% saved)

simplify13.0ms (0%)

Algorithm
egg-herbie
Rules
1-exp
+-commutative
sub-neg
*-commutative
neg-sub0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01438
12338
22738
32938
43038
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))
Outputs
(-.f64 #s(literal 1 binary64) (sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (hypot.f64 #s(literal 1 binary64) x))))))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 13 to 9 computations (30.8% saved)

preprocess94.0ms (0.3%)

Remove

(abs x)

Compiler

Compiled 104 to 72 computations (30.8% saved)

end0.0ms (0%)

Profiling

Loading profile data...