diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 16:34:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 18:34:47 -0300 |
commit | 85a8dfddd887a041f397d1ff2c3a6c34900c5775 (patch) | |
tree | 81344647d0ac9c61040dfa3954c8200c8efbf561 /src/theory/uf | |
parent | bd184f9813a91d8f60eb0521893a5154b9f92357 (diff) |
(proof-new) Improve robustness of CONG rule (#4882)
This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/proof_checker.cpp | 22 |
1 files changed, 15 insertions, 7 deletions
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++) { |