From: Andrew Reynolds Date: Tue, 8 Mar 2022 18:29:06 +0000 (-0600) Subject: Fixes and additions to LFSC signature (#8205) X-Git-Tag: cvc5-1.0.0~303 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=beb261d1ea803818e0b33ab8f96d23f2495530a5;p=cvc5.git Fixes and additions to LFSC signature (#8205) Includes: Proper printing of various FP terms and constants. Distinguishing "variants" of overloaded symbols, in case a user declares 2 symbols with the same name. Miscellaneous fixes for printing terms. --- diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index da9689ab9..4e57abb37 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -345,8 +345,10 @@ ;; ---- Floating points -; a floating point constant is indexed by 3 bitvector constants -(declare fp (! s bitvec (! e bitvec (! i bitvec term)))) +; A floating point constant is a term having 3 bitvector children. +; Note this is used for both FLOATINGPOINT_FP and CONST_FLOATINGPOINT +(declare f_fp term) +(define fp (# x term (# y term (# z term (apply (apply (apply f_fp x) y) z))))) (declare f_fp.add term) (define fp.add (# x term (# y term (# z term (apply (apply (apply f_fp.add x) y) z))))) (declare f_fp.sub term) diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 865e471ef..ca120c241 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -15,10 +15,12 @@ #include "proof/lfsc/lfsc_node_converter.h" +#include #include #include #include "expr/array_store_all.h" +#include "expr/cardinality_constraint.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/nary_term_util.h" @@ -31,6 +33,7 @@ #include "theory/strings/word.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/bitvector.h" +#include "util/floatingpoint.h" #include "util/iand.h" #include "util/rational.h" #include "util/regexp.h" @@ -86,6 +89,8 @@ Node LfscNodeConverter::postConvert(Node n) { NodeManager* nm = NodeManager::currentNM(); Kind k = n.getKind(); + // we eliminate MATCH at preConvert above + Assert(k != MATCH); if (k == ASCRIPTION_TYPE) { // dummy node, return it @@ -158,6 +163,19 @@ Node LfscNodeConverter::postConvert(Node n) { return mkInternalSymbol(getNameForUserNameOf(n), tn); } + else if (k == CARDINALITY_CONSTRAINT) + { + Trace("lfsc-term-process-debug") + << "...convert cardinality constraint" << std::endl; + const CardinalityConstraint& cc = + n.getOperator().getConst(); + Node tnn = typeAsNode(convertType(cc.getType())); + Node ub = nm->mkConstInt(Rational(cc.getUpperBound())); + TypeNode tnc = + nm->mkFunctionType({tnn.getType(), ub.getType()}, nm->booleanType()); + Node fcard = getSymbolInternal(k, tnc, "fmf.card"); + return nm->mkNode(APPLY_UF, fcard, tnn, ub); + } else if (k == APPLY_UF) { return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n)); @@ -238,21 +256,23 @@ Node LfscNodeConverter::postConvert(Node n) { TypeNode btn = nm->booleanType(); TypeNode tnv = nm->mkFunctionType(btn, tn); - TypeNode btnv = nm->mkFunctionType({btn, btn}, btn); BitVector bv = n.getConst(); - size_t w = bv.getSize(); - Node ret = getSymbolInternal(k, btn, "bvn"); - Node b0 = getSymbolInternal(k, btn, "b0"); - Node b1 = getSymbolInternal(k, btn, "b1"); - Node bvc = getSymbolInternal(k, btnv, "bvc"); - for (size_t i = 0; i < w; i++) - { - Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0; - ret = nm->mkNode(APPLY_UF, bvc, arg, ret); - } + Node ret = convertBitVector(bv); Node bconstf = getSymbolInternal(k, tnv, "bv"); return nm->mkNode(APPLY_UF, bconstf, ret); } + else if (k == CONST_FLOATINGPOINT) + { + BitVector s, e, i; + n.getConst().getIEEEBitvectors(s, e, i); + Node sn = convert(nm->mkConst(s)); + Node en = convert(nm->mkConst(e)); + Node in = convert(nm->mkConst(i)); + TypeNode btn = nm->booleanType(); + TypeNode tnv = nm->mkFunctionType({btn, btn, btn}, tn); + Node bconstf = getSymbolInternal(k, tnv, "fp"); + return nm->mkNode(APPLY_UF, {bconstf, sn, en, in}); + } else if (k == CONST_STRING) { //"" is emptystr @@ -361,11 +381,6 @@ Node LfscNodeConverter::postConvert(Node n) Node n2 = nm->mkConstInt(Rational(op.d_loopMaxOcc)); return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]); } - else if (k == MATCH) - { - // currently unsupported - return n; - } else if (k == BITVECTOR_BB_TERM) { TypeNode btn = nm->booleanType(); @@ -613,7 +628,8 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn) return cur; } -std::string LfscNodeConverter::getNameForUserName(const std::string& name) +std::string LfscNodeConverter::getNameForUserName(const std::string& name, + size_t variant) { // For user name X, we do cvc.Y, where Y contains an escaped version of X. // Specifically, since LFSC does not allow these characters in identifier @@ -626,7 +642,14 @@ std::string LfscNodeConverter::getNameForUserName(const std::string& name) // The "cvc." prefix ensures we do not clash with LFSC definitions. // // The escaping ensures that all names are valid LFSC identifiers. - std::string sanitized("cvc."); + std::stringstream ss; + ss << "cvc"; + if (variant != 0) + { + ss << variant; + } + ss << "."; + std::string sanitized = ss.str(); size_t found = sanitized.size(); sanitized += name; // The following sanitizes symbols that are not allowed in LFSC identifiers @@ -656,7 +679,19 @@ std::string LfscNodeConverter::getNameForUserNameOf(Node v) { std::string name; v.getAttribute(expr::VarNameAttr(), name); - return getNameForUserName(name); + std::vector& syms = d_userSymbolList[name]; + size_t variant = 0; + std::vector::iterator itr = std::find(syms.begin(), syms.end(), v); + if (itr != syms.cend()) + { + variant = std::distance(syms.begin(), itr); + } + else + { + variant = syms.size(); + syms.push_back(v); + } + return getNameForUserName(name, variant); } bool LfscNodeConverter::shouldTraverse(Node n) @@ -780,13 +815,35 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector& chars) } } +Node LfscNodeConverter::convertBitVector(const BitVector& bv) +{ + NodeManager* nm = NodeManager::currentNM(); + TypeNode btn = nm->booleanType(); + TypeNode btnv = nm->mkFunctionType({btn, btn}, btn); + size_t w = bv.getSize(); + Node ret = getSymbolInternal(CONST_BITVECTOR, btn, "bvn"); + Node b0 = getSymbolInternal(CONST_BITVECTOR, btn, "b0"); + Node b1 = getSymbolInternal(CONST_BITVECTOR, btn, "b1"); + Node bvc = getSymbolInternal(CONST_BITVECTOR, btnv, "bvc"); + for (size_t i = 0; i < w; i++) + { + Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0; + ret = nm->mkNode(APPLY_UF, bvc, arg, ret); + } + return ret; +} + bool LfscNodeConverter::isIndexedOperatorKind(Kind k) { return k == REGEXP_LOOP || k == BITVECTOR_EXTRACT || k == BITVECTOR_REPEAT || k == BITVECTOR_ZERO_EXTEND || k == BITVECTOR_SIGN_EXTEND || k == BITVECTOR_ROTATE_LEFT || k == BITVECTOR_ROTATE_RIGHT - || k == INT_TO_BITVECTOR || k == IAND || k == APPLY_UPDATER - || k == APPLY_TESTER; + || k == INT_TO_BITVECTOR || k == IAND + || k == FLOATINGPOINT_TO_FP_FLOATINGPOINT + || k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR + || k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR + || k == FLOATINGPOINT_TO_FP_REAL || k == FLOATINGPOINT_TO_FP_GENERIC + || k == APPLY_UPDATER || k == APPLY_TESTER; } std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) @@ -836,6 +893,45 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) case IAND: indices.push_back(nm->mkConstInt(Rational(n.getConst().d_size))); break; + case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + { + const FloatingPointToFPFloatingPoint& ffp = + n.getConst(); + indices.push_back(nm->mkConstInt(ffp.getSize().exponentWidth())); + indices.push_back(nm->mkConstInt(ffp.getSize().significandWidth())); + } + break; + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + { + const FloatingPointToFPIEEEBitVector& fbv = + n.getConst(); + indices.push_back(nm->mkConstInt(fbv.getSize().exponentWidth())); + indices.push_back(nm->mkConstInt(fbv.getSize().significandWidth())); + } + break; + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + { + const FloatingPointToFPSignedBitVector& fsbv = + n.getConst(); + indices.push_back(nm->mkConstInt(fsbv.getSize().exponentWidth())); + indices.push_back(nm->mkConstInt(fsbv.getSize().significandWidth())); + } + break; + case FLOATINGPOINT_TO_FP_REAL: + { + const FloatingPointToFPReal& fr = n.getConst(); + indices.push_back(nm->mkConstInt(fr.getSize().exponentWidth())); + indices.push_back(nm->mkConstInt(fr.getSize().significandWidth())); + } + break; + case FLOATINGPOINT_TO_FP_GENERIC: + { + const FloatingPointToFPGeneric& fg = + n.getConst(); + indices.push_back(nm->mkConstInt(fg.getSize().exponentWidth())); + indices.push_back(nm->mkConstInt(fg.getSize().significandWidth())); + } + break; case APPLY_TESTER: { unsigned index = DType::indexOf(n); @@ -960,7 +1056,31 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) opName << "f_"; } } - opName << printer::smt2::Smt2Printer::smtKindString(k); + // must avoid overloading for to_fp variants + if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) + { + opName << "to_fp_fp"; + } + else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) + { + opName << "to_fp_ieee_bv"; + } + else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) + { + opName << "to_fp_sbv"; + } + else if (k == FLOATINGPOINT_TO_FP_REAL) + { + opName << "to_fp_real"; + } + else if (k == FLOATINGPOINT_TO_FP_GENERIC) + { + opName << "to_fp_generic"; + } + else + { + opName << printer::smt2::Smt2Printer::smtKindString(k); + } } else if (k == APPLY_CONSTRUCTOR) { @@ -969,7 +1089,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) // get its variable name opName << getNameForUserNameOf(dt[index].getConstructor()); } - else if (k == APPLY_SELECTOR) + else if (k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL) { if (k == APPLY_SELECTOR_TOTAL) { @@ -980,9 +1100,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) unsigned index = DType::indexOf(op); const DType& dt = DType::datatypeOf(op); unsigned cindex = DType::cindexOf(op); - std::stringstream sss; - sss << dt[cindex][index].getSelector(); - opName << getNameForUserName(sss.str()); + opName << getNameForUserNameOf(dt[cindex][index].getSelector()); } } else if (k == SET_SINGLETON || k == BAG_MAKE) @@ -999,6 +1117,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) } if (ret.isNull()) { + Trace("lfsc-term-process-debug2") << "...default symbol" << std::endl; ret = getSymbolInternal(k, ftype, opName.str()); } // if indexed, apply to index diff --git a/src/proof/lfsc/lfsc_node_converter.h b/src/proof/lfsc/lfsc_node_converter.h index bd65af503..44250b8aa 100644 --- a/src/proof/lfsc/lfsc_node_converter.h +++ b/src/proof/lfsc/lfsc_node_converter.h @@ -103,10 +103,16 @@ class LfscNodeConverter : public NodeConverter */ Kind getBuiltinKindForInternalSymbol(Node op) const; - /** get name for user name */ - static std::string getNameForUserName(const std::string& name); + /** + * get name for user name + * @param name The user provided name for the symbol + * @param variant A unique index for the symbol to resolve multiple symbols + * with the same name. + */ + static std::string getNameForUserName(const std::string& name, + size_t variant = 0); /** get name for the name of node v, where v should be a variable */ - static std::string getNameForUserNameOf(Node v); + std::string getNameForUserNameOf(Node v); private: /** Should we traverse n? */ @@ -140,6 +146,8 @@ class LfscNodeConverter : public NodeConverter * Get character vector, add internal vector of characters for c. */ void getCharVectorInternal(Node c, std::vector& chars); + /** convert bitvector to its LFSC term (of LFSC sort bitvec) */ + Node convertBitVector(const BitVector& bv); /** Is k a kind that is printed as an indexed operator in LFSC? */ static bool isIndexedOperatorKind(Kind k); /** get indices for printing the operator of n in the LFSC format */ @@ -148,6 +156,11 @@ class LfscNodeConverter : public NodeConverter std::map, Node> d_symbolsMap; /** the set of all internally generated symbols */ std::unordered_set d_symbols; + /** + * Mapping from user symbols to the (list of) symbols with that name. This + * is used to resolve symbol overloading, which is forbidden in LFSC. + */ + std::map > d_userSymbolList; /** symbols to builtin kinds*/ std::map d_symbolToBuiltinKind; /** arrow type constructor */