[proofs] [alethe] Print valid arguments in hole steps (cvc5#11287)

Before we were printing an undeclared identifier for an unknown rule or trust id. This commit also updates the version of Carcara, which was not parsing arguments of the `hole` rule before, which could lead to issues if a shared term has a name introduced to it in the arguments of a `hole` rule.
abdoo8080 · Oct 16, 2024 · ff5c97b · ff5c97b
1 parent 8c74b38
commit ff5c97b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 5 deletions.
diff --git a/contrib/get-carcara-checker b/contrib/get-carcara-checker
@@ -24,7 +24,7 @@ CARCARA_DIR="$BASE_DIR/carcara"
 mkdir -p $CARCARA_DIR
 
 # download and unpack Carcara
-CARCARA_VERSION="d434d5caa0f2dad65aaa9ac9c20817af53004088"
+CARCARA_VERSION="6eb3cd069773b0f0bec4c312e30b2bf921681e74"
 download "https://github.com/hanielb/carcara/archive/$CARCARA_VERSION.tar.gz" $BASE_DIR/tmp/carcara.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/carcara.tgz -C $CARCARA_DIR
 rm $BASE_DIR/tmp/carcara.tgz

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -513,11 +513,15 @@ bool AletheProofPostprocessCallback::update(Node res,
           }
         }
       }
+      std::stringstream ss;
+      ss << "\"" << args[0] << "\"";
+      std::vector<Node> newArgs{nm->mkRawSymbol(ss.str(), nm->sExprType())};
+      newArgs.insert(newArgs.end(), args.begin() + 1, args.end());
       return addAletheStep(AletheRule::HOLE,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           args,
+                           newArgs,
                            *cdp);
     }
     // ======== Resolution and N-ary Resolution
@@ -2120,9 +2124,8 @@ bool AletheProofPostprocessCallback::update(Node res,
           << "... rule not translated yet " << id << " / " << res << " "
           << children << " " << args << std::endl;
       std::stringstream ss;
-      ss << id;
-      Node newVar = nm->mkBoundVar(ss.str(), nm->sExprType());
-      std::vector<Node> newArgs{newVar};
+      ss << "\"" << id << "\"";
+      std::vector<Node> newArgs{nm->mkRawSymbol(ss.str(), nm->sExprType())};
       newArgs.insert(newArgs.end(), args.begin(), args.end());
       return addAletheStep(AletheRule::HOLE,
                            res,