Added command-line arg check to not test identity

For those configurations of aA and cC that would cause the weight distribution to be an identity operation, DDFw short-circuits early so as not to enter into an infinite loop dependent only on imprecisions in floating-point arithmetic
ccodel · Jan 21, 2021 · 6e06dae · 6e06dae
1 parent 1f4e27d
commit 6e06dae
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/main.c b/main.c
@@ -15,6 +15,11 @@
 #include "ddfw.h"
 #include "logger.h"
 
+/** Calculates the absolute value of the number passed in. */
+#ifndef ABS
+#define ABS(x)     (((x) < 0) ? -(x) : (x))
+#endif
+
 /** @brief Main function. Processes command-line arguments and kicks off DDFW.
  *
  *  @param argc  The number of arguments given on the command line.
@@ -139,6 +144,15 @@ int main(int argc, char *argv[]) {
     return 0;
   }
 
+  // Check that a weight change will *actually* have an effect, otherwise
+  // the weight distribution is an identity, which just won't do
+  double change_in_weight = (mult_a * init_clause_weight) + add_c;
+  if (ABS(change_in_weight - init_clause_weight) < 0.001) {
+    fprintf(stderr, "No change in weight if transfer, not testing\n");
+    return 0;
+  }
+
+
   // All command-line arguments have been validated, proceed with setup
   // Print banner
   log_str("c ------------------------------------------------------------\n");