Home
last modified time | relevance | path

Searched refs:useless_simpl_refs (Results 1 – 3 of 3) sorted by relevance

/dports/math/eprover/eprover-E-2.0/PCL2/
H A Dpcl_analysis.c82 w1 = s1->useless_gen_refs/(float)(s1->useless_simpl_refs+1); in pcl_example_cmp()
83 w2 = s2->useless_gen_refs/(float)(s2->useless_simpl_refs+1); in pcl_example_cmp()
279 parent->useless_simpl_refs++; in PCLExprUpdateGRefs()
H A Dpcl_steps.c330 step->useless_simpl_refs, in PCLStepPrintExtra()
586 step->useless_simpl_refs/(float)(total_steps-proof_steps+1), in PCLStepPrintExample()
641 step->useless_simpl_refs = 0; in PCLStepResetTreeData()
H A Dpcl_steps.h91 long useless_simpl_refs; /* Simplification of member