diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 20 | ||||
-rw-r--r-- | src/expr/proof_checker.cpp | 16 | ||||
-rw-r--r-- | src/expr/proof_checker.h | 4 | ||||
-rw-r--r-- | src/expr/skolem_manager.cpp (renamed from src/expr/proof_skolem_cache.cpp) | 92 | ||||
-rw-r--r-- | src/expr/skolem_manager.h (renamed from src/expr/proof_skolem_cache.h) | 61 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 23 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 20 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 2 |
11 files changed, 157 insertions, 94 deletions
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<SkolemManager> 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<Node> childrenw = children; std::vector<Node> 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<Node> cchildren; for (const std::shared_ptr<ProofNode>& 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<PfRule> 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/skolem_manager.cpp index da991415e..0570af687 100644 --- a/src/expr/proof_skolem_cache.cpp +++ b/src/expr/skolem_manager.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file proof_skolem_cache.cpp +/*! \file skolem_manager.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds @@ -9,10 +9,10 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Implementation of proof skolem cache + ** \brief Implementation of skolem manager class **/ -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" #include "expr/attribute.h" @@ -35,11 +35,12 @@ 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) +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 @@ -49,14 +50,17 @@ Node ProofSkolemCache::mkSkolem(Node v, 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 ProofSkolemCache::mkSkolemExists(Node v, - Node q, - const std::string& prefix, - const std::string& comment, - int 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; @@ -82,13 +86,13 @@ Node ProofSkolemCache::mkSkolemExists(Node v, Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars); pred = nm->mkNode(EXISTS, bvl, pred); } - return mkSkolem(v, pred, prefix, comment, flags); + return mkSkolem(v, pred, prefix, comment, flags, pg); } -Node ProofSkolemCache::mkPurifySkolem(Node t, - const std::string& prefix, - const std::string& comment, - int flags) +Node SkolemManager::mkPurifySkolem(Node t, + const std::string& prefix, + const std::string& comment, + int flags) { PurifySkolemAttribute psa; if (t.hasAttribute(psa)) @@ -107,23 +111,27 @@ Node ProofSkolemCache::mkPurifySkolem(Node t, return k; } -Node ProofSkolemCache::getWitnessForm(Node n) +ProofGenerator* SkolemManager::getProofGenerator(Node t) { - return convertInternal(n, true); + std::map<Node, ProofGenerator*>::iterator it = d_gens.find(t); + if (it != d_gens.end()) + { + return it->second; + } + return nullptr; } -Node ProofSkolemCache::getSkolemForm(Node n) -{ - return convertInternal(n, false); -} +Node SkolemManager::getWitnessForm(Node n) { return convertInternal(n, true); } + +Node SkolemManager::getSkolemForm(Node n) { return convertInternal(n, false); } -Node ProofSkolemCache::convertInternal(Node n, bool toWitness) +Node SkolemManager::convertInternal(Node n, bool toWitness) { if (n.isNull()) { return n; } - Trace("pf-skolem-debug") << "ProofSkolemCache::convertInternal: " << toWitness + Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness << " " << n << std::endl; WitnessFormAttribute wfa; SkolemFormAttribute sfa; @@ -153,6 +161,10 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness) { 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); @@ -166,7 +178,11 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness) std::vector<Node> children; if (cur.getMetaKind() == metakind::PARAMETERIZED) { - children.push_back(cur.getOperator()); + 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) { @@ -186,6 +202,14 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness) } 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; @@ -197,14 +221,14 @@ Node ProofSkolemCache::convertInternal(Node n, bool toWitness) return visited[n]; } -void ProofSkolemCache::convertToWitnessFormVec(std::vector<Node>& vec) +void SkolemManager::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) +void SkolemManager::convertToSkolemFormVec(std::vector<Node>& vec) { for (unsigned i = 0, nvec = vec.size(); i < nvec; i++) { @@ -212,10 +236,10 @@ void ProofSkolemCache::convertToSkolemFormVec(std::vector<Node>& vec) } } -Node ProofSkolemCache::getOrMakeSkolem(Node w, - const std::string& prefix, - const std::string& comment, - int flags) +Node SkolemManager::getOrMakeSkolem(Node w, + const std::string& prefix, + const std::string& comment, + int flags) { Assert(w.getKind() == WITNESS); SkolemFormAttribute sfa; @@ -232,7 +256,7 @@ Node ProofSkolemCache::getOrMakeSkolem(Node w, k.setAttribute(wfa, w); // set skolem form attribute for w w.setAttribute(sfa, k); - Trace("pf-skolem") << "ProofSkolemCache::mkSkolem: " << k << " : " << w + Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w << std::endl; return k; } diff --git a/src/expr/proof_skolem_cache.h b/src/expr/skolem_manager.h index c0de1e472..eaf74bcce 100644 --- a/src/expr/proof_skolem_cache.h +++ b/src/expr/skolem_manager.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file proof_skolem_cache.h +/*! \file skolem_manager.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds @@ -9,13 +9,13 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Proof skolem cache utility + ** \brief Skolem manager utility **/ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_SKOLEM_CACHE_H -#define CVC4__EXPR__PROOF_SKOLEM_CACHE_H +#ifndef CVC4__EXPR__SKOLEM_MANAGER_H +#define CVC4__EXPR__SKOLEM_MANAGER_H #include <string> @@ -23,6 +23,8 @@ 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 @@ -34,11 +36,11 @@ namespace CVC4 { * reference counting of skolem variables which may be deleted if they are not * used. */ -class ProofSkolemCache +class SkolemManager { public: - ProofSkolemCache() {} - ~ProofSkolemCache() {} + 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 @@ -81,13 +83,17 @@ class ProofSkolemCache * @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. */ - static Node mkSkolem(Node v, - Node pred, - const std::string& prefix, - const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT); + 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: @@ -97,21 +103,30 @@ class ProofSkolemCache * 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); + 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. */ - static Node mkPurifySkolem(Node t, - const std::string& prefix, - const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT); + ProofGenerator* getProofGenerator(Node t); /** convert to witness form * * @param n The term or formula to convert to witness form described above @@ -130,6 +145,10 @@ class ProofSkolemCache static void convertToSkolemFormVec(std::vector<Node>& vec); 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 */ 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<Node>& 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<Node>& 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 <unordered_set> #include "expr/node.h" -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" namespace CVC4 { namespace theory { |