diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-20 14:49:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-20 14:49:02 -0600 |
commit | 5489ef01beb91e256e343e2fd2d734b48b42ad6e (patch) | |
tree | f6a535c768ae4f3cfbbed765b0697300f4412657 /src/proof | |
parent | 32fdf625f66b8ebf260756962a53d63eec771c12 (diff) |
Remove front-end support for Chain (#3767)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/theory_proof.cpp | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 88a53062a..7e2ed84b1 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1050,42 +1050,6 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, return; } - case kind::CHAIN: { - // LFSC doesn't allow declarations with variable numbers of - // arguments, so we have to flatten chained operators, like =. - Kind op = term.getOperator().getConst<Chain>().getOperator(); - std::string op_str; - bool booleanCase = false; - if (op==kind::EQUAL && term[0].getType().isBoolean()) { - booleanCase = term[0].getType().isBoolean(); - op_str = "iff"; - } else { - op_str = utils::toLFSCKind(op); - } - size_t n = term.getNumChildren(); - std::ostringstream paren; - for(size_t i = 1; i < n; ++i) { - if(i + 1 < n) { - os << "(" << utils::toLFSCKind(kind::AND) << " "; - paren << ")"; - } - os << "(" << op_str << " "; - if (booleanCase && printsAsBool(term[i - 1])) os << "(p_app "; - printBoundTerm(term[i - 1], os, map); - if (booleanCase && printsAsBool(term[i - 1])) os << ")"; - os << " "; - if (booleanCase && printsAsBool(term[i])) os << "(p_app "; - printBoundTerm(term[i], os, map); - if (booleanCase && printsAsBool(term[i])) os << ")"; - os << ")"; - if(i + 1 < n) { - os << " "; - } - } - os << paren.str(); - return; - } - default: Unhandled() << k; } } |