More general formulas for Pick, Fill and Decide

[nimec01]

First steps towards an implementation for #98

[nimec01]

I just stumbled upon the pickCnf option in PickConfig. What is its meaning? It's not getting used, apparently.

[jvoigtlaender]

I've looked into the distant past. There once was this code:

genPickExercise :: PickConfig -> IO (String,Either ([(Int,Cnf)],Table) ([(Int,Table)],Cnf))
genPickExercise
    PickConfig {cnfConfig = CnfConfig {clauseConf = ClauseConfig {..}, ..}, ..}
  = do
    first <- generate (getCnf usedLiterals)
    let satForm = convert first
    rest <- generate (vectorOf (amountOfOptions-1) (getWithSameLiterals first satForm))
    let cnfs = first : rest
    rightCnf <- generate (elements cnfs)
    if pickCnf
      then do
        let
          table = getTable rightCnf
          zippedCnfs = zip [1..] cnfs
          desc = exerciseDescPick2 zippedCnfs table
        pure (desc,Left (zippedCnfs,table))
      else do
        let
          tables = zip [1..] (map getTable cnfs)
          desc = exerciseDescPick tables rightCnf
        pure (desc,Right (tables,rightCnf))
  where
    getCnf :: [Char] -> Gen Cnf
    getCnf lits = genCnf (minClauseAmount, maxClauseAmount) (minClauseLength, maxClauseLength)
                     lits


    getWithSameLiterals :: Cnf -> Sat.Formula Char -> Gen Cnf
    getWithSameLiterals cnf sat = do
        let cnfLits = getLiterals cnf
        newCnf <- getCnf (map getC cnfLits)
        if getLiterals newCnf == cnfLits && Sat.satisfiable (sat Sat.:++: convert newCnf)
          then pure newCnf
          else getWithSameLiterals cnf sat








exerciseDescPick :: [(Int,Table)] -> Cnf -> String
exerciseDescPick tables cnf =
    "Betrachten Sie die folgende Formel in konjunktiver Normalform: \n\n" ++
    show cnf ++
    "\n Welche der folgenden Wahrheitstafeln passt zu der Formel?\n\n" ++
    showIndexedList tables ++
    "\nGeben Sie die richtige Tafel durch ihre Nummer an."






exerciseDescPick2 :: [(Int,Cnf)] -> Table -> String
exerciseDescPick2 cnfs table =
    "Betrachten Sie die folgende Wahrheitstafel: \n\n" ++
    show table ++
    "\n Welche der folgenden Formeln in konjunktiver Normalform passt zu der Wahrheitstafel?\n\n" ++
    showIndexedList cnfs ++
    "\nGeben Sie die richtige Tafel durch ihre Nummer an."

So it looks like at some point that parameter was used to decide whether to let the student choose one of three formulas for one given truth table, or one of three truth tables for one given formula.

Wheras by now only one of these modes is still supported, I guess.

[nimec01]

PickConfig definitely needs more constraints (probably in regard to whether amountOfOptions is achievable with a given minAmountOfUniqueAtoms).

Here are some problematic examples:

PickConfig {
  syntaxTreeConfig = SynTreeConfig {
    minNodes = 8, 
    maxNodes = 9, 
    minDepth = 4, 
    maxDepth = 4, 
    availableAtoms = "FGIKLSUVWXYZ", 
    minAmountOfUniqueAtoms = 2, 
    allowArrowOperators = False, 
    maxConsecutiveNegations = 2, 
    minUniqueBinOperators = 1}, 
  amountOfOptions = 5, 
  pickCnf = False, 
  printSolution = False, 
  extraText = Nothing
}

-- fails to fill these shapes with "FKV" such that the formulas are not semantically equivalent
[
  Binary And (Binary And (Not (Leaf ())) (Binary Or (Leaf ()) (Leaf ()))) (Leaf ()),
  Binary And (Not (Leaf ())) (Binary And (Not (Leaf ())) (Not (Leaf ()))),
  Binary And (Binary And (Not (Leaf ())) (Not (Leaf ()))) (Not (Leaf ())),
  Binary And (Binary And (Leaf ()) (Binary And (Leaf ()) (Leaf ()))) (Binary Or (Leaf ()) (Leaf ())),
  Binary Or (Not (Leaf ())) (Binary Or (Binary Or (Leaf ()) (Leaf ())) (Not (Leaf ())))
]

-- same here with "DZ"
PickConfig {
  syntaxTreeConfig = SynTreeConfig {
    minNodes = 6, 
    maxNodes = 12, 
    minDepth = 3, 
    maxDepth = 4, 
    availableAtoms = "ABDEFGJKRSTVXZ", 
    minAmountOfUniqueAtoms = 2, 
    allowArrowOperators = True, 
    maxConsecutiveNegations = 2, 
    minUniqueBinOperators = 1}, 
  amountOfOptions = 5, 
  pickCnf = False, 
  printSolution = False, 
  extraText = Nothing
}

[
  Binary And (Not (Not (Leaf ()))) (Binary And (Binary Equi (Leaf ()) (Leaf ())) (Not (Leaf ()))),
  Binary Or (Leaf ()) (Binary Impl (Not (Leaf ())) (Binary Or (Leaf ()) (Leaf ()))),
  Not (Binary Or (Binary And (Leaf ()) (Leaf ())) (Binary Or (Leaf ()) (Leaf ()))),
  Binary And (Leaf ()) (Not (Binary And (Leaf ()) (Leaf ()))),
  Binary Impl (Not (Leaf ())) (Not (Not (Leaf ())))
]

[nimec01]

I guess it would make sense to write a more efficient helper vectorOfUniqueBy :: Int -> (a -> a -> Bool) -> Gen a -> Gen [a] and use that here.

I could not really perceive any decrease in the duration, but there is no harm in implementing it anyway.

[nimec01]

Once one is at that, though, one might also wonder whether one shouldn't go the full way and offer three options to the user here:

• generate CNFs
• generate DNFs
• generate arbitrary formulas

I will probably just go ahead and implement it this way.

[nimec01]

This is not quite finished yet. I will have another look at it the next days.

[nimec01]

I would say this is good for now. The tests currently only work for syntax trees, as the tasks assume that the configurations are valid. This has to do with the usage of tryGen #106.

It might also be a good idea to refactor the structure of this repo a bit. The current structure creates a few scenarios leading into circular dependencies (this is why some functions are defined in LogicTasks.Util and not Util itself). But this should really be part of a separate pull request.

[jvoigtlaender]

This:

It might also be a good idea to refactor the structure of this repo a bit.

is already the subject of #27.

What currently holds this back is that there is another Bachelor thesis whose task types are waiting for being merged into this repo, and which still uses the old naming schemes/hierarchy. It seems that a refactoring/restructuring would be better applied after that stuff has arrived here.