summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/CMakeLists.txt2
-rw-r--r--src/expr/proof_skolem_cache.cpp240
-rw-r--r--src/expr/proof_skolem_cache.h144
3 files changed, 386 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 41df85455..36675a148 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -43,6 +43,8 @@ libcvc4_add_sources(
proof_node_manager.h
proof_rule.cpp
proof_rule.h
+ proof_skolem_cache.cpp
+ proof_skolem_cache.h
symbol_table.cpp
symbol_table.h
term_canonize.cpp
diff --git a/src/expr/proof_skolem_cache.cpp b/src/expr/proof_skolem_cache.cpp
new file mode 100644
index 000000000..da991415e
--- /dev/null
+++ b/src/expr/proof_skolem_cache.cpp
@@ -0,0 +1,240 @@
+/********************* */
+/*! \file proof_skolem_cache.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Implementation of proof skolem cache
+ **/
+
+#include "expr/proof_skolem_cache.h"
+
+#include "expr/attribute.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+struct WitnessFormAttributeId
+{
+};
+typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
+
+struct SkolemFormAttributeId
+{
+};
+typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
+
+struct PurifySkolemAttributeId
+{
+};
+typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute;
+
+Node ProofSkolemCache::mkSkolem(Node v,
+ Node pred,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags)
+{
+ 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);
+ return getOrMakeSkolem(w, prefix, comment, flags);
+}
+
+Node ProofSkolemCache::mkSkolemExists(Node v,
+ Node q,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags)
+{
+ Assert(q.getKind() == EXISTS);
+ bool foundVar = false;
+ std::vector<Node> ovars;
+ for (const Node& av : q[0])
+ {
+ if (av == v)
+ {
+ foundVar = true;
+ continue;
+ }
+ ovars.push_back(av);
+ }
+ if (!foundVar)
+ {
+ Assert(false);
+ return Node::null();
+ }
+ Node pred = q[1];
+ if (!ovars.empty())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+ pred = nm->mkNode(EXISTS, bvl, pred);
+ }
+ return mkSkolem(v, pred, prefix, comment, flags);
+}
+
+Node ProofSkolemCache::mkPurifySkolem(Node t,
+ const std::string& prefix,
+ 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(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);
+ return k;
+}
+
+Node ProofSkolemCache::getWitnessForm(Node n)
+{
+ return convertInternal(n, true);
+}
+
+Node ProofSkolemCache::getSkolemForm(Node n)
+{
+ return convertInternal(n, false);
+}
+
+Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
+{
+ if (n.isNull())
+ {
+ return n;
+ }
+ Trace("pf-skolem-debug") << "ProofSkolemCache::convertInternal: " << toWitness
+ << " " << n << std::endl;
+ WitnessFormAttribute wfa;
+ SkolemFormAttribute sfa;
+ NodeManager* nm = NodeManager::currentNM();
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ if (toWitness && cur.hasAttribute(wfa))
+ {
+ visited[cur] = cur.getAttribute(wfa);
+ }
+ else if (!toWitness && cur.hasAttribute(sfa))
+ {
+ visited[cur] = cur.getAttribute(sfa);
+ }
+ else
+ {
+ visited[cur] = Node::null();
+ visit.push_back(cur);
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ }
+ else if (it->second.isNull())
+ {
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ if (cur.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& cn : cur)
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cn != it->second;
+ children.push_back(it->second);
+ }
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ }
+ if (toWitness)
+ {
+ cur.setAttribute(wfa, ret);
+ }
+ else
+ {
+ cur.setAttribute(sfa, ret);
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ Assert(!visited.find(n)->second.isNull());
+ Trace("pf-skolem-debug") << "..return " << visited[n] << std::endl;
+ return visited[n];
+}
+
+void ProofSkolemCache::convertToWitnessFormVec(std::vector<Node>& vec)
+{
+ for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
+ {
+ vec[i] = getWitnessForm(vec[i]);
+ }
+}
+void ProofSkolemCache::convertToSkolemFormVec(std::vector<Node>& vec)
+{
+ for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
+ {
+ vec[i] = getSkolemForm(vec[i]);
+ }
+}
+
+Node ProofSkolemCache::getOrMakeSkolem(Node w,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags)
+{
+ Assert(w.getKind() == WITNESS);
+ SkolemFormAttribute sfa;
+ // 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 = 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("pf-skolem") << "ProofSkolemCache::mkSkolem: " << k << " : " << w
+ << std::endl;
+ return k;
+}
+
+} // namespace CVC4
diff --git a/src/expr/proof_skolem_cache.h b/src/expr/proof_skolem_cache.h
new file mode 100644
index 000000000..c0de1e472
--- /dev/null
+++ b/src/expr/proof_skolem_cache.h
@@ -0,0 +1,144 @@
+/********************* */
+/*! \file proof_skolem_cache.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Proof skolem cache utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_SKOLEM_CACHE_H
+#define CVC4__EXPR__PROOF_SKOLEM_CACHE_H
+
+#include <string>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * A manager for skolems that can be used in proofs. This is designed to be
+ * a trusted interface to NodeManager::mkSkolem, where one
+ * must provide a definition for the skolem they create in terms of a
+ * 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.
+ */
+class ProofSkolemCache
+{
+ public:
+ ProofSkolemCache() {}
+ ~ProofSkolemCache() {}
+ /**
+ * This makes a skolem of same type as bound variable v, (say its type is T),
+ * whose definition is (witness ((v T)) pred). This definition is maintained
+ * by this class.
+ *
+ * Notice that (exists ((v T)) pred) should be a valid formula. This fact
+ * captures the reason for why the returned Skolem was introduced.
+ *
+ * Take as an example extensionality in arrays:
+ *
+ * (declare-fun a () (Array Int Int))
+ * (declare-fun b () (Array Int Int))
+ * (assert (not (= a b)))
+ *
+ * To witness the index where the arrays a and b are disequal, it is intended
+ * we call this method on:
+ * Node k = mkSkolem( x, F )
+ * where F is:
+ * (=> (not (= a b)) (not (= (select a x) (select b x))))
+ * and x is a fresh bound variable of integer type. Internally, this will map
+ * k to the term:
+ * (witness ((x Int)) (=> (not (= a b))
+ * (not (= (select a x) (select b x)))))
+ * A lemma generated by the array solver for extensionality may safely use
+ * the skolem k in the standard way:
+ * (=> (not (= a b)) (not (= (select a k) (select b k))))
+ * Furthermore, notice that the following lemma does not involve fresh
+ * skolem variables and is valid according to the theory of arrays extended
+ * with support for witness:
+ * (let ((w (witness ((x Int)) (=> (not (= a b))
+ * (not (= (select a x) (select b x)))))))
+ * (=> (not (= a b)) (not (= (select a w) (select b w)))))
+ * This version of the lemma, which requires no explicit tracking of free
+ * Skolem variables, can be obtained by a call to getWitnessForm(...)
+ * below. We call this the "witness form" of the lemma above.
+ *
+ * @param v The bound variable of the same type of the Skolem to create.
+ * @param pred The desired property of the Skolem to create, in terms of bound
+ * variable v.
+ * @param prefix The prefix of the name of the Skolem
+ * @param comment Debug information about the Skolem
+ * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+ * @return The skolem whose witness form is registered by this class.
+ */
+ static Node mkSkolem(Node v,
+ Node pred,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT);
+ /**
+ * 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.
+ */
+ static Node mkSkolemExists(Node v,
+ Node q,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT);
+ /**
+ * 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
+ * implement via an attribute on t. This attribute is used to ensure to
+ * associate a unique skolem for each t.
+ */
+ static Node mkPurifySkolem(Node t,
+ const std::string& prefix,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT);
+ /** convert to witness form
+ *
+ * @param n The term or formula to convert to witness form described above
+ * @return n in witness form.
+ */
+ static Node getWitnessForm(Node n);
+ /** convert to Skolem form
+ *
+ * @param n The term or formula to convert to Skolem form described above
+ * @return n in Skolem 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);
+
+ private:
+ /** 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);
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback