performance improvements (CNF printing and parsing)

ekmett / ersatz

A monad for interfacing with external SAT solvers

Other

62 stars 15 forks source link

performance improvements (CNF printing and parsing) #18

Closed jwaldmann closed 8 years ago

jwaldmann commented 8 years ago

Hi, I have noticed performance problems (issues #16 and #17) and made some improvements (example: from 40 seconds to 7 seconds)

Writing the CNF still feels sluggish - for large trivial formulas, minisat can (read and) solve much faster than Ersatz writes.

ekmett commented 8 years ago

I have no objection to merging this.

ion1 commented 8 years ago

Thanks for your work! Feel free to destroy Ersatz.Internal.Parser, it was just a fun little hack, but as its description says, it's an "inefficient parser with no support for error reporting".

jwaldmann commented 8 years ago

OK. I will look into this more alongside using Ersatz in some application, which will also give plenty of test cases. I might be slow to respond next week(s) because of other commitments (start of teaching term).