Now the giving of maxpt when no errors are found applies to singletasks and...

Now the giving of maxpt when no errors are found applies to singletasks and configured inductioncases instead of only to the whole proof

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>