From: Andrew Reynolds Date: Wed, 20 May 2020 14:14:54 +0000 (-0500) Subject: Add proof skolem cache (#4485) X-Git-Tag: cvc5-1.0.0~3309 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c010efcdea8e96f3d423d8cebdfd0f3c19a379c7;p=cvc5.git Add proof skolem cache (#4485) This adds the general utility for maintaining mappings from Skolems to their witness form via attributes. I am sending this as a PR now since it would be helpful to use this class for fixing some of the recent unconstrained-simp bugs. --- 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 WitnessFormAttribute; + +struct SkolemFormAttributeId +{ +}; +typedef expr::Attribute SkolemFormAttribute; + +struct PurifySkolemAttributeId +{ +}; +typedef expr::Attribute 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 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 visited; + std::unordered_map::iterator it; + std::vector 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 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& vec) +{ + for (unsigned i = 0, nvec = vec.size(); i < nvec; i++) + { + vec[i] = getWitnessForm(vec[i]); + } +} +void ProofSkolemCache::convertToSkolemFormVec(std::vector& 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 + +#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& vec); + /** convert to Skolem form vector */ + static void convertToSkolemFormVec(std::vector& 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 */