summaryrefslogtreecommitdiff
path: root/src/proof/lfsc/lfsc_node_converter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/lfsc/lfsc_node_converter.cpp')
-rw-r--r--src/proof/lfsc/lfsc_node_converter.cpp59
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback