From 25b8d01a989a51763e2130384c800a5732d4e06a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 3 Nov 2021 12:43:02 -0500 Subject: [PATCH] Refactor skolem construction (#7561) This makes all methods for constructing skolems local to SkolemManager. It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things: (1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon. (2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions. This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager. --- src/expr/dtype.cpp | 5 +- src/expr/dtype_cons.cpp | 45 ++++++------- src/expr/node_manager.cpp | 29 +-------- src/expr/node_manager.h | 42 ------------- src/expr/skolem_manager.cpp | 51 ++++++++++----- src/expr/skolem_manager.h | 63 ++++++++++++++----- src/preprocessing/passes/miplib_trick.cpp | 50 ++++++++------- src/preprocessing/passes/miplib_trick.h | 12 ++-- src/smt/listeners.cpp | 14 ----- src/smt/listeners.h | 4 -- src/smt/term_formula_removal.cpp | 2 +- src/theory/arith/nl/cad_solver.cpp | 3 +- src/theory/arith/operator_elim.cpp | 4 +- src/theory/fp/fp_expand_defs.cpp | 23 +++---- .../quantifiers/sygus/sygus_unif_rl.cpp | 6 +- src/theory/sets/theory_sets_private.cpp | 3 +- src/theory/strings/skolem_cache.cpp | 4 +- test/unit/node/node_black.cpp | 24 +++---- test/unit/node/node_manager_black.cpp | 2 +- test/unit/theory/theory_arith_cad_white.cpp | 10 +-- 20 files changed, 175 insertions(+), 221 deletions(-) diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index d8ec0cb61..4a0ed994f 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -867,10 +867,7 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const SkolemManager* sm = nm->getSkolemManager(); TypeNode stype = nm->mkSelectorType(dtt, t); Node nindex = nm->mkConst(Rational(index)); - s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, - stype, - nindex, - NodeManager::SKOLEM_NO_NOTIFY); + s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, stype, nindex); d_sharedSel[dtt][t][index] = s; Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t << std::endl; diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index ddb88499b..f23cfa4f9 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -49,11 +49,10 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType) Assert(!isResolved()); Assert(!selectorType.isNull()); SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node sel = sm->mkDummySkolem( - "unresolved_" + selectorName, - selectorType, - "is an unresolved selector type placeholder", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + Node sel = sm->mkDummySkolem("unresolved_" + selectorName, + selectorType, + "is an unresolved selector type placeholder", + SkolemManager::SKOLEM_EXACT_NAME); // can use null updater for now Node nullNode; Trace("datatypes") << "DTypeConstructor::addArg: " << sel << std::endl; @@ -562,17 +561,15 @@ bool DTypeConstructor::resolve( } // Internally, selectors (and updaters) are fresh internal skolems which // we constructor via mkDummySkolem. - arg->d_selector = sm->mkDummySkolem( - argName, - nm->mkSelectorType(self, range), - "is a selector", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + arg->d_selector = sm->mkDummySkolem(argName, + nm->mkSelectorType(self, range), + "is a selector", + SkolemManager::SKOLEM_EXACT_NAME); std::string updateName("update_" + argName); - arg->d_updater = sm->mkDummySkolem( - updateName, - nm->mkDatatypeUpdateType(self, range), - "is a selector", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + arg->d_updater = sm->mkDummySkolem(updateName, + nm->mkDatatypeUpdateType(self, range), + "is a selector", + SkolemManager::SKOLEM_EXACT_NAME); // must set indices to ensure datatypes::utils::indexOf works arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex); arg->d_selector.setAttribute(DTypeIndexAttr(), index); @@ -600,16 +597,14 @@ bool DTypeConstructor::resolve( // The name of the tester variable does not matter, it is only used // internally. std::string testerName("is_" + d_name); - d_tester = sm->mkDummySkolem( - testerName, - nm->mkTesterType(self), - "is a tester", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); - d_constructor = sm->mkDummySkolem( - getName(), - nm->mkConstructorType(argTypes, self), - "is a constructor", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + d_tester = sm->mkDummySkolem(testerName, + nm->mkTesterType(self), + "is a tester", + SkolemManager::SKOLEM_EXACT_NAME); + d_constructor = sm->mkDummySkolem(getName(), + nm->mkConstructorType(argTypes, self), + "is a constructor", + SkolemManager::SKOLEM_EXACT_NAME); Assert(d_constructor.getType().isConstructor()); // associate constructor with all selectors for (std::shared_ptr sel : d_args) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a9e5854b0..3734e5860 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -100,8 +100,7 @@ NodeManager::NodeManager() d_attrManager(new expr::attr::AttributeManager()), d_nodeUnderDeletion(nullptr), d_inReclaimZombies(false), - d_abstractValueCount(0), - d_skolemCounter(0) + d_abstractValueCount(0) { } @@ -503,25 +502,6 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } -Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) { - Node n = NodeBuilder(this, kind::SKOLEM); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - if((flags & SKOLEM_EXACT_NAME) == 0) { - stringstream name; - name << prefix << '_' << ++d_skolemCounter; - setAttribute(n, expr::VarNameAttr(), name.str()); - } else { - setAttribute(n, expr::VarNameAttr(), prefix); - } - if((flags & SKOLEM_NO_NOTIFY) == 0) { - for(vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL); - } - } - return n; -} - TypeNode NodeManager::mkBagType(TypeNode elementType) { CheckArgument( @@ -1061,13 +1041,6 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } -Node NodeManager::mkBooleanTermVariable() { - Node n = NodeBuilder(this, kind::BOOLEAN_TERM_VARIABLE); - n.setAttribute(TypeAttr(), booleanType()); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b526efc80..5b5f07e6f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -72,8 +72,6 @@ class NodeManagerListener { { } virtual void nmNotifyNewVar(TNode n) {} - virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, - uint32_t flags) {} /** * Notify a listener of a Node that's being GCed. If this function stores a * reference @@ -211,15 +209,6 @@ class NodeManager */ unsigned d_abstractValueCount; - /** - * A counter used to produce unique skolem names. - * - * Note that it is NOT incremented when skolems are created using - * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced - * by this node manager. - */ - unsigned d_skolemCounter; - /** * Look up a NodeValue in the pool associated to this NodeManager. * The NodeValue argument need not be a "completely-constructed" @@ -365,19 +354,6 @@ class NodeManager /** Create a variable with the given type. */ Node mkVar(const TypeNode& type); - /** - * Create a skolem constant with the given name, type, and comment. For - * details, see SkolemManager::mkDummySkolem, which calls this method. - * - * This method is intentionally private. To create skolems, one should - * call a method from SkolemManager for allocating a skolem in a standard - * way, or otherwise use SkolemManager::mkDummySkolem. - */ - Node mkSkolem(const std::string& prefix, - const TypeNode& type, - const std::string& comment = "", - int flags = SKOLEM_DEFAULT); - public: /** * Initialize the node manager by adding a null node to the pool and filling @@ -555,27 +531,9 @@ class NodeManager */ Node mkChain(Kind kind, const std::vector& children); - /** - * Optional flags used to control behavior of NodeManager::mkSkolem(). - * They should be composed with a bitwise OR (e.g., - * "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 */ - SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ - }; /* enum SkolemFlags */ - /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - /** Create a boolean term variable. */ - Node mkBooleanTermVariable(); - /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index e8651ea75..c1741beac 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -20,6 +20,7 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" #include "expr/node_algorithm.h" +#include "expr/node_manager_attributes.h" using namespace cvc5::kind; @@ -79,6 +80,8 @@ std::ostream& operator<<(std::ostream& out, SkolemFunId id) return out; } +SkolemManager::SkolemManager() : d_skolemCounter(0) {} + Node SkolemManager::mkSkolem(Node v, Node pred, const std::string& prefix, @@ -217,10 +220,9 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, d_skolemFuns.find(key); if (it == d_skolemFuns.end()) { - NodeManager* nm = NodeManager::currentNM(); std::stringstream ss; ss << "SKOLEM_FUN_" << id; - Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags); + Node k = mkSkolemNode(ss.str(), tn, "an internal skolem function", flags); d_skolemFuns[key] = k; d_skolemFunMap[k] = key; return k; @@ -264,7 +266,7 @@ Node SkolemManager::mkDummySkolem(const std::string& prefix, const std::string& comment, int flags) { - return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags); + return mkSkolemNode(prefix, type, comment, flags); } ProofGenerator* SkolemManager::getProofGenerator(Node t) const @@ -367,25 +369,15 @@ Node SkolemManager::mkSkolemInternal(Node w, int flags) { // note that witness, original forms are independent, but share skolems - NodeManager* nm = NodeManager::currentNM(); // w is not necessarily a witness term SkolemFormAttribute sfa; - Node k; // could already have a skolem if we used w already if (w.hasAttribute(sfa)) { return w.getAttribute(sfa); } // make the new skolem - if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR) - { - Assert (w.getType().isBoolean()); - k = nm->mkBooleanTermVariable(); - } - else - { - k = nm->mkSkolem(prefix, w.getType(), comment, flags); - } + Node k = mkSkolemNode(prefix, w.getType(), comment, flags); // set skolem form attribute for w w.setAttribute(sfa, k); Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w @@ -393,4 +385,35 @@ Node SkolemManager::mkSkolemInternal(Node w, return k; } +Node SkolemManager::mkSkolemNode(const std::string& prefix, + const TypeNode& type, + const std::string& comment, + int flags) +{ + NodeManager* nm = NodeManager::currentNM(); + Node n; + if (flags & SKOLEM_BOOL_TERM_VAR) + { + Assert(type.isBoolean()); + n = NodeBuilder(nm, BOOLEAN_TERM_VARIABLE); + } + else + { + n = NodeBuilder(nm, SKOLEM); + if ((flags & SKOLEM_EXACT_NAME) == 0) + { + std::stringstream name; + name << prefix << '_' << ++d_skolemCounter; + n.setAttribute(expr::VarNameAttr(), name.str()); + } + else + { + n.setAttribute(expr::VarNameAttr(), prefix); + } + } + n.setAttribute(expr::TypeAttr(), type); + n.setAttribute(expr::TypeCheckedAttr(), true); + return n; +} + } // namespace cvc5 diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 16cab62ca..0556185df 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -174,8 +174,21 @@ std::ostream& operator<<(std::ostream& out, SkolemFunId id); class SkolemManager { public: - SkolemManager() {} + SkolemManager(); ~SkolemManager() {} + + /** + * Optional flags used to control behavior of skolem creation. + * They should be composed with a bitwise OR (e.g., + * "SKOLEM_BOOL_TERM_VAR | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT + * cannot be composed in such a manner. + */ + enum SkolemFlags + { + SKOLEM_DEFAULT = 0, /**< default behavior */ + SKOLEM_EXACT_NAME = 1, /**< do not make the name unique by adding the id */ + SKOLEM_BOOL_TERM_VAR = 2 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ + }; /** * 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 @@ -217,7 +230,7 @@ class SkolemManager * 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 flags The flags for the Skolem (see SkolemFlags) * @param pg The proof generator for this skolem. If non-null, this proof * generator must respond to a call to getProofFor(exists v. pred) during * the lifetime of the current node manager. @@ -227,7 +240,7 @@ class SkolemManager Node pred, const std::string& prefix, const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT, + int flags = SKOLEM_DEFAULT, ProofGenerator* pg = nullptr); /** * Make skolemized form of existentially quantified formula q, and store its @@ -255,7 +268,7 @@ class SkolemManager * @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 flags The flags for the Skolem (see SkolemFlags) * @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. @@ -265,7 +278,7 @@ class SkolemManager std::vector& skolems, const std::string& prefix, const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT, + int flags = SKOLEM_DEFAULT, ProofGenerator* pg = nullptr); /** * Same as above, but for special case of (witness ((x T)) (= x t)) @@ -288,7 +301,7 @@ class SkolemManager Node mkPurifySkolem(Node t, const std::string& prefix, const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT); + int flags = SKOLEM_DEFAULT); /** * Make skolem function. This method should be used for creating fixed * skolem functions of the forms described in SkolemFunId. The user of this @@ -321,12 +334,12 @@ class SkolemManager Node mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal = Node::null(), - int flags = NodeManager::SKOLEM_DEFAULT); + int flags = SKOLEM_DEFAULT); /** Same as above, with multiple cache values */ Node mkSkolemFunction(SkolemFunId id, TypeNode tn, const std::vector& cacheVals, - int flags = NodeManager::SKOLEM_DEFAULT); + int flags = SKOLEM_DEFAULT); /** * Is k a skolem function? Returns true if k was generated by the above call. * Updates the arguments to the values used when constructing it. @@ -348,12 +361,12 @@ class SkolemManager * being dumped, this is included in a comment before the declaration * and can be quite useful for debugging * @param flags an optional mask of bits from SkolemFlags to control - * mkSkolem() behavior + * skolem behavior */ Node mkDummySkolem(const std::string& prefix, const TypeNode& type, const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT); + int flags = SKOLEM_DEFAULT); /** * Get proof generator for existentially quantified formula q. This returns * the proof generator that was provided in a call to mkSkolem above. @@ -386,11 +399,20 @@ class SkolemManager * Mapping from witness terms to proof generators. */ std::map d_gens; + + /** + * A counter used to produce unique skolem names. + * + * Note that it is NOT incremented when skolems are created using + * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced + * by this node manager. + */ + size_t d_skolemCounter; /** Get or make skolem attribute for term w, which may be a witness term */ - static Node mkSkolemInternal(Node w, - const std::string& prefix, - const std::string& comment, - int flags); + Node mkSkolemInternal(Node 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: @@ -408,7 +430,18 @@ class SkolemManager Node& qskolem, const std::string& prefix, const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT); + int flags = SKOLEM_DEFAULT); + /** + * Create a skolem constant with the given name, type, and comment. + * + * This method is intentionally private. To create skolems, one should + * call a public method from SkolemManager for allocating a skolem in a + * proper way, or otherwise use SkolemManager::mkDummySkolem. + */ + Node mkSkolemNode(const std::string& prefix, + const TypeNode& type, + const std::string& comment = "", + int flags = SKOLEM_DEFAULT); }; } // namespace cvc5 diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 8202acb15..d432d8ed1 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -76,18 +76,10 @@ MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "miplib-trick"), d_statistics(statisticsRegistry()) { - if (!options().base.incrementalSolving) - { - NodeManager::currentNM()->subscribeEvents(this); - } } MipLibTrick::~MipLibTrick() { - if (!options().base.incrementalSolving) - { - NodeManager::currentNM()->unsubscribeEvents(this); - } } /** @@ -166,22 +158,34 @@ size_t MipLibTrick::removeFromConjunction( return 0; } -void MipLibTrick::nmNotifyNewVar(TNode n) +void MipLibTrick::collectBooleanVariables( + AssertionPipeline* assertionsToPreprocess) { - if (n.getType().isBoolean()) + d_boolVars.clear(); + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector visit; + TNode cur; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { - d_boolVars.push_back(n); + visit.push_back((*assertionsToPreprocess)[i]); } -} - -void MipLibTrick::nmNotifyNewSkolem(TNode n, - const std::string& comment, - uint32_t flags) -{ - if (n.getType().isBoolean()) + do { - d_boolVars.push_back(n); - } + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + visited.insert(cur); + if (cur.isVar() && cur.getType().isBoolean()) + { + d_boolVars.push_back(cur); + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } while (!visit.empty()); } PreprocessingPassResult MipLibTrick::applyInternal( @@ -191,6 +195,9 @@ PreprocessingPassResult MipLibTrick::applyInternal( == assertionsToPreprocess->size()); Assert(!options().base.incrementalSolving); + // collect Boolean variables + collectBooleanVariables(assertionsToPreprocess); + context::Context fakeContext; TheoryEngine* te = d_preprocContext->getTheoryEngine(); booleans::CircuitPropagator* propagator = @@ -529,8 +536,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node newVar = sm->mkDummySkolem( ss.str(), nm->integerType(), - "a variable introduced due to scrubbing a miplib encoding", - NodeManager::SKOLEM_EXACT_NAME); + "a variable introduced due to scrubbing a miplib encoding"); Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero)); Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one)); TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr); diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 796063b46..65779f90d 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -25,18 +25,12 @@ namespace cvc5 { namespace preprocessing { namespace passes { -class MipLibTrick : public PreprocessingPass, public NodeManagerListener +class MipLibTrick : public PreprocessingPass { public: MipLibTrick(PreprocessingPassContext* preprocContext); ~MipLibTrick(); - // NodeManagerListener callbacks to collect d_boolVars. - void nmNotifyNewVar(TNode n) override; - void nmNotifyNewSkolem(TNode n, - const std::string& comment, - uint32_t flags) override; - protected: PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; @@ -51,6 +45,10 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener size_t removeFromConjunction( Node& n, const std::unordered_set& toRemove); + /** + * Collect Boolean variables in the given pipeline, store them in d_boolVars. + */ + void collectBooleanVariables(AssertionPipeline* assertionsToPreprocess); Statistics d_statistics; diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index de6368951..7a1951d95 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -89,19 +89,5 @@ void SmtNodeManagerListener::nmNotifyNewVar(TNode n) d_dm.addToDump(c); } -void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, - const std::string& comment, - uint32_t flags) -{ - std::string id = n.getAttribute(expr::VarNameAttr()); - DeclareFunctionNodeCommand c(id, n, n.getType()); - if (Dump.isOn("skolems") && comment != "") - { - d_outMgr.getPrinter().toStreamCmdSetInfo( - d_outMgr.getDumpOut(), "notes", id + " is " + comment); - } - d_dm.addToDump(c, "skolems"); -} - } // namespace smt } // namespace cvc5 diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 60ec6b4ed..df99f8008 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -61,10 +61,6 @@ class SmtNodeManagerListener : public NodeManagerListener uint32_t flags) override; /** Notify when new variable is created */ void nmNotifyNewVar(TNode n) override; - /** Notify when new skolem is created */ - void nmNotifyNewSkolem(TNode n, - const std::string& comment, - uint32_t flags) override; /** Notify when a term is deleted */ void nmNotifyDeleteNode(TNode n) override {} diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 07100576d..c633ecb63 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -439,7 +439,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, node, "btvK", "a Boolean term variable introduced during term formula removal", - NodeManager::SKOLEM_BOOL_TERM_VAR); + SkolemManager::SKOLEM_BOOL_TERM_VAR); d_skolem_cache.insert(node, skolem); // The new assertion diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 6b1749305..a3dd77fd1 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -38,8 +38,7 @@ CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - d_ranVariable = sm->mkDummySkolem( - "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME); + d_ranVariable = sm->mkDummySkolem("__z", nm->realType(), ""); #ifdef CVC5_POLY_IMP if (env.isTheoryProofProducing()) { diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 90f4a2cc7..afbb9b70f 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -462,8 +462,8 @@ Node OperatorElim::mkWitnessTerm(Node v, NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); // we mark that we should send a lemma - Node k = - sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this); + Node k = sm->mkSkolem( + v, pred, prefix, comment, SkolemManager::SKOLEM_DEFAULT, this); if (d_pnm != nullptr) { Node lem = SkolemLemma::getSkolemLemmaFor(k); diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index a499b9666..de86626af 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -50,11 +50,8 @@ Node FpExpandDefs::minUF(Node node) args[0] = t; args[1] = t; fun = sm->mkDummySkolem("floatingpoint_min_zero_case", - nm->mkFunctionType(args, - nm->mkBitVectorType(1U) - ), - "floatingpoint_min_zero_case", - NodeManager::SKOLEM_EXACT_NAME); + nm->mkFunctionType(args, nm->mkBitVectorType(1U)), + "floatingpoint_min_zero_case"); d_minMap.insert(t, fun); } else @@ -84,11 +81,8 @@ Node FpExpandDefs::maxUF(Node node) args[0] = t; args[1] = t; fun = sm->mkDummySkolem("floatingpoint_max_zero_case", - nm->mkFunctionType(args, - nm->mkBitVectorType(1U) - ), - "floatingpoint_max_zero_case", - NodeManager::SKOLEM_EXACT_NAME); + nm->mkFunctionType(args, nm->mkBitVectorType(1U)), + "floatingpoint_max_zero_case"); d_maxMap.insert(t, fun); } else @@ -121,8 +115,7 @@ Node FpExpandDefs::toUBVUF(Node node) args[1] = source; fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case", nm->mkFunctionType(args, target), - "floatingpoint_to_ubv_out_of_range_case", - NodeManager::SKOLEM_EXACT_NAME); + "floatingpoint_to_ubv_out_of_range_case"); d_toUBVMap.insert(p, fun); } else @@ -155,8 +148,7 @@ Node FpExpandDefs::toSBVUF(Node node) args[1] = source; fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case", nm->mkFunctionType(args, target), - "floatingpoint_to_sbv_out_of_range_case", - NodeManager::SKOLEM_EXACT_NAME); + "floatingpoint_to_sbv_out_of_range_case"); d_toSBVMap.insert(p, fun); } else @@ -183,8 +175,7 @@ Node FpExpandDefs::toRealUF(Node node) args[0] = t; fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case", nm->mkFunctionType(args, nm->realType()), - "floatingpoint_to_real_infinity_and_NaN_case", - NodeManager::SKOLEM_EXACT_NAME); + "floatingpoint_to_real_infinity_and_NaN_case"); d_toRealMap.insert(t, fun); } else diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 5af838354..b3033aedb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -188,10 +188,8 @@ Node SygusUnifRl::purifyLemma(Node n, // Build purified head with fresh skolem and recreate node std::stringstream ss; ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++; - Node new_f = sm->mkDummySkolem(ss.str(), - nb[0].getType(), - "head of unif evaluation point", - NodeManager::SKOLEM_EXACT_NAME); + Node new_f = sm->mkDummySkolem( + ss.str(), nb[0].getType(), "head of unif evaluation point"); // Adds new enumerator to map from candidate Trace("sygus-unif-rl-purify") << "...new enum " << new_f << " for candidate " << nb[0] << "\n"; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 324d6b7dc..a87466fab 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1407,8 +1407,7 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) stringstream stream; stream << "chooseUf" << setType.getId(); string name = stream.str(); - Node chooseSkolem = sm->mkDummySkolem( - name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME); + Node chooseSkolem = sm->mkDummySkolem(name, chooseUf, "choose function"); d_chooseFunctions[setType] = chooseSkolem; return chooseSkolem; } diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 60e6b6a01..fc68ddfc4 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -109,8 +109,8 @@ Node SkolemCache::mkTypedSkolemCached( { // for sequences of Booleans, we may purify Boolean terms, in which case // they must be Boolean term variables. - int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR - : NodeManager::SKOLEM_DEFAULT; + int flags = a.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR + : SkolemManager::SKOLEM_DEFAULT; sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags); } break; diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 5ad7010ed..b170ccbb6 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -532,13 +532,13 @@ TEST_F(TestNodeBlackNode, toString) TypeNode booleanType = d_nodeManager->booleanType(); Node w = d_skolemManager->mkDummySkolem( - "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "w", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node x = d_skolemManager->mkDummySkolem( - "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "x", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node y = d_skolemManager->mkDummySkolem( - "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "y", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node z = d_skolemManager->mkDummySkolem( - "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "z", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder() << w << x << kind::OR; Node n = NodeBuilder() << m << y << z << kind::AND; @@ -550,13 +550,13 @@ TEST_F(TestNodeBlackNode, toStream) TypeNode booleanType = d_nodeManager->booleanType(); Node w = d_skolemManager->mkDummySkolem( - "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "w", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node x = d_skolemManager->mkDummySkolem( - "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "x", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node y = d_skolemManager->mkDummySkolem( - "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "y", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node z = d_skolemManager->mkDummySkolem( - "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + "z", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder() << x << y << kind::OR; Node n = NodeBuilder() << w << m << z << kind::AND; Node o = NodeBuilder() << n << n << kind::XOR; @@ -619,13 +619,13 @@ TEST_F(TestNodeBlackNode, dagifier) TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType); Node x = d_skolemManager->mkDummySkolem( - "x", intType, "", NodeManager::SKOLEM_EXACT_NAME); + "x", intType, "", SkolemManager::SKOLEM_EXACT_NAME); Node y = d_skolemManager->mkDummySkolem( - "y", intType, "", NodeManager::SKOLEM_EXACT_NAME); + "y", intType, "", SkolemManager::SKOLEM_EXACT_NAME); Node f = d_skolemManager->mkDummySkolem( - "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + "f", fnType, "", SkolemManager::SKOLEM_EXACT_NAME); Node g = d_skolemManager->mkDummySkolem( - "g", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + "g", fnType, "", SkolemManager::SKOLEM_EXACT_NAME); Node fx = d_nodeManager->mkNode(APPLY_UF, f, x); Node fy = d_nodeManager->mkNode(APPLY_UF, f, y); Node gx = d_nodeManager->mkNode(APPLY_UF, g, x); diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index de0c76ce1..b02790cb5 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -122,7 +122,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode) TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name) { Node x = d_skolemManager->mkDummySkolem( - "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME); + "x", *d_boolTypeNode, "", SkolemManager::SKOLEM_EXACT_NAME); ASSERT_EQ(x.getKind(), SKOLEM); ASSERT_EQ(x.getNumChildren(), 0u); ASSERT_EQ(x.getAttribute(VarNameAttr()), "x"); diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 0a2bcb532..4d6bade95 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -90,13 +90,15 @@ Node operator*(const Node& a, const Node& b) Node operator!(const Node& a) { return nodeManager->mkNode(Kind::NOT, a); } Node make_real_variable(const std::string& s) { - return nodeManager->mkSkolem( - s, nodeManager->realType(), "", NodeManager::SKOLEM_EXACT_NAME); + SkolemManager* sm = nodeManager->getSkolemManager(); + return sm->mkDummySkolem( + s, nodeManager->realType(), "", SkolemManager::SKOLEM_EXACT_NAME); } Node make_int_variable(const std::string& s) { - return nodeManager->mkSkolem( - s, nodeManager->integerType(), "", NodeManager::SKOLEM_EXACT_NAME); + SkolemManager* sm = nodeManager->getSkolemManager(); + return sm->mkDummySkolem( + s, nodeManager->integerType(), "", SkolemManager::SKOLEM_EXACT_NAME); } TEST_F(TestTheoryWhiteArithCAD, test_univariate_isolation) -- 2.30.2