From: Andrew Reynolds Date: Fri, 5 Jun 2020 15:19:10 +0000 (-0500) Subject: (proof-new) Rename ProofSkolemCache to SkolemManager (#4556) X-Git-Tag: cvc5-1.0.0~3248 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e9c29bb348bd8fab5cedc48ab96ce2a0e6f98078;p=cvc5.git (proof-new) Rename ProofSkolemCache to SkolemManager (#4556) This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing. This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form. Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler. Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 3d41b7a72..6415e2132 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -49,10 +49,10 @@ libcvc4_add_sources( proof_node_manager.h proof_rule.cpp proof_rule.h - proof_skolem_cache.cpp - proof_skolem_cache.h proof_step_buffer.cpp proof_step_buffer.h + skolem_manager.cpp + skolem_manager.h symbol_table.cpp symbol_table.h term_canonize.cpp diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 427afd5af..6f8934645 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -27,6 +27,7 @@ #include "expr/dtype.h" #include "expr/node_manager_attributes.h" #include "expr/node_manager_listeners.h" +#include "expr/skolem_manager.h" #include "expr/type_checker.h" #include "options/options.h" #include "options/smt_options.h" @@ -95,6 +96,7 @@ NodeManager::NodeManager(ExprManager* exprManager) : d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)), + d_skManager(new SkolemManager), d_registrations(new ListenerRegistrationList()), next_id(0), d_attrManager(new expr::attr::AttributeManager()), @@ -111,6 +113,7 @@ NodeManager::NodeManager(ExprManager* exprManager, const Options& options) : d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)), + d_skManager(new SkolemManager), d_registrations(new ListenerRegistrationList()), next_id(0), d_attrManager(new expr::attr::AttributeManager()), @@ -230,6 +233,7 @@ NodeManager::~NodeManager() { // defensive coding, in case destruction-order issues pop up (they often do) delete d_resourceManager; d_resourceManager = NULL; + d_skManager = nullptr; delete d_statisticsRegistry; d_statisticsRegistry = NULL; delete d_registrations; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1fab328e9..7fa2d147a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -42,6 +42,7 @@ namespace CVC4 { class StatisticsRegistry; class ResourceManager; +class SkolemManager; class DType; @@ -113,6 +114,9 @@ class NodeManager { ResourceManager* d_resourceManager; + /** The skolem manager */ + std::shared_ptr d_skManager; + /** * A list of registrations on d_options to that call into d_resourceManager. * These must be garbage collected before d_options and d_resourceManager. @@ -405,6 +409,8 @@ public: /** Get this node manager's resource manager */ ResourceManager* getResourceManager() { return d_resourceManager; } + /** Get this node manager's skolem manager */ + SkolemManager* getSkolemManager() { return d_skManager.get(); } /** Get this node manager's statistics registry */ StatisticsRegistry* getStatisticsRegistry() const @@ -539,13 +545,13 @@ public: * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT * cannot be composed in such a manner. */ - enum SkolemFlags { - SKOLEM_DEFAULT = 0, /**< default behavior */ - SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ - SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */ - SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ - };/* enum SkolemFlags */ - + enum SkolemFlags + { + SKOLEM_DEFAULT = 0, /**< default behavior */ + SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ + SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */ + SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ + }; /** * Create a skolem constant with the given name, type, and comment. * diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index 7e7a26c5b..ffd1bdc9c 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -14,7 +14,7 @@ #include "expr/proof_checker.h" -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" #include "smt/smt_statistics_registry.h" using namespace CVC4::kind; @@ -28,11 +28,11 @@ Node ProofRuleChecker::check(PfRule id, // convert to witness form std::vector childrenw = children; std::vector argsw = args; - ProofSkolemCache::convertToWitnessFormVec(childrenw); - ProofSkolemCache::convertToWitnessFormVec(argsw); + SkolemManager::convertToWitnessFormVec(childrenw); + SkolemManager::convertToWitnessFormVec(argsw); Node res = checkInternal(id, childrenw, argsw); // res is in terms of witness form, convert back to Skolem form - return ProofSkolemCache::getSkolemForm(res); + return SkolemManager::getSkolemForm(res); } Node ProofRuleChecker::checkChildrenArg(PfRule id, @@ -92,14 +92,17 @@ bool ProofRuleChecker::getBool(TNode n, bool& b) } ProofCheckerStatistics::ProofCheckerStatistics() - : d_ruleChecks("ProofCheckerStatistics::ruleChecks") + : d_ruleChecks("ProofCheckerStatistics::ruleChecks"), + d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0) { smtStatisticsRegistry()->registerStat(&d_ruleChecks); + smtStatisticsRegistry()->registerStat(&d_totalRuleChecks); } ProofCheckerStatistics::~ProofCheckerStatistics() { smtStatisticsRegistry()->unregisterStat(&d_ruleChecks); + smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks); } Node ProofChecker::check(ProofNode* pn, Node expected) @@ -123,6 +126,7 @@ Node ProofChecker::check( } // record stat d_stats.d_ruleChecks << id; + ++d_stats.d_totalRuleChecks; Trace("pfcheck") << "ProofChecker::check: " << id << std::endl; std::vector cchildren; for (const std::shared_ptr& pc : children) @@ -183,6 +187,8 @@ Node ProofChecker::checkDebug(PfRule id, { Trace(traceTag) << " success" << std::endl; } + Trace(traceTag) << "cchildren: " << cchildren << std::endl; + Trace(traceTag) << " args: " << args << std::endl; return res; } diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index 99c02b8dc..f04587a7d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -77,7 +77,7 @@ class ProofRuleChecker /** * This checks a single step in a proof. It is identical to check above * except that children and args have been converted to "witness form" - * (see ProofSkolemCache). Likewise, its output should be in witness form. + * (see SkolemManager). Likewise, its output should be in witness form. * * @param id The id of the proof node to check * @param children The premises of the proof node to check. These are nodes @@ -100,6 +100,8 @@ class ProofCheckerStatistics ~ProofCheckerStatistics(); /** Counts the number of checks for each kind of proof rule */ HistogramStat d_ruleChecks; + /** Total number of rule checks */ + IntStat d_totalRuleChecks; }; /** A class for checking proofs */ diff --git a/src/expr/proof_skolem_cache.cpp b/src/expr/proof_skolem_cache.cpp deleted file mode 100644 index da991415e..000000000 --- a/src/expr/proof_skolem_cache.cpp +++ /dev/null @@ -1,240 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index c0de1e472..000000000 --- a/src/expr/proof_skolem_cache.h +++ /dev/null @@ -1,144 +0,0 @@ -/********************* */ -/*! \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 */ diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp new file mode 100644 index 000000000..0570af687 --- /dev/null +++ b/src/expr/skolem_manager.cpp @@ -0,0 +1,264 @@ +/********************* */ +/*! \file skolem_manager.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 skolem manager class + **/ + +#include "expr/skolem_manager.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 SkolemManager::mkSkolem(Node v, + Node pred, + const std::string& prefix, + const std::string& comment, + int flags, + ProofGenerator* pg) +{ + 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); + // store the mapping to proof generator + d_gens[w] = 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) +{ + 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, pg); +} + +Node SkolemManager::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; +} + +ProofGenerator* SkolemManager::getProofGenerator(Node t) +{ + std::map::iterator it = d_gens.find(t); + if (it != d_gens.end()) + { + return it->second; + } + return nullptr; +} + +Node SkolemManager::getWitnessForm(Node n) { return convertInternal(n, true); } + +Node SkolemManager::getSkolemForm(Node n) { return convertInternal(n, false); } + +Node SkolemManager::convertInternal(Node n, bool toWitness) +{ + if (n.isNull()) + { + return n; + } + Trace("pf-skolem-debug") << "SkolemManager::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); + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + visit.push_back(cur.getOperator()); + } + 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) + { + it = visited.find(cur.getOperator()); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cur.getOperator() != it->second; + children.push_back(it->second); + } + 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 + { + // 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. + 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 SkolemManager::convertToWitnessFormVec(std::vector& vec) +{ + for (unsigned i = 0, nvec = vec.size(); i < nvec; i++) + { + vec[i] = getWitnessForm(vec[i]); + } +} +void SkolemManager::convertToSkolemFormVec(std::vector& 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); + 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") << "SkolemManager::mkSkolem: " << k << " : " << w + << std::endl; + return k; +} + +} // namespace CVC4 diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h new file mode 100644 index 000000000..eaf74bcce --- /dev/null +++ b/src/expr/skolem_manager.h @@ -0,0 +1,163 @@ +/********************* */ +/*! \file skolem_manager.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 Skolem manager utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__SKOLEM_MANAGER_H +#define CVC4__EXPR__SKOLEM_MANAGER_H + +#include + +#include "expr/node.h" + +namespace CVC4 { + +class ProofGenerator; + +/** + * 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 SkolemManager +{ + public: + SkolemManager() {} + ~SkolemManager() {} + /** + * 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) + * @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 + * the lifetime of the current node manager. + * @return The skolem whose witness form is registered by this class. + */ + Node mkSkolem(Node v, + Node pred, + const std::string& prefix, + const std::string& comment = "", + 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. + */ + Node mkSkolemExists(Node v, + Node q, + 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 + * implement via an attribute on t. This attribute is used to ensure to + * associate a unique skolem for each t. + * + * Notice that a purification skolem is trivial to justify, and hence it + * does not require a proof generator. + */ + Node mkPurifySkolem(Node t, + const std::string& prefix, + 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. + */ + ProofGenerator* getProofGenerator(Node t); + /** 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: + /** + * Mapping from witness terms to proof generators. + */ + std::map 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); +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 3ff3966cc..443aaa9b7 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -34,7 +34,7 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "preprocessing/util/ite_utilities.h" @@ -1178,6 +1178,7 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) Node TheoryArithPrivate::eliminateOperators(Node node) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Kind k = node.getKind(); switch (k) @@ -1206,9 +1207,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node) Node zero = mkRationalNode(0); Node diff = nm->mkNode(kind::MINUS, node[0], v); Node lem = mkInRange(diff, zero, one); - toIntSkolem = ProofSkolemCache::mkSkolem( + toIntSkolem = sm->mkSkolem( v, lem, "toInt", "a conversion of a Real term to its Integer part"); - toIntSkolem = ProofSkolemCache::getWitnessForm(toIntSkolem); + toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem); d_to_int_skolem[node[0]] = toIntSkolem; } else @@ -1303,9 +1304,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node) nm->mkNode( PLUS, v, nm->mkConst(Rational(-1)))))))); } - intVar = ProofSkolemCache::mkSkolem( + intVar = sm->mkSkolem( v, lem, "linearIntDiv", "the result of an intdiv-by-k term"); - intVar = ProofSkolemCache::getWitnessForm(intVar); + intVar = SkolemManager::getWitnessForm(intVar); d_int_div_skolem[rw] = intVar; } else @@ -1345,9 +1346,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node) Node lem = nm->mkNode(IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(MULT, den, v).eqNode(num)); - var = ProofSkolemCache::mkSkolem( + var = sm->mkSkolem( v, lem, "nonlinearDiv", "the result of a non-linear div term"); - var = ProofSkolemCache::getWitnessForm(var); + var = SkolemManager::getWitnessForm(var); d_div_skolem[rw] = var; } else @@ -1490,12 +1491,12 @@ Node TheoryArithPrivate::eliminateOperators(Node node) lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); } Assert(!lem.isNull()); - Node ret = ProofSkolemCache::mkSkolem( + Node ret = sm->mkSkolem( var, lem, "tfk", "Skolem to eliminate a non-standard transcendental function"); - ret = ProofSkolemCache::getWitnessForm(ret); + ret = SkolemManager::getWitnessForm(ret); d_nlin_inverse_skolem[node] = ret; return ret; } @@ -4269,8 +4270,8 @@ bool TheoryArithPrivate::needsCheckLastEffort() { } } -Node TheoryArithPrivate::explain(TNode n) { - +Node TheoryArithPrivate::explain(TNode n) +{ Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl; ConstraintP c = d_constraintDatabase.lookup(n); diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 8d2a1540c..1884d3890 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -14,7 +14,7 @@ #include "theory/builtin/proof_checker.h" -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -63,9 +63,9 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) { - Node nk = ProofSkolemCache::getSkolemForm(n); + Node nk = SkolemManager::getSkolemForm(n); Node nkr = applyRewriteExternal(nk, idr); - return ProofSkolemCache::getWitnessForm(nkr); + return SkolemManager::getWitnessForm(nkr); } Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) @@ -74,27 +74,27 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) { return Node::null(); } - Node nk = ProofSkolemCache::getSkolemForm(n); + Node nk = SkolemManager::getSkolemForm(n); Node nks = applySubstitutionExternal(nk, exp, ids); - return ProofSkolemCache::getWitnessForm(nks); + return SkolemManager::getWitnessForm(nks); } Node BuiltinProofRuleChecker::applySubstitution(Node n, const std::vector& exp, MethodId ids) { - Node nk = ProofSkolemCache::getSkolemForm(n); + Node nk = SkolemManager::getSkolemForm(n); Node nks = applySubstitutionExternal(nk, exp, ids); - return ProofSkolemCache::getWitnessForm(nks); + return SkolemManager::getWitnessForm(nks); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( Node n, const std::vector& exp, MethodId ids, MethodId idr) { - Node nk = ProofSkolemCache::getSkolemForm(n); + Node nk = SkolemManager::getSkolemForm(n); Node nks = applySubstitutionExternal(nk, exp, ids); Node nksr = applyRewriteExternal(nks, idr); - return ProofSkolemCache::getWitnessForm(nksr); + return SkolemManager::getWitnessForm(nksr); } Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr) @@ -122,7 +122,7 @@ Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, MethodId ids) { Assert(!exp.isNull()); - Node expk = ProofSkolemCache::getSkolemForm(exp); + Node expk = SkolemManager::getSkolemForm(exp); TNode var, subs; if (ids == MethodId::SB_DEFAULT) { diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 4af75f1cc..85a948567 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -82,12 +82,13 @@ Node SkolemCache::mkTypedSkolemCached( } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node sk; switch (id) { // exists k. k = a case SK_PURIFY: - sk = ProofSkolemCache::mkPurifySkolem(a, c, "string purify skolem"); + sk = sm->mkPurifySkolem(a, c, "string purify skolem"); break; // these are eliminated by normalizeStringSkolem case SK_ID_V_SPT: @@ -113,7 +114,7 @@ Node SkolemCache::mkTypedSkolemCached( Notice() << "Don't know how to handle Skolem ID " << id << std::endl; Node v = nm->mkBoundVar(tn); Node cond = nm->mkConst(true); - sk = ProofSkolemCache::mkSkolem(v, cond, c, "string skolem"); + sk = sm->mkSkolem(v, cond, c, "string skolem"); } break; } diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 0ebbb3277..7ce507f29 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -22,7 +22,7 @@ #include #include "expr/node.h" -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" namespace CVC4 { namespace theory {