diff options
| -rw-r--r-- | src/expr/proof_rule.h | 9 | ||||
| -rw-r--r-- | src/theory/uf/proof_checker.cpp | 22 |
2 files changed, 21 insertions, 10 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index beff92bd4..364598cf4 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -481,11 +481,14 @@ enum class PfRule : uint32_t // ----------------------- // Conclusion: (= t1 tn) TRANS, - // ======== Congruence (subsumed by Substitute?) + // ======== Congruence // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) - // Arguments: (f) + // Arguments: (<kind> f?) // --------------------------------------------- - // Conclusion: (= (f t1 ... tn) (f s1 ... sn)) + // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn)) + // Notice that f must be provided iff <kind> is a parameterized kind, e.g. + // APPLY_UF. The actual node for <kind> is constructible via + // ProofRuleChecker::mkKindNode. CONG, // ======== True intro // Children: (P:F) diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp index f866e77dd..b010b6d17 100644 --- a/src/theory/uf/proof_checker.cpp +++ b/src/theory/uf/proof_checker.cpp @@ -86,15 +86,15 @@ Node UfProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::CONG) { Assert(children.size() > 0); - Assert(args.size() == 1); + Assert(args.size() >= 1 && args.size() <= 2); // We do congruence over builtin kinds using operatorToKind std::vector<Node> lchildren; std::vector<Node> rchildren; - // get the expected kind for args[0] - Kind k = NodeManager::getKindForFunction(args[0]); - if (k == kind::UNDEFINED_KIND) + // get the kind encoded as args[0] + Kind k; + if (!getKind(args[0], k)) { - k = NodeManager::operatorToKind(args[0]); + return Node::null(); } if (k == kind::UNDEFINED_KIND) { @@ -104,9 +104,17 @@ Node UfProofRuleChecker::checkInternal(PfRule id, << ", metakind=" << kind::metaKindOf(k) << std::endl; if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED) { + if (args.size() <= 1) + { + return Node::null(); + } // parameterized kinds require the operator - lchildren.push_back(args[0]); - rchildren.push_back(args[0]); + lchildren.push_back(args[1]); + rchildren.push_back(args[1]); + } + else if (args.size() > 1) + { + return Node::null(); } for (size_t i = 0, nchild = children.size(); i < nchild; i++) { |