From: Andrew Reynolds Date: Tue, 3 May 2022 19:47:44 +0000 (-0500) Subject: Use (non-recursive) unpurified form instead of original form for defining Skolems... X-Git-Tag: cvc5-1.0.1~181 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70b5c27382628cc0e3d7bf6cbae58c8532668023;p=cvc5.git Use (non-recursive) unpurified form instead of original form for defining Skolems (#8699) This modifies our treatment of purification Skolems in the internal proof calculus. In particular, we now use an "unpurified form" instead of "original form" for defining Skolems. SKOLEM_INTRO is modified to prove the equality between a skolem and its unpurified form. For example: k1 purifies (ite A B C) k2 purifies (+ k1 1) The unpurified form of k2 is (+ k1 1), its original form is (+ (ite A B C) 1). As a consequence: (1) Our global skolem sharing is now slightly weaker, for example a k3 could be constructed whose unpurified form is (+ (ite A B C) 1); previously this would guaranteed to be k1. (2) We do not require recursively computing the original form of terms when constructing purification Skolems, (3) The witness form proof generator requires a fix point. (4) The LFSC signature is simplified, and does not require a side condition to recursively compute the original form of a Skolem. Fixes cvc5/LFSC#81. --- diff --git a/proofs/lfsc/signatures/quantifiers_rules.plf b/proofs/lfsc/signatures/quantifiers_rules.plf index 6c30ca523..b7ab95b62 100644 --- a/proofs/lfsc/signatures/quantifiers_rules.plf +++ b/proofs/lfsc/signatures/quantifiers_rules.plf @@ -45,7 +45,5 @@ (! r (^ (sc_substitute body v s) bodyi) (holds (exists v u body)))))))))) -(declare skolem_intro (! u term - (! t term - (! r (^ (sc_mk_skolem t) u) - (holds (= u t)))))) +(declare skolem_intro (! t term + (holds (= (skolem t) t)))) diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf index e280bc77b..a110af913 100644 --- a/proofs/lfsc/signatures/strings_programs.plf +++ b/proofs/lfsc/signatures/strings_programs.plf @@ -16,6 +16,14 @@ (emptystr tt) (default ff))) +;;-------------------- Skolem terms +; The following side conditions are used for computing terms that define +; Skolems, which are used in reductions. Notice that Skolem terms may use +; terms that are not in original form, meaning that the definitions of Skolems +; may themselves contain Skolems. This is to avoid the use of a side condition +; for computing the original form of a term in the LFSC signature, which +; naively is exponential. + ; Get the term corresponding to the prefix of term s of fixed length n. (program sc_skolem_prefix ((s term) (n term)) term (str.substr s (int 0) n) @@ -34,7 +42,9 @@ ; Get the term corresponding to the suffix of s after the first occurrence of ; t in s. (program sc_skolem_first_ctn_post ((s term) (t term)) term - (sc_skolem_suffix_rem s (a.+ (str.len (sc_skolem_first_ctn_pre s t)) (a.+ (str.len t) (int 0))))) + (sc_skolem_suffix_rem s (a.+ (str.len (skolem (sc_skolem_first_ctn_pre s t))) (a.+ (str.len t) (int 0))))) + +;;-------------------- Utilities ; Head and tail for string concatenation. Fails if not a concatentation term. (program sc_string_head ((t term)) term (nary_head f_str.++ t)) @@ -62,15 +72,17 @@ ; Convert t into a str.++ application, if it is not already in n-ary form. (program sc_string_nary_intro ((t term) (u sort)) term (nary_intro f_str.++ t (sc_mk_emptystr u))) +;;-------------------- Reductions + ; In the following, a "reduction predicate" refers to a formula that is used ; to axiomatize an extended string function in terms of (simpler) functions. ; Compute the reduction predicate for (str.substr x n m) of sort s. (program sc_string_reduction_substr ((x term) (n term) (m term) (u sort)) term - (let k (sc_mk_skolem (str.substr x n m)) + (let k (skolem (str.substr x n m)) (let npm (a.+ n (a.+ m (int 0))) - (let k1 (sc_mk_skolem (sc_skolem_prefix x n)) - (let k2 (sc_mk_skolem (sc_skolem_suffix_rem x npm)) + (let k1 (skolem (sc_skolem_prefix x n)) + (let k2 (skolem (sc_skolem_suffix_rem x npm)) (ite ; condition (and (a.>= n (int 0)) @@ -92,10 +104,10 @@ ; Compute the reduction predicate for (str.indexof x y n) of sort s. (program sc_string_reduction_indexof ((x term) (y term) (n term) (u sort)) term - (let k (sc_mk_skolem (str.indexof x y n)) + (let k (skolem (str.indexof x y n)) (let xn (str.substr x n (a.- (str.len x) n)) - (let k1 (sc_mk_skolem (sc_skolem_first_ctn_pre xn y)) - (let k2 (sc_mk_skolem (sc_skolem_first_ctn_post xn y)) + (let k1 (skolem (sc_skolem_first_ctn_pre xn y)) + (let k2 (skolem (sc_skolem_first_ctn_post xn y)) (ite (or (not (str.contains xn y)) (or (a.> n (str.len x)) @@ -144,7 +156,7 @@ ; Returns the reduction predicate and purification equality for term t ; of sort s. (program sc_string_reduction ((t term) (u sort)) term - (and (sc_string_reduction_pred t u) (and (= t (sc_mk_skolem t)) true)) + (and (sc_string_reduction_pred t u) (and (= t (skolem t)) true)) ) ; Compute the eager reduction predicate for (str.contains t r) where s @@ -152,8 +164,8 @@ ; This is the formula: ; (ite (str.contains t r) (= t (str.++ sk1 r sk2)) (not (= t r))) (program sc_string_eager_reduction_contains ((t term) (r term) (u sort)) term - (let k1 (sc_mk_skolem (sc_skolem_first_ctn_pre t r)) - (let k2 (sc_mk_skolem (sc_skolem_first_ctn_post t r)) + (let k1 (skolem (sc_skolem_first_ctn_pre t r)) + (let k2 (skolem (sc_skolem_first_ctn_post t r)) (ite (str.contains t r) (= t (str.++ k1 (str.++ r (str.++ k2 (sc_mk_emptystr u))))) diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf index 46c6f67e8..6454de2fd 100644 --- a/proofs/lfsc/signatures/strings_rules.plf +++ b/proofs/lfsc/signatures/strings_rules.plf @@ -73,8 +73,8 @@ ((char n) (= thead (ifequal rev ff - (str.++ s12 (str.++ (sc_mk_skolem (sc_skolem_suffix_rem thead (int 1))) emptystr)) - (str.++ (sc_mk_skolem (sc_skolem_prefix thead (a.- (str.len thead) (int 1)))) (str.++ s12 emptystr))))))))) + (str.++ s12 (str.++ (skolem (sc_skolem_suffix_rem thead (int 1))) emptystr)) + (str.++ (skolem (sc_skolem_prefix thead (a.- (str.len thead) (int 1)))) (str.++ s12 emptystr))))))))) (fail term)))) ) diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf index 5880ab8fc..c645aeea7 100644 --- a/proofs/lfsc/signatures/util_defs.plf +++ b/proofs/lfsc/signatures/util_defs.plf @@ -69,13 +69,6 @@ (default t) )) -; Make a skolem, which ensures that the given term is in original form. For -; consistency, we require that the witness term for all Skolems are in -; original form. Failure to use this side condition when introducing fresh -; Skolems will result in proofs failing to check due to mismatched uses of -; Skolem variables in conclusions. -(program sc_mk_skolem ((t term)) term (skolem (sc_to_original t))) - ;; ---- Proof rules ; "proof-let", which is used to introduce a variable corresponding to the diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 4d5a53fd7..993d9b4d8 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -43,6 +43,11 @@ struct OriginalFormAttributeId }; typedef expr::Attribute OriginalFormAttribute; +struct UnpurifiedFormAttributeId +{ +}; +typedef expr::Attribute UnpurifiedFormAttribute; + struct AbstractValueId { }; @@ -220,16 +225,16 @@ Node SkolemManager::mkPurifySkolem(Node t, const std::string& comment, int flags) { - Node to = getOriginalForm(t); - // We do not currently insist that to does not contain witness terms - - Node k = mkSkolemInternal(to, prefix, comment, flags); - // set original form attribute for k - OriginalFormAttribute ofa; - k.setAttribute(ofa, to); + // We do not recursively compute the original form of t here + Node k = mkSkolemInternal(t, prefix, comment, flags); + // set unpurified form attribute for k + UnpurifiedFormAttribute ufa; + k.setAttribute(ufa, t); + // the original form of k can be computed by calling getOriginalForm, but + // it is not computed here Trace("sk-manager-skolem") - << "skolem: " << k << " purify " << to << std::endl; + << "skolem: " << k << " purify " << t << std::endl; return k; } @@ -325,6 +330,7 @@ Node SkolemManager::getOriginalForm(Node n) Trace("sk-manager-debug") << "SkolemManager::getOriginalForm " << n << std::endl; OriginalFormAttribute ofa; + UnpurifiedFormAttribute ufa; NodeManager* nm = NodeManager::currentNM(); std::unordered_map visited; std::unordered_map::iterator it; @@ -343,6 +349,25 @@ Node SkolemManager::getOriginalForm(Node n) { visited[cur] = cur.getAttribute(ofa); } + else if (cur.hasAttribute(ufa)) + { + // if it has an unpurified form, compute the original form of it + Node ucur = cur.getAttribute(ufa); + if (ucur.hasAttribute(ofa)) + { + // Already computed, set. This always happens after cur is visited + // again after computing the original form of its unpurified form. + Node ucuro = ucur.getAttribute(ofa); + cur.setAttribute(ofa, ucuro); + visited[cur] = ucuro; + } + else + { + // visit ucur then visit cur again + visit.push_back(cur); + visit.push_back(ucur); + } + } else { visited[cur] = Node::null(); @@ -392,6 +417,16 @@ Node SkolemManager::getOriginalForm(Node n) return visited[n]; } +Node SkolemManager::getUnpurifiedForm(Node k) +{ + UnpurifiedFormAttribute ufa; + if (k.hasAttribute(ufa)) + { + return k.getAttribute(ufa); + } + return k; +} + Node SkolemManager::mkSkolemInternal(Node w, const std::string& prefix, const std::string& comment, diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 5736b1722..2480d1d0c 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -340,22 +340,19 @@ class SkolemManager int flags = SKOLEM_DEFAULT, ProofGenerator* pg = nullptr); /** - * Same as above, but for special case of (witness ((x T)) (= x t)) - * where T is the type of t. This skolem is unique for each t, which we + * Make purification skolem. This skolem is unique for each t, which we * implement via an attribute on t. This attribute is used to ensure to * associate a unique skolem for each t. * - * Notice that a purification skolem is trivial to justify, and hence it - * does not require a proof generator. + * Notice that a purification skolem is trivial to justify (via SKOLEM_INTRO), + * and hence it does not require a proof generator. * - * Notice that in very rare cases, two different terms may have the - * same purification skolem. For example, let k be the skolem introduced to - * eliminate (ite A B C). Then, the pair of terms: + * Notice that we do not convert t to original form in this call. Thus, + * in very rare cases, two Skolems may be introduced that have the same + * original form. For example, let k be the skolem introduced to eliminate + * (ite A B C). Then, asking for the purify skolem for: * (ite (ite A B C) D E) and (ite k D E) - * have the same purification skolem. In the implementation, this is a result - * of the fact that the above terms have the same original form. It is sound - * to use the same skolem to purify these two terms, since they are - * definitionally equivalent. + * will return two different Skolems. */ Node mkPurifySkolem(Node t, const std::string& prefix, @@ -452,6 +449,17 @@ class SkolemManager * @return n in original form. */ static Node getOriginalForm(Node n); + /** + * Convert to unpurified form, which returns the term that k purifies. This + * is literally the term that was passed as an argument to mkPurify on the + * call that created k. In contrast to getOriginalForm, this is not recursive + * w.r.t. skolems, so that the term purified by k may itself contain + * purification skolems that are not expanded. + * + * @param k The skolem to convert to unpurified form + * @return the unpurified form of k. + */ + static Node getUnpurifiedForm(Node k); private: /** Cache of skolem functions for mkSkolemFunction above. */ diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 6cd2d56eb..8c4261f4c 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -132,7 +132,7 @@ Node LfscNodeConverter::postConvert(Node n) } // skolems v print as their witness forms // v is (skolem W) where W is the original or witness form of v - Node wi = SkolemManager::getOriginalForm(n); + Node wi = SkolemManager::getUnpurifiedForm(n); if (wi == n) { // if it is not a purification skolem, maybe it is a witness skolem diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 59230870b..ad5cd5347 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -683,7 +683,7 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, // quantifiers case PfRule::SKOLEM_INTRO: { - pf << h << d_tproc.convert(SkolemManager::getOriginalForm(args[0])); + pf << d_tproc.convert(SkolemManager::getUnpurifiedForm(args[0])); } break; // ---------- arguments of non-translated rules go here diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 7bfb389d5..0ef84f232 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1313,7 +1313,7 @@ enum class PfRule : uint32_t * * \inferrule{-\mid k}{k = t} * - * where :math:`t` is the original form of skolem :math:`k`. + * where :math:`t` is the unpurified form of skolem :math:`k`. * \endverbatim */ SKOLEM_INTRO, diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 7c64802ba..36dc798cf 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -86,24 +86,27 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) { d_visited.insert(cur); curw = SkolemManager::getOriginalForm(cur); - // if its witness form is different + // if its original form is different if (cur != curw) { if (cur.isVar()) { + curw = SkolemManager::getUnpurifiedForm(cur); Node eq = cur.eqNode(curw); - // equality between a variable and its original form + // equality between a variable and its unpurified form d_eqs.insert(eq); // ------- SKOLEM_INTRO // k = t d_wintroPf.addStep(eq, PfRule::SKOLEM_INTRO, {}, {cur}); d_tcpg.addRewriteStep( cur, curw, &d_wintroPf, true, PfRule::ASSUME, true); + // recursively transform + visit.push_back(curw); } else { - // A term whose witness form is different from itself, recurse. - // It should be the case that cur has children, since the witness + // A term whose original form is different from itself, recurse. + // It should be the case that cur has children, since the original // form of constants are themselves. Assert(cur.getNumChildren() > 0); if (cur.hasOperator()) diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 5c418edb2..d9da511e4 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -45,7 +45,7 @@ Node QuantifiersProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 1); - Node t = SkolemManager::getOriginalForm(args[0]); + Node t = SkolemManager::getUnpurifiedForm(args[0]); return args[0].eqNode(t); } else if (id == PfRule::SKOLEMIZE)