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.

Sign up for GitHub

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

Jump to bottom

CNF conversion refactoring #5547

Merged
merged 2 commits into from
Sep 20, 2021
Merged

CNF conversion refactoring #5547

merged 2 commits into from
Sep 20, 2021

Commits on Sep 13, 2021

  1. split sat2goal out of goal2sat 

    These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.

I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.
    @jameysharp
    jameysharp committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    3ec1a10 View commit details
    Browse the repository at this point in the history

  2. limit solver_core methods to those needed by goal2sat 

    And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.

I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
    @jameysharp
    jameysharp committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    52432c1 View commit details
    Browse the repository at this point in the history