Temporary revert back to no quotationmarks in arguments of rewrite ru…

…les for easier development in Isabelle
HanielB · Feb 16, 2024 · c38a5db · c38a5db
1 parent c6e809f
commit c38a5db
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -396,7 +396,8 @@ bool AletheProofPostprocessCallback::update(Node res,
       if (rewriter::getDslProofRule(args[0], di))
       {
         std::stringstream ss;
-        ss << "\"" << di << "\"";
+        //ss << "\"" << di << "\"";
+        ss << di;
         rule = nm->mkRawSymbol(ss.str(), nm->sExprType());
       }
       else
@@ -437,7 +438,8 @@ bool AletheProofPostprocessCallback::update(Node res,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {nm->mkRawSymbol("\"arith-poly-norm\"", nm->sExprType())},
+                           {nm->mkRawSymbol("arith-poly-norm", nm->sExprType())},
+                           //{nm->mkRawSymbol("\"arith-poly-norm\"", nm->sExprType())},
                            *cdp);
     }
     case ProofRule::EVALUATE:
@@ -446,7 +448,8 @@ bool AletheProofPostprocessCallback::update(Node res,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {nm->mkRawSymbol("\"evaluate\"", nm->sExprType())},
+                           {nm->mkRawSymbol("evaluate", nm->sExprType())},
+                           //{nm->mkRawSymbol("\"evaluate\"", nm->sExprType())},
                            *cdp);
     }
     case ProofRule::TRUST_THEORY_REWRITE: