diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-11-02 16:45:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-02 16:45:44 -0500 |
commit | 0c16abf2d7fe9a18494d3c9867567c43a1655200 (patch) | |
tree | 872289a5e10301a5602979860fd473f0ea2eb5c7 /src/printer | |
parent | 51382b96a76c6ddef0c1a6aae2139203f20bced1 (diff) |
Move `fmf.card` printing code. (#7559)
The code for printing fmf.card does not run in its current location. This PR moves the code to a different switch statement to ensure that it runs.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d6e6fc4eb..da8e56448 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -332,13 +332,6 @@ void Smt2Printer::toStream(std::ostream& out, out << ss.str(); break; } - case kind::CARDINALITY_CONSTRAINT: - out << "(_ fmf.card "; - out << n.getConst<CardinalityConstraint>().getType(); - out << " "; - out << n.getConst<CardinalityConstraint>().getUpperBound(); - out << ")"; - break; case kind::EMPTYSET: out << "(as emptyset "; toStreamType(out, n.getConst<EmptySet>().getType()); @@ -818,6 +811,15 @@ void Smt2Printer::toStream(std::ostream& out, out << "(as sep.nil " << n.getType() << ")"; break; + // cardinality constraints. + case kind::CARDINALITY_CONSTRAINT: + out << "(_ fmf.card "; + out << n.getOperator().getConst<CardinalityConstraint>().getType(); + out << " "; + out << n.getOperator().getConst<CardinalityConstraint>().getUpperBound(); + out << ")"; + return; + // quantifiers case kind::FORALL: case kind::EXISTS: |