namespace CVC4 {
+// Attributes are global maps from Nodes to data. Thus, note that these could
+// be implemented as internal maps in SkolemManager.
struct WitnessFormAttributeId
{
};
Node predw = getWitnessForm(pred);
// make the witness term, which should not contain any skolem
Node w = nm->mkNode(WITNESS, bvl, predw);
- // store the mapping to proof generator
- d_gens[w] = pg;
+ // store the mapping to proof generator if it exists
+ if (pg != nullptr)
+ {
+ Node q = nm->mkNode(EXISTS, w[0], w[1]);
+ // Notice this may overwrite an existing proof generator. This does not
+ // matter since either should be able to prove q.
+ d_gens[q] = pg;
+ }
return getOrMakeSkolem(w, prefix, comment, flags);
}
-Node SkolemManager::mkSkolemExists(Node v,
- Node q,
- const std::string& prefix,
- const std::string& comment,
- int flags,
- ProofGenerator* pg)
+Node SkolemManager::mkSkolemize(Node q,
+ std::vector<Node>& skolems,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags,
+ ProofGenerator* pg)
+{
+ Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
+ Assert(q.getKind() == EXISTS);
+ Node currQ = q;
+ for (const Node& av : q[0])
+ {
+ Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
+ // currQ is updated to the result of skolemizing its first variable in
+ // the method below.
+ Node sk = skolemize(currQ, currQ, prefix, comment, flags);
+ Trace("sk-manager-debug")
+ << "made skolem " << sk << " for " << av << std::endl;
+ skolems.push_back(sk);
+ }
+ if (pg != nullptr)
+ {
+ // Same as above, this may overwrite an existing proof generator
+ d_gens[q] = pg;
+ }
+ return currQ;
+}
+
+Node SkolemManager::skolemize(Node q,
+ Node& qskolem,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags)
{
Assert(q.getKind() == EXISTS);
- bool foundVar = false;
+ Node v;
std::vector<Node> ovars;
+ std::vector<Node> ovarsW;
+ Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
for (const Node& av : q[0])
{
- if (av == v)
+ if (v.isNull())
{
- foundVar = true;
+ 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 = getOrMakeBoundVariable(av, av);
+ ovarsW.push_back(avp);
ovars.push_back(av);
}
- if (!foundVar)
- {
- Assert(false);
- return Node::null();
- }
+ Assert(!v.isNull());
Node pred = q[1];
+ qskolem = q[1];
+ Trace("sk-manager-debug") << "make exists predicate" << std::endl;
if (!ovars.empty())
{
- NodeManager* nm = NodeManager::currentNM();
- Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW);
pred = nm->mkNode(EXISTS, bvl, pred);
+ // skolem form keeps the old variables
+ bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+ qskolem = nm->mkNode(EXISTS, bvl, pred);
}
- return mkSkolem(v, pred, prefix, comment, flags, pg);
+ Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
+ // don't use a proof generator, since this may be an intermediate, partially
+ // skolemized formula.
+ Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
+ Assert(k.getType() == v.getType());
+ TNode tv = v;
+ TNode tk = k;
+ Trace("sk-manager-debug")
+ << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
+ qskolem = qskolem.substitute(tv, tk);
+ Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
+ return k;
}
Node SkolemManager::mkPurifySkolem(Node t,
return k;
}
+Node SkolemManager::mkExistential(Node t, Node p)
+{
+ Assert(p.getType().isBoolean());
+ NodeManager* nm = NodeManager::currentNM();
+ Node v = getOrMakeBoundVariable(t, p);
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
+ Node psubs = p.substitute(TNode(t), TNode(v));
+ return nm->mkNode(EXISTS, bvl, psubs);
+}
+
ProofGenerator* SkolemManager::getProofGenerator(Node t)
{
std::map<Node, ProofGenerator*>::iterator it = d_gens.find(t);
{
return n;
}
- Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness
- << " " << n << std::endl;
+ Trace("sk-manager-debug") << "SkolemManager::convertInternal: " << toWitness
+ << " " << n << std::endl;
WitnessFormAttribute wfa;
SkolemFormAttribute sfa;
NodeManager* nm = NodeManager::currentNM();
} while (!visit.empty());
Assert(visited.find(n) != visited.end());
Assert(!visited.find(n)->second.isNull());
- Trace("pf-skolem-debug") << "..return " << visited[n] << std::endl;
+ Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
return visited[n];
}
k.setAttribute(wfa, w);
// set skolem form attribute for w
w.setAttribute(sfa, k);
- Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w
- << std::endl;
+ Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
+ << std::endl;
return k;
}
+Node SkolemManager::getOrMakeBoundVariable(Node t, Node s)
+{
+ std::pair<Node, Node> key(t, s);
+ std::map<std::pair<Node, Node>, Node>::iterator it =
+ d_witnessBoundVar.find(key);
+ if (it != d_witnessBoundVar.end())
+ {
+ return it->second;
+ }
+ TypeNode tt = t.getType();
+ Node v = NodeManager::currentNM()->mkBoundVar(tt);
+ d_witnessBoundVar[key] = v;
+ return v;
+}
+
} // namespace CVC4
* @param comment Debug information about the Skolem
* @param flags The flags for the Skolem (see NodeManager::mkSkolem)
* @param pg The proof generator for this skolem. If non-null, this proof
- * generator must respond to a call to getProofFor(exists x. pred) during
+ * generator must respond to a call to getProofFor(exists v. pred) during
* the lifetime of the current node manager.
* @return The skolem whose witness form is registered by this class.
*/
int flags = NodeManager::SKOLEM_DEFAULT,
ProofGenerator* pg = nullptr);
/**
- * Same as above, but where pred is an existential quantified formula
- * whose bound variable list contains v. For example, calling this method on:
- * x, (exists ((x Int) (y Int)) (P x y))
- * will return:
- * (witness ((x Int)) (exists ((y Int)) (P x y)))
- * If the variable v is not in the bound variable list of q, then null is
- * returned and an assertion failure is thrown.
+ * Make skolemized form of existentially quantified formula q, and store its
+ * Skolems into the argument skolems.
+ *
+ * For example, calling this method on:
+ * (exists ((x Int) (y Int)) (P x y))
+ * returns:
+ * (P w1 w2)
+ * where w1 and w2 are skolems with witness forms:
+ * (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
+ * shadowing.
+ *
+ * In contrast to mkSkolem, the proof generator is for the *entire*
+ * existentially quantified formula q, which may have multiple variables in
+ * its prefix.
+ *
+ * @param q The existentially quantified formula to skolemize,
+ * @param skolems Vector to add Skolems of q to,
+ * @param prefix The prefix of the name of each of the Skolems
+ * @param comment Debug information about each of the Skolems
+ * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+ * @param pg The proof generator for this skolem. If non-null, this proof
+ * generator must respond to a call to getProofFor(q) during
+ * the lifetime of the current node manager.
+ * @return The skolemized form of q.
*/
- Node mkSkolemExists(Node v,
- Node q,
- const std::string& prefix,
- const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT,
- ProofGenerator* pg = nullptr);
+ Node mkSkolemize(Node q,
+ std::vector<Node>& skolems,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::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
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT);
/**
- * Get proof generator for witness term t. This returns the proof generator
- * that was provided in a call to mkSkolem above.
+ * Get proof generator for existentially quantified formula q. This returns
+ * the proof generator that was provided in a call to mkSkolem above.
*/
- ProofGenerator* getProofGenerator(Node t);
+ ProofGenerator* getProofGenerator(Node q);
+ /**
+ * Make existential. Given t and p[t] where p is a formula, this returns
+ * (exists ((x T)) p[x])
+ * where T is the type of t, and x is a variable unique to t,p.
+ */
+ Node mkExistential(Node t, Node p);
/** convert to witness form
*
* @param n The term or formula to convert to witness form described above
* Mapping from witness terms to proof generators.
*/
std::map<Node, ProofGenerator*> d_gens;
+ /**
+ * Map to canonical bound variables. This is used for example by the method
+ * mkExistential.
+ */
+ std::map<std::pair<Node, Node>, Node> d_witnessBoundVar;
/** Convert to witness or skolem form */
static Node convertInternal(Node n, bool toWitness);
/** Get or make skolem attribute for witness term 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:
+ * (exists ((x Int) (y Int)) (P x y))
+ * will return:
+ * (witness ((x Int)) (exists ((y Int)) (P x y)))
+ * If q is not an existentially quantified formula, then null is
+ * returned and an assertion failure is thrown.
+ *
+ * This method additionally updates qskolem to be the skolemized form of q.
+ * In the above example, this is set to:
+ * (exists ((y Int)) (P (witness ((x Int)) (exists ((y' Int)) (P x y'))) y))
+ */
+ Node skolemize(Node q,
+ Node& qskolem,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT);
+ /**
+ * Get or make bound variable unique to (s,t), for d_witnessBoundVar, where
+ * t and s are terms.
+ */
+ Node getOrMakeBoundVariable(Node t, Node s);
};
} // namespace CVC4
projects / cvc5.git / commitdiff