fix issue with repeated subproof assumption and update disabled regre…

…ssions
HanielB · May 28, 2024 · f69492f · f69492f
1 parent b326b7c
commit f69492f
Show file tree

Hide file tree

Showing 8 changed files with 16 additions and 9 deletions.
diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp
@@ -241,6 +241,7 @@ void AletheProofPrinter::printInternal(
     std::string subproofPrefix = prefix + "t" + std::to_string(id) + ".";
     std::unordered_map<Node, std::string> subproofAssumptionsMap{assumptionsMap.begin(), assumptionsMap.end()};
     std::unordered_map<std::shared_ptr<ProofNode>, std::string> subproofPfMap{pfMap.begin(), pfMap.end()};
+    std::vector<std::string> dischargeIds;
     // since the subproof shape relies on having at least one step inside it, if
     // the step relative to children[0] is already pfMap, we remove it from
     // subproofPfMap
@@ -263,6 +264,7 @@ void AletheProofPrinter::printInternal(
         printTerm(out, args[i]);
         out << ")\n";
         subproofAssumptionsMap[args[i]] = assumptionId;
+        dischargeIds.push_back(assumptionId);
       }
     }
     else
@@ -298,8 +300,7 @@ void AletheProofPrinter::printInternal(
       out << " :discharge (";
       for (size_t i = 3, size = args.size(); i < size; ++i)
       {
-        out << subproofAssumptionsMap[args[i]]
-            << (i < args.size() - 1 ? " " : "");
+        out << dischargeIds[i - 3] << (i < args.size() - 1 ? " " : "");
       }
       out << ")";
     }

diff --git a/test/regress/cli/regress1/datatypes/dt-color-2.6.smt2 b/test/regress/cli/regress1/datatypes/dt-color-2.6.smt2
@@ -10,12 +10,7 @@
 (declare-fun d () Color)
 
 (assert (or (distinct a b c d)
-          (< (match a (
-                        (red 5)
-                        (green 3)
-                        (blue 2)
-                        )
-               ) 0)
+ (< (match a ((red 5) (green 3) (blue 2))) 0)
  (< (match b ((red 2) (x 1))) 0)
  ))
 

diff --git a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --ee-mode=distributed
 ; COMMAND-LINE: --ee-mode=central
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :fmf-bound true)

diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: unsat
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-sort e 0)
 (declare-sort p 0)

diff --git a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2
@@ -1,3 +1,5 @@
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort U 0)

diff --git a/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 b/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --quant-ind --conjecture-gen
 ; EXPECT: unsat
+; Instantiation with fresh constants not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic UFDTLIA)
 (set-info :status unsat)
 (declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero))

diff --git a/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 b/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --sygus-inst
 ; EXPECT: unsat
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-sort a 0)
 (declare-datatypes ((t 0)) (((L (s a)))))

diff --git a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2
@@ -1,4 +1,5 @@
-(set-logic ALL)
+;; Non-standard Datatypes syntax not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-datatypes ((D 0) (T@t 0)) (((err)) ((t (|v#t| U) (|l#t| Int)))))