speeduping constrain_assertion
renaming check_p_r_l to inferSATFormula_plr to ease understanding
findLR_checkO_nonloop to inferSATFormula_plr_nonloop
findLR_checkO_loop_wrap to inferSATFormula_plr_loop