EdvardHolden / axiom_caption

1 stars 0 forks source link

Fix clausification merge #20

Closed EdvardHolden closed 2 years ago

EdvardHolden commented 2 years ago

This branch updates generate_problems.py to only clausify the generated problem after all formulae are collected. The previous behaviour where the problems were merged (even with renaming of Skolem functions) seemed questionable when running it by hand. Therefore, I changed the setup to collect the non-clausified formulae from SInE instead of appending a clausified version to the final problem.

Also multiple refactoring elements related to classification and processing of problems.