Use raw symbols in proofs (#8550)

This ensures we don't quote symbols that should not be quoted, fixing two issues:
(1) Proofs in the internal calculus don't convert `:args` to `|:args|`.
(2) LFSC identifiers for terms are not quoted based on SMT-LIB restrictions.

Work towards https://github.com/cvc5/cvc5-projects/issues/466, quoted TypeNode names still need to be addressed.

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 9a5d575b2fa007ae1273b7c05e2e337f4079aaeb..01f52924f54fbfd84df8375e4cd35a9bfae3a3a8 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -1097,6 +1097,15 @@ Node NodeManager::mkInstConstant(const TypeNode& type)
   return n;
 }
 
+Node NodeManager::mkRawSymbol(const std::string& name, const TypeNode& type)
+{
+  Node n = NodeBuilder(this, kind::RAW_SYMBOL);
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  setAttribute(n, expr::VarNameAttr(), name);
+  return n;
+}
+
 Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k)
 {
   std::map<TypeNode, Node>::iterator it = d_unique_vars[k].find(type);

diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h
index 2d384f0d539c4aadff33aeb58dfd744f8d687e38..6741e43ad18858349975cf63462b705f9f0af6b2 100644 (file)
--- a/src/expr/node_manager_template.h
+++ b/src/expr/node_manager_template.h
@@ -652,6 +652,9 @@ class NodeManager
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
 
+  /** Create a raw symbol with the given type. */
+  Node mkRawSymbol(const std::string& name, const TypeNode& type);
+
   /** Make a new uninterpreted sort value with the given type. */
   Node mkUninterpretedSortValue(const TypeNode& type);
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f8f3af1b54822a70cd5563f9c1c28e4676a7bebf..c85f2769e9ffa5ff1b6b4fe9071ec6558b042648 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -553,7 +553,15 @@ void Smt2Printer::toStream(std::ostream& out,
     string s;
     if (n.getAttribute(expr::VarNameAttr(), s))
     {
-      out << cvc5::internal::quoteSymbol(s);
+      if (n.getKind() == kind::RAW_SYMBOL)
+      {
+        // raw symbols are never quoted
+        out << s;
+      }
+      else
+      {
+        out << cvc5::internal::quoteSymbol(s);
+      }
     }
     else
     {

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index c56aae9b91c2ee0f891f91b04c023ab2d9540e4f..54392392ced32a5b48abc172f27ba024d53a6e26 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -101,9 +101,9 @@ Node LfscNodeConverter::postConvert(Node n)
       << "postConvert " << n << " " << k << std::endl;
   if (k == BOUND_VARIABLE)
   {
-    // ignore internally generated symbols
     if (d_symbols.find(n) != d_symbols.end())
     {
+      // ignore internally generated symbols
       return n;
     }
     // bound variable v is (bvar x T)
@@ -114,6 +114,11 @@ Node LfscNodeConverter::postConvert(Node n)
     Node bvarOp = getSymbolInternal(k, ftype, "bvar");
     return nm->mkNode(APPLY_UF, bvarOp, x, tc);
   }
+  else if (k == RAW_SYMBOL)
+  {
+    // ignore internally generated symbols
+    return n;
+  }
   else if (k == SKOLEM || k == BOOLEAN_TERM_VARIABLE)
   {
     // constructors/selectors are represented by skolems, which are defined
@@ -566,7 +571,7 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
       {
         std::stringstream sss;
         sss << LfscNodeConverter::getNameForUserName(ss.str());
-        tnn = getSymbolInternal(k, d_sortType, sss.str());
+        tnn = getSymbolInternal(k, d_sortType, sss.str(), false);
         cur = nm->mkSort(sss.str());
       }
       else
@@ -603,7 +608,7 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
       TypeNode ftype = nm->mkFunctionType(types, d_sortType);
       std::string name;
       tn.getAttribute(expr::VarNameAttr(), name);
-      op = getSymbolInternal(k, ftype, name);
+      op = getSymbolInternal(k, ftype, name, false);
     }
     else
     {
@@ -767,21 +772,28 @@ Node LfscNodeConverter::typeAsNode(TypeNode tni) const
   return it->second;
 }
 
-Node LfscNodeConverter::mkInternalSymbol(const std::string& name, TypeNode tn)
+Node LfscNodeConverter::mkInternalSymbol(const std::string& name,
+                                         TypeNode tn,
+                                         bool useRawSym)
 {
-  Node sym = NodeManager::currentNM()->mkBoundVar(name, tn);
+  // use raw symbol so that it is never quoted
+  NodeManager* nm = NodeManager::currentNM();
+  Node sym = useRawSym ? nm->mkRawSymbol(name, tn) : nm->mkBoundVar(name, tn);
   d_symbols.insert(sym);
   return sym;
 }
 
-Node LfscNodeConverter::getSymbolInternalFor(Node n, const std::string& name)
+Node LfscNodeConverter::getSymbolInternalFor(Node n,
+                                             const std::string& name,
+                                             bool useRawSym)
 {
-  return getSymbolInternal(n.getKind(), n.getType(), name);
+  return getSymbolInternal(n.getKind(), n.getType(), name, useRawSym);
 }
 
 Node LfscNodeConverter::getSymbolInternal(Kind k,
                                           TypeNode tn,
-                                          const std::string& name)
+                                          const std::string& name,
+                                          bool useRawSym)
 {
   std::tuple<Kind, TypeNode, std::string> key(k, tn, name);
   std::map<std::tuple<Kind, TypeNode, std::string>, Node>::iterator it =
@@ -790,7 +802,7 @@ Node LfscNodeConverter::getSymbolInternal(Kind k,
   {
     return it->second;
   }
-  Node sym = mkInternalSymbol(name, tn);
+  Node sym = mkInternalSymbol(name, tn, useRawSym);
   d_symbolToBuiltinKind[sym] = k;
   d_symbolsMap[key] = sym;
   return sym;

diff --git a/src/proof/lfsc/lfsc_node_converter.h b/src/proof/lfsc/lfsc_node_converter.h
index 8a1add912e6b0d927e4215aa1bb35f0483a96c7e..fe62e87ba8f534d601d03d83b90394a9248b4412 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.h
+++ b/src/proof/lfsc/lfsc_node_converter.h
@@ -97,7 +97,9 @@ class LfscNodeConverter : public NodeConverter
    * has a distinguished status so that it is *not* printed as (bvar ...). The
    * returned variable is always fresh.
    */
-  Node mkInternalSymbol(const std::string& name, TypeNode tn);
+  Node mkInternalSymbol(const std::string& name,
+                        TypeNode tn,
+                        bool useRawSym = true);
   /**
    * Get builtin kind for internal symbol op
    */
@@ -134,14 +136,19 @@ class LfscNodeConverter : public NodeConverter
    * Get symbol for term, a special case of the method below for the type and
    * kind of n.
    */
-  Node getSymbolInternalFor(Node n, const std::string& name);
+  Node getSymbolInternalFor(Node n,
+                            const std::string& name,
+                            bool useRawSym = true);
   /**
    * Get symbol internal, (k,tn,name) are for caching, name is the name. This
    * method returns a fresh symbol of the given name and type. It is frequently
    * used when the type of a native operator does not match the type of the
    * LFSC operator.
    */
-  Node getSymbolInternal(Kind k, TypeNode tn, const std::string& name);
+  Node getSymbolInternal(Kind k,
+                         TypeNode tn,
+                         const std::string& name,
+                         bool useRawSym = true);
   /**
    * Get character vector, add internal vector of characters for c.
    */

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index d412b8330f5ecba218128ee50292af7704284146..13ed67d046a2001a54e0f24ba0508335e9d5b748 100644 (file)
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -97,12 +97,7 @@ void LfscPrinter::print(std::ostream& out,
     {
       const DTypeConstructor& cons = dt[i];
       std::string cname = d_tproc.getNameForUserNameOf(cons.getConstructor());
-      // for now, must print as node to ensure same policy for printing
-      // variable names. For instance, this means that cvc.X is printed as
-      // LFSC identifier |cvc.X| if X contains symbols legal in LFSC but not
-      // SMT-LIB. (cvc5-projects/issues/466) We should disable printing quote
-      // escapes in the smt2 printing of LFSC converted terms.
-      Node cc = nm->mkBoundVar(cname, stc);
+      Node cc = nm->mkRawSymbol(cname, stc);
       // print constructor/tester
       preamble << "(declare " << cc << " term)" << std::endl;
       for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
@@ -110,7 +105,7 @@ void LfscPrinter::print(std::ostream& out,
         const DTypeSelector& arg = cons[j];
         // print selector
         std::string sname = d_tproc.getNameForUserNameOf(arg.getSelector());
-        Node sc = nm->mkBoundVar(sname, stc);
+        Node sc = nm->mkRawSymbol(sname, stc);
         preamble << "(declare " << sc << " term)" << std::endl;
       }
     }

diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp
index fa4469618a9a45cd46b7f5b4826b7547e554bfd9..fb9d25311393b0f0d3e308cb4cf32df1563aabf1 100644 (file)
--- a/src/proof/proof_node_to_sexpr.cpp
+++ b/src/proof/proof_node_to_sexpr.cpp
@@ -30,8 +30,9 @@ namespace cvc5::internal {
 ProofNodeToSExpr::ProofNodeToSExpr()
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType());
-  d_argsMarker = nm->mkBoundVar(":args", nm->sExprType());
+  // use raw symbols so that `:args` is not converted to `|:args|`
+  d_conclusionMarker = nm->mkRawSymbol(":conclusion", nm->sExprType());
+  d_argsMarker = nm->mkRawSymbol(":args", nm->sExprType());
 }
 
 Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 37f030f4247a88f2db931b79e2eceeba5e350ec2..fafeb6e2f6abb59d80cd7cbb1925885d2df40264 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -310,4 +310,6 @@ typerule DISTINCT ::cvc5::internal::theory::builtin::DistinctTypeRule
 typerule SEXPR ::cvc5::internal::theory::builtin::SExprTypeRule
 typerule WITNESS ::cvc5::internal::theory::builtin::WitnessTypeRule
 
+variable RAW_SYMBOL "a variable that is not quoted in the smt2 printer (internal only)"
+
 endtheory