================
@@ -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*/) {
+ ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
+ ++NumTimesZ3QueryRejectEQClass;
+ return RejectEQClass;
}
+ // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
+ // then reject the report.
++NumTimesZ3QueryRejectReport;
return RejectReport; // unsat
----------------
NagyDonat wrote:
```suggestion
return RejectReport;
```
This doesn't add anything and is technically incorrect.
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
