================
@@ -101,18 +123,37 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID
&ID) const {
Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
const Z3CrosscheckVisitor::Z3Result &Query) {
++NumZ3QueriesDone;
+ ++NumZ3QueriesDoneInEqClass;
+ AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
- if (!Query.IsSAT.has_value()) {
- // For backward compatibility, let's accept the first timeout.
+ if (Query.IsSAT && Query.IsSAT.value()) {
+ ++NumTimesZ3QueryAcceptsReport;
+ return AcceptReport; // sat
+ }
+
+ // Suggest cutting the EQClass if certain heuristics trigger.
+ if (Opts.Z3CrosscheckTimeoutThreshold &&
+ Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
++NumTimesZ3TimedOut;
- return AcceptReport;
+ ++NumTimesZ3QueryRejectEQClass;
+ return RejectEQClass;
}
- if (Query.IsSAT.value()) {
- ++NumTimesZ3QueryAcceptsReport;
- return AcceptReport; // sat
+ if (Opts.Z3CrosscheckRLimitThreshold &&
+ Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
+ ++NumTimesZ3ExhaustedRLimit;
+ ++NumTimesZ3QueryRejectEQClass;
+ return RejectEQClass;
+ }
+
+ if (AccumulatedZ3QueryTimeInEqClass > 700 /*ms*/) {
----------------
NagyDonat wrote:
It's counter-intuitive that this limit is hardcoded, while the others are not
-- e.g. this will silently override timeout thresholds above 700 ms.
Obviously this is bikeshedding, because practically nobody will use these
config options, but if we want to make this configurable, then we should make
the config clear and user-friendly. Either introduce this limit as a third
configurable value, or e.g. say that it's always twice the individual timeout
(which would yield 600 ms instead of 700 ms).
https://github.com/llvm/llvm-project/pull/95129
_______________________________________________
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
