limo1996 / SAT-Solver

Parallel SAT Solver
8 stars 1 forks source link

Move encoding and parsing of variables from worker to CNF #2

Closed limo1996 closed 6 years ago

limo1996 commented 6 years ago

Jan, I think it would be better to move encoding and parsing of formula to CNF class so I can reuse it in Master class (I need to parse final formula and print it). I will push in few minutes data class named State that basically hold array of unsigned ints and its size + getter and setter.

Your methods can looks like: State CNF::encode(); //cnf will encode itself to State object

CNF cnf = new CNF(State state); // cnf will parse itself from State object // ---- or ----- CNF cnf = new CNF(); cnf.parse(State state);

What do you think about that?

ebhardjan commented 6 years ago

Sounds good. I think "Model" would be a better name (since that's what it's called in this context) but otherwise I agree.

limo1996 commented 6 years ago

Yeah. I will rename it to model and then you can merge branches and use the class

limo1996 commented 6 years ago

Not necessary... Partially done...