Merge branch 'main' into f-RealWorld-Regressions

PicoSATLoadTime/allsat_blocksol.info

@@ -0,0 +1,15 @@
+description: Introduces an artificial regression of 1000ms into picosat that is related to the ALLSAT feature.
+include_revisions:
+  revision_range:
+    start: b25ef90e7bb4578d54ef9f4fef9fb3ee7a4e62c8
+path: allsat_blocksol.patch
+project_name: PicoSATLoadTime
+regression_severity: 1000
+shortname: allsat_blocksol
+tags:
+- load-time
+- regression
+- 1000ms
+- synthetic
+- AllSat
+- picosat

PicoSATLoadTime/allsat_blocksol.patch

@@ -0,0 +1,46 @@
+diff --git a/app.c b/app.c
+index 5f66ef8..17f127d 100644
+--- a/app.c
++++ b/app.c
+@@ -12,6 +12,33 @@
+ #define BUNZIP2 "bzcat %s"
+ #define GZIP "gzip -c -f > %s"
+
++#include <time.h>
++void busy_sleep_for_millisecs(unsigned long long Millisecs) {
++ printf("Sleepings for %llu milliseconds\n", Millisecs);
++ struct timespec ts;
++ timespec_get(&ts, TIME_UTC);
++
++ unsigned long long start_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ unsigned long long end_ns = start_ns + (Millisecs * 1000000);
++
++printf("Calculated diff: %u\n", (end_ns-start_ns));
++
++ unsigned long long current_ns = start_ns;
++  printf("busy_sleep start time: %llu\n",current_ns);
++  printf("busy_sleep end time:   %llu\n",end_ns);
++
++ while (current_ns < end_ns) {
++  for (long counter = 0; counter < 100000; ++counter) {
++   asm volatile("" : "+g"(counter) : :); // prevent optimization
++  }
++
++  timespec_get(&ts, TIME_UTC);
++  current_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ }
++
++  printf("busy_sleep current_ns at end: %llu\n",current_ns);
++}
++
+ FILE * popen (const char *, const char*);
+ int pclose (FILE *);
+
+@@ -229,6 +256,7 @@ printa (PicoSAT * picosat, int partial)
+ static void
+ blocksol (PicoSAT * picosat)
+ {
++  busy_sleep_for_millisecs(1000);
+   int max_idx = picosat_variables (picosat), i;
+
+   if (!sol)

PicoSATLoadTime/compact_trace_write_to_file.info

@@ -0,0 +1,16 @@
+description: Introduces an artificial regression of 1000ms into picosat that is related to the compact trace feature.
+include_revisions:
+  revision_range:
+    start: b25ef90e7bb4578d54ef9f4fef9fb3ee7a4e62c8
+path: compact_trace_write_to_file.patch
+project_name: PicoSATLoadTime
+regression_severity: 1000
+shortname: compact_trace_write_to_file
+tags:
+- load-time
+- regression
+- 1000ms
+- synthetic
+- compact_trace
+- picosat
+- perf_prec

PicoSATLoadTime/compact_trace_write_to_file.patch

@@ -0,0 +1,47 @@
+diff --git a/app.c b/app.c
+index 5f66ef8..1471146 100644
+--- a/app.c
++++ b/app.c
+@@ -12,6 +12,34 @@
+ #define BUNZIP2 "bzcat %s"
+ #define GZIP "gzip -c -f > %s"
+
++
++#include <time.h>
++void busy_sleep_for_millisecs(unsigned long long Millisecs) {
++ printf("Sleepings for %llu milliseconds\n", Millisecs);
++ struct timespec ts;
++ timespec_get(&ts, TIME_UTC);
++
++ unsigned long long start_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ unsigned long long end_ns = start_ns + (Millisecs * 1000000);
++
++printf("Calculated diff: %llu\n", (end_ns-start_ns));
++
++ unsigned long long current_ns = start_ns;
++  printf("busy_sleep start time: %llu\n",current_ns);
++  printf("busy_sleep end time:   %llu\n",end_ns);
++
++ while (current_ns < end_ns) {
++  for (long counter = 0; counter < 100000; ++counter) {
++   asm volatile("" : "+g"(counter) : :); // prevent optimization
++  }
++
++  timespec_get(&ts, TIME_UTC);
++  current_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ }
++
++  printf("busy_sleep current_ns at end: %llu\n",current_ns);
++}
++
+ FILE * popen (const char *, const char*);
+ int pclose (FILE *);
+
+@@ -741,6 +769,7 @@ picosat_main (int argc, char **argv)
+ 	    }
+ 	  else
+ 	    {
++	  	  busy_sleep_for_millisecs(1000);
+ 	      COMPACT_TRACE_NAME = argv[i];
+ 	      trace = 1;
+ 	    }

PicoSATLoadTime/extended_trace_write_to_file.info

@@ -0,0 +1,16 @@
+description: Introduces an artificial regression of 1000ms into picosat that is related to the extended trace feature.
+include_revisions:
+  revision_range:
+    start: b25ef90e7bb4578d54ef9f4fef9fb3ee7a4e62c8
+path: extended_trace_write_to_file.patch
+project_name: PicoSATLoadTime
+regression_severity: 1000
+shortname: extended_trace_write_to_file
+tags:
+- load-time
+- regression
+- 1000ms
+- synthetic
+- extended_trace
+- picosat
+- perf_prec

PicoSATLoadTime/extended_trace_write_to_file.patch

@@ -0,0 +1,47 @@
+diff --git a/app.c b/app.c
+index 5f66ef8..cc2fae5 100644
+--- a/app.c
++++ b/app.c
+@@ -12,6 +12,34 @@
+ #define BUNZIP2 "bzcat %s"
+ #define GZIP "gzip -c -f > %s"
+
++
++#include <time.h>
++void busy_sleep_for_millisecs(unsigned long long Millisecs) {
++ printf("Sleepings for %llu milliseconds\n", Millisecs);
++ struct timespec ts;
++ timespec_get(&ts, TIME_UTC);
++
++ unsigned long long start_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ unsigned long long end_ns = start_ns + (Millisecs * 1000000);
++
++printf("Calculated diff: %llu\n", (end_ns-start_ns));
++
++ unsigned long long current_ns = start_ns;
++  printf("busy_sleep start time: %llu\n",current_ns);
++  printf("busy_sleep end time:   %llu\n",end_ns);
++
++ while (current_ns < end_ns) {
++  for (long counter = 0; counter < 100000; ++counter) {
++   asm volatile("" : "+g"(counter) : :); // prevent optimization
++  }
++
++  timespec_get(&ts, TIME_UTC);
++  current_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ }
++
++  printf("busy_sleep current_ns at end: %llu\n",current_ns);
++}
++
+ FILE * popen (const char *, const char*);
+ int pclose (FILE *);
+
+@@ -762,6 +790,7 @@ picosat_main (int argc, char **argv)
+ 	    }
+ 	  else
+ 	    {
++	  	  busy_sleep_for_millisecs(1000);
+ 	      EXTENDED_TRACE_NAME = argv[i];
+ 	      trace = 1;
+ 	    }

PicoSATLoadTime/global_default_phase_jwh.info

@@ -0,0 +1,16 @@
+description: Introduces an artificial regression of 1000ms into picosat that is related to the Global Default Phase feature. Only occurs if JWH is used.
+include_revisions:
+  revision_range:
+    start: b25ef90e7bb4578d54ef9f4fef9fb3ee7a4e62c8
+path: global_default_phase_jwh.patch
+project_name: PicoSATLoadTime
+regression_severity: 1000
+shortname: global_default_phase_jwh
+tags:
+- load-time
+- regression
+- 1000ms
+- synthetic
+- GlobalDefaultPhase
+- picosat
+- perf_prec

PicoSATLoadTime/global_default_phase_jwh.patch

@@ -0,0 +1,49 @@
+diff --git a/picosat.c b/picosat.c
+index f97e3cb..ce115cd 100644
+--- a/picosat.c
++++ b/picosat.c
+@@ -31,6 +31,33 @@ IN THE SOFTWARE.
+
+ #include "picosat.h"
+
++#include <time.h>
++void busy_sleep_for_millisecs(unsigned long long Millisecs) {
++ printf("Sleepings for %llu milliseconds\n", Millisecs);
++ struct timespec ts;
++ timespec_get(&ts, TIME_UTC);
++
++ unsigned long long start_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ unsigned long long end_ns = start_ns + (Millisecs * 1000000);
++
++printf("Calculated diff: %llu\n", (end_ns-start_ns));
++
++ unsigned long long current_ns = start_ns;
++  printf("busy_sleep start time: %llu\n",current_ns);
++  printf("busy_sleep end time:   %llu\n",end_ns);
++
++ while (current_ns < end_ns) {
++  for (long counter = 0; counter < 100000; ++counter) {
++   asm volatile("" : "+g"(counter) : :); // prevent optimization
++  }
++
++  timespec_get(&ts, TIME_UTC);
++  current_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ }
++
++  printf("busy_sleep current_ns at end: %llu\n",current_ns);
++}
++
+ /* By default code for 'all different constraints' is disabled, since 'NADC'
+  * is defined.
+  */
+@@ -1269,6 +1296,10 @@ init (void * pmgr,
+   ps->state = READY;
+   ps->last_sat_call_result = 0;
+
++  if(GLOBAL_DEFAULT_PHASE == JWLPHASE) {
++    busy_sleep_for_millisecs(1000);
++  }
++
+   return ps;
+ }
+

PicoSATLoadTime/global_default_phase_neg.info

@@ -0,0 +1,16 @@
+description: Introduces an artificial regression of 1000ms into picosat that is related to the Global Default Phase feature. Only occurs if "Negative" is used.
+include_revisions:
+  revision_range:
+    start: b25ef90e7bb4578d54ef9f4fef9fb3ee7a4e62c8
+path: global_default_phase_neg.patch
+project_name: PicoSATLoadTime
+regression_severity: 1000
+shortname: global_default_phase_neg
+tags:
+- load-time
+- regression
+- 1000ms
+- synthetic
+- GlobalDefaultPhase
+- picosat
+- perf_prec

PicoSATLoadTime/global_default_phase_neg.patch

@@ -0,0 +1,49 @@
+diff --git a/picosat.c b/picosat.c
+index f97e3cb..83d8210 100644
+--- a/picosat.c
++++ b/picosat.c
+@@ -31,6 +31,33 @@ IN THE SOFTWARE.
+
+ #include "picosat.h"
+
++#include <time.h>
++void busy_sleep_for_millisecs(unsigned long long Millisecs) {
++ printf("Sleepings for %llu milliseconds\n", Millisecs);
++ struct timespec ts;
++ timespec_get(&ts, TIME_UTC);
++
++ unsigned long long start_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ unsigned long long end_ns = start_ns + (Millisecs * 1000000);
++
++printf("Calculated diff: %llu\n", (end_ns-start_ns));
++
++ unsigned long long current_ns = start_ns;
++  printf("busy_sleep start time: %llu\n",current_ns);
++  printf("busy_sleep end time:   %llu\n",end_ns);
++
++ while (current_ns < end_ns) {
++  for (long counter = 0; counter < 100000; ++counter) {
++   asm volatile("" : "+g"(counter) : :); // prevent optimization
++  }
++
++  timespec_get(&ts, TIME_UTC);
++  current_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ }
++
++  printf("busy_sleep current_ns at end: %llu\n",current_ns);
++}
++
+ /* By default code for 'all different constraints' is disabled, since 'NADC'
+  * is defined.
+  */
+@@ -1269,6 +1296,10 @@ init (void * pmgr,
+   ps->state = READY;
+   ps->last_sat_call_result = 0;
+
++  if(GLOBAL_DEFAULT_PHASE == NEGPHASE) {
++    busy_sleep_for_millisecs(1000);
++  }
++
+   return ps;
+ }
+

PicoSATLoadTime/global_default_phase_pos.info

@@ -0,0 +1,16 @@
+description: Introduces an artificial regression of 1000ms into picosat that is related to the Global Default Phase feature. Only occurs if "Positive" is used.
+include_revisions:
+  revision_range:
+    start: b25ef90e7bb4578d54ef9f4fef9fb3ee7a4e62c8
+path: global_default_phase_pos.patch
+project_name: PicoSATLoadTime
+regression_severity: 1000
+shortname: global_default_phase_pos
+tags:
+- load-time
+- regression
+- 1000ms
+- synthetic
+- GlobalDefaultPhase
+- picosat
+- perf_prec

PicoSATLoadTime/global_default_phase_pos.patch

@@ -0,0 +1,49 @@
+diff --git a/picosat.c b/picosat.c
+index f97e3cb..f481800 100644
+--- a/picosat.c
++++ b/picosat.c
+@@ -31,6 +31,33 @@ IN THE SOFTWARE.
+
+ #include "picosat.h"
+
++#include <time.h>
++void busy_sleep_for_millisecs(unsigned long long Millisecs) {
++ printf("Sleepings for %llu milliseconds\n", Millisecs);
++ struct timespec ts;
++ timespec_get(&ts, TIME_UTC);
++
++ unsigned long long start_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ unsigned long long end_ns = start_ns + (Millisecs * 1000000);
++
++printf("Calculated diff: %llu\n", (end_ns-start_ns));
++
++ unsigned long long current_ns = start_ns;
++  printf("busy_sleep start time: %llu\n",current_ns);
++  printf("busy_sleep end time:   %llu\n",end_ns);
++
++ while (current_ns < end_ns) {
++  for (long counter = 0; counter < 100000; ++counter) {
++   asm volatile("" : "+g"(counter) : :); // prevent optimization
++  }
++
++  timespec_get(&ts, TIME_UTC);
++  current_ns = ts.tv_sec * 1000000000 + ts.tv_nsec;
++ }
++
++  printf("busy_sleep current_ns at end: %llu\n",current_ns);
++}
++
+ /* By default code for 'all different constraints' is disabled, since 'NADC'
+  * is defined.
+  */
+@@ -1269,6 +1296,10 @@ init (void * pmgr,
+   ps->state = READY;
+   ps->last_sat_call_result = 0;
+
++  if(GLOBAL_DEFAULT_PHASE == POSPHASE) {
++    busy_sleep_for_millisecs(1000);
++  }
++
+   return ps;
+ }
+