From f1559c05eb317a591bb18a832d0e87078d85218b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Apr 2022 12:41:40 -0500 Subject: [PATCH] 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. --- src/expr/node_manager_template.cpp | 9 ++++++++ src/expr/node_manager_template.h | 3 +++ src/printer/smt2/smt2_printer.cpp | 10 ++++++++- src/proof/lfsc/lfsc_node_converter.cpp | 30 ++++++++++++++++++-------- src/proof/lfsc/lfsc_node_converter.h | 13 ++++++++--- src/proof/lfsc/lfsc_printer.cpp | 9 ++------ src/proof/proof_node_to_sexpr.cpp | 5 +++-- src/theory/builtin/kinds | 2 ++ 8 files changed, 59 insertions(+), 22 deletions(-) diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 9a5d575b2..01f52924f 100644 --- 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::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 2d384f0d5..6741e43ad 100644 --- 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 f8f3af1b5..c85f2769e 100644 --- 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 c56aae9b9..54392392c 100644 --- 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 key(k, tn, name); std::map, 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 8a1add912..fe62e87ba 100644 --- 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 d412b8330..13ed67d04 100644 --- 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 fa4469618..fb9d25311 100644 --- 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 37f030f42..fafeb6e2f 100644 --- 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 -- 2.30.2