Retire Tasks.LegalCNF.GenerateLegal.genCnf?

[jvoigtlaender]

... replacing it with Formula.Types.genCnf everywhere.

One impact would be that externalGenFormulas in

logic-tasks/src/Tasks/LegalCNF/Config.hs

Lines 27 to 32 in 6c75adc

	data LegalCNFConfig =
	LegalCNFConfig
	{
	cnfConfig :: CnfConfig
	, formulas :: Int
	, externalGenFormulas :: Int

would become superfluous as configuration option.

[owestphal]

Some quick statistics for both generators on 1000 Formulas generated from

CnfConfig {
  baseConf = BaseConfig {
    minClauseLength = 3,
    maxClauseLength = 7,
    usedLiterals = "ABCDEFG" }
  minClauseAmount = 3,
  maxClauseAmount = 9 }

The biggest difference is the generation of trivial clauses like, e.g. (A ∨ ¬B ∨ B ∨ F ∨ ¬G), by Tasks.LegalCNF.GenerateLegal.genCnf.

Formula.Types.genCnf

all literals (12620 in total):
 7.282% ¬E
 7.274% B
 7.195% G
 7.187% F
 7.147% C
 7.132% ¬C
 7.116% E
 7.108% A
 7.100% D
 7.100% ¬B
 7.100% ¬D
 7.092% ¬A
 7.084% ¬F
 7.084% ¬G

clause lengths (5935 in total):
20.61% 7
20.37% 6
19.88% 5
19.70% 4
19.44% 3

negative literals (6294 in total):
14.60% ¬E
14.30% ¬C
14.24% ¬B
14.24% ¬D
14.22% ¬A
14.20% ¬F
14.20% ¬G

number of clauses (1000 in total):
15.5% 3
14.7% 8
14.6% 4
14.6% 5
13.6% 7
13.6% 9
13.4% 6

positive literals (6326 in total):
14.51% B
14.35% G
14.34% F
14.26% C
14.20% E
14.18% A
14.16% D

trivial clauses (containing both X and not X) (5935 in total):
100.00% False

Tasks.LegalCNF.GenerateLegal.genCnf

all literals (12610 in total):
 7.264% ¬C
 7.224% ¬E
 7.216% B
 7.201% A
 7.177% ¬B
 7.161% ¬F
 7.153% C
 7.153% ¬D
 7.121% ¬A
 7.121% ¬G
 7.098% G
 7.066% F
 7.026% E
 7.018% D

clause lengths (5968 in total):
20.84% 7
20.12% 3
19.76% 6
19.69% 4
19.59% 5

negative literals (6333 in total):
14.46% ¬C
14.38% ¬E
14.29% ¬B
14.26% ¬F
14.24% ¬D
14.18% ¬A
14.18% ¬G

number of clauses (1000 in total):
15.6% 5
15.4% 4
15.1% 7
14.2% 6
13.7% 9
13.0% 3
13.0% 8

positive literals (6277 in total):
14.50% B
14.47% A
14.37% C
14.26% G
14.19% F
14.12% E
14.10% D

trivial clauses (containing both X and not X) (5968 in total):
62.78% True
37.22% False

[owestphal]

As a consequence of the changes from 6f7d1a0 we als have

Formula.Types.genCnf

usage of atomic propositions (1000 in total):
100.0% ABCDEFG

Tasks.LegalCNF.GenerateLegal.genCnf

usage of atomic propositions (1000 in total):
90.6% ABCDEFG
 1.4% ABCEFG
 1.3% ABCDFG
 1.3% BCDEFG
 1.1% ABCDEF
 0.9% ABDEFG
 0.9% ACDEFG
 0.6% ABCDEG
 0.2% ACDEG
 0.2% BDEFG
 0.1% ABCDF
 0.1% ABCDG
 0.1% ABCEF
 0.1% ABCEG
 0.1% ABCFG
 0.1% ABDEF
 0.1% ABDEG
 0.1% ABDFG
 0.1% ABEF
 0.1% ACDEF
 0.1% ACDFG
 0.1% ACEFG
 0.1% ADEFG
 0.1% BCDEG
 0.1% CDEFG

[jvoigtlaender]

I guess in all current uses of Tasks.LegalCNF.GenerateLegal.genCnf it's okay to not use all atomic propositions? Because it's just used in syntax tasks, where it doesn't matter much what is at the leaves, as long as it is "a letter"?