src/proof/lfsc/lfsc_node_converter.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Implementation of LFSC node conversion
  14  */
  15
  16 #include "proof/lfsc/lfsc_node_converter.h"
  17
  18 #include <sstream>
  19
  20 #include "expr/array_store_all.h"
  21 #include "expr/dtype.h"
  22 #include "expr/dtype_cons.h"
  23 #include "expr/nary_term_util.h"
  24 #include "expr/node_manager_attributes.h"
  25 #include "expr/sequence.h"
  26 #include "expr/skolem_manager.h"
  27 #include "printer/smt2/smt2_printer.h"
  28 #include "theory/bv/theory_bv_utils.h"
  29 #include "theory/strings/word.h"
  30 #include "theory/uf/theory_uf_rewriter.h"
  31 #include "util/bitvector.h"
  32 #include "util/iand.h"
  33 #include "util/rational.h"
  34 #include "util/regexp.h"
  35 #include "util/string.h"
  36
  37 using namespace cvc5::kind;
  38
  39 namespace cvc5 {
  40 namespace proof {
  41
  42 LfscNodeConverter::LfscNodeConverter()
  43 {
  44   NodeManager* nm = NodeManager::currentNM();
  45   d_arrow = nm->mkSortConstructor("arrow", 2);
  46
  47   d_sortType = nm->mkSort("sortType");
  48   // the embedding of arrow into Node, which is binary constructor over sorts
  49   TypeNode anfType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
  50   d_typeAsNode[d_arrow] = getSymbolInternal(FUNCTION_TYPE, anfType, "arrow");
  51
  52   TypeNode intType = nm->integerType();
  53   TypeNode arrType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
  54   d_typeKindToNodeCons[ARRAY_TYPE] =
  55       getSymbolInternal(FUNCTION_TYPE, arrType, "Array");
  56   TypeNode bvType = nm->mkFunctionType(intType, d_sortType);
  57   d_typeKindToNodeCons[BITVECTOR_TYPE] =
  58       getSymbolInternal(FUNCTION_TYPE, bvType, "BitVec");
  59   TypeNode fpType = nm->mkFunctionType({intType, intType}, d_sortType);
  60   d_typeKindToNodeCons[FLOATINGPOINT_TYPE] =
  61       getSymbolInternal(FUNCTION_TYPE, fpType, "FloatingPoint");
  62   TypeNode setType = nm->mkFunctionType(d_sortType, d_sortType);
  63   d_typeKindToNodeCons[SET_TYPE] =
  64       getSymbolInternal(FUNCTION_TYPE, setType, "Set");
  65   d_typeKindToNodeCons[BAG_TYPE] =
  66       getSymbolInternal(FUNCTION_TYPE, setType, "Bag");
  67   d_typeKindToNodeCons[SEQUENCE_TYPE] =
  68       getSymbolInternal(FUNCTION_TYPE, setType, "Seq");
  69 }
  70
  71 Node LfscNodeConverter::postConvert(Node n)
  72 {
  73   NodeManager* nm = NodeManager::currentNM();
  74   Kind k = n.getKind();
  75   if (k == ASCRIPTION_TYPE)
  76   {
  77     // dummy node, return it
  78     return n;
  79   }
  80   TypeNode tn = n.getType();
  81   Trace("lfsc-term-process-debug")
  82       << "postConvert " << n << " " << k << std::endl;
  83   if (k == BOUND_VARIABLE)
  84   {
  85     // ignore internally generated symbols
  86     if (d_symbols.find(n) != d_symbols.end())
  87     {
  88       return n;
  89     }
  90     // bound variable v is (bvar x T)
  91     TypeNode intType = nm->integerType();
  92     Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
  93     Node tc = typeAsNode(convertType(tn));
  94     TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn);
  95     Node bvarOp = getSymbolInternal(k, ftype, "bvar");
  96     return nm->mkNode(APPLY_UF, bvarOp, x, tc);
  97   }
  98   else if (k == SKOLEM || k == BOOLEAN_TERM_VARIABLE)
  99   {
 100     // constructors/selectors are represented by skolems, which are defined
 101     // symbols
 102     if (tn.isConstructor() || tn.isSelector() || tn.isTester()
 103         || tn.isUpdater())
 104     {
 105       // note these are not converted to their user named (cvc.) symbols here,
 106       // to avoid type errors when constructing terms for postConvert
 107       return n;
 108     }
 109     // skolems v print as their witness forms
 110     // v is (skolem W) where W is the original or witness form of v
 111     Node wi = SkolemManager::getOriginalForm(n);
 112     if (wi == n)
 113     {
 114       // if it is not a purification skolem, maybe it is a witness skolem
 115       wi = SkolemManager::getWitnessForm(n);
 116     }
 117     if (!wi.isNull() && wi != n)
 118     {
 119       Trace("lfsc-term-process-debug") << "...witness form " << wi << std::endl;
 120       wi = convert(wi);
 121       Trace("lfsc-term-process-debug")
 122           << "...converted witness for " << wi << std::endl;
 123       TypeNode ftype = nm->mkFunctionType(tn, tn);
 124       Node skolemOp = getSymbolInternal(k, ftype, "skolem");
 125       return nm->mkNode(APPLY_UF, skolemOp, wi);
 126     }
 127     // might be a skolem function
 128     Node ns = maybeMkSkolemFun(n);
 129     if (!ns.isNull())
 130     {
 131       return ns;
 132     }
 133     // Otherwise, it is an uncategorized skolem, must use a fresh variable.
 134     // This case will only apply for terms originating from places with no
 135     // proof support.
 136     TypeNode intType = nm->integerType();
 137     TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn);
 138     Node var = mkInternalSymbol("var", varType);
 139     Node index =
 140         nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
 141     Node tc = typeAsNode(convertType(tn));
 142     return nm->mkNode(APPLY_UF, var, index, tc);
 143   }
 144   else if (n.isVar())
 145   {
 146     std::stringstream ss;
 147     ss << n;
 148     Node nn = mkInternalSymbol(getNameForUserName(ss.str()), tn);
 149     return nn;
 150   }
 151   else if (k == APPLY_UF)
 152   {
 153     return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n));
 154   }
 155   else if (k == APPLY_CONSTRUCTOR || k == APPLY_SELECTOR || k == APPLY_TESTER
 156            || k == APPLY_SELECTOR_TOTAL || k == APPLY_UPDATER)
 157   {
 158     // must convert other kinds of apply to functions, since we convert to
 159     // HO_APPLY
 160     Node opc = getOperatorOfTerm(n, true);
 161     if (n.getNumChildren() == 0)
 162     {
 163       return opc;
 164     }
 165     std::vector<Node> children;
 166     children.push_back(opc);
 167     children.insert(children.end(), n.begin(), n.end());
 168     return postConvert(nm->mkNode(APPLY_UF, children));
 169   }
 170   else if (k == HO_APPLY)
 171   {
 172     std::vector<TypeNode> argTypes;
 173     argTypes.push_back(n[0].getType());
 174     argTypes.push_back(n[1].getType());
 175     TypeNode tnh = nm->mkFunctionType(argTypes, tn);
 176     Node hconstf = getSymbolInternal(k, tnh, "apply");
 177     return nm->mkNode(APPLY_UF, hconstf, n[0], n[1]);
 178   }
 179   else if (k == CONST_RATIONAL || k == CAST_TO_REAL)
 180   {
 181     if (k == CAST_TO_REAL)
 182     {
 183       // already converted
 184       do
 185       {
 186         n = n[0];
 187         Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL);
 188       } while (n.getKind() != CONST_RATIONAL);
 189     }
 190     TypeNode tnv = nm->mkFunctionType(tn, tn);
 191     Node rconstf;
 192     Node arg;
 193     Rational r = n.getConst<Rational>();
 194     if (tn.isInteger())
 195     {
 196       rconstf = getSymbolInternal(k, tnv, "int");
 197       if (r.sgn() == -1)
 198       {
 199         // use LFSC syntax for mpz negation
 200         Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~");
 201         arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs()));
 202       }
 203       else
 204       {
 205         arg = n;
 206       }
 207     }
 208     else
 209     {
 210       rconstf = getSymbolInternal(k, tnv, "real");
 211       // ensure rationals are printed properly here using mpq syntax
 212       // Note that inconvieniently, LFSC uses (non-sexpr) syntax n/m for
 213       // constant rationals, hence we must use a string
 214       std::stringstream ss;
 215       ss << "__LFSC_TMP" << r.getNumerator().abs() << "/" << r.getDenominator();
 216       arg = mkInternalSymbol(ss.str(), tn);
 217       // negative (~ n/m)
 218       if (r.sgn() == -1)
 219       {
 220         Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~");
 221         arg = nm->mkNode(APPLY_UF, mpzn, arg);
 222       }
 223     }
 224     return nm->mkNode(APPLY_UF, rconstf, arg);
 225   }
 226   else if (k == CONST_BITVECTOR)
 227   {
 228     TypeNode btn = nm->booleanType();
 229     TypeNode tnv = nm->mkFunctionType(btn, tn);
 230     TypeNode btnv = nm->mkFunctionType({btn, btn}, btn);
 231     BitVector bv = n.getConst<BitVector>();
 232     size_t w = bv.getSize();
 233     Node ret = getSymbolInternal(k, btn, "bvn");
 234     Node b0 = getSymbolInternal(k, btn, "b0");
 235     Node b1 = getSymbolInternal(k, btn, "b1");
 236     Node bvc = getSymbolInternal(k, btnv, "bvc");
 237     for (size_t i = 0; i < w; i++)
 238     {
 239       Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0;
 240       ret = nm->mkNode(APPLY_UF, bvc, arg, ret);
 241     }
 242     Node bconstf = getSymbolInternal(k, tnv, "bv");
 243     return nm->mkNode(APPLY_UF, bconstf, ret);
 244   }
 245   else if (k == CONST_STRING)
 246   {
 247     //"" is emptystr
 248     //"A" is (char 65)
 249     //"ABC" is (str.++ (char 65) (str.++ (char 66) (str.++ (char 67) emptystr)))
 250     std::vector<Node> charVec;
 251     getCharVectorInternal(n, charVec);
 252     Assert(!charVec.empty());
 253     if (charVec.size() == 1)
 254     {
 255       // handles empty string and singleton character
 256       return charVec[0];
 257     }
 258     std::reverse(charVec.begin(), charVec.end());
 259     Node ret = postConvert(getNullTerminator(STRING_CONCAT, tn));
 260     for (size_t i = 0, size = charVec.size(); i < size; i++)
 261     {
 262       ret = nm->mkNode(STRING_CONCAT, charVec[i], ret);
 263     }
 264     return ret;
 265   }
 266   else if (k == CONST_SEQUENCE)
 267   {
 268     const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
 269     TypeNode etype = nm->mkFunctionType(d_sortType, tn);
 270     Node ret = getSymbolInternal(k, etype, "seq.empty");
 271     ret = nm->mkNode(APPLY_UF, ret, typeAsNode(convertType(tn)));
 272     std::vector<Node> vecu;
 273     for (size_t i = 0, size = charVec.size(); i < size; i++)
 274     {
 275       Node u = nm->mkNode(SEQ_UNIT, postConvert(charVec[size - (i + 1)]));
 276       if (size == 1)
 277       {
 278         // singleton case
 279         return u;
 280       }
 281       ret = nm->mkNode(STRING_CONCAT, u, ret);
 282     }
 283     return ret;
 284   }
 285   else if (k == STORE_ALL)
 286   {
 287     Node t = typeAsNode(convertType(tn));
 288     TypeNode caRetType = nm->mkFunctionType(tn.getArrayConstituentType(), tn);
 289     TypeNode catype = nm->mkFunctionType(d_sortType, caRetType);
 290     Node bconstf = getSymbolInternal(k, catype, "array_const");
 291     Node f = nm->mkNode(APPLY_UF, bconstf, t);
 292     ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
 293     return nm->mkNode(APPLY_UF, f, convert(storeAll.getValue()));
 294   }
 295   else if (k == GEQ || k == GT || k == LEQ || k == LT || k == MINUS
 296            || k == DIVISION || k == DIVISION_TOTAL || k == INTS_DIVISION
 297            || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS
 298            || k == INTS_MODULUS_TOTAL || k == UMINUS || k == POW
 299            || isIndexedOperatorKind(k))
 300   {
 301     // must give special names to SMT-LIB operators with arithmetic subtyping
 302     // note that MINUS is not n-ary
 303     // get the macro-apply version of the operator
 304     Node opc = getOperatorOfTerm(n, true);
 305     std::vector<Node> children;
 306     children.push_back(opc);
 307     children.insert(children.end(), n.begin(), n.end());
 308     return nm->mkNode(APPLY_UF, children);
 309   }
 310   else if (k == SET_EMPTY || k == SET_UNIVERSE || k == BAG_EMPTY)
 311   {
 312     Node t = typeAsNode(convertType(tn));
 313     TypeNode etype = nm->mkFunctionType(d_sortType, tn);
 314     Node ef = getSymbolInternal(
 315         k,
 316         etype,
 317         k == SET_EMPTY ? "set.empty"
 318                        : (k == SET_UNIVERSE ? "set.universe" : "bag.empty"));
 319     return nm->mkNode(APPLY_UF, ef, t);
 320   }
 321   else if (n.isClosure())
 322   {
 323     // (forall ((x1 T1) ... (xn Tk)) P) is
 324     // ((forall x1 T1) ((forall x2 T2) ... ((forall xk Tk) P))). We use
 325     // SEXPR to do this, which avoids the need for indexed operators.
 326     Node ret = n[1];
 327     Node cop = getOperatorOfClosure(n, true);
 328     for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++)
 329     {
 330       size_t ii = (nchild - 1) - i;
 331       Node v = n[0][ii];
 332       Node vop = getOperatorOfBoundVar(cop, v);
 333       ret = nm->mkNode(APPLY_UF, vop, ret);
 334     }
 335     // notice that intentionally we drop annotations here
 336     return ret;
 337   }
 338   else if (k == REGEXP_LOOP)
 339   {
 340     // ((_ re.loop n1 n2) t) is ((re.loop n1 n2) t)
 341     TypeNode intType = nm->integerType();
 342     TypeNode relType =
 343         nm->mkFunctionType({intType, intType}, nm->mkFunctionType(tn, tn));
 344     Node rop = getSymbolInternal(
 345         k, relType, printer::smt2::Smt2Printer::smtKindString(k));
 346     RegExpLoop op = n.getOperator().getConst<RegExpLoop>();
 347     Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc));
 348     Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc));
 349     return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]);
 350   }
 351   else if (k == MATCH)
 352   {
 353     // currently unsupported
 354     return n;
 355   }
 356   else if (k == BITVECTOR_BB_TERM)
 357   {
 358     TypeNode btn = nm->booleanType();
 359     // (bbT t1 ... tn) is (bbT t1 (bbT t2 ... (bbT tn emptybv)))
 360     // where notice that each bbT has a different type
 361     Node curr = getNullTerminator(BITVECTOR_CONCAT, tn);
 362     for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
 363     {
 364       TypeNode bvt = nm->mkBitVectorType(i + 1);
 365       TypeNode ftype = nm->mkFunctionType({btn, curr.getType()}, bvt);
 366       Node bbt = getSymbolInternal(k, ftype, "bbT");
 367       curr = nm->mkNode(APPLY_UF, bbt, n[nchild - (i + 1)], curr);
 368     }
 369     return curr;
 370   }
 371   else if (k == SEP_NIL)
 372   {
 373     Node tnn = typeAsNode(convertType(tn));
 374     TypeNode ftype = nm->mkFunctionType(d_sortType, tn);
 375     Node s = getSymbolInternal(k, ftype, "sep.nil");
 376     return nm->mkNode(APPLY_UF, s, tnn);
 377   }
 378   else if (NodeManager::isNAryKind(k) && n.getNumChildren() >= 2)
 379   {
 380     size_t nchild = n.getNumChildren();
 381     Assert(n.getMetaKind() != metakind::PARAMETERIZED);
 382     // convert all n-ary applications to binary
 383     std::vector<Node> children(n.begin(), n.end());
 384     // distinct is special case
 385     if (k == DISTINCT)
 386     {
 387       // DISTINCT(x1,...,xn) --->
 388       // AND(DISTINCT(x1,x2), AND(,..., AND(,..,DISTINCT(x_{n-1},x_n))))
 389       Node ret = nm->mkNode(k, children[0], children[1]);
 390       for (unsigned i = 0; i < nchild; i++)
 391         for (unsigned j = i + 1; j < nchild; j++)
 392         {
 393           if (i != 0 && j != 1)
 394           {
 395             ret = nm->mkNode(AND, ret, nm->mkNode(k, children[i], children[j]));
 396           }
 397         }
 398       Trace("lfsc-term-process-debug") << "n: " << n << std::endl
 399                                        << "ret: " << ret << std::endl;
 400       return ret;
 401     }
 402     std::reverse(children.begin(), children.end());
 403     // Add the null-terminator. This is done to disambiguate the number
 404     // of children for term with n-ary operators. In particular note that
 405     // (or A B C (or D E)) has representation:
 406     //   (or A (or B (or C (or (or D E) false))))
 407     // This makes the AST above distinguishable from (or A B C D E),
 408     // which otherwise would both have representation:
 409     //   (or A (or B (or C (or D E))))
 410     Node nullTerm = getNullTerminator(k, tn);
 411     // Most operators simply get binarized
 412     Node ret;
 413     size_t istart = 0;
 414     if (nullTerm.isNull())
 415     {
 416       ret = children[0];
 417       istart = 1;
 418     }
 419     else
 420     {
 421       // must convert recursively, since nullTerm may have subterms.
 422       ret = convert(nullTerm);
 423     }
 424     // the kind to chain
 425     Kind ck = k;
 426     // check whether we are also changing the operator name, in which case
 427     // we build a binary uninterpreted function opc
 428     Node opc;
 429     if (k == PLUS || k == MULT || k == NONLINEAR_MULT)
 430     {
 431       std::stringstream opName;
 432       // currently allow subtyping
 433       opName << "a.";
 434       opName << printer::smt2::Smt2Printer::smtKindString(k);
 435       TypeNode ftype = nm->mkFunctionType({tn, tn}, tn);
 436       opc = getSymbolInternal(k, ftype, opName.str());
 437       ck = APPLY_UF;
 438     }
 439     // now, iterate over children and make binary conversion
 440     for (size_t i = istart, npchild = children.size(); i < npchild; i++)
 441     {
 442       if (!opc.isNull())
 443       {
 444         ret = nm->mkNode(ck, opc, children[i], ret);
 445       }
 446       else
 447       {
 448         ret = nm->mkNode(ck, children[i], ret);
 449       }
 450     }
 451     return ret;
 452   }
 453   return n;
 454 }
 455
 456 TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
 457 {
 458   NodeManager* nm = NodeManager::currentNM();
 459   TypeNode cur = tn;
 460   Node tnn;
 461   Kind k = tn.getKind();
 462   Trace("lfsc-term-process-debug")
 463       << "postConvertType " << tn << " " << tn.getNumChildren() << " " << k
 464       << std::endl;
 465   if (k == FUNCTION_TYPE)
 466   {
 467     // (-> T1 ... Tn T) is (arrow T1 .... (arrow Tn T))
 468     std::vector<TypeNode> argTypes = tn.getArgTypes();
 469     // also make the node embedding of the type
 470     Node arrown = d_typeAsNode[d_arrow];
 471     Assert(!arrown.isNull());
 472     cur = tn.getRangeType();
 473     tnn = typeAsNode(cur);
 474     for (std::vector<TypeNode>::reverse_iterator it = argTypes.rbegin();
 475          it != argTypes.rend();
 476          ++it)
 477     {
 478       std::vector<TypeNode> aargs;
 479       aargs.push_back(*it);
 480       aargs.push_back(cur);
 481       cur = nm->mkSort(d_arrow, aargs);
 482       tnn = nm->mkNode(APPLY_UF, arrown, typeAsNode(*it), tnn);
 483     }
 484   }
 485   else if (k == BITVECTOR_TYPE)
 486   {
 487     tnn = d_typeKindToNodeCons[k];
 488     Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize()));
 489     tnn = nm->mkNode(APPLY_UF, tnn, w);
 490   }
 491   else if (k == FLOATINGPOINT_TYPE)
 492   {
 493     tnn = d_typeKindToNodeCons[k];
 494     Node e = nm->mkConst(CONST_RATIONAL,
 495                          Rational(tn.getFloatingPointExponentSize()));
 496     Node s = nm->mkConst(CONST_RATIONAL,
 497                          Rational(tn.getFloatingPointSignificandSize()));
 498     tnn = nm->mkNode(APPLY_UF, tnn, e, s);
 499   }
 500   else if (tn.getNumChildren() == 0)
 501   {
 502     // special case: tuples must be distinguished by their arity
 503     if (tn.isTuple())
 504     {
 505       const DType& dt = tn.getDType();
 506       unsigned int nargs = dt[0].getNumArgs();
 507       if (nargs > 0)
 508       {
 509         std::vector<TypeNode> types;
 510         std::vector<TypeNode> convTypes;
 511         std::vector<Node> targs;
 512         for (unsigned int i = 0; i < nargs; i++)
 513         {
 514           // it is not converted yet, convert here
 515           TypeNode tnc = convertType(dt[0][i].getRangeType());
 516           types.push_back(d_sortType);
 517           convTypes.push_back(tnc);
 518           targs.push_back(typeAsNode(tnc));
 519         }
 520         TypeNode ftype = nm->mkFunctionType(types, d_sortType);
 521         // must distinguish by arity
 522         std::stringstream ss;
 523         ss << "Tuple_" << nargs;
 524         targs.insert(targs.begin(), getSymbolInternal(k, ftype, ss.str()));
 525         tnn = nm->mkNode(APPLY_UF, targs);
 526         // we are changing its name, we must make a sort constructor
 527         cur = nm->mkSortConstructor(ss.str(), nargs);
 528         cur = nm->mkSort(cur, convTypes);
 529       }
 530     }
 531     if (tnn.isNull())
 532     {
 533       std::stringstream ss;
 534       options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
 535       tn.toStream(ss);
 536       if (tn.isSort() || (tn.isDatatype() && !tn.isTuple()))
 537       {
 538         std::stringstream sss;
 539         sss << LfscNodeConverter::getNameForUserName(ss.str());
 540         tnn = getSymbolInternal(k, d_sortType, sss.str());
 541         cur = nm->mkSort(sss.str());
 542       }
 543       else
 544       {
 545         tnn = getSymbolInternal(k, d_sortType, ss.str());
 546       }
 547     }
 548   }
 549   else
 550   {
 551     // to build the type-as-node, must convert the component types
 552     std::vector<Node> targs;
 553     std::vector<TypeNode> types;
 554     for (const TypeNode& tnc : tn)
 555     {
 556       targs.push_back(typeAsNode(tnc));
 557       types.push_back(d_sortType);
 558     }
 559     Node op;
 560     if (k == PARAMETRIC_DATATYPE)
 561     {
 562       // erase first child, which repeats the datatype
 563       targs.erase(targs.begin(), targs.begin() + 1);
 564       types.erase(types.begin(), types.begin() + 1);
 565       TypeNode ftype = nm->mkFunctionType(types, d_sortType);
 566       // the operator has been converted; it is no longer a datatype, thus
 567       // we must print to get its name.
 568       std::stringstream ss;
 569       ss << tn[0];
 570       op = getSymbolInternal(k, ftype, ss.str());
 571     }
 572     else if (k == SORT_TYPE)
 573     {
 574       TypeNode ftype = nm->mkFunctionType(types, d_sortType);
 575       std::string name;
 576       tn.getAttribute(expr::VarNameAttr(), name);
 577       op = getSymbolInternal(k, ftype, name);
 578     }
 579     else
 580     {
 581       std::map<Kind, Node>::iterator it = d_typeKindToNodeCons.find(k);
 582       if (it != d_typeKindToNodeCons.end())
 583       {
 584         op = it->second;
 585       }
 586     }
 587     if (!op.isNull())
 588     {
 589       targs.insert(targs.begin(), op);
 590       tnn = nm->mkNode(APPLY_UF, targs);
 591     }
 592     else
 593     {
 594       AlwaysAssert(false);
 595     }
 596   }
 597   Assert(!tnn.isNull());
 598   Trace("lfsc-term-process-debug") << "...type as node: " << tnn << std::endl;
 599   d_typeAsNode[cur] = tnn;
 600   return cur;
 601 }
 602
 603 std::string LfscNodeConverter::getNameForUserName(const std::string& name)
 604 {
 605   std::stringstream ss;
 606   ss << "cvc." << name;
 607   return ss.str();
 608 }
 609
 610 bool LfscNodeConverter::shouldTraverse(Node n)
 611 {
 612   Kind k = n.getKind();
 613   // don't convert bound variable or instantiation pattern list directly
 614   if (k == BOUND_VAR_LIST || k == INST_PATTERN_LIST)
 615   {
 616     return false;
 617   }
 618   // should not traverse internal applications
 619   if (k == APPLY_UF)
 620   {
 621     if (d_symbols.find(n.getOperator()) != d_symbols.end())
 622     {
 623       return false;
 624     }
 625   }
 626   return true;
 627 }
 628
 629 Node LfscNodeConverter::maybeMkSkolemFun(Node k, bool macroApply)
 630 {
 631   NodeManager* nm = NodeManager::currentNM();
 632   SkolemManager* sm = nm->getSkolemManager();
 633   SkolemFunId sfi = SkolemFunId::NONE;
 634   Node cacheVal;
 635   TypeNode tn = k.getType();
 636   if (sm->isSkolemFunction(k, sfi, cacheVal))
 637   {
 638     if (sfi == SkolemFunId::SHARED_SELECTOR)
 639     {
 640       // a skolem corresponding to shared selector should print in
 641       // LFSC as (sel T n) where T is the type and n is the index of the
 642       // shared selector.
 643       TypeNode fselt = nm->mkFunctionType(tn.getSelectorDomainType(),
 644                                           tn.getSelectorRangeType());
 645       TypeNode intType = nm->integerType();
 646       TypeNode selt = nm->mkFunctionType({d_sortType, intType}, fselt);
 647       Node sel = getSymbolInternal(k.getKind(), selt, "sel");
 648       Node kn = typeAsNode(convertType(tn.getSelectorRangeType()));
 649       Assert(!cacheVal.isNull() && cacheVal.getKind() == CONST_RATIONAL);
 650       return nm->mkNode(APPLY_UF, sel, kn, cacheVal);
 651     }
 652     else if (sfi == SkolemFunId::RE_UNFOLD_POS_COMPONENT)
 653     {
 654       // a skolem corresponding to a regular expression unfolding component
 655       // should print as (skolem_re_unfold_pos t R n) where the skolem is the
 656       // n^th component for the unfolding of (str.in_re t R).
 657       TypeNode strType = nm->stringType();
 658       TypeNode reType = nm->regExpType();
 659       TypeNode intType = nm->integerType();
 660       TypeNode reut = nm->mkFunctionType({strType, reType, intType}, strType);
 661       Node sk = getSymbolInternal(k.getKind(), reut, "skolem_re_unfold_pos");
 662       Assert(!cacheVal.isNull() && cacheVal.getKind() == SEXPR
 663              && cacheVal.getNumChildren() == 3);
 664       // third value is mpz, which is not converted
 665       return nm->mkNode(
 666           APPLY_UF,
 667           {sk, convert(cacheVal[0]), convert(cacheVal[1]), cacheVal[2]});
 668     }
 669   }
 670   return Node::null();
 671 }
 672
 673 Node LfscNodeConverter::typeAsNode(TypeNode tni) const
 674 {
 675   // should always exist in the cache, as we always run types through
 676   // postConvertType before calling this method.
 677   std::map<TypeNode, Node>::const_iterator it = d_typeAsNode.find(tni);
 678   AlwaysAssert(it != d_typeAsNode.end()) << "Missing typeAsNode " << tni;
 679   return it->second;
 680 }
 681
 682 Node LfscNodeConverter::mkInternalSymbol(const std::string& name, TypeNode tn)
 683 {
 684   Node sym = NodeManager::currentNM()->mkBoundVar(name, tn);
 685   d_symbols.insert(sym);
 686   return sym;
 687 }
 688
 689 Node LfscNodeConverter::getSymbolInternalFor(Node n, const std::string& name)
 690 {
 691   return getSymbolInternal(n.getKind(), n.getType(), name);
 692 }
 693
 694 Node LfscNodeConverter::getSymbolInternal(Kind k,
 695                                           TypeNode tn,
 696                                           const std::string& name)
 697 {
 698   std::tuple<Kind, TypeNode, std::string> key(k, tn, name);
 699   std::map<std::tuple<Kind, TypeNode, std::string>, Node>::iterator it =
 700       d_symbolsMap.find(key);
 701   if (it != d_symbolsMap.end())
 702   {
 703     return it->second;
 704   }
 705   Node sym = mkInternalSymbol(name, tn);
 706   d_symbolToBuiltinKind[sym] = k;
 707   d_symbolsMap[key] = sym;
 708   return sym;
 709 }
 710
 711 void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars)
 712 {
 713   Assert(c.getKind() == CONST_STRING);
 714   NodeManager* nm = NodeManager::currentNM();
 715   const std::vector<unsigned>& vec = c.getConst<String>().getVec();
 716   if (vec.size() == 0)
 717   {
 718     Node ec = getSymbolInternalFor(c, "emptystr");
 719     chars.push_back(ec);
 720     return;
 721   }
 722   TypeNode tnc = nm->mkFunctionType(nm->integerType(), c.getType());
 723   Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char");
 724   for (unsigned i = 0, size = vec.size(); i < size; i++)
 725   {
 726     Node cc = nm->mkNode(
 727         APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i])));
 728     chars.push_back(cc);
 729   }
 730 }
 731
 732 bool LfscNodeConverter::isIndexedOperatorKind(Kind k)
 733 {
 734   return k == BITVECTOR_EXTRACT || k == BITVECTOR_REPEAT
 735          || k == BITVECTOR_ZERO_EXTEND || k == BITVECTOR_SIGN_EXTEND
 736          || k == BITVECTOR_ROTATE_LEFT || k == BITVECTOR_ROTATE_RIGHT
 737          || k == INT_TO_BITVECTOR || k == IAND || k == APPLY_UPDATER
 738          || k == APPLY_TESTER;
 739 }
 740
 741 std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
 742 {
 743   NodeManager* nm = NodeManager::currentNM();
 744   std::vector<Node> indices;
 745   switch (k)
 746   {
 747     case BITVECTOR_EXTRACT:
 748     {
 749       BitVectorExtract p = n.getConst<BitVectorExtract>();
 750       indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high)));
 751       indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low)));
 752       break;
 753     }
 754     case BITVECTOR_REPEAT:
 755       indices.push_back(
 756           nm->mkConst(CONST_RATIONAL,
 757                       Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
 758       break;
 759     case BITVECTOR_ZERO_EXTEND:
 760       indices.push_back(nm->mkConst(
 761           CONST_RATIONAL,
 762           Rational(n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount)));
 763       break;
 764     case BITVECTOR_SIGN_EXTEND:
 765       indices.push_back(nm->mkConst(
 766           CONST_RATIONAL,
 767           Rational(n.getConst<BitVectorSignExtend>().d_signExtendAmount)));
 768       break;
 769     case BITVECTOR_ROTATE_LEFT:
 770       indices.push_back(nm->mkConst(
 771           CONST_RATIONAL,
 772           Rational(n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount)));
 773       break;
 774     case BITVECTOR_ROTATE_RIGHT:
 775       indices.push_back(nm->mkConst(
 776           CONST_RATIONAL,
 777           Rational(n.getConst<BitVectorRotateRight>().d_rotateRightAmount)));
 778       break;
 779     case INT_TO_BITVECTOR:
 780       indices.push_back(nm->mkConst(
 781           CONST_RATIONAL, Rational(n.getConst<IntToBitVector>().d_size)));
 782       break;
 783     case IAND:
 784       indices.push_back(
 785           nm->mkConst(CONST_RATIONAL, Rational(n.getConst<IntAnd>().d_size)));
 786       break;
 787     case APPLY_TESTER:
 788     {
 789       unsigned index = DType::indexOf(n);
 790       const DType& dt = DType::datatypeOf(n);
 791       indices.push_back(dt[index].getConstructor());
 792     }
 793     break;
 794     case APPLY_UPDATER:
 795     {
 796       unsigned index = DType::indexOf(n);
 797       const DType& dt = DType::datatypeOf(n);
 798       unsigned cindex = DType::cindexOf(n);
 799       indices.push_back(dt[cindex][index].getSelector());
 800     }
 801     break;
 802     default: Assert(false); break;
 803   }
 804   return indices;
 805 }
 806
 807 Node LfscNodeConverter::getNullTerminator(Kind k, TypeNode tn)
 808 {
 809   NodeManager* nm = NodeManager::currentNM();
 810   Node nullTerm;
 811   switch (k)
 812   {
 813     case REGEXP_CONCAT:
 814       // the language containing only the empty string, which has special
 815       // syntax in LFSC
 816       nullTerm = getSymbolInternal(k, tn, "re.empty");
 817       break;
 818     case BITVECTOR_CONCAT:
 819     {
 820       // the null terminator of bitvector concat is a dummy variable of
 821       // bit-vector type with zero width, regardless of the type of the overall
 822       // concat.
 823       TypeNode bvz = nm->mkBitVectorType(0);
 824       nullTerm = getSymbolInternal(k, bvz, "emptybv");
 825     }
 826     break;
 827     default:
 828       // no special handling, or not null terminated
 829       break;
 830   }
 831   if (!nullTerm.isNull())
 832   {
 833     return nullTerm;
 834   }
 835   // otherwise, fall back to standard utility
 836   return expr::getNullTerminator(k, tn);
 837 }
 838
 839 Kind LfscNodeConverter::getBuiltinKindForInternalSymbol(Node op) const
 840 {
 841   std::map<Node, Kind>::const_iterator it = d_symbolToBuiltinKind.find(op);
 842   if (it != d_symbolToBuiltinKind.end())
 843   {
 844     return it->second;
 845   }
 846   return UNDEFINED_KIND;
 847 }
 848
 849 Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
 850 {
 851   Assert(n.hasOperator());
 852   Assert(!n.isClosure());
 853   NodeManager* nm = NodeManager::currentNM();
 854   Kind k = n.getKind();
 855   std::stringstream opName;
 856   Trace("lfsc-term-process-debug2")
 857       << "getOperatorOfTerm " << n << " " << k << " "
 858       << (n.getMetaKind() == metakind::PARAMETERIZED) << " "
 859       << isIndexedOperatorKind(k) << std::endl;
 860   if (n.getMetaKind() == metakind::PARAMETERIZED)
 861   {
 862     Node op = n.getOperator();
 863     std::vector<Node> indices;
 864     if (isIndexedOperatorKind(k))
 865     {
 866       indices = getOperatorIndices(k, n.getOperator());
 867       // we must convert the name of indices on updaters and testers
 868       if (k == APPLY_UPDATER || k == APPLY_TESTER)
 869       {
 870         Assert(indices.size() == 1);
 871         // must convert to user name
 872         std::stringstream sss;
 873         sss << indices[0];
 874         TypeNode intType = nm->integerType();
 875         indices[0] =
 876             getSymbolInternal(k, intType, getNameForUserName(sss.str()));
 877       }
 878     }
 879     else if (op.getType().isFunction())
 880     {
 881       return op;
 882     }
 883     // note other kinds of functions (e.g. selectors and testers)
 884     std::vector<TypeNode> argTypes;
 885     for (const Node& nc : n)
 886     {
 887       argTypes.push_back(nc.getType());
 888     }
 889     TypeNode ftype = n.getType();
 890     if (!argTypes.empty())
 891     {
 892       ftype = nm->mkFunctionType(argTypes, ftype);
 893     }
 894     Node ret;
 895     if (isIndexedOperatorKind(k))
 896     {
 897       std::vector<TypeNode> itypes;
 898       for (const Node& i : indices)
 899       {
 900         itypes.push_back(i.getType());
 901       }
 902       if (!itypes.empty())
 903       {
 904         ftype = nm->mkFunctionType(itypes, ftype);
 905       }
 906       if (!macroApply)
 907       {
 908         if (k != APPLY_UPDATER && k != APPLY_TESTER)
 909         {
 910           opName << "f_";
 911         }
 912       }
 913       opName << printer::smt2::Smt2Printer::smtKindString(k);
 914     }
 915     else if (k == APPLY_CONSTRUCTOR)
 916     {
 917       unsigned index = DType::indexOf(op);
 918       const DType& dt = DType::datatypeOf(op);
 919       std::stringstream ssc;
 920       ssc << dt[index].getConstructor();
 921       opName << getNameForUserName(ssc.str());
 922     }
 923     else if (k == APPLY_SELECTOR)
 924     {
 925       unsigned index = DType::indexOf(op);
 926       const DType& dt = DType::datatypeOf(op);
 927       unsigned cindex = DType::cindexOf(op);
 928       std::stringstream sss;
 929       sss << dt[cindex][index].getSelector();
 930       opName << getNameForUserName(sss.str());
 931     }
 932     else if (k == APPLY_SELECTOR_TOTAL)
 933     {
 934       ret = maybeMkSkolemFun(op, macroApply);
 935       Assert(!ret.isNull());
 936     }
 937     else if (k == SET_SINGLETON || k == BAG_MAKE)
 938     {
 939       if (!macroApply)
 940       {
 941         opName << "f_";
 942       }
 943       opName << printer::smt2::Smt2Printer::smtKindString(k);
 944     }
 945     else
 946     {
 947       opName << op;
 948     }
 949     if (ret.isNull())
 950     {
 951       ret = getSymbolInternal(k, ftype, opName.str());
 952     }
 953     // if indexed, apply to index
 954     if (!indices.empty())
 955     {
 956       std::vector<Node> ichildren;
 957       ichildren.push_back(ret);
 958       ichildren.insert(ichildren.end(), indices.begin(), indices.end());
 959       ret = nm->mkNode(APPLY_UF, ichildren);
 960     }
 961     Trace("lfsc-term-process-debug2") << "...return " << ret << std::endl;
 962     return ret;
 963   }
 964   std::vector<TypeNode> argTypes;
 965   for (const Node& nc : n)
 966   {
 967     argTypes.push_back(nc.getType());
 968   }
 969   // we only use binary operators
 970   if (NodeManager::isNAryKind(k))
 971   {
 972     argTypes.resize(2);
 973   }
 974   TypeNode tn = n.getType();
 975   TypeNode ftype = nm->mkFunctionType(argTypes, tn);
 976   // most functions are called f_X where X is the SMT-LIB name, if we are
 977   // getting the macroApply variant, then we don't prefix with `f_`.
 978   if (!macroApply)
 979   {
 980     opName << "f_";
 981   }
 982   // all arithmetic kinds must explicitly deal with real vs int subtyping
 983   if (k == PLUS || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT
 984       || k == LEQ || k == LT || k == MINUS || k == DIVISION
 985       || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
 986       || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == UMINUS
 987       || k == POW)
 988   {
 989     // currently allow subtyping
 990     opName << "a.";
 991   }
 992   if (k == UMINUS)
 993   {
 994     opName << "u";
 995   }
 996   opName << printer::smt2::Smt2Printer::smtKindString(k);
 997   if (k == DIVISION_TOTAL || k == INTS_DIVISION_TOTAL
 998       || k == INTS_MODULUS_TOTAL)
 999   {
1000     opName << "_total";
1001   }
1002   return getSymbolInternal(k, ftype, opName.str());
1003 }
1004
1005 Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply)
1006 {
1007   NodeManager* nm = NodeManager::currentNM();
1008   TypeNode bodyType = nm->mkFunctionType(q[1].getType(), q.getType());
1009   // We permit non-flat function types here
1010   // intType is used here for variable indices
1011   TypeNode intType = nm->integerType();
1012   TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, bodyType);
1013   Kind k = q.getKind();
1014   std::stringstream opName;
1015   if (!macroApply)
1016   {
1017     opName << "f_";
1018   }
1019   opName << printer::smt2::Smt2Printer::smtKindString(k);
1020   return getSymbolInternal(k, ftype, opName.str());
1021 }
1022
1023 Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
1024 {
1025   NodeManager* nm = NodeManager::currentNM();
1026   Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v)));
1027   Node tc = typeAsNode(convertType(v.getType()));
1028   return nm->mkNode(APPLY_UF, cop, x, tc);
1029 }
1030
1031 size_t LfscNodeConverter::getOrAssignIndexForVar(Node v)
1032 {
1033   Assert(v.isVar());
1034   std::map<Node, size_t>::iterator it = d_varIndex.find(v);
1035   if (it != d_varIndex.end())
1036   {
1037     return it->second;
1038   }
1039   size_t id = d_varIndex.size();
1040   d_varIndex[v] = id;
1041   return id;
1042 }
1043
1044 }  // namespace proof
1045 }  // namespace cvc5