diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/lfsc/lfsc_util.cpp | 88 | ||||
| -rw-r--r-- | src/proof/lfsc/lfsc_util.h | 105 | ||||
| -rw-r--r-- | src/proof/print_expr.cpp | 58 | ||||
| -rw-r--r-- | src/proof/print_expr.h | 86 | ||||
| -rw-r--r-- | src/proof/proof_checker.cpp | 7 | ||||
| -rw-r--r-- | src/proof/proof_checker.h | 11 | ||||
| -rw-r--r-- | src/proof/proof_letify.cpp | 124 | ||||
| -rw-r--r-- | src/proof/proof_letify.h | 98 | ||||
| -rw-r--r-- | src/proof/proof_rule.cpp | 4 | ||||
| -rw-r--r-- | src/proof/proof_rule.h | 29 |
10 files changed, 606 insertions, 4 deletions
diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp new file mode 100644 index 000000000..d8bd8f548 --- /dev/null +++ b/src/proof/lfsc/lfsc_util.cpp @@ -0,0 +1,88 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for LFSC proofs. + */ + +#include "proof/lfsc/lfsc_util.h" + +#include "proof/proof_checker.h" +#include "util/rational.h" + +namespace cvc5 { +namespace proof { + +const char* toString(LfscRule id) +{ + switch (id) + { + case LfscRule::SCOPE: return "scope"; + case LfscRule::NEG_SYMM: return "neg_symm"; + case LfscRule::CONG: return "cong"; + case LfscRule::AND_INTRO1: return "and_intro1"; + case LfscRule::AND_INTRO2: return "and_intro2"; + case LfscRule::NOT_AND_REV: return "not_and_rev"; + case LfscRule::PROCESS_SCOPE: return "process_scope"; + case LfscRule::ARITH_SUM_UB: return "arith_sum_ub"; + case LfscRule::INSTANTIATE: return "instantiate"; + case LfscRule::SKOLEMIZE: return "skolemize"; + case LfscRule::LAMBDA: return "\\"; + case LfscRule::PLET: return "plet"; + default: return "?"; + } +} +std::ostream& operator<<(std::ostream& out, LfscRule id) +{ + out << toString(id); + return out; +} + +bool getLfscRule(Node n, LfscRule& lr) +{ + uint32_t id; + if (ProofRuleChecker::getUInt32(n, id)) + { + lr = static_cast<LfscRule>(id); + return true; + } + return false; +} + +LfscRule getLfscRule(Node n) +{ + LfscRule lr = LfscRule::UNKNOWN; + getLfscRule(n, lr); + return lr; +} + +Node mkLfscRuleNode(LfscRule r) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(r))); +} + +bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) +{ + if (pn->getRule() == PfRule::SCOPE) + { + return false; + } + if (pn->getRule() != PfRule::LFSC_RULE) + { + return true; + } + // do not traverse under LFSC (lambda) scope + LfscRule lr = getLfscRule(pn->getArguments()[0]); + return lr != LfscRule::LAMBDA; +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_util.h b/src/proof/lfsc/lfsc_util.h new file mode 100644 index 000000000..c97c07489 --- /dev/null +++ b/src/proof/lfsc/lfsc_util.h @@ -0,0 +1,105 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for LFSC proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__LFSC__LFSC_UTIL_H +#define CVC5__PROOF__LFSC__LFSC_UTIL_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "proof/proof_letify.h" + +namespace cvc5 { +namespace proof { + +/** + * LFSC rules. The enum below contains all rules that don't correspond to a + * PfRule, e.g. congruence in LFSC does not have the same form as congruence + * in the internal calculus. + */ +enum class LfscRule : uint32_t +{ + //----------- translated rules + + // We defined LFSC versions for rules that either don't exist in the internal + // calculus, or have a different set of arugments/children. + + // scope has a different structure, e.g. uses lambdas + SCOPE, + // must distinguish equalities and disequalities + NEG_SYMM, + // congruence is done via a higher-order variant of congruence + CONG, + // we use unrolled binary versions of and intro + AND_INTRO1, + AND_INTRO2, + // needed as a helper for SCOPE + NOT_AND_REV, + PROCESS_SCOPE, + // arithmetic + ARITH_SUM_UB, + + // form of quantifier rules varies from internal calculus + INSTANTIATE, + SKOLEMIZE, + + // a lambda with argument + LAMBDA, + // a proof-let "plet" + PLET, + //----------- unknown + UNKNOWN, +}; + +/** + * Converts a lfsc rule to a string. Note: This function is also used in + * `safe_print()`. Changing this function name or signature will result in + * `safe_print()` printing "<unsupported>" instead of the proper strings for + * the enum values. + * + * @param id The lfsc rule + * @return The name of the lfsc rule + */ +const char* toString(LfscRule id); + +/** + * Writes a lfsc rule name to a stream. + * + * @param out The stream to write to + * @param id The lfsc rule to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, LfscRule id); +/** Get LFSC rule from a node */ +LfscRule getLfscRule(Node n); +/** Get LFSC rule from a node, return true if success and store in lr */ +bool getLfscRule(Node n, LfscRule& lr); +/** Make node for LFSC rule */ +Node mkLfscRuleNode(LfscRule r); + +/** Helper class used for letifying LFSC proofs. */ +class LfscProofLetifyTraverseCallback : public ProofLetifyTraverseCallback +{ + public: + bool shouldTraverse(const ProofNode* pn) override; +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/print_expr.cpp b/src/proof/print_expr.cpp new file mode 100644 index 000000000..becd9195a --- /dev/null +++ b/src/proof/print_expr.cpp @@ -0,0 +1,58 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for printing expressions in proofs + */ + +#include "proof/print_expr.h" + +namespace cvc5 { +namespace proof { + +PExprStream::PExprStream(std::vector<PExpr>& stream, Node tt, Node ff) + : d_stream(stream), d_tt(tt), d_ff(ff) +{ +} + +PExprStream& PExprStream::operator<<(const ProofNode* pn) +{ + d_stream.push_back(PExpr(pn)); + return *this; +} + +PExprStream& PExprStream::operator<<(Node n) +{ + d_stream.push_back(PExpr(n)); + return *this; +} + +PExprStream& PExprStream::operator<<(TypeNode tn) +{ + d_stream.push_back(PExpr(tn)); + return *this; +} + +PExprStream& PExprStream::operator<<(bool b) +{ + Assert(!d_tt.isNull() && !d_ff.isNull()); + d_stream.push_back(b ? d_tt : d_ff); + return *this; +} + +PExprStream& PExprStream::operator<<(PExpr p) +{ + d_stream.push_back(p); + return *this; +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/print_expr.h b/src/proof/print_expr.h new file mode 100644 index 000000000..15a8bb6c2 --- /dev/null +++ b/src/proof/print_expr.h @@ -0,0 +1,86 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for printing expressions in proofs + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PRINT_EXPR_H +#define CVC5__PROOF__PRINT_EXPR_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * A term, type or a proof. This class is used for printing combinations of + * proofs terms and types. + */ +class PExpr +{ + public: + PExpr() : d_node(), d_pnode(nullptr), d_typeNode() {} + PExpr(Node n) : d_node(n), d_pnode(nullptr), d_typeNode() {} + PExpr(const ProofNode* pn) : d_node(), d_pnode(pn), d_typeNode() {} + PExpr(TypeNode tn) : d_node(), d_pnode(nullptr), d_typeNode(tn) {} + ~PExpr() {} + /** The node, if this p-exression is a node */ + Node d_node; + /** The proof node, if this p-expression is a proof */ + const ProofNode* d_pnode; + /** The type node, if this p-expression is a type */ + TypeNode d_typeNode; +}; + +/** + * A stream of p-expressions, which appends p-expressions to a reference vector. + * That vector can then be used when printing a proof. + */ +class PExprStream +{ + public: + /** + * Takes a reference to a stream (vector of p-expressions), and the + * representation true/false (tt/ff). + */ + PExprStream(std::vector<PExpr>& stream, + Node tt = Node::null(), + Node ff = Node::null()); + /** Append a proof node */ + PExprStream& operator<<(const ProofNode* pn); + /** Append a node */ + PExprStream& operator<<(Node n); + /** Append a type node */ + PExprStream& operator<<(TypeNode tn); + /** Append a Boolean */ + PExprStream& operator<<(bool b); + /** Append a pexpr */ + PExprStream& operator<<(PExpr p); + + private: + /** Reference to the stream */ + std::vector<PExpr>& d_stream; + /** Builtin nodes for true and false */ + Node d_tt; + Node d_ff; +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 96f5197e3..6a9979f75 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -85,6 +85,11 @@ ProofCheckerStatistics::ProofCheckerStatistics() { } +ProofChecker::ProofChecker(uint32_t pclevel, theory::RewriteDb* rdb) + : d_pclevel(pclevel), d_rdb(rdb) +{ +} + Node ProofChecker::check(ProofNode* pn, Node expected) { return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); @@ -303,6 +308,8 @@ ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) return it->second; } +theory::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; } + uint32_t ProofChecker::getPedanticLevel(PfRule id) const { std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index ac5531bf4..f1f10eedb 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -29,6 +29,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class RewriteDb; +} + /** A virtual base class for checking a proof rule */ class ProofRuleChecker { @@ -101,7 +105,7 @@ class ProofCheckerStatistics class ProofChecker { public: - ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {} + ProofChecker(uint32_t pclevel = 0, theory::RewriteDb* rdb = nullptr); ~ProofChecker() {} /** * Return the formula that is proven by proof node pn, or null if pn is not @@ -162,7 +166,8 @@ class ProofChecker uint32_t plevel = 10); /** get checker for */ ProofRuleChecker* getCheckerFor(PfRule id); - + /** get the rewrite database */ + theory::RewriteDb* getRewriteDatabase(); /** * Get the pedantic level for id if it has been assigned a pedantic * level via registerTrustedChecker above, or zero otherwise. @@ -186,6 +191,8 @@ class ProofChecker std::map<PfRule, uint32_t> d_plevel; /** The pedantic level of this checker */ uint32_t d_pclevel; + /** Pointer to the rewrite database */ + theory::RewriteDb* d_rdb; /** * Check internal. This is used by check and checkDebug above. It writes * checking errors on out when enableOutput is true. We treat trusted checkers diff --git a/src/proof/proof_letify.cpp b/src/proof/proof_letify.cpp new file mode 100644 index 000000000..c6269631c --- /dev/null +++ b/src/proof/proof_letify.cpp @@ -0,0 +1,124 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for computing letification of proofs. + */ + +#include "proof/proof_letify.h" + +namespace cvc5 { +namespace proof { + +bool ProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) +{ + return pn->getRule() != PfRule::SCOPE; +} + +void ProofLetify::computeProofLet(const ProofNode* pn, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh, + ProofLetifyTraverseCallback* pltc) +{ + Assert(pletList.empty() && pletMap.empty()); + if (thresh == 0) + { + // value of 0 means do not introduce let + return; + } + std::vector<const ProofNode*> visitList; + std::map<const ProofNode*, size_t> pcount; + if (pltc == nullptr) + { + // use default callback + ProofLetifyTraverseCallback defaultPltc; + computeProofCounts(pn, visitList, pcount, &defaultPltc); + } + else + { + computeProofCounts(pn, visitList, pcount, pltc); + } + // Now populate the pletList and pletMap + convertProofCountToLet(visitList, pcount, pletList, pletMap, thresh); +} + +void ProofLetify::computeProofCounts(const ProofNode* pn, + std::vector<const ProofNode*>& visitList, + std::map<const ProofNode*, size_t>& pcount, + ProofLetifyTraverseCallback* pltc) +{ + std::map<const ProofNode*, size_t>::iterator it; + std::vector<const ProofNode*> visit; + const ProofNode* cur; + visit.push_back(pn); + do + { + cur = visit.back(); + it = pcount.find(cur); + if (it == pcount.end()) + { + pcount[cur] = 0; + if (!pltc->shouldTraverse(cur)) + { + // callback indicated we should not traverse + continue; + } + const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : pc) + { + visit.push_back(cp.get()); + } + } + else + { + if (it->second == 0) + { + visitList.push_back(cur); + } + pcount[cur]++; + visit.pop_back(); + } + } while (!visit.empty()); +} + +void ProofLetify::convertProofCountToLet( + const std::vector<const ProofNode*>& visitList, + const std::map<const ProofNode*, size_t>& pcount, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh) +{ + Assert(pletList.empty() && pletMap.empty()); + if (thresh == 0) + { + // value of 0 means do not introduce let + return; + } + // Assign ids for those whose count is > 1, traverse in reverse order + // so that deeper proofs are assigned lower identifiers + std::map<const ProofNode*, size_t>::const_iterator itc; + for (const ProofNode* pn : visitList) + { + itc = pcount.find(pn); + Assert(itc != pcount.end()); + if (itc->second >= thresh && pn->getRule() != PfRule::ASSUME) + { + pletList.push_back(pn); + // start with id 1 + size_t id = pletMap.size() + 1; + pletMap[pn] = id; + } + } +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/proof_letify.h b/src/proof/proof_letify.h new file mode 100644 index 000000000..cfe1259e5 --- /dev/null +++ b/src/proof/proof_letify.h @@ -0,0 +1,98 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for computing letification of proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_LETIFY_H +#define CVC5__PROOF__PROOF_LETIFY_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * A callback which asks whether a proof node should be traversed for + * proof letification. For example, this may make it so that SCOPE is not + * traversed. + */ +class ProofLetifyTraverseCallback +{ + public: + virtual ~ProofLetifyTraverseCallback() {} + /** + * Should we traverse proof node pn for letification? If this returns false, + * then pn is being treated as a black box for letification. + */ + virtual bool shouldTraverse(const ProofNode* pn); +}; + +/** + * Utilities for letification. + */ +class ProofLetify +{ + public: + /** + * Stores proofs in map that require letification, mapping them to a unique + * identifier. For each proof node in the domain of pletMap in the list + * pletList such that pletList[i] does not contain subproof pletList[j] for + * j>i. + * + * @param pn The proof node to letify + * @param pletList The list of proofs occurring in pn that should be letified + * @param pletMap Mapping from proofs in pletList to an identifier + * @param thresh The number of times a proof node has to occur to be added + * to pletList + * @param pltc A callback indicating whether to traverse a proof node during + * this call. + */ + static void computeProofLet(const ProofNode* pn, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh = 2, + ProofLetifyTraverseCallback* pltc = nullptr); + + private: + /** + * Convert a map from proof nodes to # occurrences (pcount) to a list + * pletList / pletMap as described in the method above, where thresh + * is the minimum number of occurrences to be added to the list. + */ + static void convertProofCountToLet( + const std::vector<const ProofNode*>& visitList, + const std::map<const ProofNode*, size_t>& pcount, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh = 2); + /** + * Compute the count of sub proof nodes in pn, store in pcount. Additionally, + * store each proof node in the domain of pcount in an order in visitList + * such that visitList[i] does not contain sub proof visitList[j] for j>i. + */ + static void computeProofCounts(const ProofNode* pn, + std::vector<const ProofNode*>& visitList, + std::map<const ProofNode*, size_t>& pcount, + ProofLetifyTraverseCallback* pltc); +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 7be07f7f5..7e1cdf8d3 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -47,6 +47,7 @@ const char* toString(PfRule id) case PfRule::TRUST_SUBS: return "TRUST_SUBS"; case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ"; + case PfRule::THEORY_INFERENCE: return "THEORY_INFERENCE"; //================================================= Boolean rules case PfRule::RESOLUTION: return "RESOLUTION"; case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; @@ -119,6 +120,7 @@ const char* toString(PfRule id) case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; + case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; @@ -200,6 +202,8 @@ const char* toString(PfRule id) return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; + //================================================= External rules + case PfRule::LFSC_RULE: return "LFSC_RULE"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 9625e1d28..78e773bdc 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -257,6 +257,8 @@ enum class PfRule : uint32_t // where F is a solved equality of the form (= x t) derived as the solved // form of F', where F' is given as a child. TRUST_SUBS_EQ, + // where F is a fact derived by a theory-specific inference + THEORY_INFERENCE, // ========= SAT Refutation for assumption-based unsat cores // Children: (P1, ..., Pn) // Arguments: none @@ -711,6 +713,15 @@ enum class PfRule : uint32_t // Conclusion: (not (= (select a k) (select b k))) // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). ARRAYS_EXT, + // ======== EQ_RANGE expansion + // Children: none + // Arguments: ((eqrange a b i j)) + // ---------------------------------------- + // Conclusion: (= + // (eqrange a b i j) + // (forall ((x T)) + // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x))))) + ARRAYS_EQ_RANGE_EXPAND, // ======== Array Trust // Children: (P1 ... Pn) // Arguments: (F) @@ -825,10 +836,16 @@ enum class PfRule : uint32_t SKOLEMIZE, // ======== Instantiate // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) - // Arguments: (t1 ... tn) + // Arguments: (t1 ... tn, (id (t)?)? ) // ---------------------------------------- // Conclusion: F*sigma - // sigma maps x1 ... xn to t1 ... tn. + // where sigma maps x1 ... xn to t1 ... tn. + // + // The optional argument id indicates the inference id that caused the + // instantiation. The term t indicates an additional term (e.g. the trigger) + // associated with the instantiation, which depends on the id. If the id + // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that + // generated the instantiation. INSTANTIATE, // ======== (Trusted) quantifiers preprocess // Children: ? @@ -1387,6 +1404,14 @@ enum class PfRule : uint32_t // that extends the Cell and satisfies all assumptions. ARITH_NL_CAD_RECURSIVE, + //================================================ Place holder for Lfsc rules + // ======== Lfsc rule + // Children: (P1 ... Pn) + // Arguments: (id, Q, A1, ..., Am) + // --------------------- + // Conclusion: (Q) + LFSC_RULE, + //================================================= Unknown rule UNKNOWN, }; |