diff options
-rw-r--r-- | src/expr/proof_rule.cpp | 2 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 34 | ||||
-rw-r--r-- | src/expr/skolem_manager.cpp | 157 | ||||
-rw-r--r-- | src/expr/skolem_manager.h | 72 | ||||
-rw-r--r-- | src/smt/quant_elim_solver.cpp | 2 | ||||
-rw-r--r-- | src/smt/witness_form.cpp | 40 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/proof_checker.cpp | 20 |
8 files changed, 132 insertions, 203 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 0b7c8cc69..579b06c76 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -127,7 +127,7 @@ const char* toString(PfRule id) case PfRule::DT_CLASH: return "DT_CLASH"; case PfRule::DT_TRUST: return "DT_TRUST"; //================================================= Quantifiers rules - case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; + case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; case PfRule::SKOLEMIZE: return "SKOLEMIZE"; case PfRule::INSTANTIATE: return "INSTANTIATE"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index b25866b5e..909f7b7cd 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -133,16 +133,16 @@ enum class PfRule : uint32_t // where ids and idr are method identifiers. // // More generally, this rule also holds when: - // Rewriter::rewrite(toWitness(F')) == true + // Rewriter::rewrite(toOriginal(F')) == true // where F' is the result of the left hand side of the equality above. Here, - // notice that we apply rewriting on the witness form of F', meaning that this - // rule may conclude an F whose Skolem form is justified by the definition of - // its (fresh) Skolem variables. For example, this rule may justify the - // conclusion (= k t) where k is the purification Skolem for t, whose - // witness form is (witness ((x T)) (= x t)). + // notice that we apply rewriting on the original form of F', meaning that + // this rule may conclude an F whose Skolem form is justified by the + // definition of its (fresh) Skolem variables. For example, this rule may + // justify the conclusion (= k t) where k is the purification Skolem for t, + // e.g. where the original form of k is t. // // Furthermore, notice that the rewriting and substitution is applied only - // within the side condition, meaning the rewritten form of the witness form + // within the side condition, meaning the rewritten form of the original form // of F does not escape this rule. MACRO_SR_PRED_INTRO, // ======== Substitution + Rewriting predicate elimination @@ -176,9 +176,9 @@ enum class PfRule : uint32_t // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1)) // // More generally, this rule also holds when: - // Rewriter::rewrite(toWitness(F')) == Rewriter::rewrite(toWitness(G')) + // Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G')) // where F' and G' are the result of each side of the equation above. Here, - // witness forms are used in a similar manner to MACRO_SR_PRED_INTRO above. + // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. MACRO_SR_PRED_TRANSFORM, //================================================= Processing rules @@ -759,13 +759,13 @@ enum class PfRule : uint32_t DT_TRUST, //================================================= Quantifiers rules - // ======== Witness intro - // Children: (P:(exists ((x T)) F[x])) - // Arguments: none + // ======== Skolem intro + // Children: none + // Arguments: (k) // ---------------------------------------- - // Conclusion: (= k (witness ((x T)) F[x])) - // where k is the Skolem form of (witness ((x T)) F[x]). - WITNESS_INTRO, + // Conclusion: (= k t) + // where t is the original form of skolem k. + SKOLEM_INTRO, // ======== Exists intro // Children: (P:F[t]) // Arguments: ((exists ((x T)) F[x])) @@ -781,7 +781,9 @@ enum class PfRule : uint32_t // Conclusion: F*sigma // sigma maps x1 ... xn to their representative skolems obtained by // SkolemManager::mkSkolemize, returned in the skolems argument of that - // method. Alternatively, can use negated forall as a premise. + // method. Alternatively, can use negated forall as a premise. The witness + // terms for the returned skolems can be obtained by + // SkolemManager::getWitnessForm. SKOLEMIZE, // ======== Instantiate // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 3f77a170a..23ae919d3 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -22,17 +22,6 @@ using namespace CVC4::kind; namespace CVC4 { -/** - * Attribute for associating terms to a unique bound variable. This - * is used to construct canonical bound variables e.g. for constructing - * bound variables for witness terms in the skolemize method below. - */ -struct WitnessBoundVarAttributeId -{ -}; -typedef expr::Attribute<WitnessBoundVarAttributeId, Node> - WitnessBoundVarAttribute; - // Attributes are global maps from Nodes to data. Thus, note that these could // be implemented as internal maps in SkolemManager. struct WitnessFormAttributeId @@ -45,11 +34,10 @@ struct SkolemFormAttributeId }; typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute; -// Maps terms to their purify skolem variables -struct PurifySkolemAttributeId +struct OriginalFormAttributeId { }; -typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute; +typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute; Node SkolemManager::mkSkolem(Node v, Node pred, @@ -59,25 +47,31 @@ Node SkolemManager::mkSkolem(Node v, ProofGenerator* pg, bool retWitness) { + // We do not currently insist that pred does not contain witness terms Assert(v.getKind() == BOUND_VARIABLE); // make the witness term NodeManager* nm = NodeManager::currentNM(); Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - // translate pred to witness form, since pred itself may contain skolem - Node predw = getWitnessForm(pred); - // make the witness term, which should not contain any skolem - Node w = nm->mkNode(WITNESS, bvl, predw); + // Make the witness term, where notice that pred may contain skolems. We do + // not recursively convert pred to witness form, since witness terms should + // be treated as opaque. Moreover, the use of witness forms leads to + // variable shadowing issues in e.g. skolemization. + Node w = nm->mkNode(WITNESS, bvl, pred); // store the mapping to proof generator if it exists if (pg != nullptr) { - // We cache based on the original (Skolem) form, since the user of this - // method operates on Skolem forms. + // We cache based on the existential of the original predicate Node q = nm->mkNode(EXISTS, bvl, pred); // Notice this may overwrite an existing proof generator. This does not // matter since either should be able to prove q. d_gens[q] = pg; } - Node k = getOrMakeSkolem(w, prefix, comment, flags); + Node k = mkSkolemInternal(w, prefix, comment, flags); + // set witness form attribute for k + WitnessFormAttribute wfa; + k.setAttribute(wfa, w); + Trace("sk-manager-skolem") + << "skolem: " << k << " witness " << w << std::endl; // if we want to return the witness term, make it if (retWitness) { @@ -124,10 +118,8 @@ Node SkolemManager::skolemize(Node q, Assert(q.getKind() == EXISTS); Node v; std::vector<Node> ovars; - std::vector<Node> ovarsW; Trace("sk-manager-debug") << "mkSkolemize..." << std::endl; NodeManager* nm = NodeManager::currentNM(); - BoundVarManager* bvm = nm->getBoundVarManager(); for (const Node& av : q[0]) { if (v.isNull()) @@ -135,26 +127,17 @@ Node SkolemManager::skolemize(Node q, v = av; continue; } - // must make fresh variable to avoid shadowing, which is unique per - // variable av to ensure that this method is deterministic. Having this - // method deterministic ensures that the proof checker (e.g. for - // quantifiers) is capable of proving the expected value for conclusions - // of proof rules, instead of an alpha-equivalent variant of a conclusion. - Node avp = bvm->mkBoundVar<WitnessBoundVarAttribute>(av, av.getType()); - ovarsW.push_back(avp); ovars.push_back(av); } Assert(!v.isNull()); + // make the predicate with one variable stripped off Node pred = q[1]; - qskolem = q[1]; Trace("sk-manager-debug") << "make exists predicate" << std::endl; if (!ovars.empty()) { - // skolem form keeps the old variables + // keeps the same variables Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars); - qskolem = nm->mkNode(EXISTS, bvl, pred); // update the predicate - bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW); pred = nm->mkNode(EXISTS, bvl, pred); } Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl; @@ -166,7 +149,8 @@ Node SkolemManager::skolemize(Node q, TNode tk = k; Trace("sk-manager-debug") << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl; - qskolem = qskolem.substitute(tv, tk); + // the quantified formula with one step of skolemization + qskolem = pred.substitute(tv, tk); Trace("sk-manager-debug") << "qskolem done substitution" << std::endl; return k; } @@ -176,20 +160,16 @@ Node SkolemManager::mkPurifySkolem(Node t, const std::string& comment, int flags) { - PurifySkolemAttribute psa; - if (t.hasAttribute(psa)) - { - return t.getAttribute(psa); - } - // The case where t is a witness term is special: we set its Skolem attribute - // directly. - if (t.getKind() == WITNESS) - { - return getOrMakeSkolem(getWitnessForm(t), prefix, comment, flags); - } - Node v = NodeManager::currentNM()->mkBoundVar(t.getType()); - Node k = mkSkolem(v, v.eqNode(t), prefix, comment, flags); - t.setAttribute(psa, k); + 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); + + Trace("sk-manager-skolem") + << "skolem: " << k << " purify " << to << std::endl; return k; } @@ -208,20 +188,23 @@ ProofGenerator* SkolemManager::getProofGenerator(Node t) const return nullptr; } -Node SkolemManager::getWitnessForm(Node n) { return convertInternal(n, true); } - -Node SkolemManager::getSkolemForm(Node n) { return convertInternal(n, false); } +Node SkolemManager::getWitnessForm(Node k) +{ + Assert(k.getKind() == SKOLEM); + // simply look up the witness form for k via an attribute + WitnessFormAttribute wfa; + return k.getAttribute(wfa); +} -Node SkolemManager::convertInternal(Node n, bool toWitness) +Node SkolemManager::getOriginalForm(Node n) { if (n.isNull()) { return n; } - Trace("sk-manager-debug") << "SkolemManager::convertInternal: " << toWitness - << " " << n << std::endl; - WitnessFormAttribute wfa; - SkolemFormAttribute sfa; + Trace("sk-manager-debug") + << "SkolemManager::getOriginalForm " << n << std::endl; + OriginalFormAttribute ofa; NodeManager* nm = NodeManager::currentNM(); std::unordered_map<TNode, Node, TNodeHashFunction> visited; std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; @@ -236,13 +219,9 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) if (it == visited.end()) { - if (toWitness && cur.hasAttribute(wfa)) - { - visited[cur] = cur.getAttribute(wfa); - } - else if (!toWitness && cur.hasAttribute(sfa)) + if (cur.hasAttribute(ofa)) { - visited[cur] = cur.getAttribute(sfa); + visited[cur] = cur.getAttribute(ofa); } else { @@ -283,24 +262,7 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) { ret = nm->mkNode(cur.getKind(), children); } - if (toWitness) - { - cur.setAttribute(wfa, ret); - } - else - { - // notice that WITNESS terms t may be assigned a skolem form that is - // of kind WITNESS here, if t contains a free variable. This is due to - // the fact that witness terms in the bodies of quantified formulas are - // not eliminated and thus may appear in places where getSkolemForm is - // called on them. Regardless, witness terms with free variables - // should never be themselves assigned skolems (otherwise we would have - // assertions with free variables), and thus they can be treated like - // ordinary terms here. We use an assertion to check that this is - // indeed the case. - Assert(cur.getKind() != WITNESS || expr::hasFreeVar(cur)); - cur.setAttribute(sfa, ret); - } + cur.setAttribute(ofa, ret); visited[cur] = ret; } } while (!visit.empty()); @@ -310,36 +272,22 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) return visited[n]; } -void SkolemManager::convertToWitnessFormVec(std::vector<Node>& vec) +Node SkolemManager::mkSkolemInternal(Node w, + const std::string& prefix, + const std::string& comment, + int flags) { - for (unsigned i = 0, nvec = vec.size(); i < nvec; i++) - { - vec[i] = getWitnessForm(vec[i]); - } -} -void SkolemManager::convertToSkolemFormVec(std::vector<Node>& vec) -{ - for (unsigned i = 0, nvec = vec.size(); i < nvec; i++) - { - vec[i] = getSkolemForm(vec[i]); - } -} - -Node SkolemManager::getOrMakeSkolem(Node w, - const std::string& prefix, - const std::string& comment, - int flags) -{ - Assert(w.getKind() == WITNESS); + // note that witness, original forms are independent, but share skolems + NodeManager* nm = NodeManager::currentNM(); + // w is not necessarily a witness term SkolemFormAttribute sfa; + Node k; // could already have a skolem if we used w already if (w.hasAttribute(sfa)) { return w.getAttribute(sfa); } - NodeManager* nm = NodeManager::currentNM(); // make the new skolem - Node k; if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR) { Assert (w.getType().isBoolean()); @@ -349,9 +297,6 @@ Node SkolemManager::getOrMakeSkolem(Node w, { k = nm->mkSkolem(prefix, w.getType(), comment, flags); } - // set witness form attribute for k - WitnessFormAttribute wfa; - k.setAttribute(wfa, w); // set skolem form attribute for w w.setAttribute(sfa, k); Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 6e44db263..1a78bfc83 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -32,9 +32,30 @@ class ProofGenerator; * predicate that the introduced variable is intended to witness. * * It is implemented by mapping terms to an attribute corresponding to their - * "witness form" as described below. Hence, this class does not impact the - * reference counting of skolem variables which may be deleted if they are not - * used. + * "original form" and "witness form" as described below. Hence, this class does + * not impact the reference counting of skolem variables which may be deleted if + * they are not used. + * + * We distinguish two kinds of mappings between terms and skolems: + * + * (1) "Original form", which associates skolems with the terms they purify. + * This is used in mkPurifySkolem below. + * + * (2) "Witness form", which associates skolems with their formal definition + * as a witness term. This is used in mkSkolem below. + * + * It is possible to unify these so that purification skolems for t are skolems + * whose witness form is (witness ((x T)) (= x t)). However, there are + * motivations not to do so. In particular, witness terms in most contexts + * should be seen as black boxes, converting something to witness form may have + * unintended consequences e.g. variable shadowing. In contrast, converting to + * original form does not have these complications. Furthermore, having original + * form greatly simplifies reasoning in the proof, in particular, it avoids the + * need to reason about identifiers for introduced variables x. + * + * Furthermore, note that original form and witness form may share skolems + * in the rare case that a witness term is purified. This is currently only the + * case for algorithms that introduce witness, e.g. BV/set instantiation. */ class SkolemManager { @@ -110,10 +131,13 @@ class SkolemManager * returns: * (P w1 w2) * where w1 and w2 are skolems with witness forms: - * (witness ((x Int)) (exists ((y' Int)) (P x y'))) + * (witness ((x Int)) (exists ((y Int)) (P x y))) * (witness ((y Int)) (P w1 y)) * respectively. Additionally, this method will add { w1, w2 } to skolems. - * Notice that y is renamed to y' in the witness form of w1 to avoid variable + * Notice that y is *not* renamed in the witness form of w1. This is not + * necessary since w1 is skolem. Although its witness form contains + * quantification on y, we never construct a term where the witness form + * of w1 is expanded in the witness form of w2. This avoids variable * shadowing. * * In contrast to mkSkolem, the proof generator is for the *entire* @@ -161,39 +185,33 @@ class SkolemManager */ ProofGenerator* getProofGenerator(Node q) const; /** - * Convert to witness form, where notice this recursively replaces *all* - * skolems in n by their corresponding witness term. This is intended to be - * used by the proof checker only. + * Convert to witness form, which gets the witness form of a skolem k. + * Notice this method is *not* recursive, instead, it is a simple attribute + * lookup. * - * @param n The term or formula to convert to witness form described above - * @return n in witness form. + * @param k The variable to convert to witness form described above + * @return k in witness form. */ - static Node getWitnessForm(Node n); + static Node getWitnessForm(Node k); /** - * Convert to Skolem form, which recursively replaces all witness terms in n - * by their corresponding Skolems. + * Convert to original form, which recursively replaces all skolems terms in n + * by the term they purify. * - * @param n The term or formula to convert to Skolem form described above - * @return n in Skolem form. + * @param n The term or formula to convert to original form described above + * @return n in original form. */ - static Node getSkolemForm(Node n); - /** convert to witness form vector */ - static void convertToWitnessFormVec(std::vector<Node>& vec); - /** convert to Skolem form vector */ - static void convertToSkolemFormVec(std::vector<Node>& vec); + static Node getOriginalForm(Node n); private: /** * Mapping from witness terms to proof generators. */ std::map<Node, ProofGenerator*> d_gens; - /** Convert to witness or skolem form */ - static Node convertInternal(Node n, bool toWitness); - /** Get or make skolem attribute for witness term w */ - static Node getOrMakeSkolem(Node w, - const std::string& prefix, - const std::string& comment, - int flags); + /** Get or make skolem attribute for term w, which may be a witness term */ + static Node mkSkolemInternal(Node w, + const std::string& prefix, + const std::string& comment, + int flags); /** * Skolemize the first variable of existentially quantified formula q. * For example, calling this method on: diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index bc62448fe..9a0178cfe 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -131,7 +131,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // internally generated skolems should not escape if (!isInternalSubsolver) { - ret = SkolemManager::getWitnessForm(ret); + ret = SkolemManager::getOriginalForm(ret); } return ret; } diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 603e6e60c..a339210c0 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -59,9 +59,7 @@ std::string WitnessFormGenerator::identify() const Node WitnessFormGenerator::convertToWitnessForm(Node t) { - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* skm = nm->getSkolemManager(); - Node tw = SkolemManager::getWitnessForm(t); + Node tw = SkolemManager::getOriginalForm(t); if (t == tw) { // trivial case @@ -80,44 +78,18 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) if (it == d_visited.end()) { d_visited.insert(cur); - curw = SkolemManager::getWitnessForm(cur); + curw = SkolemManager::getOriginalForm(cur); // if its witness form is different if (cur != curw) { if (cur.isVar()) { Node eq = cur.eqNode(curw); - // equality between a variable and its witness form + // equality between a variable and its original form d_eqs.insert(eq); - Assert(curw.getKind() == kind::WITNESS); - Node skBody = SkolemManager::getSkolemForm(curw[1]); - Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody); - ProofGenerator* pg = skm->getProofGenerator(exists); - if (pg == nullptr) - { - // it may be a purification skolem - pg = convertExistsInternal(exists); - if (pg == nullptr) - { - // if no proof generator is provided, we justify the existential - // using the WITNESS_AXIOM trusted rule by providing it to the - // call to addLazyStep below. - Trace("witness-form") - << "WitnessFormGenerator: No proof generator for " << exists - << std::endl; - } - } - // --------------------------- from pg - // (exists ((x T)) (P x)) - // --------------------------- WITNESS_INTRO - // k = (witness ((x T)) (P x)) - d_wintroPf.addLazyStep( - exists, - pg, - PfRule::WITNESS_AXIOM, - true, - "WitnessFormGenerator::convertToWitnessForm:witness_axiom"); - d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); + // ------- SKOLEM_INTRO + // k = t + d_wintroPf.addStep(eq, PfRule::SKOLEM_INTRO, {}, {cur}); d_tcpg.addRewriteStep( cur, curw, &d_wintroPf, true, PfRule::ASSUME, true); } diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 75f93af47..5d05e5383 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -350,10 +350,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } Trace("builtin-pfcheck") << "Result is " << res << std::endl; Trace("builtin-pfcheck") << "Witness form is " - << SkolemManager::getWitnessForm(res) << std::endl; + << SkolemManager::getOriginalForm(res) << std::endl; // **** NOTE: can rewrite the witness form here. This enables certain lemmas // to be provable, e.g. (= k t) where k is a purification Skolem for t. - res = Rewriter::rewrite(SkolemManager::getWitnessForm(res)); + res = Rewriter::rewrite(SkolemManager::getOriginalForm(res)); if (!res.isConst() || !res.getConst<bool>()) { Trace("builtin-pfcheck") @@ -400,8 +400,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, if (res1 != res2) { // can rewrite the witness forms - res1 = Rewriter::rewrite(SkolemManager::getWitnessForm(res1)); - res2 = Rewriter::rewrite(SkolemManager::getWitnessForm(res2)); + res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1)); + res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2)); if (res1.isNull() || res1 != res2) { Trace("builtin-pfcheck") << "Failed to match results" << std::endl; diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 81273fdf9..afbc9efca 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -27,7 +27,7 @@ namespace quantifiers { void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc) { // add checkers - pc->registerChecker(PfRule::WITNESS_INTRO, this); + pc->registerChecker(PfRule::SKOLEM_INTRO, this); pc->registerChecker(PfRule::EXISTS_INTRO, this); pc->registerChecker(PfRule::SKOLEMIZE, this); pc->registerChecker(PfRule::INSTANTIATE, this); @@ -64,20 +64,12 @@ Node QuantifiersProofRuleChecker::checkInternal( } return exists; } - else if (id == PfRule::WITNESS_INTRO) + else if (id == PfRule::SKOLEM_INTRO) { - Assert(children.size() == 1); - Assert(args.empty()); - if (children[0].getKind() != EXISTS || children[0][0].getNumChildren() != 1) - { - return Node::null(); - } - std::vector<Node> skolems; - sm->mkSkolemize(children[0], skolems, "k"); - Assert(skolems.size() == 1); - Node witness = SkolemManager::getWitnessForm(skolems[0]); - Assert(witness.getKind() == WITNESS && witness[0] == children[0][0]); - return skolems[0].eqNode(witness); + Assert(children.empty()); + Assert(args.size() == 1); + Node t = SkolemManager::getOriginalForm(args[0]); + return args[0].eqNode(t); } else if (id == PfRule::SKOLEMIZE) { |