diff options
Diffstat (limited to 'src/proof/lfsc/lfsc_node_converter.cpp')
-rw-r--r-- | src/proof/lfsc/lfsc_node_converter.cpp | 59 |
1 files changed, 25 insertions, 34 deletions
diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 6eab9b036..5af1c2b7e 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -89,7 +89,7 @@ Node LfscNodeConverter::postConvert(Node n) } // bound variable v is (bvar x T) TypeNode intType = nm->integerType(); - Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n))); + Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(n))); Node tc = typeAsNode(convertType(tn)); TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn); Node bvarOp = getSymbolInternal(k, ftype, "bvar"); @@ -136,8 +136,7 @@ Node LfscNodeConverter::postConvert(Node n) TypeNode intType = nm->integerType(); TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn); Node var = mkInternalSymbol("var", varType); - Node index = - nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n))); + Node index = nm->mkConstInt(Rational(getOrAssignIndexForVar(n))); Node tc = typeAsNode(convertType(tn)); return nm->mkNode(APPLY_UF, var, index, tc); } @@ -176,7 +175,7 @@ Node LfscNodeConverter::postConvert(Node n) Node hconstf = getSymbolInternal(k, tnh, "apply"); return nm->mkNode(APPLY_UF, hconstf, n[0], n[1]); } - else if (k == CONST_RATIONAL || k == CAST_TO_REAL) + else if (k == CONST_RATIONAL || k == CONST_INTEGER || k == CAST_TO_REAL) { if (k == CAST_TO_REAL) { @@ -184,8 +183,9 @@ Node LfscNodeConverter::postConvert(Node n) do { n = n[0]; - Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL); - } while (n.getKind() != CONST_RATIONAL); + Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL + || n.getKind() == CONST_INTEGER); + } while (n.getKind() != CONST_RATIONAL && n.getKind() != CONST_INTEGER); } TypeNode tnv = nm->mkFunctionType(tn, tn); Node rconstf; @@ -198,7 +198,7 @@ Node LfscNodeConverter::postConvert(Node n) { // use LFSC syntax for mpz negation Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~"); - arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs())); + arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConstInt(r.abs())); } else { @@ -344,8 +344,8 @@ Node LfscNodeConverter::postConvert(Node n) Node rop = getSymbolInternal( k, relType, printer::smt2::Smt2Printer::smtKindString(k)); RegExpLoop op = n.getOperator().getConst<RegExpLoop>(); - Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc)); - Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc)); + Node n1 = nm->mkConstInt(Rational(op.d_loopMinOcc)); + 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) @@ -485,16 +485,14 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn) else if (k == BITVECTOR_TYPE) { tnn = d_typeKindToNodeCons[k]; - Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize())); + Node w = nm->mkConstInt(Rational(tn.getBitVectorSize())); tnn = nm->mkNode(APPLY_UF, tnn, w); } else if (k == FLOATINGPOINT_TYPE) { tnn = d_typeKindToNodeCons[k]; - Node e = nm->mkConst(CONST_RATIONAL, - Rational(tn.getFloatingPointExponentSize())); - Node s = nm->mkConst(CONST_RATIONAL, - Rational(tn.getFloatingPointSignificandSize())); + Node e = nm->mkConstInt(Rational(tn.getFloatingPointExponentSize())); + Node s = nm->mkConstInt(Rational(tn.getFloatingPointSignificandSize())); tnn = nm->mkNode(APPLY_UF, tnn, e, s); } else if (tn.getNumChildren() == 0) @@ -723,8 +721,7 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars) Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char"); for (unsigned i = 0, size = vec.size(); i < size; i++) { - Node cc = nm->mkNode( - APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i]))); + Node cc = nm->mkNode(APPLY_UF, aconstf, nm->mkConstInt(Rational(vec[i]))); chars.push_back(cc); } } @@ -747,42 +744,36 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n) case BITVECTOR_EXTRACT: { BitVectorExtract p = n.getConst<BitVectorExtract>(); - indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high))); - indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low))); + indices.push_back(nm->mkConstInt(Rational(p.d_high))); + indices.push_back(nm->mkConstInt(Rational(p.d_low))); break; } case BITVECTOR_REPEAT: - indices.push_back( - nm->mkConst(CONST_RATIONAL, - Rational(n.getConst<BitVectorRepeat>().d_repeatAmount))); + indices.push_back(nm->mkConstInt( + Rational(n.getConst<BitVectorRepeat>().d_repeatAmount))); break; case BITVECTOR_ZERO_EXTEND: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount))); break; case BITVECTOR_SIGN_EXTEND: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst<BitVectorSignExtend>().d_signExtendAmount))); break; case BITVECTOR_ROTATE_LEFT: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount))); break; case BITVECTOR_ROTATE_RIGHT: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst<BitVectorRotateRight>().d_rotateRightAmount))); break; case INT_TO_BITVECTOR: - indices.push_back(nm->mkConst( - CONST_RATIONAL, Rational(n.getConst<IntToBitVector>().d_size))); + indices.push_back( + nm->mkConstInt(Rational(n.getConst<IntToBitVector>().d_size))); break; case IAND: - indices.push_back( - nm->mkConst(CONST_RATIONAL, Rational(n.getConst<IntAnd>().d_size))); + indices.push_back(nm->mkConstInt(Rational(n.getConst<IntAnd>().d_size))); break; case APPLY_TESTER: { @@ -1023,7 +1014,7 @@ Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply) Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v) { NodeManager* nm = NodeManager::currentNM(); - Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v))); + Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(v))); Node tc = typeAsNode(convertType(v.getType())); return nm->mkNode(APPLY_UF, cop, x, tc); } |