Move assertion out of loop for better performance

This is related to bug 508. The debug build was taking much longer than the
production build to compute the result. The issue was an assertion in a loop in
nonClausalSimplify(). By moving the assertion outside of the loop, the debug
build is now roughly an order of magnitude slower than the production build
(instead of two orders of magnitude), which seems to be roughly in line with
the difference for other benchmarks:

Debug version before change:
- Bug (minified version): 1065.6s
- regress3/friedman_n6_i4.smt: 6.9s
- regress2/uflia-error0.smt2: 6.3s
- regress2/fuzz_2.smt: 2.3s

Debug version after change:
- Bug (minified version): 131.4s
- regress3/friedman_n6_i4.smt: 6.7s
- regress2/uflia-error0.smt2: 6.2s
- regress2/fuzz_2.smt: 1.9s

Production version:
- Bug (minified version): 18.8s
- regress3/friedman_n6_i4.smt: 0.8s
- regress2/uflia-error0.smt2: 0.8s
- regress2/fuzz_2.smt: 0.2s

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a95ce7b8d1df860468ade7f00216378f58153339..31b62f25a62e9d92d6fe097d93afc68b4eb8ae03 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2997,39 +2997,44 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         }
         break;
     }
+  }
 
 #ifdef CVC4_ASSERTIONS
-    // Check data structure invariants:
-    // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
-    // 2. each lhs of constantPropagations rewrites to itself
-    // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
-    //    constant propagation too
-    // 4. each lhs of constantPropagations is different from each rhs
-    for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
-      Assert((*pos).first.isVar());
-      Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
-      Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
-      Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
-    }
-    for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
-      Assert((*pos).second.isConst());
-      Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
-      // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
-      // if (newLeft != (*pos).first) {
-      //   newLeft = Rewriter::rewrite(newLeft);
-      //   Assert(newLeft == (*pos).second ||
-      //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
-      // }
-      // newLeft = constantPropagations.apply((*pos).first);
-      // if (newLeft != (*pos).first) {
-      //   newLeft = Rewriter::rewrite(newLeft);
-      //   Assert(newLeft == (*pos).second ||
-      //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
-      // }
-      Assert(constantPropagations.apply((*pos).second) == (*pos).second);
-    }
-#endif /* CVC4_ASSERTIONS */
+  // NOTE: When debugging this code, consider moving this check inside of the
+  // loop over d_nonClausalLearnedLiterals. This check has been moved outside
+  // because it is costly for certain inputs (see bug 508).
+  //
+  // Check data structure invariants:
+  // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
+  // 2. each lhs of constantPropagations rewrites to itself
+  // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
+  //    constant propagation too
+  // 4. each lhs of constantPropagations is different from each rhs
+  for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
+    Assert((*pos).first.isVar());
+    Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
+    Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
+    Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
   }
+  for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
+    Assert((*pos).second.isConst());
+    Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
+    // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
+    // if (newLeft != (*pos).first) {
+    //   newLeft = Rewriter::rewrite(newLeft);
+    //   Assert(newLeft == (*pos).second ||
+    //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+    // }
+    // newLeft = constantPropagations.apply((*pos).first);
+    // if (newLeft != (*pos).first) {
+    //   newLeft = Rewriter::rewrite(newLeft);
+    //   Assert(newLeft == (*pos).second ||
+    //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+    // }
+    Assert(constantPropagations.apply((*pos).second) == (*pos).second);
+  }
+#endif /* CVC4_ASSERTIONS */
+
   // Resize the learnt
   Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
   d_nonClausalLearnedLiterals.resize(j);