From a1beb1740386f87e7efa3c26df771fb90501028e Mon Sep 17 00:00:00 2001
From: Edward <edward.sabinus@informatik.uni-halle.de>
Date: Wed, 6 Dec 2023 17:17:15 +0100
Subject: [PATCH] Now the giving of maxpt when no errors are found applies to
singletasks and configured inductioncases instead of only to the whole proof
---
.../Bewertung/Bewerter.cs | 60 +++++++++++++------
1 file changed, 43 insertions(+), 17 deletions(-)
diff --git a/BewerterStrukturellerInduktion/Bewertung/Bewerter.cs b/BewerterStrukturellerInduktion/Bewertung/Bewerter.cs
index ea6ec24..1760d98 100644
--- a/BewerterStrukturellerInduktion/Bewertung/Bewerter.cs
+++ b/BewerterStrukturellerInduktion/Bewertung/Bewerter.cs
@@ -13,27 +13,19 @@ namespace Bewertung {
public override void Bewerte()
{
- initializeBewertung();
- bool NoErrors()
- {
- Ausgabeverwaltung.Ausgabeverwalter aus = new Ausgabeverwaltung.Ausgabeverwalter();
- return aus.printAllErrors(con) == aus.NoErrors();
- }
- if (NoErrors())
- { // if NoErrors, don't calculate assessment, instead give maxPt.
- // Cause: due to wrong configuration of minSteps calculation of assessment could give less than maxPt for a correct proof.
- foreach(AssessmentObject aO in bewertung)
- {
+ initializeBewertung();
+ foreach(AssessmentObject aO in bewertung)
+ {
+ if (aO.usefulLemmata.Count == 0) continue;
+ if (NoErrors(aO))
+ { // if NoErrors, don't calculate assessment, instead give maxPt.
+ // Cause: due to wrong configuration of minSteps calculation of assessment could give less than maxPt for a correct proof.
aO.assessment = aO.task.config.MaxPt();
- if (aO.task.config is InductionConfig indConf)
+ if (aO.task.config is InductionConfig)
foreach (InductionPartAssessment ipa in aO.confIndAssessment)
ipa.Assessment = ipa.maxPt;
+ continue;
}
- return;
- }
- foreach(AssessmentObject aO in bewertung)
- {
- if (aO.usefulLemmata.Count == 0) continue;
List<Lemma> usefulLemmata = new List<Lemma>(aO.usefulLemmata);
Lemma mainLemma = usefulLemmata[0];
if (aO.task.config is InductionConfig indConf && mainLemma.proof is Induction ind) // Assessment with induction config ( is 0.0 if mainLemma.proof is Transformation)
@@ -46,6 +38,13 @@ namespace Bewertung {
aO.findIPA("IH").Assessment = indConf.indHypConfig.maxPt * Bewertung(ind.indHyps);
foreach (InductionCase ic in ind.indCases)
{
+ if (NoErrors(ic))
+ {
+ // if NoErrors, don't calculate assessment, instead give maxPt.
+ // Cause: due to wrong configuration of minSteps calculation of assessment could give less than maxPt for a correct proof.
+ aO.findIPA("Fall " + ic.Constructor.name).Assessment = indConf.GetIndCaseConfig(ic.Constructor).config.MaxPt();
+ continue;
+ }
bool err33 = false;
foreach (Error err in ic.errors)
if (err.errorCode == 33) { err33 = true; break; } // invalid ind cases are not assessed
@@ -96,6 +95,33 @@ namespace Bewertung {
}
}
+ /// <summary>
+ /// Returns true if in aO are no errors
+ /// </summary>
+ /// <param name="aO"></param>
+ /// <returns></returns>
+ private bool NoErrors(AssessmentObject aO)
+ {
+ if (aO.usefulLemmata.Count == 0) return false;
+ Ausgabeverwaltung.Ausgabeverwalter aus = new Ausgabeverwaltung.Ausgabeverwalter();
+ Container aOcon = new Container();
+ aOcon.Proof = new Proof(aO.usefulLemmata[0].proof, aO.usefulLemmata);
+ return aus.printAllErrors(aOcon) == aus.NoErrors();
+ }
+
+ /// <summary>
+ /// Returns true if in ic are no errors
+ /// </summary>
+ /// <param name="ic"></param>
+ /// <returns></returns>
+ bool NoErrors(InductionCase ic)
+ {
+ Ausgabeverwaltung.Ausgabeverwalter aus = new Ausgabeverwaltung.Ausgabeverwalter();
+ Container iccon = new Container();
+ iccon.Proof = new Proof(new Induction(ic.coords,ic.eq,ic.fixedVars,new Variable("",new Sort("")),new List<InductionCase>() { ic },new List<InductionHypothesis>()),new List<Lemma>());
+ return aus.printAllErrors(iccon) == aus.NoErrors();
+ }
+
/// <summary>
/// Abstract Assessment of one lemma.
/// </summary>
--
GitLab