fixed cases where Alpha-inferences were left out

uuverifiers · Jun 24, 2022 · a8b8e52 · a8b8e52
1 parent 8746d88
commit a8b8e52
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 11 deletions.
diff --git a/src/ap/proof/ModelSearchProver.scala b/src/ap/proof/ModelSearchProver.scala
@@ -445,7 +445,8 @@ class ModelSearchProver(defaultSettings : GoalSettings) {
                 ((lemmaBase allKnownWitness cert.assumedFormulas) match {
                     case Some(f) => {
                       throw new Exception(
-                        "unasserted, but assumed formula: " + f)
+                        "unasserted, but assumed formula: " + f +
+                          " in certificate: " + cert)
                       false
                     }
                     case None =>

diff --git a/src/ap/proof/certificates/BranchInferenceCollection.scala b/src/ap/proof/certificates/BranchInferenceCollection.scala
@@ -3,7 +3,7 @@
  * arithmetic with uninterpreted predicates.
  * <http://www.philipp.ruemmer.org/princess.shtml>
  *
- * Copyright (C) 2009-2019 Philipp Ruemmer <[email protected]>
+ * Copyright (C) 2009-2022 Philipp Ruemmer <[email protected]>
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -190,6 +190,19 @@ class BranchInferenceCollection private (val inferences : List[BranchInference])
        yield i).toList
     BranchInferenceCollection(defaultInfs ::: inf :: inferences)
   }
+
+  def addWithDefaultInfs(infs : Seq[BranchInference])
+                              : BranchInferenceCollection = {
+    var allInfs = inferences
+    for (inf <- infs) {
+      allInfs = inf :: allInfs
+      for (f <- inf.providedFormulas;
+           i <- BranchInferenceCollection.genDefaultInferences(f)) {
+        allInfs = i :: allInfs
+      }
+    }
+    BranchInferenceCollection(allInfs)
+  }
 
   def getCertificate(child : Certificate, order : TermOrder) : Certificate =
     BranchInferenceCollection.getCertificateHelp(inferences, child, order)

diff --git a/src/ap/proof/theoryPlugins/Plugin.scala b/src/ap/proof/theoryPlugins/Plugin.scala
@@ -466,9 +466,8 @@ abstract class PluginTask(plugin : TheoryProcedure) extends Task {
             val Seq((axiomCase, rest)) =
               cases
             val newInferences =
-              branchInferences ++
-              axiomInferences(CertFormula(axiomCase),
-                              predAssumptions, theory)
+              branchInferences addWithDefaultInfs axiomInferences(
+                CertFormula(axiomCase), predAssumptions, theory)
             handleActionsRec(rest.toList,
                              AddFormula(!axiomCase) :: contActions,
                              goal,
@@ -484,8 +483,8 @@ abstract class PluginTask(plugin : TheoryProcedure) extends Task {
             val negA =
               !assumption
             val newInferences =
-              branchInferences ++
-              axiomInferences(negA, predAssumptions, theory)
+              branchInferences addWithDefaultInfs axiomInferences(
+                negA, predAssumptions, theory)
             applyActions(AddFormula(assumption.toConj) :: contActions,
                          goal,
                          newInferences,
@@ -659,21 +658,23 @@ abstract class PluginTask(plugin : TheoryProcedure) extends Task {
         implicit val order = goal.order
         import TerForConvenience._
 
+        val certCutFormula = CertFormula(cutFormula)
+
         val leftSubtree =
           handleActionsRec(left.toList,
                            AddFormula(!cutFormula) :: contActions,
                            goal,
-                           goal.startNewInferenceCollection,
+                           goal.startNewInferenceCollectionCert(
+                             List(certCutFormula)),
                            ptf)
         val rightSubtree =
           handleActionsRec(right.toList,
                            AddFormula(cutFormula) :: contActions,
                            goal,
-                           goal.startNewInferenceCollection,
+                           goal.startNewInferenceCollectionCert(
+                             List(!certCutFormula)),
                            ptf)
 
-        val certCutFormula = CertFormula(cutFormula)
-
         // certificate constructor, to be applied once all sub-goals have
         // been closed
         def comb(certs : Seq[Certificate]) : Certificate =