diff options
Diffstat (limited to 'src/proof/lfsc/lfsc_printer.cpp')
| -rw-r--r-- | src/proof/lfsc/lfsc_printer.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 3772e2386..8c659dc0c 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -568,6 +568,15 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, pf << h << h << h << cs[0] << cs[1]; } break; + case PfRule::INT_TIGHT_UB: + case PfRule::INT_TIGHT_LB: + { + Node res = pn->getResult(); + Assert(res.getNumChildren() == 2); + Assert(res[1].getKind() == CONST_RATIONAL); + pf << h << h << d_tproc.convert(res[1]) << cs[0]; + } + break; // strings case PfRule::STRING_LENGTH_POS: pf << as[0]; break; case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << cs[0]; break; @@ -581,6 +590,8 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, case PfRule::CONCAT_CSPLIT: pf << h << h << h << h << args[0].getConst<bool>() << cs[0] << cs[1]; break; + case PfRule::CONCAT_CONFLICT: + pf << h << h << args[0].getConst<bool>() << cs[0]; break; case PfRule::RE_UNFOLD_POS: if (children[0]->getResult()[1].getKind() != REGEXP_CONCAT) |