From 0e38ef567365681e3305d69f5b57b399ff3367e9 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 7 Feb 2020 10:37:33 -0800 Subject: [PATCH] Propagate expected types through UF arguments (#3717) --- src/proof/uf_proof.cpp | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 3c4c7d381..214198756 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -628,32 +628,35 @@ void LFSCUFProof::printOwnedTermAsType(Expr term, const ProofLetMap& map, TypeNode expectedType) { - Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; + Node node = Node::fromExpr(term); + Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << node << std::endl; - Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF); + Assert(theory::Theory::theoryOf(node) == theory::THEORY_UF); - if (term.getKind() == kind::VARIABLE || - term.getKind() == kind::SKOLEM || - term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { - os << term; + if (node.getKind() == kind::VARIABLE || + node.getKind() == kind::SKOLEM || + node.getKind() == kind::BOOLEAN_TERM_VARIABLE) { + os << node; return; } - Assert(term.getKind() == kind::APPLY_UF); + Assert(node.getKind() == kind::APPLY_UF); - if(term.getType().isBoolean()) { + if(node.getType().isBoolean()) { os << "(p_app "; } - Expr func = term.getOperator(); + Node func = node.getOperator(); for (unsigned i = 0; i < term.getNumChildren(); ++i) { os << "(apply _ _ "; } os << func << " "; - for (unsigned i = 0; i < term.getNumChildren(); ++i) { + Assert(func.getType().isFunction()); + std::vector argsTypes = node.getOperator().getType().getArgTypes(); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { - bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i])); + bool convertToBool = (node[i].getType().isBoolean() && !d_proofEngine->printsAsBool(node[i])); if (convertToBool) os << "(f_to_b "; - d_proofEngine->printBoundTerm(term[i], os, map); + d_proofEngine->printBoundTerm(term[i], os, map, argsTypes[i]); if (convertToBool) os << ")"; os << ")"; } -- 2.30.2