[WIP] NUSMods Optimizer Prototyping

codecov.yml

@@ -2,3 +2,7 @@ fixes:
   # For now we only report website coverage, and since tests are run directly in
   # the /website folder we need to add this
   - "::website/"
+ignore:
+  # Ignore webworkers since we can't test them
+  - "**/*.worker.ts" 
+  - "**/*.worker.js" 

website/package.json

@@ -120,7 +120,8 @@
     "webpack": "5.15.0",
     "webpack-cli": "4.3.1",
     "webpack-dev-server": "3.11.2",
-    "webpack-merge": "5.7.3"
+    "webpack-merge": "5.7.3",
+    "worker-loader": "^3.0.8"
   },
   "dependencies": {
     "@authenio/samlify-node-xmllint": "2.0.0",
@@ -168,6 +169,8 @@
     "reselect": "4.0.0",
     "samlify": "2.7.7",
     "searchkit": "2.4.1-alpha.5",
+    "sexpr-plus": "^7.0.0",
+    "smtlib-ext": "^1.0.0",
     "use-subscription": "1.5.1"
   },
   "browserslist": [

website/src/actions/optimizer.ts

@@ -0,0 +1,7 @@
+export const TOGGLE_OPTIMIZER_DISPLAY = 'TOGGLE_OPTIMIZER_DISPLAY' as const;
+export function toggleOptimizerDisplay() {
+  return {
+    type: TOGGLE_OPTIMIZER_DISPLAY,
+    payload: null,
+  };
+}

website/src/reducers/index.ts

@@ -8,6 +8,7 @@ import { Actions } from 'types/actions';
 import requests from './requests';
 import app from './app';
 import createUndoReducer from './undoHistory';
+import optimizer from './optimizer';
 
 // Persisted reducers
 import moduleBankReducer, { persistConfig as moduleBankPersistConfig } from './moduleBank';
@@ -41,6 +42,7 @@ export default function reducers(state: State = defaultState, action: Actions):
     requests: requests(state.requests, action),
     timetables: timetables(state.timetables, action),
     app: app(state.app, action),
+    optimizer: optimizer(state.optimizer, action),
     theme: theme(state.theme, action),
     settings: settings(state.settings, action),
     planner: planner(state.planner, action),

website/src/reducers/optimizer.ts

@@ -0,0 +1,22 @@
+import { OptimizerState } from 'types/reducers';
+import { Actions } from 'types/actions';
+
+import { TOGGLE_OPTIMIZER_DISPLAY } from 'actions/optimizer';
+
+export const defaultOptimizerState: OptimizerState = {
+  isOptimizerShown: false,
+};
+
+function optimizer(state: OptimizerState = defaultOptimizerState, action: Actions): OptimizerState {
+  switch (action.type) {
+    case TOGGLE_OPTIMIZER_DISPLAY:
+      return {
+        ...state,
+        isOptimizerShown: !state.isOptimizerShown,
+      };
+    default:
+      return state;
+  }
+}
+
+export default optimizer;

website/src/types/optimizer.ts

@@ -0,0 +1,165 @@
+// Intermediate types used to contain timetable information relevant to the optimizer
+import { mapValues, groupBy } from 'lodash';
+import { Module, RawLesson, StartTime, EndTime } from 'types/modules';
+import { SemTimetableConfig } from 'types/timetables';
+
+// {module id}__{lesson type}__{lesson id} e.g., CS3203__Lecture__1
+export type UniqueLessonString = string;
+export type Z3LessonID = number;
+
+/**
+ * Main input format into the optimizer layers
+ * */
+export type OptimizerInput = {
+  moduleInfo: ModuleInfoWithConstraints[];
+  constraints: GlobalConstraints;
+};
+
+/**
+ * Callbacks to communicate with the caller of TimetableOptimizer
+ * */
+export interface OptimizerCallbacks {
+  onOptimizerInitialized(): void;
+  onSmtlib2InputCreated(s: string): void;
+  onSmtLib2ResultOutput(s: string): void;
+  onTimetableOutput(timetable: OptimizerOutput): void;
+}
+
+/**
+ * Final timetable output to the optimizer caller
+ * */
+export type OptimizerOutput = {
+  isSat: boolean;
+  timetable: SemTimetableConfig;
+};
+
+/**
+ * Modules for optimizer to consider.
+ *  required is a constraint indicating if the module can be dropped to fulfil other constraints
+ * */
+export type ModuleInfoWithConstraints = {
+  mod: Module;
+  required: boolean;
+  lessonsGrouped: LessonsByGroupsByClassNo;
+};
+
+// Mapping between lesson types -> classNo -> lessons.
+//  We have to take one classNo of each lessonType, so this indicates all the slots to be filled
+//    per classNo per lessonType
+export type LessonsByGroupsByClassNo = {
+  [lessonType: string]: LessonsForLessonType;
+};
+
+export type LessonsForLessonType = { [classNo: string]: readonly RawLesson[] };
+
+/*
+ * A list of times that are assigned to a particular owner (e.g., a lesson)
+ * Used throughout optimizer to indicate that a particular block of time should be reserved if a owner id is chosen
+ */
+export interface SlotConstraint {
+  startEndTimes: Array<[number, number]>; // Array of start and end times as integers
+  ownerId: number; // Numeric ID of owner, since we will encode this as an integer constraint
+  ownerString: string; // string representing the owner: user-interpretable, used for varnames
+}
+
+/*
+ * Indicating that a varname (boolean selector) has a cost attached to it if it is chosen.
+ */
+export interface WorkloadCost {
+  varname: string;
+  cost: number;
+}
+
+// User-selected constraints to pass to optimizer
+export interface GlobalConstraints {
+  // Min/max number of MCs + whether the constraint is active
+  isWorkloadActive: boolean;
+  minWorkload: number;
+  maxWorkload: number;
+  // Find exactly N free days + whether the constraint is active
+  isFreeDayActive: boolean;
+  numRequiredFreeDays: number;
+  // Force these exact free days + whether the constraint is active
+  isSpecificFreeDaysActive: boolean;
+  specificFreeDays: Array<string>;
+  // When lessons should start and end + whether the constraint is active
+  isTimeConstraintActive: boolean;
+  earliestLessonStartTime: StartTime;
+  latestLessonEndTime: EndTime;
+  // The hours where a lunch break should be allocated,
+  //  how many half-hour slots to allocate, and whether the constraint is active
+  isLunchBreakActive: boolean;
+  lunchStart: StartTime;
+  lunchEnd: EndTime;
+  lunchHalfHours: number;
+  // Ask optimizer to compact timetable to leave as few gaps between lessons as possible
+  isPreferCompactTimetable: boolean;
+}
+
+/**
+ * Defs for communicating between Optimizer <-> WebWorker <-> WASM wrapper
+ * */
+// Need to disable since there's an eslint bug with enums
+// eslint-disable-next-line no-shadow
+export enum Z3WorkerMessageKind {
+  // Request to init
+  INIT = 'INIT',
+  // Z3 initialized
+  INITIALIZED = 'INITIALIZED',
+  // Run the optimizer
+  OPTIMIZE = 'OPTIMIZE',
+  // Print output
+  PRINT = 'PRINT',
+  // Error
+  ERR = 'ERR',
+  // Z3 finished runnung
+  EXIT = 'EXIT',
+  // Z3 aborted
+  ABORT = 'ABORT',
+}
+
+/**
+ * Message to be sent back and forth between a Z3 webworker and any callers
+ * */
+export interface Z3WorkerMessage {
+  kind: Z3WorkerMessageKind;
+  msg: string;
+}
+
+// TODO Shouldn't be here
+export const defaultConstraints: GlobalConstraints = {
+  isWorkloadActive: false,
+  minWorkload: 0,
+  maxWorkload: 30,
+  isFreeDayActive: false,
+  numRequiredFreeDays: 1,
+  isSpecificFreeDaysActive: false,
+  specificFreeDays: [],
+  earliestLessonStartTime: '0800',
+  latestLessonEndTime: '2200',
+  lunchStart: '1100',
+  lunchEnd: '1500',
+  lunchHalfHours: 2,
+  isLunchBreakActive: false,
+  isTimeConstraintActive: false,
+  isPreferCompactTimetable: false,
+};
+
+/**
+ * TODO move to utils
+ * Transforms a module's lessons into a mapping from
+ *  lessonType ==> (classNo ==> list of lessons)
+ * The optimizer cares that a classNo contains all the slots that should be filled.
+ * */
+export function lessonByGroupsByClassNo(lessons: readonly RawLesson[]): LessonsByGroupsByClassNo {
+  const lessonByGroups: { [lessonType: string]: readonly RawLesson[] } = groupBy(
+    lessons,
+    (lesson) => lesson.lessonType,
+  );
+  const lessonByGroupsByClassNumber = mapValues(
+    lessonByGroups,
+    (lessonsOfSamelessonType: readonly RawLesson[]) =>
+      groupBy(lessonsOfSamelessonType, (lesson) => lesson.classNo),
+  );
+  return lessonByGroupsByClassNumber;
+}

website/src/types/reducers.ts

@@ -83,6 +83,11 @@ export type ThemeState = Readonly<{
   showTitle: boolean;
 }>;
 
+/* optimizer */
+export type OptimizerState = Readonly<{
+  isOptimizerShown: boolean;
+}>;
+
 /* settings */
 export type ModRegRoundKey = { type: RegPeriodType; name?: string };
 

website/src/types/state.ts

@@ -4,6 +4,7 @@ import {
   Requests,
   SettingsState,
   ThemeState,
+  OptimizerState,
   TimetablesState,
   UndoHistoryState,
   VenueBank,
@@ -17,6 +18,7 @@ export type State = {
   timetables: TimetablesState;
   app: AppState;
   theme: ThemeState;
+  optimizer: OptimizerState;
   settings: SettingsState;
   planner: PlannerState;
   undoHistory: UndoHistoryState<State>;

website/src/types/vendor/sexpr-plus.d.ts

@@ -0,0 +1,30 @@
+declare module 'sexpr-plus' {
+  // Parses string into expressions
+  export function parse(input: string): Expr;
+  // Location of start or end of an expression
+  export type ExprLocation = {
+    offset: number;
+    line: number;
+    column: number;
+  };
+  // Location information for expressions
+  export type ExprLocations = {
+    start: ExprLocation;
+    end: ExprLocation;
+  };
+  // Base output type from parsing
+  export type ExprNode = {
+    type: string;
+    content: Expr;
+    location: ExprLocations;
+  };
+  export type Expr = string | ExprNode[];
+  // try-catch with instanceof during parsing
+  export interface SyntaxError {
+    message: string;
+    expected: string;
+    found: string;
+    location: ExprLocations;
+    name: string;
+  }
+}

website/src/types/vendor/worker-loader.d.ts

@@ -0,0 +1,10 @@
+declare module '*.worker.ts' {
+  // You need to change `Worker`, if you specified a different value for the `workerType` option
+  class WebpackWorker extends Worker {
+    constructor();
+  }
+
+  // Uncomment this if you set the `esModule` option to `false`
+  // export = WebpackWorker;
+  export default WebpackWorker;
+}

website/src/utils/optimizer/__mocks__/converter.ts

@@ -0,0 +1,9 @@
+export const mockOnmessage = jest.fn();
+export const mockPostMessage = jest.fn();
+
+const WebpackWorker = jest.fn().mockImplementation(() => ({
+  onmessage: mockOnmessage,
+  postMessage: mockPostMessage,
+}));
+
+export default WebpackWorker;

website/src/utils/optimizer/__mocks__/z3WebWorker.worker.ts

@@ -0,0 +1,9 @@
+export const mockOnmessage = jest.fn();
+export const mockPostMessage = jest.fn();
+
+const WebpackWorker = jest.fn().mockImplementation(() => ({
+  onmessage: mockOnmessage,
+  postMessage: mockPostMessage,
+}));
+
+export default WebpackWorker;

website/src/utils/optimizer/constants.ts

@@ -0,0 +1,22 @@
+import { invert } from 'lodash';
+import { WorkingDays } from 'types/modules';
+
+export const DAYS = WorkingDays.length; // One week mon - sat
+export const DAY_START_HOUR = 8; // This just needs to be earlier than the earliest lesson
+export const DAY_END_HOUR = 22; // Similarly, later than the latest lesson.
+export const HOURS_PER_DAY = DAY_END_HOUR - DAY_START_HOUR; // 14 8 am --> 10 pm. We save 24 - HOURS_PER_DAY variables per day.
+export const HOURS_PER_WEEK = HOURS_PER_DAY * DAYS;
+export const NUM_WEEKS = 13;
+
+export const DAY_IDXS: Record<string, number> = {
+  monday: 0,
+  tuesday: 1,
+  wednesday: 2,
+  thursday: 3,
+  friday: 4,
+  saturday: 5,
+};
+export const IDX_DAYS = invert(DAY_IDXS);
+
+// All possible week numbers we should encounter (except WeekRange)
+export const ALL_WEEKS = [[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13]];