Implement printSolution option for all tasks

nimec01 commented 8 months ago

This adds the option to display solutions for each task.

nimec01 commented 8 months ago

I know there are still some lines that are too long. All of these are related to the SynTreeConfig and should probably be addressed in #79.

jvoigtlaender commented 8 months ago

In IllegalFormulas.hs, completeGrade now shows the toList (serialsOfWrong inst) irrespective of whether the student already had a correct answer. The idea was to do the feedback as follows:

If the student didn't have a correct answer, they are told that they their answer was wrong.
If the student didn't have a correct answer and printSolution was set, they are shown the toList (serialsOfWrong inst) bit.
If printSolution was set, they are shown the correct syntax trees.

jvoigtlaender commented 7 months ago

Apart from (or actually, after) resolving the merge conflicts here, I'd still like to have a look at example feedback for the following two task types as arising from the changes in this PR:

Resolution
Step

Can you post some console output here for those with correct and with incorrect input?

nimec01 commented 7 months ago

Ignore the typo in the latest commit...

Here are some outputs with printSolution = True:

Feedback for the `Resolve` task:

Correct answer

Consider the following formula in cnf:>>>> <¬D ∧ (¬A ∨ D) ∧ (A ∨ D)> <<<<

Use the resolution technique on this formula to derive the empty clause.
Provide the solution as a list of triples with this structure: (first clause, second clause, resolvent).
You can use any of the following notations:
>>>>Negation: <-, ~, not> <<<<

>>>>Or: <\/, or> <<<<

>>>>Empty clause: <{ }> <<<<

You can optionally replace clauses with numbers.
Clauses in the starting formula are already numbered by their order. first clause = 1, second clause = 2, ...).
Newly resolved clauses can be associated with a number by attaching '= NUMBER' behind them.
>>>>A valid solution could look like this:  <[(1, 2, {A, not B} = 5), (4, 5, { })]> <<<<

Just ()
[(1,2,{~A} = 4),(1,3,{A} = 5),(4,5,{})]
---- Input ----
[Res {trip = (Right 1,Right 2,(¬A,Just 4))},Res {trip = (Right 1,Right 3,(A,Just 5))},Res {trip = (Right 4,Right 5,({ },Nothing))}]
---- Partial ----
All steps use valid indices?
>>>> <Yes.> <<<<

No index is in duplicate use?
>>>> <Yes.> <<<<

All steps use valid indices?
>>>> <Yes.> <<<<

No index is in duplicate use?
>>>> <Yes.> <<<<

All steps use valid indices?
>>>> <Yes.> <<<<

No index is in duplicate use?        
>>>> <Yes.> <<<<

Used literals are present in formula?
>>>> <Yes.> <<<<

All steps are valid?
>>>> <Yes.> <<<<

The last step derives the empty clause?
>>>> <Yes.> <<<<

Just ()
---- Complete ----
Just ()

Wrong answer

Consider the following formula in cnf:>>>> <¬C ∧ (¬B ∨ C) ∧ (B ∨ C)> <<<<

Use the resolution technique on this formula to derive the empty clause.
Provide the solution as a list of triples with this structure: (first clause, second clause, resolvent).
You can use any of the following notations:
>>>>Negation: <-, ~, not> <<<<

>>>>Or: <\/, or> <<<<

>>>>Empty clause: <{ }> <<<<

You can optionally replace clauses with numbers.
Clauses in the starting formula are already numbered by their order. first clause = 1, second clause = 2, ...).
Newly resolved clauses can be associated with a number by attaching '= NUMBER' behind them.
>>>>A valid solution could look like this:  <[(1, 2, {A, not B} = 5), (4, 5, { })]> <<<<

Just ()
[]
---- Input ----
[]
---- Partial ----
Used literals are present in formula?
>>>> <Yes.> <<<<

All steps are valid?
>>>> <Yes.> <<<<

The last step derives the empty clause?
>>>> <No.> <<<<

Nothing
---- Complete ----
>>>>The Empty clause was not derived correctly.>>>>A possible solution for this task is:
 <["(1, 3, B = 4)","(4, 2, C = 5)","(1, 5, { })"]> <<<<
<<<<
Nothing

I just found out that there is a difference between the syntax used in the "possible solution" and the actual desired input. I will adapt it to use the input syntax.

Feedback for the `Step` task:

Correct answer

Consider the two following clauses:>>>> <A ∨ C ∨ D> <<<<
>>>> <A ∨ B ∨ ¬D> <<<<

Resolve the clauses and give the resulting resolvent.
Provide the literal (in positive or negative form) used for the step and the resolvent in the following tuple form: (literal, resolvent).
You can use any of the following notations:
>>>>Negation: <-, ~, not> <<<<

>>>>Or: <\/, or> <<<<

>>>>A valid solution could look like this:  <(A, not B or C)> <<<<

Just ()
(D, A or B or C)
---- Input ----
(D, A ∨ B ∨ C)
---- Partial ----
The solution is not empty?
>>>> <Yes.> <<<<

The chosen literal is contained in any of the clauses?
>>>> <Yes.> <<<<

Resolvent contains only known literals?
>>>> <Yes.> <<<<

Just ()
---- Complete ----
Just ()

Wrong answer

Consider the two following clauses:>>>> <¬B ∨ ¬C ∨ D> <<<<
>>>> <¬A ∨ B ∨ D> <<<<

Resolve the clauses and give the resulting resolvent.
Provide the literal (in positive or negative form) used for the step and the resolvent in the following tuple form: (literal, resolvent).
You can use any of the following notations:
>>>>Negation: <-, ~, not> <<<<

>>>>Or: <\/, or> <<<<

>>>>A valid solution could look like this:  <(A, not B or C)> <<<<

Just ()
(D,A or B)
---- Input ----
(D, A ∨ B)
---- Partial ----
The solution is not empty?
>>>> <Yes.> <<<<

The chosen literal is contained in any of the clauses?
>>>> <Yes.> <<<<

Resolvent contains only known literals?
>>>> <No.> <<<<

>>>>The resolvent contains unknown literals. These literals are incorrect: -  A

<<<<
Nothing
---- Complete ----
>>>>This literal cannot be used for a resolution step!>>>>A possible solution for this task is:
 <(¬B, ¬A ∨ ¬C ∨ D)> <<<<
<<<<
Nothing

fmidue / logic-tasks