tlopex commented on PR #19667: URL: https://github.com/apache/tvm/pull/19667#issuecomment-4617857865
Z3 fallback currently ignores the strength gate, so enabling it at all (especially in deeply recursive kDefault CanProve calls) causes unnecessary Z3 invocations and a measurable perf hit; it should be gated behind a higher threshold like kSymbolicBound to avoid paying prover cost on cheap paths I think. And EnterConstraint duplicates EnterWithScope without any real caller in this PR, and the new is_assume flag is effectively dead code since it is never set to true, so we should either deduplicate the entry logic and wire the flag with a real use/test or drop both changes until they’re actually needed. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected] --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
