Option für zusätzliche Hinweise und Feedback bzgl. semantisch äquivalenter Lösungen bei TreeToFormula

[nimec01]

In Bezug auf #60 wird in Abhängigkeit von allowArrowOperators der Aufgabentext angepasst und überprüft, ob eine zur Lösung semantisch äquivalente Formel abgegeben wurde. Im letzteren Fall wird der Nutzer darauf aufmerksam gemacht und der Lösungsversuch nicht akzeptiert. Folgendes könnte man nochmal hinterfragen:

• Soll der Lösungsversuch trotzdem akzeptiert werden (der Nutzer wurde ja schließlich angewiesen, keine semantischen Umformungen anzuwenden)?
• Soll anstatt allowArrowOperators eine eigene Variable bestimmen, ob die semantische Äquivalenz überprüft wird (ich würde die dann aber wahrscheinlich nicht in SynTreeConfig packen, da es schließlich nur von TreeToFormula verwendet wird)?

[jvoigtlaender]

Vermutlich sollte (abweichend von meinem ursprünglichen Vorschlag in #60) das Ganze tatsächlich unabhängig von allowArrowOperators passieren.

Lösungsversuche mit semantisch äquivalenten Formeln sollten wohl tatsächlich erstmal akzeptiert (und dann später als falsch deklariert) werden. Eventuell lassen sich noch Teilpunkte geben, das ist aber eine separate Frage. Bereits bei der Eingabeüberprüfung diesen semantischen Test zu machen, und zu "leaken", ist vielleicht nicht so geschickt.

[jvoigtlaender]

Als Kontext, folgender extraText wurde im aktuellen Semester letztlich verwendet:

extraText = Just "Hinweise: Es muss die exakte Formel des Syntaxbaums angegeben werden. Andere, selbst zu dieser Formel semantisch äquivalente Formeln sind keine korrekte Lösung! Auch dürfen Sie bei dieser Aufgabe nicht Assoziativität verwenden, um Klammern einzusparen."

[nimec01]

Ich habe es entsprechend geändert.

[jvoigtlaender]

Hmm, allowSemanticallyEquivalentSolutions ist vielleicht aus Lehrendensicht (andere Dozenten, die den Code nicht kennen) verwirrend benannt. Es klingt irgendwie so, also würde man durch Setzen von allowSemanticallyEquivalentSolutions = True dafür sorgen, dass die Studierenden auch zum gegebenen Syntaxbaum äquivalente Formeln eingeben dürfen (und dies dann als richtig gilt). So ist es ja aber nicht. Sondern die Option hat nur Auswirkungen auf angezeigte Hinweise in der Aufgabenstellung und auf den Feedback-Text. Sie "erlaubt" nicht wirklich äquivalente Formeln im Sinne, dass diese auch als richtig akzeptiert würden.

[nimec01]

Ich habe die Option umbenannt. Passt onlyAcceptExactFormula besser?

[jvoigtlaender]

Ich habe die Option nochmal umbenannt, und das Feedback angepasst.

[jvoigtlaender]

@owestphal, can you review the accumulated changes here, both concerning the new hints and feedback, and concerning the use of minisat for equivalence checking?

[jvoigtlaender]

There is another aspect in play here, that I think will require some more "major" refactoring.

The SynTreeConfig type now has the fields extraText and extraHintsOnSemanticEquivalence. That is fine when SynTreeConfig is being used as "its own task type" (namely, for TreeToFormula), but actually SynTreeConfig also appears as subpart of other task types' config types. For example, in LegalPropositionConfig. There, it doesn't make sense to specify extraHintsOnSemanticEquivalence. And having extraText via SynTreeConfig there is also quite strange, since any extra text to give there from the lecturer'S perspective would more reasonably be associated with LegalProposition (as a task type), rather than with SynTree (which only happens to be part of the specification of LegalProposition).

This all comes down to a previously reasonable - but now not so much anymore - double role of SynTreeConfig. It would probably be better to separate these roles, by introducing a dedicated config type for TreeToFormula, and sharing SynTreeConfig (minus the extra fields) between TreeToFormulaConfig and LegalPropositionConfig etc.

[owestphal]

I simplified equivalence checking by checking for validity instead of comparing (and sorting) satisfying assignments. And I moved some tests around to better reflect what parts of the logic are actually tested. Other than that this looks fine to me.