Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use Dolmen in the JS worker #1249

Merged
merged 4 commits into from
Oct 7, 2024
Merged

Commits on Oct 3, 2024

  1. Configuration menu
    Copy the full SHA
    f193259 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. Use Dolmen in the Javascript Worker

    This PR removes the dependency of the Javascript worker to the legacy
    frontend in order to remove it completely. In order to avoid code
    duplication as it was done with the legacy frontend, we reuse the
    `Solving_loop` module in the worker. This requires some modifications:
    
    - Add a new argument to the main function of `Solving_loop` to give
      different kind of sources instead of reading the file at the path
      `Options.get_file ()`. The worker used a raw string as input. I reused
      the type `Dolmen_loop.State.source`.
    
    - Add a new argument to the main function of `Solving_loop` to pass the
      selector hook to the constructor of the environment of the SAT solver.
      This hook is not used by the worker to select instantiations but just to
      record them. I have no strong opinion to preserve this feature but I
      try to keep all the feature of the Javascript worker.
    
    - Remove the unused `sat_env` argument of the constructor `init_env` in
      `Frontend`. This removal is mostly motivated by the fact the semantic
      of `init_env = Some env` + `selector_inst = Some f` is not clear at
      all.
    
    - Monomophize the `status` type in `Frontend`. This status is only used
      for printting purposes but we kept the SAT environment in some of its
      constructors. Unfortunately, the type of the SAT can change at the
      very beginning of the main function of `Solving_loop`, which means it
      is not easy to add a new argument for the `hook_status`. This hook is
      required to print the result of AE in the worker.
    Halbaroth committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    f6b986e View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. Configuration menu
    Copy the full SHA
    3a3a8b8 View commit details
    Browse the repository at this point in the history
  2. Simplify mk_files in Solving_loop

    We do not need `In_channel.input_all` too ;)
    Halbaroth committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    27cf381 View commit details
    Browse the repository at this point in the history