summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof_rule.cpp2
-rw-r--r--src/expr/proof_rule.h34
-rw-r--r--src/expr/skolem_manager.cpp157
-rw-r--r--src/expr/skolem_manager.h72
-rw-r--r--src/smt/quant_elim_solver.cpp2
-rw-r--r--src/smt/witness_form.cpp40
-rw-r--r--src/theory/builtin/proof_checker.cpp8
-rw-r--r--src/theory/quantifiers/proof_checker.cpp20
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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback