From 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Apr 2021 13:36:15 -0500 Subject: [PATCH] Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291) This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions. This PR also eliminates some unused code in TheoryArithPrivate. Followup PRs will start formalizing/eliminating calls to mkDummySkolem. --- src/expr/dtype.cpp | 10 +- src/expr/dtype_cons.cpp | 16 +- src/expr/node_manager.h | 37 +- src/expr/skolem_manager.cpp | 8 + src/expr/skolem_manager.h | 22 + src/expr/subs.cpp | 4 +- src/expr/sygus_datatype.cpp | 4 +- src/preprocessing/passes/ackermann.cpp | 14 +- src/preprocessing/passes/bv_to_int.cpp | 15 +- src/preprocessing/passes/fun_def_fmf.cpp | 6 +- src/preprocessing/passes/ho_elim.cpp | 12 +- src/preprocessing/passes/int_to_bv.cpp | 10 +- src/preprocessing/passes/miplib_trick.cpp | 4 +- src/preprocessing/passes/nl_ext_purify.cpp | 12 +- .../passes/quantifier_macros.cpp | 15 +- src/preprocessing/passes/real_to_int.cpp | 9 +- src/preprocessing/passes/sep_skolem_emp.cpp | 18 +- .../passes/unconstrained_simplifier.cpp | 4 +- src/preprocessing/util/ite_utilities.cpp | 16 +- src/smt/quant_elim_solver.cpp | 3 +- src/smt/sygus_solver.cpp | 4 +- src/theory/arith/arith_ite_utils.cpp | 4 +- src/theory/arith/arith_utilities.h | 14 - src/theory/arith/callbacks.cpp | 5 +- src/theory/arith/dio_solver.cpp | 8 +- src/theory/arith/nl/cad_solver.cpp | 12 +- .../arith/nl/transcendental/sine_solver.cpp | 4 +- .../transcendental/transcendental_solver.cpp | 6 +- src/theory/arith/theory_arith_private.cpp | 418 ------------------ src/theory/arith/theory_arith_private.h | 6 - .../builtin/theory_builtin_type_rules.cpp | 4 +- src/theory/bv/abstraction.cpp | 13 +- src/theory/bv/bv_subtheory_core.cpp | 4 +- src/theory/bv/theory_bv_utils.cpp | 9 +- src/theory/datatypes/sygus_extension.cpp | 17 +- src/theory/datatypes/theory_datatypes.cpp | 24 +- src/theory/engine_output_channel.cpp | 8 +- src/theory/fp/theory_fp.cpp | 76 ++-- src/theory/quantifiers/bv_inverter.cpp | 9 +- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 8 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 4 +- .../quantifiers/cegqi/vts_term_cache.cpp | 17 +- .../quantifiers/conjecture_generator.cpp | 8 +- src/theory/quantifiers/dynamic_rewrite.cpp | 8 +- src/theory/quantifiers/expr_miner.cpp | 4 +- .../quantifiers/fmf/bounded_integers.cpp | 9 +- .../quantifiers/fmf/first_order_model_fmc.cpp | 6 +- .../quantifiers/fmf/full_model_check.cpp | 4 +- .../quantifiers/quantifiers_rewriter.cpp | 4 +- .../quantifiers/single_inv_partition.cpp | 4 +- src/theory/quantifiers/skolemize.cpp | 44 +- .../sygus/ce_guided_single_inv.cpp | 15 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 19 +- .../quantifiers/sygus/rcons_type_info.cpp | 4 +- src/theory/quantifiers/sygus/sygus_abduct.cpp | 4 +- .../quantifiers/sygus/sygus_qe_preproc.cpp | 6 +- .../quantifiers/sygus/sygus_reconstruct.cpp | 9 +- .../quantifiers/sygus/sygus_repair_const.cpp | 4 +- .../quantifiers/sygus/sygus_unif_rl.cpp | 10 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 10 +- src/theory/quantifiers/sygus/sygus_utils.cpp | 7 +- .../quantifiers/sygus/synth_conjecture.cpp | 12 +- .../quantifiers/sygus/template_infer.cpp | 4 +- .../quantifiers/sygus/term_database_sygus.cpp | 11 +- .../sygus/transition_inference.cpp | 8 +- src/theory/quantifiers/sygus_inst.cpp | 4 +- src/theory/quantifiers/term_database.cpp | 20 +- src/theory/sep/theory_sep.cpp | 31 +- src/theory/sets/cardinality_extension.cpp | 8 +- src/theory/sets/skolem_cache.cpp | 4 +- src/theory/sets/term_registry.cpp | 4 +- src/theory/sets/theory_sets_private.cpp | 3 +- src/theory/sets/theory_sets_rels.cpp | 36 +- src/theory/sort_inference.cpp | 62 ++- src/theory/strings/regexp_operation.cpp | 4 +- src/theory/strings/skolem_cache.cpp | 3 +- .../strings/theory_strings_preprocess.cpp | 18 +- src/theory/uf/cardinality_extension.cpp | 8 +- src/theory/uf/ho_extension.cpp | 11 +- test/unit/node/attribute_black.cpp | 10 +- test/unit/node/node_algorithm_black.cpp | 13 +- test/unit/node/node_black.cpp | 89 ++-- test/unit/node/node_builder_black.cpp | 26 +- test/unit/node/node_manager_black.cpp | 50 +-- test/unit/node/node_manager_white.cpp | 4 +- test/unit/node/node_self_iterator_black.cpp | 4 +- test/unit/test_node.h | 3 + test/unit/test_smt.h | 5 + .../theory/theory_bags_rewriter_white.cpp | 27 +- .../theory_quantifiers_bv_inverter_white.cpp | 10 +- .../theory_strings_skolem_cache_black.cpp | 10 +- .../util/boolean_simplification_black.cpp | 16 +- 92 files changed, 703 insertions(+), 907 deletions(-) diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 3302be018..48c0e9f00 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -17,6 +17,7 @@ #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "expr/type_matcher.h" using namespace cvc5::kind; @@ -882,10 +883,11 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const NodeManager* nm = NodeManager::currentNM(); std::stringstream ss; ss << "sel_" << index; - s = nm->mkSkolem(ss.str(), - nm->mkSelectorType(dtt, t), - "is a shared selector", - NodeManager::SKOLEM_NO_NOTIFY); + SkolemManager* sm = nm->getSkolemManager(); + s = sm->mkDummySkolem(ss.str(), + nm->mkSelectorType(dtt, t), + "is a shared selector", + NodeManager::SKOLEM_NO_NOTIFY); 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 ce15c7ede..927c48dda 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -15,6 +15,7 @@ #include "expr/dtype.h" #include "expr/node_manager.h" +#include "expr/skolem_manager.h" #include "expr/type_matcher.h" #include "options/datatypes_options.h" @@ -45,8 +46,8 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType) // create the proper selector type) Assert(!isResolved()); Assert(!selectorType.isNull()); - - Node type = NodeManager::currentNM()->mkSkolem( + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node type = sm->mkDummySkolem( "unresolved_" + selectorName, selectorType, "is an unresolved selector type placeholder", @@ -505,6 +506,7 @@ bool DTypeConstructor::resolve( << std::endl; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); size_t index = 0; std::vector argTypes; Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl; @@ -523,7 +525,7 @@ bool DTypeConstructor::resolve( { Trace("datatypes-init") << " ...self selector" << std::endl; range = self; - arg->d_selector = nm->mkSkolem( + arg->d_selector = sm->mkDummySkolem( argName, nm->mkSelectorType(self, self), "is a selector", @@ -544,7 +546,7 @@ bool DTypeConstructor::resolve( { Trace("datatypes-init") << " ...resolved selector" << std::endl; range = (*j).second; - arg->d_selector = nm->mkSkolem( + arg->d_selector = sm->mkDummySkolem( argName, nm->mkSelectorType(self, range), "is a selector", @@ -574,7 +576,7 @@ bool DTypeConstructor::resolve( } Trace("datatypes-init") << " ...range after parametric substitution " << range << std::endl; - arg->d_selector = nm->mkSkolem( + arg->d_selector = sm->mkDummySkolem( argName, nm->mkSelectorType(self, range), "is a selector", @@ -603,12 +605,12 @@ 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 = nm->mkSkolem( + d_tester = sm->mkDummySkolem( testerName, nm->mkTesterType(self), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); - d_constructor = nm->mkSkolem( + d_constructor = sm->mkDummySkolem( getName(), nm->mkConstructorType(argTypes, self), "is a constructor", diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index a72eada23..465ddf588 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -87,6 +87,7 @@ class NodeManager friend class api::Solver; friend class expr::NodeValue; friend class expr::TypeChecker; + friend class SkolemManager; friend class NodeBuilder; friend class NodeManagerScope; @@ -366,7 +367,7 @@ class NodeManager * lookup is done on the name. If you mkVar("a", type) and then * mkVar("a", type) again, you have two variables. The NodeManager * version of this is private to avoid internal uses of mkVar() from - * within CVC4. Such uses should employ mkSkolem() instead. + * within CVC4. Such uses should employ SkolemManager::mkSkolem() instead. */ Node mkVar(const std::string& name, const TypeNode& type); Node* mkVarPtr(const std::string& name, const TypeNode& type); @@ -375,6 +376,19 @@ class NodeManager Node mkVar(const TypeNode& type); Node* mkVarPtr(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: explicit NodeManager(); ~NodeManager(); @@ -578,27 +592,6 @@ class NodeManager SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ }; /* enum SkolemFlags */ - /** - * Create a skolem constant with the given name, type, and comment. - * - * @param prefix the name of the new skolem variable is the prefix - * appended with a unique ID. This way a family of skolem variables - * can be made with unique identifiers, used in dump, tracing, and - * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want - * a unique ID appended and use prefix as the name. - * - * @param type the type of the skolem variable to create - * - * @param comment a comment for dumping output; if declarations are - * 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 - */ - Node mkSkolem(const std::string& prefix, const TypeNode& type, - const std::string& comment = "", int flags = SKOLEM_DEFAULT); - /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index a823d5b60..8ca8810b1 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -204,6 +204,14 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal) return it->second; } +Node SkolemManager::mkDummySkolem(const std::string& prefix, + const TypeNode& type, + const std::string& comment, + int flags) +{ + return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags); +} + Node SkolemManager::mkBooleanTermVariable(Node t) { return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR); diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 1295b2249..6cebee5d9 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -227,6 +227,28 @@ class SkolemManager Node mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal = Node::null()); + /** + * Create a skolem constant with the given name, type, and comment. This + * should only be used if the definition of the skolem does not matter. + * The definition of a skolem matters e.g. when the skolem is used in a + * proof. + * + * @param prefix the name of the new skolem variable is the prefix + * appended with a unique ID. This way a family of skolem variables + * can be made with unique identifiers, used in dump, tracing, and + * debugging output. Use SKOLEM_EXACT_NAME flag if you don't want + * a unique ID appended and use prefix as the name. + * @param type the type of the skolem variable to create + * @param comment a comment for dumping output; if declarations are + * 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 + */ + Node mkDummySkolem(const std::string& prefix, + const TypeNode& type, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT); /** * Make Boolean term variable for term t. This is a special case of * mkPurifySkolem above, where the returned term has kind diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index c2138499b..8c1d67c47 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -16,6 +16,7 @@ #include +#include "expr/skolem_manager.h" #include "theory/rewriter.h" namespace cvc5 { @@ -44,8 +45,9 @@ Node Subs::getSubs(Node v) const void Subs::add(Node v) { + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); // default, use a fresh skolem of the same type - Node s = NodeManager::currentNM()->mkSkolem("sk", v.getType()); + Node s = sm->mkDummySkolem("sk", v.getType()); add(v, s); } diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index 929c8a97c..82585eabe 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -15,6 +15,7 @@ #include "expr/sygus_datatype.h" #include +#include "expr/skolem_manager.h" using namespace cvc5::kind; @@ -38,8 +39,9 @@ void SygusDatatype::addConstructor(Node op, void SygusDatatype::addAnyConstantConstructor(TypeNode tn) { + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); // add an "any constant" proxy variable - Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn); + Node av = sm->mkDummySkolem("_any_constant", tn); // mark that it represents any constant SygusAnyConstAttribute saca; av.setAttribute(saca, true); diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index a19994ad9..525d0b243 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -27,6 +27,7 @@ #include "base/check.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" @@ -105,10 +106,12 @@ void storeFunctionAndAddLemmas(TNode func, if (set.find(term) == set.end()) { TypeNode tn = term.getType(); - Node skolem = nm->mkSkolem("SKOLEM$$", - tn, - "is a variable created by the ackermannization " - "preprocessing pass"); + SkolemManager* sm = nm->getSkolemManager(); + Node skolem = + sm->mkDummySkolem("SKOLEM$$", + tn, + "is a variable created by the ackermannization " + "preprocessing pass"); for (const auto& t : set) { addLemmaForPair(t, term, func, assertions, nm); @@ -206,12 +209,13 @@ void collectUSortsToBV(const std::unordered_set& vars, SubstitutionMap& usVarsToBVVars) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (TNode var : vars) { TypeNode type = var.getType(); size_t size = getBVSkolemSize(usortCardinality.at(type)); - Node skolem = nm->mkSkolem( + Node skolem = sm->mkDummySkolem( "BVSKOLEM$$", nm->mkBitVectorType(size), "a variable created by the ackermannization " diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index c5f24c15c..28dcc1949 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" @@ -702,6 +703,7 @@ Node BVToInt::translateWithChildren(Node original, Node BVToInt::translateNoChildren(Node original) { + SkolemManager* sm = d_nm->getSkolemManager(); Node translation; Assert(original.isVar() || original.isConst()); if (original.isVar()) @@ -722,11 +724,11 @@ Node BVToInt::translateNoChildren(Node original) // New integer variables that are not bound (symbolic constants) // are added together with range constraints induced by the // bit-width of the original bit-vector variables. - Node newVar = d_nm->mkSkolem("__bvToInt_var", - d_nm->integerType(), - "Variable introduced in bvToInt " - "pass instead of original variable " - + original.toString()); + Node newVar = sm->mkDummySkolem("__bvToInt_var", + d_nm->integerType(), + "Variable introduced in bvToInt " + "pass instead of original variable " + + original.toString()); uint64_t bvsize = original.getType().getBitVectorSize(); translation = newVar; d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize)); @@ -783,9 +785,10 @@ Node BVToInt::translateFunctionSymbol(Node bvUF) { intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d); } + SkolemManager* sm = d_nm->getSkolemManager(); ostringstream os; os << "__bvToInt_fun_" << bvUF << "_int"; - intUF = d_nm->mkSkolem( + intUF = sm->mkDummySkolem( os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function"); // introduce a `define-fun` in the smt-engine to keep // the correspondence between the original diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index c6ea0ee27..8d1fed4a3 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -16,6 +16,7 @@ #include +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" @@ -92,6 +93,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) std::map subs_head; // first pass : find defined functions, transform quantifiers NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (size_t i = 0, asize = assertions.size(); i < asize; i++) { Node n = QuantAttributes::getFunDefHead(assertions[i]); @@ -129,8 +131,8 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) TypeNode typ = nm->mkFunctionType(iType, n[j].getType()); std::stringstream ssf; ssf << f << "_arg_" << j; - d_input_arg_inj[f].push_back( - nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf")); + d_input_arg_inj[f].push_back(sm->mkDummySkolem( + ssf.str(), typ, "op created during fun def fmf")); } // construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 1bf980c49..619f3cfe2 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -19,6 +19,7 @@ #include #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" @@ -36,6 +37,7 @@ HoElim::HoElim(PreprocessingPassContext* preprocContext) Node HoElim::eliminateLambdaComplete(Node n, std::map& newLambda) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::unordered_map::iterator it; std::vector visit; TNode cur; @@ -90,7 +92,7 @@ Node HoElim::eliminateLambdaComplete(Node n, std::map& newLambda) } TypeNode rangeType = cur.getType().getRangeType(); TypeNode nft = nm->mkFunctionType(ftypes, rangeType); - Node nf = nm->mkSkolem("ll", nft); + Node nf = sm->mkDummySkolem("ll", nft); Trace("ho-elim-ll") << "...introduce: " << nf << " of type " << nft << std::endl; newLambda[nf] = nlambda; @@ -151,6 +153,7 @@ Node HoElim::eliminateHo(Node n) { Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::unordered_map::iterator it; std::map preReplace; std::map::iterator itr; @@ -187,7 +190,7 @@ Node HoElim::eliminateHo(Node n) } else { - ret = nm->mkSkolem("k", ut); + ret = sm->mkDummySkolem("k", ut); } // must get the ho apply to ensure extensionality is applied Node hoa = getHoApplyUf(tn); @@ -260,7 +263,7 @@ Node HoElim::eliminateHo(Node n) { Assert(!childrent.empty()); TypeNode newFType = nm->mkFunctionType(childrent, cur.getType()); - retOp = nm->mkSkolem("rf", newFType); + retOp = sm->mkDummySkolem("rf", newFType); d_visited_op[op] = retOp; } else @@ -485,12 +488,13 @@ Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr) if (it == d_hoApplyUf.end()) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::vector hoTypeArgs; hoTypeArgs.push_back(tnf); hoTypeArgs.push_back(tna); TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr); - Node k = NodeManager::currentNM()->mkSkolem("ho", tnh); + Node k = sm->mkDummySkolem("ho", tnh); d_hoApplyUf[tnf] = k; return k; } diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index ef9b261b0..1f223ad4f 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" @@ -102,13 +103,14 @@ Node intToBV(TNode n, NodeMap& cache) AlwaysAssert(size > 0); AlwaysAssert(!options::incrementalSolving()); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); NodeMap binaryCache; Node n_binary = intToBVMakeBinary(n, binaryCache); for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER, [&cache](TNode nn) { return cache.count(nn) > 0; })) { - NodeManager* nm = NodeManager::currentNM(); if (current.getNumChildren() > 0) { // Not a leaf @@ -208,9 +210,9 @@ Node intToBV(TNode n, NodeMap& cache) { if (current.getType() == nm->integerType()) { - result = nm->mkSkolem("__intToBV_var", - nm->mkBitVectorType(size), - "Variable introduced in intToBV pass"); + result = sm->mkDummySkolem("__intToBV_var", + nm->mkBitVectorType(size), + "Variable introduced in intToBV pass"); } } else if (current.isConst()) diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index f3c4d2e12..9ca58c334 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -19,6 +19,7 @@ #include #include "expr/node_self_iterator.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" @@ -201,6 +202,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( SubstitutionMap& top_level_substs = tlsm.get(); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); Node trueNode = nm->mkConst(true); @@ -522,7 +524,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( { stringstream ss; ss << "mipvar_" << *ii; - Node newVar = nm->mkSkolem( + Node newVar = sm->mkDummySkolem( ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index 838a2a767..f07c5419f 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -16,6 +16,7 @@ #include "preprocessing/passes/nl_ext_purify.h" +#include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" @@ -32,6 +33,8 @@ Node NlExtPurify::purifyNlTerms(TNode n, std::vector& var_eq, bool beneathMult) { + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (beneathMult) { NodeMap::iterator find = bcache.find(n); @@ -69,10 +72,9 @@ Node NlExtPurify::purifyNlTerms(TNode n, else { // new variable - ret = NodeManager::currentNM()->mkSkolem( - "__purifyNl_var", - n.getType(), - "Variable introduced in purifyNl pass"); + ret = sm->mkDummySkolem("__purifyNl_var", + n.getType(), + "Variable introduced in purifyNl pass"); Node np = purifyNlTerms(n, cache, bcache, var_eq, false); var_eq.push_back(np.eqNode(ret)); Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np @@ -92,7 +94,7 @@ Node NlExtPurify::purifyNlTerms(TNode n, } if (childChanged) { - ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + ret = nm->mkNode(n.getKind(), children); } } } diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 8251183dd..6c97936b0 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -18,6 +18,7 @@ #include +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" @@ -323,6 +324,8 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ Trace("macros-debug") << " process " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if( n.getKind()==NOT ){ return process( n[0], !pol, args, f ); }else if( n.getKind()==AND || n.getKind()==OR ){ @@ -335,11 +338,14 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod if( isBoundVarApplyUf( n ) ){ Node op = n.getOperator(); if( d_macro_defs.find( op )==d_macro_defs.end() ){ - Node n_def = NodeManager::currentNM()->mkConst( pol ); + Node n_def = nm->mkConst(pol); for( unsigned i=0; imkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" ); + Node v = + sm->mkDummySkolem(ss.str(), + n[i].getType(), + "created during macro definition recognition"); d_macro_basis[op].push_back( v ); } //contains no ops @@ -392,7 +398,10 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod for( size_t a=0; amkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); + Node v = sm->mkDummySkolem( + ss.str(), + m[a].getType(), + "created during macro definition recognition"); d_macro_basis[op].push_back( v ); } } diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index c80d55d3d..d8993ff1b 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -18,6 +18,7 @@ #include +#include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "theory/arith/arith_msum.h" @@ -42,6 +43,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va else { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node ret = n; if (n.getNumChildren() > 0) { @@ -178,9 +180,10 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va } else if (n.isVar()) { - ret = nm->mkSkolem("__realToIntInternal_var", - nm->integerType(), - "Variable introduced in realToIntInternal pass"); + ret = sm->mkDummySkolem( + "__realToIntInternal_var", + nm->integerType(), + "Variable introduced in realToIntInternal pass"); var_eq.push_back(n.eqNode(ret)); // ensure that the original variable is defined to be the returned // one, which is important for models and for incremental solving. diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 8c130768d..0c5ca9af9 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -20,6 +20,7 @@ #include #include "expr/node.h" +#include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" #include "theory/quantifiers/quant_util.h" #include "theory/rewriter.h" @@ -41,6 +42,8 @@ Node preSkolemEmp(Node n, std::map::iterator it = visited[pol].find(n); if (it == visited[pol].end()) { + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol << std::endl; Node ret = n; @@ -50,14 +53,13 @@ Node preSkolemEmp(Node n, { TypeNode tnx = n[0].getType(); TypeNode tny = n[1].getType(); - Node x = NodeManager::currentNM()->mkSkolem( - "ex", tnx, "skolem location for negated emp"); - Node y = NodeManager::currentNM()->mkSkolem( - "ey", tny, "skolem data for negated emp"); - return NodeManager::currentNM() + Node x = + sm->mkDummySkolem("ex", tnx, "skolem location for negated emp"); + Node y = sm->mkDummySkolem("ey", tny, "skolem data for negated emp"); + return nm ->mkNode(kind::SEP_STAR, - NodeManager::currentNM()->mkNode(kind::SEP_PTO, x, y), - NodeManager::currentNM()->mkConst(true)) + nm->mkNode(kind::SEP_PTO, x, y), + nm->mkConst(true)) .negate(); } } @@ -83,7 +85,7 @@ Node preSkolemEmp(Node n, } if (childChanged) { - return NodeManager::currentNM()->mkNode(n.getKind(), children); + return nm->mkNode(n.getKind(), children); } } visited[pol][n] = ret; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 9a9aaa366..2c01bd6d2 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -19,6 +19,7 @@ #include "preprocessing/passes/unconstrained_simplifier.h" #include "expr/dtype.h" +#include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/logic_exception.h" @@ -126,7 +127,8 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkSkolem( + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node n = sm->mkDummySkolem( "unconstrained", t, "a new var introduced because of unconstrained variable " diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 7826c207b..5433368fa 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -21,6 +21,7 @@ #include +#include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/passes/rewrite.h" #include "smt/smt_statistics_registry.h" @@ -353,7 +354,8 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed) else { NodeManager* nm = NodeManager::currentNM(); - Node skolem = nm->mkSkolem("compress", nm->booleanType()); + SkolemManager* sm = nm->getSkolemManager(); + Node skolem = sm->mkDummySkolem("compress", nm->booleanType()); d_compressed[rewritten] = skolem; d_compressed[original] = skolem; d_compressed[compressed] = skolem; @@ -1386,13 +1388,11 @@ Node ITESimplifier::getSimpVar(TypeNode t) { return (*it).second; } - else - { - Node var = NodeManager::currentNM()->mkSkolem( - "iteSimp", t, "is a variable resulting from ITE simplification"); - d_simpVars[t] = var; - return var; - } + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node var = sm->mkDummySkolem( + "iteSimp", t, "is a variable resulting from ITE simplification"); + d_simpVars[t] = var; + return var; } Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index ddc20ee8d..436d6618d 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -45,6 +45,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, "Expecting a quantified formula as argument to get-qe."); } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); // ensure the body is rewritten q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary @@ -53,7 +54,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, << q << std::endl; // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); - Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); + Node n_attr = sm->mkDummySkolem("qe", t, "Auxiliary variable for qe attr."); std::vector node_values; TheoryEngine* te = d_smtSolver.getTheoryEngine(); Assert(te != nullptr); diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 27e16ccc6..022691a12 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -17,6 +17,7 @@ #include #include "expr/dtype.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "printer/printer.h" @@ -261,6 +262,7 @@ void SygusSolver::printSynthSolution(std::ostream& out) void SygusSolver::checkSynthSolution(Assertions& as) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution" << std::endl; std::map> sol_map; @@ -363,7 +365,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) vars.push_back(conj[1][0][j]); std::stringstream ss; ss << "sk_" << j; - skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType())); + skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType())); Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to " << skos.back() << "\n"; } diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 218fdf179..64309ad16 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -20,6 +20,7 @@ #include #include "base/output.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" @@ -441,10 +442,11 @@ bool ArithIteUtils::solveBinOr(TNode binor){ // a: (sel = otherL) or (sel = otherR), otherL-otherR = c NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node cnd = findIteCnd(binor[0], binor[1]); - Node sk = nm->mkSkolem("deor", nm->booleanType()); + Node sk = sm->mkDummySkolem("deor", nm->booleanType()); Node ite = sk.iteNode(otherL, otherR); d_skolems.insert(sk, cnd); addSubstitution(sel, ite); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index bc35c6941..c9f572364 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -49,20 +49,6 @@ inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst(b); } -inline Node mkIntSkolem(const std::string& name){ - return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType()); -} - -inline Node mkRealSkolem(const std::string& name){ - return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType()); -} - -inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){ - NodeManager* currNM = NodeManager::currentNM(); - TypeNode functionType = currNM->mkFunctionType(dom, range); - return currNM->mkSkolem(name, functionType); -} - /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */ inline bool isRelationOperator(Kind k){ using namespace kind; diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index b2c48163f..0043ccae6 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -18,6 +18,7 @@ #include "theory/arith/callbacks.h" #include "expr/proof_node.h" +#include "expr/skolem_manager.h" #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" @@ -46,7 +47,9 @@ TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta) : d_ta(ta) {} ArithVar TempVarMalloc::request(){ - Node skolem = mkRealSkolem("tmpVar"); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node skolem = sm->mkDummySkolem("tmpVar", nm->realType()); return d_ta.requestArithVar(skolem, false, true); } void TempVarMalloc::release(ArithVar v){ diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 3825a3a42..6ceab1933 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -18,6 +18,7 @@ #include #include "base/output.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/partial_model.h" @@ -29,8 +30,11 @@ namespace theory { namespace arith { inline Node makeIntegerVariable(){ - NodeManager* curr = NodeManager::currentNM(); - return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver"); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + return sm->mkDummySkolem("intvar", + nm->integerType(), + "is an integer variable created by the dio solver"); } DioSolver::DioSolver(context::Context* ctxt) diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 1cf9cbc54..aa9bce776 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -14,11 +14,12 @@ #include "theory/arith/nl/cad_solver.h" -#include "theory/inference_id.h" +#include "expr/skolem_manager.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" +#include "theory/inference_id.h" namespace cvc5 { namespace theory { @@ -37,11 +38,10 @@ CadSolver::CadSolver(InferenceManager& im, d_im(im), d_model(model) { - d_ranVariable = - NodeManager::currentNM()->mkSkolem("__z", - NodeManager::currentNM()->realType(), - "", - NodeManager::SKOLEM_EXACT_NAME); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + d_ranVariable = sm->mkDummySkolem( + "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME); #ifdef CVC4_POLY_IMP ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; if (pc != nullptr) diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index c8c375096..2a1f2ad91 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -20,6 +20,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "expr/proof.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -55,10 +56,11 @@ SineSolver::~SineSolver() {} void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Assert(a.getKind() == Kind::SINE); Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl; Assert(!d_data->d_pi.isNull()); - Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts"); + Node shift = sm->mkDummySkolem("s", nm->integerType(), "number of shifts"); // TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based // refinement for constant shifts (cvc4-projects #1284) Node lem = nm->mkNode( diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index ed5ab4255..b3fd40ce7 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -56,14 +57,15 @@ void TranscendentalSolver::initLastCall(const std::vector& xts) } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (const Node& a : needsMaster) { // should not have processed this already Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end()); Kind k = a.getKind(); Assert(k == Kind::SINE || k == Kind::EXPONENTIAL); - Node y = - nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg"); + Node y = sm->mkDummySkolem( + "y", nm->realType(), "phase shifted trigonometric arg"); Node new_a = nm->mkNode(k, y); d_tstate.d_trSlaves[new_a].insert(new_a); d_tstate.d_trSlaves[new_a].insert(a); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0a64a4e63..7ad0bbfbb 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4958,16 +4958,6 @@ std::pair TheoryArithPrivate::entailmentCheck(TNode lit, const Arith setToMin(secDir * dm.sgn(), bestSecDiff, tmp); } break; - case inferbounds::Simplex: - { - // primDir * diffm * diff < c or primDir * diffm * diff > c - tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); - setToMin(primDir * dm.sgn(), bestPrimDiff, tmp); - - tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); - setToMin(secDir * dm.sgn(), bestSecDiff, tmp); - } - break; default: Unhandled(); } @@ -5298,419 +5288,11 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair& t tmp.first = nb; } -std::pair TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){ - - if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){ - return make_pair(Node::null(), DeltaRational()); - } - - Assert(d_qflraStatus == Result::SAT); - Assert(d_errorSet.noSignals()); - Assert(param.getAlgorithm() == inferbounds::Simplex); - - // TODO Move me into a new file - - enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; - ResultState finalState = Unset; - - const int maxRounds = - param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1; - - Maybe threshold; - // TODO: get this from the parameters - - // setup term - Polynomial p = Polynomial::parsePolynomial(tp); - vector variables; - vector coefficients; - asVectors(p, coefficients, variables); - if(sgn < 0){ - for(size_t i=0, N=coefficients.size(); i < N; ++i){ - coefficients[i] = -coefficients[i]; - } - } - // implicitly an upperbound - Node skolem = mkRealSkolem("tmpVar$$"); - ArithVar optVar = requestArithVar(skolem, false, true); - d_tableau.addRow(optVar, coefficients, variables); - RowIndex ridx = d_tableau.basicToRowIndex(optVar); - - DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); - d_partialModel.setAssignment(optVar, newAssignment); - d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); - - // Setup simplex - d_partialModel.stopQueueingBoundCounts(); - UpdateTrackingCallback utcb(&d_linEq); - d_partialModel.processBoundsQueue(utcb); - d_linEq.startTrackingBoundCounts(); - - // maximize optVar via primal Simplex - int rounds = 0; - while(finalState == Unset){ - ++rounds; - if(maxRounds >= 0 && rounds > maxRounds){ - finalState = ExhaustedRounds; - break; - } - - // select entering by bland's rule - // TODO improve upon bland's - ArithVar entering = ARITHVAR_SENTINEL; - const Tableau::Entry* enteringEntry = NULL; - for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ - const Tableau::Entry& entry = *ri; - ArithVar v = entry.getColVar(); - if(v != optVar){ - int sgn1 = entry.getCoefficient().sgn(); - Assert(sgn1 != 0); - bool candidate = (sgn1 > 0) - ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) - : (d_partialModel.cmpAssignmentLowerBound(v) != 0); - if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ - entering = v; - enteringEntry = &entry; - } - } - } - if(entering == ARITHVAR_SENTINEL){ - finalState = Inferred; - break; - } - Assert(entering != ARITHVAR_SENTINEL); - Assert(enteringEntry != NULL); - - int esgn = enteringEntry->getCoefficient().sgn(); - Assert(esgn != 0); - - // select leaving and ratio - ArithVar leaving = ARITHVAR_SENTINEL; - DeltaRational minRatio; - const Tableau::Entry* pivotEntry = NULL; - - // Special case check the upper/lowerbound on entering - ConstraintP cOnEntering = (esgn > 0) - ? d_partialModel.getUpperBoundConstraint(entering) - : d_partialModel.getLowerBoundConstraint(entering); - if(cOnEntering != NullConstraint){ - leaving = entering; - minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); - } - for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ - const Tableau::Entry& centry = *ci; - ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); - int csgn = centry.getCoefficient().sgn(); - int basicDir = csgn * esgn; - - ConstraintP bound = (basicDir > 0) - ? d_partialModel.getUpperBoundConstraint(basic) - : d_partialModel.getLowerBoundConstraint(basic); - if(bound != NullConstraint){ - DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); - DeltaRational ratio = diff/(centry.getCoefficient()); - bool selected = false; - if(leaving == ARITHVAR_SENTINEL){ - selected = true; - }else{ - int cmp = ratio.compare(minRatio); - if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ - selected = (cmp != 0) || - ((leaving != entering) && (basic < leaving)); - } - } - if(selected){ - leaving = basic; - minRatio = ratio; - pivotEntry = ¢ry; - } - } - } - - - if(leaving == ARITHVAR_SENTINEL){ - finalState = NoBound; - break; - }else if(leaving == entering){ - d_linEq.update(entering, minRatio); - }else{ - DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); - d_linEq.pivotAndUpdate(leaving, entering, newLeaving); - // no conflicts clear signals - Assert(d_errorSet.noSignals()); - } - - if(threshold.just()){ - if (d_partialModel.getAssignment(optVar) >= threshold.value()) - { - finalState = ReachedThreshold; - break; - } - } - }; - - result = InferBoundsResult(tp, sgn > 0); - - // tear down term - switch(finalState){ - case Inferred: - { - NodeBuilder nb(kind::AND); - for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ - const Tableau::Entry& e =*ri; - ArithVar colVar = e.getColVar(); - if(colVar != optVar){ - const Rational& q = e.getCoefficient(); - Assert(q.sgn() != 0); - ConstraintP c = (q.sgn() > 0) - ? d_partialModel.getUpperBoundConstraint(colVar) - : d_partialModel.getLowerBoundConstraint(colVar); - c->externalExplainByAssertions(nb); - } - } - Assert(nb.getNumChildren() >= 1); - Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; - result.setBound(d_partialModel.getAssignment(optVar), exp); - result.setIsOptimal(); - break; - } - case NoBound: - break; - case ReachedThreshold: - result.setReachedThreshold(); - break; - case ExhaustedRounds: - result.setBudgetExhausted(); - break; - case Unset: - default: - Unreachable(); - break; - }; - - d_linEq.stopTrackingRowIndex(ridx); - d_tableau.removeBasicRow(optVar); - releaseArithVar(optVar); - - d_linEq.stopTrackingBoundCounts(); - d_partialModel.startQueueingBoundCounts(); - - if(result.foundBound()){ - return make_pair(result.getExplanation(), result.getValue()); - }else{ - return make_pair(Node::null(), DeltaRational()); - } -} - ArithProofRuleChecker* TheoryArithPrivate::getProofChecker() { return &d_checker; } -// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const -// inferbounds::InferBoundAlgorithm& param){ -// Assert(param.findUpperBound()); - -// if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){ -// InferBoundsResult inconsistent; -// inconsistent.setInconsistent(); -// return inconsistent; -// } - -// Assert(d_qflraStatus == Result::SAT); -// Assert(d_errorSet.noSignals()); - -// // TODO Move me into a new file - -// enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; -// ResultState finalState = Unset; - -// int maxRounds = 0; -// switch(param.getParamKind()){ -// case InferBoundsParameters::Unbounded: -// maxRounds = -1; -// break; -// case InferBoundsParameters::NumVars: -// maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter(); -// break; -// case InferBoundsParameters::Direct: -// maxRounds = param.getSimplexRoundParameter(); -// break; -// default: maxRounds = 0; break; -// } - -// // setup term -// Polynomial p = Polynomial::parsePolynomial(t); -// vector variables; -// vector coefficients; -// asVectors(p, coefficients, variables); - -// Node skolem = mkRealSkolem("tmpVar$$"); -// ArithVar optVar = requestArithVar(skolem, false, true); -// d_tableau.addRow(optVar, coefficients, variables); -// RowIndex ridx = d_tableau.basicToRowIndex(optVar); - -// DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); -// d_partialModel.setAssignment(optVar, newAssignment); -// d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); - -// // Setup simplex -// d_partialModel.stopQueueingBoundCounts(); -// UpdateTrackingCallback utcb(&d_linEq); -// d_partialModel.processBoundsQueue(utcb); -// d_linEq.startTrackingBoundCounts(); - -// // maximize optVar via primal Simplex -// int rounds = 0; -// while(finalState == Unset){ -// ++rounds; -// if(maxRounds >= 0 && rounds > maxRounds){ -// finalState = ExhaustedRounds; -// break; -// } - -// // select entering by bland's rule -// // TODO improve upon bland's -// ArithVar entering = ARITHVAR_SENTINEL; -// const Tableau::Entry* enteringEntry = NULL; -// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); -// !ri.atEnd(); ++ri){ -// const Tableau::Entry& entry = *ri; -// ArithVar v = entry.getColVar(); -// if(v != optVar){ -// int sgn = entry.getCoefficient().sgn(); -// Assert(sgn != 0); -// bool candidate = (sgn > 0) -// ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) -// : (d_partialModel.cmpAssignmentLowerBound(v) != 0); -// if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ -// entering = v; -// enteringEntry = &entry; -// } -// } -// } -// if(entering == ARITHVAR_SENTINEL){ -// finalState = Inferred; -// break; -// } -// Assert(entering != ARITHVAR_SENTINEL); -// Assert(enteringEntry != NULL); - -// int esgn = enteringEntry->getCoefficient().sgn(); -// Assert(esgn != 0); - -// // select leaving and ratio -// ArithVar leaving = ARITHVAR_SENTINEL; -// DeltaRational minRatio; -// const Tableau::Entry* pivotEntry = NULL; - -// // Special case check the upper/lowerbound on entering -// ConstraintP cOnEntering = (esgn > 0) -// ? d_partialModel.getUpperBoundConstraint(entering) -// : d_partialModel.getLowerBoundConstraint(entering); -// if(cOnEntering != NullConstraint){ -// leaving = entering; -// minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); -// } -// for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ -// const Tableau::Entry& centry = *ci; -// ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); -// int csgn = centry.getCoefficient().sgn(); -// int basicDir = csgn * esgn; - -// ConstraintP bound = (basicDir > 0) -// ? d_partialModel.getUpperBoundConstraint(basic) -// : d_partialModel.getLowerBoundConstraint(basic); -// if(bound != NullConstraint){ -// DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); -// DeltaRational ratio = diff/(centry.getCoefficient()); -// bool selected = false; -// if(leaving == ARITHVAR_SENTINEL){ -// selected = true; -// }else{ -// int cmp = ratio.compare(minRatio); -// if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ -// selected = (cmp != 0) || -// ((leaving != entering) && (basic < leaving)); -// } -// } -// if(selected){ -// leaving = basic; -// minRatio = ratio; -// pivotEntry = ¢ry; -// } -// } -// } - -// if(leaving == ARITHVAR_SENTINEL){ -// finalState = NoBound; -// break; -// }else if(leaving == entering){ -// d_linEq.update(entering, minRatio); -// }else{ -// DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); -// d_linEq.pivotAndUpdate(leaving, entering, newLeaving); -// // no conflicts clear signals -// Assert(d_errorSet.noSignals()); -// } - -// if(param.useThreshold()){ -// if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){ -// finalState = ReachedThreshold; -// break; -// } -// } -// }; - -// InferBoundsResult result(t, param.findUpperBound()); - -// // tear down term -// switch(finalState){ -// case Inferred: -// { -// NodeBuilder nb(kind::AND); -// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); -// !ri.atEnd(); ++ri){ -// const Tableau::Entry& e =*ri; -// ArithVar colVar = e.getColVar(); -// if(colVar != optVar){ -// const Rational& q = e.getCoefficient(); -// Assert(q.sgn() != 0); -// ConstraintP c = (q.sgn() > 0) -// ? d_partialModel.getUpperBoundConstraint(colVar) -// : d_partialModel.getLowerBoundConstraint(colVar); -// c->externalExplainByAssertions(nb); -// } -// } -// Assert(nb.getNumChildren() >= 1); -// Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; -// result.setBound(d_partialModel.getAssignment(optVar), exp); -// result.setIsOptimal(); -// break; -// } -// case NoBound: -// break; -// case ReachedThreshold: -// result.setReachedThreshold(); -// break; -// case ExhaustedRounds: -// result.setBudgetExhausted(); -// break; -// case Unset: -// default: -// Unreachable(); -// break; -// }; - -// d_linEq.stopTrackingRowIndex(ridx); -// d_tableau.removeBasicRow(optVar); -// releaseArithVar(optVar); - -// d_linEq.stopTrackingBoundCounts(); -// d_partialModel.startQueueingBoundCounts(); - -// return result; -// } - } // namespace arith } // namespace theory } // namespace cvc5 diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index ba3fdfaf5..50fb89808 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -137,12 +137,6 @@ private: void entailmentCheckBoundLookup(std::pair& tmp, int sgn, TNode tp) const; void entailmentCheckRowSum(std::pair& tmp, int sgn, TNode tp) const; - std::pair entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out); - - //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p); - //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p); - //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p); - /** * Infers either a new upper/lower bound on term in the real relaxation. * Either: diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index c5ea17847..2d540010f 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -17,6 +17,7 @@ #include "theory/builtin/theory_builtin_type_rules.h" #include "expr/attribute.h" +#include "expr/skolem_manager.h" namespace cvc5 { namespace theory { @@ -39,7 +40,8 @@ Node SortProperties::mkGroundTerm(TypeNode type) { return type.getAttribute(gta); } - Node k = NodeManager::currentNM()->mkSkolem( + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node k = sm->mkDummySkolem( "groundTerm", type, "a ground term created for type " + type.toString()); type.setAttribute(gta, k); return k; diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index acb67a373..348c8bebb 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -14,6 +14,7 @@ **/ #include "theory/bv/abstraction.h" +#include "expr/skolem_manager.h" #include "options/bv_options.h" #include "printer/printer.h" #include "smt/dump.h" @@ -282,6 +283,7 @@ Node AbstractionModule::getSignatureSkolem(TNode node) { Assert(node.getMetaKind() == kind::metakind::VARIABLE); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); unsigned bitwidth = utils::getSize(node); if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) { @@ -296,9 +298,9 @@ Node AbstractionModule::getSignatureSkolem(TNode node) { ostringstream os; os << "sig_" << bitwidth << "_" << index; - skolems.push_back(nm->mkSkolem(os.str(), - nm->mkBitVectorType(bitwidth), - "skolem for computing signatures")); + skolems.push_back(sm->mkDummySkolem(os.str(), + nm->mkBitVectorType(bitwidth), + "skolem for computing signatures")); } ++(d_signatureIndices[bitwidth]); return skolems[index]; @@ -435,6 +437,7 @@ void AbstractionModule::storeGeneralization(TNode s, TNode t) { void AbstractionModule::finalizeSignatures() { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures num signatures = " << d_signatures.size() << "\n"; @@ -519,8 +522,8 @@ void AbstractionModule::finalizeSignatures() TypeNode range = nm->mkBitVectorType(1); TypeNode abs_type = nm->mkFunctionType(arg_types, range); - Node abs_func = - nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); + Node abs_func = sm->mkDummySkolem( + "abs_$$", abs_type, "abstraction function for bv theory"); Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; // NOTE: signature expression type is BOOLEAN diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 4f89eff71..de5210e1a 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -16,6 +16,7 @@ #include "theory/bv/bv_subtheory_core.h" +#include "expr/skolem_manager.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" @@ -537,6 +538,7 @@ bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; } bool CoreSolver::doExtfInferences(std::vector& terms) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); bool sentLemma = false; eq::EqualityEngine* ee = d_equalityEngine; std::map op_map; @@ -592,7 +594,7 @@ bool CoreSolver::doExtfInferences(std::vector& terms) // congruent modulo 2^( bv width ) unsigned bvs = n.getType().getBitVectorSize(); Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); - Node k = nm->mkSkolem( + Node k = sm->mkDummySkolem( "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence"); t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k)); } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 96f91ea9f..292010cf4 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -18,6 +18,7 @@ #include +#include "expr/skolem_manager.h" #include "options/theory_options.h" #include "theory/theory.h" @@ -278,10 +279,10 @@ Node mkConst(const BitVector& value) Node mkVar(unsigned size) { NodeManager* nm = NodeManager::currentNM(); - - return nm->mkSkolem("BVSKOLEM$$", - nm->mkBitVectorType(size), - "is a variable created by the theory of bitvectors"); + SkolemManager* sm = nm->getSkolemManager(); + return sm->mkDummySkolem("BVSKOLEM$$", + nm->mkBitVectorType(size), + "is a variable created by the theory of bitvectors"); } /* ------------------------------------------------------------------------- */ diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 14c004bda..31467df65 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -17,6 +17,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_manager.h" +#include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" #include "options/base_options.h" #include "options/datatypes_options.h" @@ -435,10 +436,11 @@ Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre) return itt->second; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::vector types; types.push_back(tn); TypeNode ptn = nm->mkPredicateType(types); - Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn); + Node pred = sm->mkDummySkolem(isPre ? "pre" : "post", ptn); d_traversal_pred[index][tn][n] = pred; return pred; } @@ -446,6 +448,7 @@ Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre) Node SygusExtension::eliminateTraversalPredicates(Node n) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::unordered_map visited; std::unordered_map::iterator it; std::map::iterator ittb; @@ -471,7 +474,7 @@ Node SygusExtension::eliminateTraversalPredicates(Node n) { std::stringstream ss; ss << "v_" << cur; - ret = nm->mkSkolem(ss.str(), cur.getType()); + ret = sm->mkDummySkolem(ss.str(), cur.getType()); d_traversal_bool[cur] = ret; } else @@ -1367,9 +1370,9 @@ void SygusExtension::registerSizeTerm(Node e) slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue()); }else{ Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(); - Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(true); + Node newMt = d_szinfo[m]->getOrMkActiveMeasureValue(true); Node ds = nm->mkNode(DT_SIZE, e); - slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds)); + slem = mt.eqNode(nm->mkNode(PLUS, newMt, ds)); } Trace("sygus-sb") << "...size lemma : " << slem << std::endl; d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND); @@ -1761,7 +1764,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue() if (d_measure_value.isNull()) { NodeManager* nm = NodeManager::currentNM(); - d_measure_value = nm->mkSkolem("mt", nm->integerType()); + SkolemManager* sm = nm->getSkolemManager(); + d_measure_value = sm->mkDummySkolem("mt", nm->integerType()); Node mtlem = nm->mkNode(kind::GEQ, d_measure_value, nm->mkConst(Rational(0))); d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); @@ -1775,7 +1779,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( if (mkNew) { NodeManager* nm = NodeManager::currentNM(); - Node new_mt = nm->mkSkolem("mt", nm->integerType()); + SkolemManager* sm = nm->getSkolemManager(); + Node new_mt = sm->mkDummySkolem("mt", nm->integerType()); Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConst(Rational(0))); d_measure_value_active = new_mt; d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 598b29cf6..df4560905 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -23,6 +23,7 @@ #include "expr/dtype_cons.h" #include "expr/kind.h" #include "expr/proof_node_manager.h" +#include "expr/skolem_manager.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -830,10 +831,12 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) { if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::stringstream ss; ss << sel << "_uf"; - d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), - NodeManager::currentNM()->mkFunctionType( dt, rt ) ); + d_exp_def_skolem[dt][sel] = + sm->mkDummySkolem(ss.str().c_str(), nm->mkFunctionType(dt, rt)); } } @@ -841,8 +844,11 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) { if( n.getKind()==APPLY_CONSTRUCTOR ){ NodeMap::const_iterator it = d_term_sk.find( n ); if( it==d_term_sk.end() ){ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); //add purification unit lemma ( k = n ) - Node k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "reference skolem for datatypes" ); + Node k = + sm->mkDummySkolem("k", n.getType(), "reference skolem for datatypes"); d_term_sk[n] = k; Node eq = k.eqNode( n ); Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl; @@ -1399,17 +1405,19 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c } Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); int index = pol ? 0 : 1; std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn ); if( it==d_singleton_lemma[index].end() ){ Node a; if( pol ){ - Node v1 = NodeManager::currentNM()->mkBoundVar( tn ); - Node v2 = NodeManager::currentNM()->mkBoundVar( tn ); - a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) ); + Node v1 = nm->mkBoundVar(tn); + Node v2 = nm->mkBoundVar(tn); + a = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v1, v2), v1.eqNode(v2)); }else{ - Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn ); - Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn ); + Node v1 = sm->mkDummySkolem("k1", tn); + Node v2 = sm->mkDummySkolem("k2", tn); a = v1.eqNode( v2 ).negate(); //send out immediately as lemma d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ); diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 0597bb3ea..08fa0164b 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -14,6 +14,7 @@ #include "theory/engine_output_channel.h" +#include "expr/skolem_manager.h" #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/theory_engine.h" @@ -118,10 +119,11 @@ void EngineOutputChannel::conflict(TNode conflictNode) void EngineOutputChannel::demandRestart() { - NodeManager* curr = NodeManager::currentNM(); - Node restartVar = curr->mkSkolem( + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node restartVar = sm->mkDummySkolem( "restartVar", - curr->booleanType(), + nm->booleanType(), "A boolean variable asserted to be true to force a restart"); Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 93b492b88..88d01ea20 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -23,6 +23,7 @@ #include #include "base/configuration.h" +#include "expr/skolem_manager.h" #include "options/fp_options.h" #include "smt/logic_exception.h" #include "theory/fp/fp_converter.h" @@ -205,6 +206,7 @@ Node TheoryFp::minUF(Node node) { Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ComparisonUFMap::const_iterator i(d_minMap.find(t)); Node fun; @@ -212,16 +214,16 @@ Node TheoryFp::minUF(Node node) { std::vector args(2); args[0] = t; args[1] = t; - fun = nm->mkSkolem("floatingpoint_min_zero_case", - nm->mkFunctionType(args, + fun = sm->mkDummySkolem("floatingpoint_min_zero_case", + nm->mkFunctionType(args, #ifdef SYMFPUPROPISBOOL - nm->booleanType() + nm->booleanType() #else - nm->mkBitVectorType(1U) + nm->mkBitVectorType(1U) #endif - ), - "floatingpoint_min_zero_case", - NodeManager::SKOLEM_EXACT_NAME); + ), + "floatingpoint_min_zero_case", + NodeManager::SKOLEM_EXACT_NAME); d_minMap.insert(t, fun); } else { fun = (*i).second; @@ -236,6 +238,7 @@ Node TheoryFp::maxUF(Node node) { Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ComparisonUFMap::const_iterator i(d_maxMap.find(t)); Node fun; @@ -243,16 +246,16 @@ Node TheoryFp::maxUF(Node node) { std::vector args(2); args[0] = t; args[1] = t; - fun = nm->mkSkolem("floatingpoint_max_zero_case", - nm->mkFunctionType(args, + fun = sm->mkDummySkolem("floatingpoint_max_zero_case", + nm->mkFunctionType(args, #ifdef SYMFPUPROPISBOOL - nm->booleanType() + nm->booleanType() #else - nm->mkBitVectorType(1U) + nm->mkBitVectorType(1U) #endif - ), - "floatingpoint_max_zero_case", - NodeManager::SKOLEM_EXACT_NAME); + ), + "floatingpoint_max_zero_case", + NodeManager::SKOLEM_EXACT_NAME); d_maxMap.insert(t, fun); } else { fun = (*i).second; @@ -271,6 +274,7 @@ Node TheoryFp::toUBVUF(Node node) { std::pair p(source, target); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ConversionUFMap::const_iterator i(d_toUBVMap.find(p)); Node fun; @@ -278,10 +282,10 @@ Node TheoryFp::toUBVUF(Node node) { std::vector args(2); args[0] = nm->roundingModeType(); args[1] = source; - fun = nm->mkSkolem("floatingpoint_to_ubv_out_of_range_case", - nm->mkFunctionType(args, target), - "floatingpoint_to_ubv_out_of_range_case", - NodeManager::SKOLEM_EXACT_NAME); + 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); d_toUBVMap.insert(p, fun); } else { fun = (*i).second; @@ -300,6 +304,7 @@ Node TheoryFp::toSBVUF(Node node) { std::pair p(source, target); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ConversionUFMap::const_iterator i(d_toSBVMap.find(p)); Node fun; @@ -307,10 +312,10 @@ Node TheoryFp::toSBVUF(Node node) { std::vector args(2); args[0] = nm->roundingModeType(); args[1] = source; - fun = nm->mkSkolem("floatingpoint_to_sbv_out_of_range_case", - nm->mkFunctionType(args, target), - "floatingpoint_to_sbv_out_of_range_case", - NodeManager::SKOLEM_EXACT_NAME); + 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); d_toSBVMap.insert(p, fun); } else { fun = (*i).second; @@ -324,16 +329,17 @@ Node TheoryFp::toRealUF(Node node) { Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ComparisonUFMap::const_iterator i(d_toRealMap.find(t)); Node fun; if (i == d_toRealMap.end()) { std::vector args(1); args[0] = t; - fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case", - nm->mkFunctionType(args, nm->realType()), - "floatingpoint_to_real_infinity_and_NaN_case", - NodeManager::SKOLEM_EXACT_NAME); + 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); d_toRealMap.insert(t, fun); } else { fun = (*i).second; @@ -348,6 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t)); Node fun; @@ -356,10 +363,10 @@ Node TheoryFp::abstractRealToFloat(Node node) std::vector args(2); args[0] = node[0].getType(); args[1] = node[1].getType(); - fun = nm->mkSkolem("floatingpoint_abstract_real_to_float", - nm->mkFunctionType(args, node.getType()), - "floatingpoint_abstract_real_to_float", - NodeManager::SKOLEM_EXACT_NAME); + fun = sm->mkDummySkolem("floatingpoint_abstract_real_to_float", + nm->mkFunctionType(args, node.getType()), + "floatingpoint_abstract_real_to_float", + NodeManager::SKOLEM_EXACT_NAME); d_realToFloatMap.insert(t, fun); } else @@ -380,6 +387,7 @@ Node TheoryFp::abstractFloatToReal(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t)); Node fun; @@ -388,10 +396,10 @@ Node TheoryFp::abstractFloatToReal(Node node) std::vector args(2); args[0] = t; args[1] = nm->realType(); - fun = nm->mkSkolem("floatingpoint_abstract_float_to_real", - nm->mkFunctionType(args, nm->realType()), - "floatingpoint_abstract_float_to_real", - NodeManager::SKOLEM_EXACT_NAME); + fun = sm->mkDummySkolem("floatingpoint_abstract_float_to_real", + nm->mkFunctionType(args, nm->realType()), + "floatingpoint_abstract_float_to_real", + NodeManager::SKOLEM_EXACT_NAME); d_floatToRealMap.insert(t, fun); } else diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 292ec2ec6..1d602b925 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -16,6 +16,7 @@ #include +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/bv_inverter_utils.h" @@ -35,14 +36,12 @@ Node BvInverter::getSolveVariable(TypeNode tn) std::map::iterator its = d_solve_var.find(tn); if (its == d_solve_var.end()) { - Node k = NodeManager::currentNM()->mkSkolem("slv", tn); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node k = sm->mkDummySkolem("slv", tn); d_solve_var[tn] = k; return k; } - else - { - return its->second; - } + return its->second; } /*---------------------------------------------------------------------------*/ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index bdd6d26ab..45433bdb6 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h" #include +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" @@ -642,6 +643,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( if (options::cegqiBvRmExtract()) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; // map from terms to bitvector extracts applied to that term std::map > extract_map; @@ -691,9 +693,9 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( Node ex = bv::utils::mkExtract( es.first, boundaries[i - 1] - 1, boundaries[i]); Node var = - nm->mkSkolem("ek", - ex.getType(), - "variable to represent disjoint extract region"); + sm->mkDummySkolem("ek", + ex.getType(), + "variable to represent disjoint extract region"); children.push_back(var); vars.push_back(var); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 5e3a64325..74469e7de 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" @@ -463,7 +464,8 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) return it->second; } NodeManager * nm = NodeManager::currentNM(); - Node g = nm->mkSkolem("g", nm->booleanType()); + SkolemManager* sm = nm->getSkolemManager(); + Node g = sm->mkDummySkolem("g", nm->booleanType()); // ensure that it is a SAT literal Node ceLit = d_qstate.getValuation().ensureLiteral(g); d_ce_lit[q] = ceLit; diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index 1974e7c7c..5f114c313 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/cegqi/vts_term_cache.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/rewriter.h" @@ -60,18 +61,19 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create) if (create) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (d_vts_delta_free.isNull()) { d_vts_delta_free = - nm->mkSkolem("delta_free", - nm->realType(), - "free delta for virtual term substitution"); + sm->mkDummySkolem("delta_free", + nm->realType(), + "free delta for virtual term substitution"); Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero); d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA); } if (d_vts_delta.isNull()) { - d_vts_delta = nm->mkSkolem( + d_vts_delta = sm->mkDummySkolem( "delta", nm->realType(), "delta for virtual term substitution"); // mark as a virtual term VirtualTermSkolemAttribute vtsa; @@ -86,15 +88,16 @@ Node VtsTermCache::getVtsInfinity(TypeNode tn, bool isFree, bool create) if (create) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (d_vts_inf_free[tn].isNull()) { - d_vts_inf_free[tn] = nm->mkSkolem( + d_vts_inf_free[tn] = sm->mkDummySkolem( "inf_free", tn, "free infinity for virtual term substitution"); } if (d_vts_inf[tn].isNull()) { - d_vts_inf[tn] = - nm->mkSkolem("inf", tn, "infinity for virtual term substitution"); + d_vts_inf[tn] = sm->mkDummySkolem( + "inf", tn, "infinity for virtual term substitution"); // mark as a virtual term VirtualTermSkolemAttribute vtsa; d_vts_inf[tn].setAttribute(vtsa, true); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 41d881f2c..ba716254a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/conjecture_generator.h" +#include "expr/skolem_manager.h" #include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" @@ -1089,8 +1090,11 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn ); if( it==d_typ_pred.end() ){ - TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." ); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType()); + Node op = sm->mkDummySkolem( + "PE", op_tn, "was created by conjecture ground term enumerator."); d_typ_pred[tn] = op; return op; }else{ diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index fe712e01e..f72acaa18 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/dynamic_rewrite.h" +#include "expr/skolem_manager.h" #include "theory/rewriter.h" using namespace std; @@ -144,6 +145,8 @@ Node DynamicRewriter::toExternal(Node ai) Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) { + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::vector ctypes; for (const Node& cn : n) { @@ -173,10 +176,9 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) } else { - utype = NodeManager::currentNM()->mkFunctionType(ctypes); + utype = nm->mkFunctionType(ctypes); } - Node f = NodeManager::currentNM()->mkSkolem( - "ufd", utype, "internal op for dynamic_rewriter"); + Node f = sm->mkDummySkolem("ufd", utype, "internal op for dynamic_rewriter"); curr->d_sym = f; return f; } diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index b21252358..801bde022 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/expr_miner.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -46,6 +47,7 @@ Node ExprMiner::convertToSkolem(Node n) std::vector sks; // map to skolems NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (unsigned i = 0, size = fvs.size(); i < size; i++) { Node v = fvs[i]; @@ -56,7 +58,7 @@ Node ExprMiner::convertToSkolem(Node n) std::map::iterator itf = d_fv_to_skolem.find(v); if (itf == d_fv_to_skolem.end()) { - Node sk = nm->mkSkolem("rrck", v.getType()); + Node sk = sm->mkDummySkolem("rrck", v.getType()); d_fv_to_skolem[v] = sk; sks.push_back(sk); } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index efa3dd160..bbbf820b6 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -18,6 +18,7 @@ #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -43,7 +44,8 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u) { if( options::fmfBoundLazy() ){ - d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() ); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + d_proxy_range = isProxy ? r : sm->mkDummySkolem("pbir", r.getType()); }else{ d_proxy_range = r; } @@ -315,6 +317,7 @@ void BoundedIntegers::checkOwnership(Node f) //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister Trace("bound-int") << "check ownership quantifier " << f << std::endl; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); bool success; do{ @@ -484,8 +487,8 @@ void BoundedIntegers::checkOwnership(Node f) if (expr::hasBoundVar(r)) { // introduce a new bound - Node new_range = NodeManager::currentNM()->mkSkolem( - "bir", r.getType(), "bound for term"); + Node new_range = + sm->mkDummySkolem("bir", r.getType(), "bound for term"); d_nground_range[f][v] = r; d_range[f][v] = new_range; r = new_range; diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index 515d9fe58..cc2e0fbf1 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "expr/attribute.h" +#include "expr/skolem_manager.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/rewriter.h" @@ -90,8 +91,9 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) { return it->second; } - Node st = NodeManager::currentNM()->mkSkolem( - "star", tn, "skolem created for full-model checking"); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node st = + sm->mkDummySkolem("star", tn, "skolem created for full-model checking"); d_type_star[tn] = st; st.setAttribute(IsStarAttribute(), true); return st; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 7dbc10f57..6f0c13f63 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/fmf/full_model_check.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/theory_options.h" #include "options/uf_options.h" @@ -1349,6 +1350,7 @@ void FullModelChecker::registerQuantifiedFormula(Node q) return; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::vector types; for (const Node& v : q[0]) { @@ -1363,7 +1365,7 @@ void FullModelChecker::registerQuantifiedFormula(Node q) types.push_back(tn); } TypeNode typ = nm->mkFunctionType(types, nm->booleanType()); - Node op = nm->mkSkolem("qfmc", typ, "op for full-model checking"); + Node op = sm->mkDummySkolem("qfmc", typ, "op for full-model checking"); d_quant_cond[q] = op; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 89358c511..7e484956e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -18,6 +18,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -1563,7 +1564,8 @@ Node QuantifiersRewriter::mkForall(const std::vector& args, children.push_back(body); if (marked) { - Node avar = nm->mkSkolem("id", nm->booleanType()); + SkolemManager* sm = nm->getSkolemManager(); + Node avar = sm->mkDummySkolem("id", nm->booleanType()); QuantIdNumAttribute ida; avar.setAttribute(ida, 0); iplc.push_back(nm->mkNode(kind::INST_ATTRIBUTE, avar)); diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 2fe173763..7a1a6fb45 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -17,6 +17,7 @@ #include #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -180,6 +181,7 @@ bool SingleInvocationPartition::init(std::vector& funcs, Assert(d_input_funcs.empty()); Assert(d_si_vars.empty()); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); d_has_input_funcs = has_funcs; d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end()); d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end()); @@ -194,7 +196,7 @@ bool SingleInvocationPartition::init(std::vector& funcs, Assert(d_si_vars.size() == d_arg_types.size()); for (const Node& inf : d_input_funcs) { - Node sk = nm->mkSkolem("_sik", inf.getType()); + Node sk = sm->mkDummySkolem("_sik", inf.getType()); d_input_func_sks.push_back(sk); } Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl; diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 51b400dbe..43d30f5bd 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -178,6 +178,7 @@ Node Skolemize::mkSkolemizedBody(Node f, std::vector& sub_vars) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Assert(sk.empty() || sk.size() == f[0].getNumChildren()); // calculate the variables and substitution std::vector ind_vars; @@ -202,21 +203,20 @@ Node Skolemize::mkSkolemizedBody(Node f, { if (argTypes.empty()) { - s = NodeManager::currentNM()->mkSkolem( + s = sm->mkDummySkolem( "skv", f[0][i].getType(), "created during skolemization"); } else { - TypeNode typ = NodeManager::currentNM()->mkFunctionType( - argTypes, f[0][i].getType()); - Node op = NodeManager::currentNM()->mkSkolem( + TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType()); + Node op = sm->mkDummySkolem( "skop", typ, "op created during pre-skolemization"); // DOTHIS: set attribute on op, marking that it should not be selected // as trigger std::vector funcArgs; funcArgs.push_back(op); funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end()); - s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs); + s = nm->mkNode(kind::APPLY_UF, funcArgs); } sk.push_back(s); } @@ -264,27 +264,19 @@ Node Skolemize::mkSkolemizedBody(Node f, { conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate()); } - disj.push_back(conj.size() == 1 - ? conj[0] - : NodeManager::currentNM()->mkNode(OR, conj)); + disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(OR, conj)); } Assert(!disj.empty()); - n_str_ind = disj.size() == 1 - ? disj[0] - : NodeManager::currentNM()->mkNode(AND, disj); + n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj); } else if (options::intWfInduction() && tn.isInteger()) { - Node icond = NodeManager::currentNM()->mkNode( - GEQ, k, NodeManager::currentNM()->mkConst(Rational(0))); - Node iret = - ret.substitute( - ind_vars[0], - NodeManager::currentNM()->mkNode( - MINUS, k, NodeManager::currentNM()->mkConst(Rational(1)))) - .negate(); - n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret); - n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind); + Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0))); + Node iret = ret.substitute(ind_vars[0], + nm->mkNode(MINUS, k, nm->mkConst(Rational(1)))) + .negate(); + n_str_ind = nm->mkNode(OR, icond.negate(), iret); + n_str_ind = nm->mkNode(AND, icond, n_str_ind); } else { @@ -299,17 +291,15 @@ Node Skolemize::mkSkolemizedBody(Node f, rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end()); if (!rem_ind_vars.empty()) { - Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars); - nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret); + Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars); + nret = nm->mkNode(FORALL, bvl, nret); nret = Rewriter::rewrite(nret); sub = nret; sub_vars.insert( sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end()); - n_str_ind = NodeManager::currentNM() - ->mkNode(FORALL, bvl, n_str_ind.negate()) - .negate(); + n_str_ind = nm->mkNode(FORALL, bvl, n_str_ind.negate()).negate(); } - ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind); + ret = nm->mkNode(OR, nret, n_str_ind); } Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 5e9f2d591..796e749cc 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "smt/logic_exception.h" #include "smt/smt_engine.h" @@ -144,6 +145,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted) return; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); d_single_inv = d_sip->getSingleInvocation(); d_single_inv = TermUtil::simpleNegate(d_single_inv); std::vector func_vars; @@ -159,8 +161,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted) d_sip->getSingleInvocationVariables(sivars); for (unsigned i = 0, size = sivars.size(); i < size; i++) { - Node v = NodeManager::currentNM()->mkSkolem( - "a", sivars[i].getType(), "single invocation arg"); + Node v = + sm->mkDummySkolem("a", sivars[i].getType(), "single invocation arg"); d_single_inv_arg_sk.push_back(v); } d_single_inv = d_single_inv.substitute(sivars.begin(), @@ -209,15 +211,16 @@ bool CegSingleInv::solve() } Trace("sygus-si") << "Solve using single invocation..." << std::endl; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); // Mark the quantified formula with the quantifier elimination attribute to // ensure its structure is preserved in the query below. Node siq = d_single_inv; if (siq.getKind() == FORALL) { - Node n_attr = - nm->mkSkolem("qe_si", - nm->booleanType(), - "Auxiliary variable for qe attr for single invocation."); + Node n_attr = sm->mkDummySkolem( + "qe_si", + nm->booleanType(), + "Auxiliary variable for qe attr for single invocation."); QuantElimAttribute qea; n_attr.setAttribute(qea, true); n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 9a5c6146d..84e9f1070 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/cegis_unif.h" +#include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -417,7 +418,8 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) { NodeManager* nm = NodeManager::currentNM(); - Node new_lit = nm->mkSkolem("G_cost", nm->booleanType()); + SkolemManager* sm = nm->getSkolemManager(); + Node newLit = sm->mkDummySkolem("G_cost", nm->booleanType()); unsigned new_size = n + 1; // allocate an enumerator for each candidate @@ -425,13 +427,13 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) { Node c = ci.first; TypeNode ct = c.getType(); - Node eu = nm->mkSkolem("eu", ct); + Node eu = sm->mkDummySkolem("eu", ct); Node ceu; if (!d_useCondPool && !ci.second.d_enums[0].empty()) { // make a new conditional enumerator as well, starting the // second type around - ceu = nm->mkSkolem("cu", ci.second.d_ce_type); + ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type); } // register the new enumerators for (unsigned index = 0; index < 2; index++) @@ -452,7 +454,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) { Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei << " to new size " << new_size << "\n"; - registerEvalPtAtSize(c, ei, new_lit, new_size); + registerEvalPtAtSize(c, ei, newLit, new_size); } } // enforce fairness between number of enumerators and enumerator size @@ -483,7 +485,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) datatypes.push_back(sdt.getDatatype()); std::vector dtypes = nm->mkMutualDatatypeTypes( datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); - d_virtual_enum = nm->mkSkolem("_ve", dtypes[0]); + d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]); d_tds->registerEnumerator( d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } @@ -497,7 +499,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); Node fair_lemma = nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1))); - fair_lemma = nm->mkNode(OR, new_lit, fair_lemma); + fair_lemma = nm->mkNode(OR, newLit, fair_lemma); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; // this lemma relates the number of conditions we enumerate and the @@ -510,7 +512,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) } } - return new_lit; + return newLit; } void CegisUnifEnumDecisionStrategy::initialize( @@ -526,6 +528,7 @@ void CegisUnifEnumDecisionStrategy::initialize( } // initialize type information for candidates NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (const Node& e : es) { Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n"; @@ -570,7 +573,7 @@ void CegisUnifEnumDecisionStrategy::initialize( // allocate a condition enumerator for each candidate for (std::pair& ci : d_ce_info) { - Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type); + Node ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type); setUpEnumerator(ceu, ci.second, 1); } } diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index 97ae4878d..0e498bb18 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/rcons_type_info.h" +#include "expr/skolem_manager.h" #include "theory/datatypes/sygus_datatype_utils.h" namespace cvc5 { @@ -26,9 +27,10 @@ void RConsTypeInfo::initialize(TermDbSygus* tds, const std::vector& builtinVars) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true)); - d_enumerator->initialize(nm->mkSkolem("sygus_rcons", stn)); + d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn)); d_crd.reset(new CandidateRewriteDatabase(true, false, true, false)); // since initial samples are not always useful for equivalence checks, set // their number to 0 diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 8df45320f..278d708ee 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -19,6 +19,7 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -43,6 +44,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, TypeNode abdGType) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::unordered_set symset; for (size_t i = 0, size = asserts.size(); i < size; i++) { @@ -166,7 +168,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, Node sc = nm->mkNode(AND, aconj, abdApp); Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); sc = nm->mkNode(EXISTS, vbvl, sc); - Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); + Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType()); sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); // build in the side condition diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 1b3a52db8..4f3d9a2e4 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_qe_preproc.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" @@ -35,6 +36,7 @@ Node SygusQePreproc::preprocess(Node q) body = body[0][1]; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Trace("cegqi-qep") << "Compute single invocation for " << q << "..." << std::endl; quantifiers::SingleInvocationPartition sip; @@ -84,7 +86,7 @@ Node SygusQePreproc::preprocess(Node q) // skolemize non-qe variables for (unsigned i = 0, size = nqe_vars.size(); i < size; i++) { - Node k = nm->mkSkolem( + Node k = sm->mkDummySkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation"); orig.push_back(nqe_vars[i]); subs.push_back(k); @@ -100,7 +102,7 @@ Node SygusQePreproc::preprocess(Node q) Node fv = sip.getFirstOrderVariableForFunction(f); Assert(!fi.isNull()); orig.push_back(fi); - Node k = nm->mkSkolem( + Node k = sm->mkDummySkolem( "k", fv.getType(), "qe for function in non-ground single invocation"); subs.push_back(k); Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 55e8c922d..70e6b7f2e 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_reconstruct.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "smt/command.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/rewriter.h" @@ -47,12 +48,13 @@ Node SygusReconstruct::reconstructSolution(Node sol, initialize(stn); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); /** a set of obligations that are not yet satisfied for each sygus datatype */ TypeObligationSetMap unsolvedObs; // paramaters sol and stn constitute the main obligation to satisfy - Node mainOb = nm->mkSkolem("sygus_rcons", stn); + Node mainOb = sm->mkDummySkolem("sygus_rcons", stn); // add the main obligation to the set of obligations that are not yet // satisfied @@ -99,7 +101,7 @@ Node SygusReconstruct::reconstructSolution(Node sol, { // if not, create an "artifical" obligation whose solution would be // the enumerated term - k = nm->mkSkolem("sygus_rcons", pair.first); + k = sm->mkDummySkolem("sygus_rcons", pair.first); d_obInfo.emplace(k, RConsObligationInfo(builtin)); d_stnInfo[pair.first].setBuiltinToOb(builtin, k); } @@ -201,6 +203,7 @@ Node SygusReconstruct::reconstructSolution(Node sol, TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); TypeObligationSetMap obsPrime; // obligations generated by match. Note that we might have already seen (and @@ -241,7 +244,7 @@ TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz) else { // otherwise, create a new obligation of the corresponding sygus type - newVar = nm->mkSkolem("sygus_rcons", stn); + newVar = sm->mkDummySkolem("sygus_rcons", stn); d_obInfo.emplace(newVar, candOb.second); d_stnInfo[stn].setBuiltinToOb(candOb.second, newVar); // if the candidate obligation is a constant and the grammar allows diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 179798222..47ead92c1 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -16,6 +16,7 @@ #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -433,6 +434,7 @@ Node SygusRepairConst::getFoQuery(Node body, const std::vector& sk_vars) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl; body = body.substitute(candidates.begin(), candidates.end(), @@ -451,7 +453,7 @@ Node SygusRepairConst::getFoQuery(Node body, if (itf == d_sk_to_fo.end()) { TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType()); - Node sk_fov = nm->mkSkolem("k", builtinType); + Node sk_fov = sm->mkDummySkolem("k", builtinType); d_sk_to_fo[v] = sk_fov; d_fo_to_sk[sk_fov] = v; Trace("sygus-repair-const-debug") diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index c3cff70d9..eade6b38e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_unif_rl.h" +#include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -133,6 +134,7 @@ Node SygusUnifRl::purifyLemma(Node n, bool childChanged = false; std::vector children; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (unsigned i = 0; i < size; ++i) { if (i == 0 && fapp) @@ -182,10 +184,10 @@ 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 = nm->mkSkolem(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", + NodeManager::SKOLEM_EXACT_NAME); // 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/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 24bcb1eab..fb93d26a9 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -16,6 +16,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "expr/skolem_manager.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_unif.h" @@ -172,6 +173,7 @@ void SygusUnifStrategy::registerStrategyPoint(Node et, void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (d_tinfo.find(tn) == d_tinfo.end()) { // register type @@ -194,7 +196,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) std::map::iterator iten = eti.d_enum.find(erole); if (iten == eti.d_enum.end()) { - ee = nm->mkSkolem("ee", tn); + ee = sm->mkDummySkolem("ee", tn); eti.d_enum[erole] = ee; Trace("sygus-unif-debug") << "...enumerator " << ee << " for " << tn.getDType().getName() @@ -245,7 +247,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) { TypeNode ttn = dt[j][k].getRangeType(); - Node kv = nm->mkSkolem("ut", ttn); + Node kv = sm->mkDummySkolem("ut", ttn); sks.push_back(kv); cop_to_sks[cop].push_back(kv); sktns.push_back(ttn); @@ -303,7 +305,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) << std::endl; Node esk = nm->mkNode(DT_SYGUS_EVAL, echildren); vs.push_back(esk); - Node tvar = nm->mkSkolem("templ", esk.getType()); + Node tvar = sm->mkDummySkolem("templ", esk.getType()); templ_var_index[tvar] = k; Trace("sygus-unif-debug2") << "* template inference : looking for " << tvar << " for arg " << k << std::endl; @@ -574,7 +576,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end()) { // it is templated, allocate a fresh variable - et = nm->mkSkolem("et", ct); + et = sm->mkDummySkolem("et", ct); Trace("sygus-unif-debug") << "...enumerate " << et << " of type " << ct.getDType().getName(); Trace("sygus-unif-debug") << " for arg " << j << " of " diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp index 6c14aaa80..4d1d0ab1d 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.cpp +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -17,6 +17,7 @@ #include #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" @@ -42,8 +43,9 @@ Node SygusUtils::mkSygusConjecture(const std::vector& fs, { Assert(!fs.empty()); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); SygusAttribute ca; - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + Node sygusVar = sm->mkDummySkolem("sygus", nm->booleanType()); sygusVar.setAttribute(ca, true); std::vector ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)}; // insert the remaining instantiation attributes @@ -65,6 +67,7 @@ Node SygusUtils::mkSygusConjecture(const std::vector& fs, { Assert(!fs.empty()); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::vector iattrs; // take existing properties, without the previous solves SygusSolutionAttribute ssa; @@ -72,7 +75,7 @@ Node SygusUtils::mkSygusConjecture(const std::vector& fs, for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++) { Node eq = solvedf.getEquality(i); - Node var = nm->mkSkolem("solved", nm->booleanType()); + Node var = sm->mkDummySkolem("solved", nm->booleanType()); var.setAttribute(ssa, eq); Node ipv = nm->mkNode(INST_ATTRIBUTE, var); iattrs.push_back(ipv); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index f7566e7a2..f63941b1c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "base/configuration.h" +#include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" @@ -29,9 +30,9 @@ #include "theory/quantifiers/sygus/enum_stream_substitution.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_enumerator_basic.h" -#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_pbe.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -102,9 +103,10 @@ void SynthConjecture::assign(Node q) Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl; d_quant = q; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); // initialize the guard - d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); + d_feasible_guard = sm->mkDummySkolem("G", nm->booleanType()); d_feasible_guard = Rewriter::rewrite(d_feasible_guard); d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard); AlwaysAssert(!d_feasible_guard.isNull()); @@ -170,8 +172,7 @@ void SynthConjecture::assign(Node q) for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++) { vars.push_back(d_embed_quant[0][i]); - Node e = - NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType()); + Node e = sm->mkDummySkolem("e", d_embed_quant[0][i].getType()); d_candidates.push_back(e); } Trace("cegqi") << "Base quantified formula is : " << d_embed_quant @@ -460,6 +461,7 @@ bool SynthConjecture::doCheck(std::vector& lems) } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); // check the side condition if we constructed a candidate if (constructed_cand) @@ -540,7 +542,7 @@ bool SynthConjecture::doCheck(std::vector& lems) { for (const Node& v : inst[0][0]) { - Node sk = nm->mkSkolem("rsk", v.getType()); + Node sk = sm->mkDummySkolem("rsk", v.getType()); sks.push_back(sk); vars.push_back(v); Trace("cegqi-check-debug") diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 875b25370..02d287fdf 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/template_infer.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" @@ -84,6 +85,7 @@ void SygusTemplateInfer::initialize(Node q) } Assert(prog == q[0][0]); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); // map the program back via non-single invocation map std::vector prog_templ_vars; d_ti.getVariables(prog_templ_vars); @@ -98,7 +100,7 @@ void SygusTemplateInfer::initialize(Node q) { atn = atn.getRangeType(); } - d_templ_arg[prog] = nm->mkSkolem("I", atn); + d_templ_arg[prog] = sm->mkDummySkolem("I", atn); // construct template Node templ; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 34a81467a..e4ecee72f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -18,6 +18,7 @@ #include "base/check.h" #include "expr/dtype_cons.h" +#include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" #include "options/base_options.h" #include "options/datatypes_options.h" @@ -165,18 +166,19 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) { SygusTypeInfo& ti = getTypeInfo(tn); int anyC = ti.getAnyConstantConsNum(); + NodeManager* nm = NodeManager::currentNM(); Node k; if (anyC == -1) { - k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy"); + SkolemManager* sm = nm->getSkolemManager(); + k = sm->mkDummySkolem("sy", tn, "sygus proxy"); SygusPrintProxyAttribute spa; k.setAttribute(spa, c); } else { const DType& dt = tn.getDType(); - k = NodeManager::currentNM()->mkNode( - APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c); + k = nm->mkNode(APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c); } d_proxy_vars[tn][c] = k; return k; @@ -562,8 +564,9 @@ void TermDbSygus::registerEnumerator(Node e, // populate a pool of terms, or (some cases) of when it is actively generated. if (isActiveGen || erole == ROLE_ENUM_POOL) { + SkolemManager* sm = nm->getSkolemManager(); // make the guard - Node ag = nm->mkSkolem("eG", nm->booleanType()); + Node ag = sm->mkDummySkolem("eG", nm->booleanType()); // must ensure it is a literal immediately here ag = d_qstate.getValuation().ensureLiteral(ag); // must ensure that it is asserted as a literal before we begin solving diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 7ee2f2ec6..eb2f0f739 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/sygus/transition_inference.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -197,6 +198,7 @@ void TransitionInference::process(Node n, Node f) void TransitionInference::process(Node n) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); d_complete = true; d_trivial = true; std::vector n_check; @@ -276,7 +278,7 @@ void TransitionInference::process(Node n) { for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++) { - Node v = nm->mkSkolem( + Node v = sm->mkDummySkolem( "ir", next[j].getType(), "template inference rev argument"); d_prime_vars.push_back(v); } @@ -426,9 +428,11 @@ bool TransitionInference::processDisjunct( d_func = op; Trace("cegqi-inv-debug") << "Use " << op << " with args "; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (const Node& l : lit) { - Node v = nm->mkSkolem("i", l.getType(), "template inference argument"); + Node v = + sm->mkDummySkolem("i", l.getType(), "template inference argument"); d_vars.push_back(v); Trace("cegqi-inv-debug") << v << " "; } diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 81dc5cecb..e394eab26 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -18,6 +18,7 @@ #include #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -462,7 +463,8 @@ Node SygusInst::getCeLiteral(Node q) } NodeManager* nm = NodeManager::currentNM(); - Node sk = nm->mkSkolem("CeLiteral", nm->booleanType()); + SkolemManager* sm = nm->getSkolemManager(); + Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType()); Node lit = d_qstate.getValuation().ensureLiteral(sk); d_ce_lits[q] = lit; return lit; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 64c2fda76..517c3ac24 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/term_database.h" +#include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -154,11 +155,11 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) d_type_fv.find(tn); if (it == d_type_fv.end()) { + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); std::stringstream ss; ss << language::SetLanguage(options::outputLanguage()); ss << "e_" << tn; - Node k = NodeManager::currentNM()->mkSkolem( - ss.str(), tn, "is a termDb fresh variable"); + Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable"); Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn << std::endl; if (options::instMaxLevel() != -1) @@ -168,10 +169,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) d_type_fv[tn] = k; return k; } - else - { - return it->second; - } + return it->second; } Node TermDb::getMatchOperator( Node n ) { @@ -468,6 +466,7 @@ void TermDb::addTermHo(Node n) return; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node curr = n; std::vector args; while (curr.getKind() == HO_APPLY) @@ -481,9 +480,9 @@ void TermDb::addTermHo(Node n) Node psk; if (itp == d_ho_fun_op_purify.end()) { - psk = nm->mkSkolem("pfun", - curr.getType(), - "purify for function operator term indexing"); + psk = sm->mkDummySkolem("pfun", + curr.getType(), + "purify for function operator term indexing"); d_ho_fun_op_purify[curr] = psk; // we do not add it to d_ops since it is an internal operator } @@ -1224,8 +1223,9 @@ Node TermDb::getHoTypeMatchPredicate(TypeNode tn) return ithp->second; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType()); - Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types"); + Node k = sm->mkDummySkolem("U", ptn, "predicate to force higher-order types"); d_ho_type_match_pred[tn] = k; return k; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 6085c034d..5585b36ab 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -20,6 +20,7 @@ #include "base/map_util.h" #include "expr/kind.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/sep_options.h" #include "options/smt_options.h" @@ -313,6 +314,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom; TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null(); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (slbl.isNull()) { Trace("sep-lemma-debug") @@ -434,8 +436,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) } else { - Node kl = nm->mkSkolem("loc", getReferenceType(satom)); - Node kd = nm->mkSkolem("data", getDataType(satom)); + Node kl = sm->mkDummySkolem("loc", getReferenceType(satom)); + Node kd = sm->mkDummySkolem("data", getDataType(satom)); Node econc = nm->mkNode( SEP_LABEL, nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true), @@ -466,7 +468,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl; - Node g = nm->mkSkolem("G", nm->booleanType()); + Node g = sm->mkDummySkolem("G", nm->booleanType()); d_neg_guard_strategy[g].reset(new DecisionStrategySingleton( "sep_neg_guard", g, getSatContext(), getValuation())); DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get(); @@ -506,6 +508,7 @@ void TheorySep::postCheck(Effort level) return; } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Trace("sep-process") << "Checking heap at full effort..." << std::endl; d_label_model.clear(); d_tmodel.clear(); @@ -849,8 +852,8 @@ void TheorySep::postCheck(Effort level) { Trace("sep-process") << "Must witness label : " << ll << ", data type is " << data_type << std::endl; - Node dsk = - nm->mkSkolem("dsk", data_type, "pto-data for implicit location"); + Node dsk = sm->mkDummySkolem( + "dsk", data_type, "pto-data for implicit location"); // if location is in the heap, then something must point to it Node lem = nm->mkNode( IMPLIES, @@ -1160,6 +1163,8 @@ void TheorySep::initializeBounds() { if( !d_bounds_init ){ Trace("sep-bound") << "Initialize sep bounds..." << std::endl; d_bounds_init = true; + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){ TypeNode tn = it->first; Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; @@ -1174,7 +1179,8 @@ void TheorySep::initializeBounds() { Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl; Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl; for( unsigned r=0; rmkSkolem( "e", tn, "cardinality bound element for seplog" ); + Node e = + sm->mkDummySkolem("e", tn, "cardinality bound element for seplog"); d_type_references_card[tn].push_back( e ); d_type_ref_card_id[e] = r; } @@ -1185,19 +1191,20 @@ void TheorySep::initializeBounds() { Node TheorySep::getBaseLabel( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_base_label.find( tn ); if( it==d_base_label.end() ){ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); initializeBounds(); Trace("sep") << "Make base label for " << tn << std::endl; std::stringstream ss; ss << "__Lb"; - TypeNode ltn = NodeManager::currentNM()->mkSetType(tn); - //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn)); - Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" ); + TypeNode ltn = nm->mkSetType(tn); + Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "base label"); d_base_label[tn] = n_lbl; //make reference bound Trace("sep") << "Make reference bound label for " << tn << std::endl; std::stringstream ss2; ss2 << "__Lu"; - d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" ); + d_reference_bound[tn] = sm->mkDummySkolem(ss2.str(), ltn, ""); d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() ); //check whether monotonic (elements can be added to tn without effecting satisfiability) @@ -1308,12 +1315,14 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { Node TheorySep::getLabel( Node atom, int child, Node lbl ) { std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child ); if( it==d_label_map[atom][lbl].end() ){ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); TypeNode refType = getReferenceType( atom ); std::stringstream ss; ss << "__Lc" << child; TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType)); - Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" ); + Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "sep label"); d_label_map[atom][lbl][child] = n_lbl; d_label_map_parent[n_lbl] = lbl; return n_lbl; diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index b67df285d..bbe100e98 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -17,6 +17,7 @@ #include "expr/emptyset.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/sets_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" @@ -1015,6 +1016,7 @@ void CardinalityExtension::mkModelValueElementsFor( std::uint32_t vu = v.getConst().getNumerator().toUnsignedInt(); Assert(els.size() <= vu); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (elementType.isInterpretedFinite()) { // get all members of this finite type @@ -1034,7 +1036,7 @@ void CardinalityExtension::mkModelValueElementsFor( // slack elements for the leaves without worrying about conflicts with // the current members of this finite type. - Node slack = nm->mkSkolem("slack", elementType); + Node slack = sm->mkDummySkolem("slack", elementType); Node singleton = nm->mkSingleton(elementType, slack); els.push_back(singleton); d_finite_type_slack_elements[elementType].push_back(slack); @@ -1043,8 +1045,8 @@ void CardinalityExtension::mkModelValueElementsFor( } else { - els.push_back( - nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType))); + els.push_back(nm->mkSingleton( + elementType, sm->mkDummySkolem("msde", elementType))); } } } diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp index c18e9406d..8c0d125d5 100644 --- a/src/theory/sets/skolem_cache.cpp +++ b/src/theory/sets/skolem_cache.cpp @@ -14,6 +14,7 @@ #include "theory/sets/skolem_cache.h" +#include "expr/skolem_manager.h" #include "theory/rewriter.h" using namespace cvc5::kind; @@ -49,7 +50,8 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn, Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c) { - Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem"); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node n = sm->mkDummySkolem(c, tn, "sets skolem"); d_allSkolems.insert(n); return n; } diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index a093840f7..43eed46a6 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/sets/term_registry.h" #include "expr/emptyset.h" +#include "expr/skolem_manager.h" using namespace std; using namespace cvc5::kind; @@ -116,7 +117,8 @@ Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn) std::map::iterator it = d_tc_skolem[n].find(tn); if (it == d_tc_skolem[n].end()) { - Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node k = sm->mkDummySkolem("tc_k", tn); d_tc_skolem[n][tn] = k; return k; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index b97d3125d..3aa97672d 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1373,11 +1373,12 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType()); stringstream stream; stream << "chooseUf" << setType.getId(); string name = stream.str(); - Node chooseSkolem = nm->mkSkolem( + Node chooseSkolem = sm->mkDummySkolem( name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME); d_chooseFunctions[setType] = chooseSkolem; return chooseSkolem; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 6609e4923..aa79f903b 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -15,8 +15,10 @@ **/ #include "theory/sets/theory_sets_rels.h" -#include "theory/sets/theory_sets_private.h" + +#include "expr/skolem_manager.h" #include "theory/sets/theory_sets.h" +#include "theory/sets/theory_sets_private.h" using namespace std; using namespace cvc5::kind; @@ -361,11 +363,11 @@ void TheorySetsRels::check(Theory::Effort level) } /* JOIN-IMAGE DOWN : (x) IS_IN (R JOIN_IMAGE n) - * ------------------------------------------------------- - * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ... , xn) - * - */ - + * ------------------------------------------------------- + * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ... + * , xn) + * + */ void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) { Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl; @@ -387,29 +389,37 @@ void TheorySetsRels::check(Theory::Effort level) } } } - + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node reason = exp; Node conclusion = d_trueNode; std::vector< Node > distinct_skolems; Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 ); if( exp[1] != join_image_term ) { - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) ); + reason = + nm->mkNode(AND, reason, nm->mkNode(EQUAL, exp[1], join_image_term)); } for( unsigned int i = 0; i < min_card; i++ ) { - Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] ); + Node skolem = sm->mkDummySkolem( + "jig", join_image_rel.getType()[0].getTupleTypes()[0]); distinct_skolems.push_back( skolem ); - conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) ); + conclusion = nm->mkNode( + AND, + conclusion, + nm->mkNode( + MEMBER, + RelsUtils::constructPair(join_image_rel, fst_mem_element, skolem), + join_image_rel)); } if( distinct_skolems.size() >= 2 ) { - conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) ); + conclusion = + nm->mkNode(AND, conclusion, nm->mkNode(DISTINCT, distinct_skolems)); } sendInfer(conclusion, InferenceId::SETS_RELS_JOIN_IMAGE_DOWN, reason); Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl; - } - /* IDENTITY-DOWN : (x, y) IS_IN IDEN(R) * ------------------------------------------------------- * x = y, (x IS_IN R) diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index fb3551e9a..9427bb1d5 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -24,11 +24,12 @@ #include #include +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" -#include "theory/rewriter.h" #include "theory/quantifiers/quant_util.h" +#include "theory/rewriter.h" using namespace cvc5; using namespace cvc5::kind; @@ -578,7 +579,7 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){ //must create new type std::stringstream ss; ss << "it_" << t << "_" << pref; - retType = NodeManager::currentNM()->mkSort( ss.str() ); + retType = NodeManager::currentNM()->mkSort(ss.str()); } Trace("sort-inference") << "-> Make type " << retType << " to correspond to "; printSort("sort-inference", t ); @@ -599,6 +600,8 @@ TypeNode SortInference::getTypeForId( int t ){ } Node SortInference::getNewSymbol( Node old, TypeNode tn ){ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); // if no sort was inferred for this node, return original if( tn.isNull() || tn.isComparableTo( old.getType() ) ){ return old; @@ -607,18 +610,20 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ std::stringstream ss; ss << "ic_" << tn << "_" << old; - d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst??? + d_const_map[tn][old] = sm->mkDummySkolem( + ss.str(), + tn, + "constant created during sort inference"); // use mkConst??? } return d_const_map[tn][ old ]; }else if( old.getKind()==kind::BOUND_VARIABLE ){ std::stringstream ss; ss << "b_" << old; - return NodeManager::currentNM()->mkBoundVar( ss.str(), tn ); - }else{ - std::stringstream ss; - ss << "i_" << old; - return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" ); + return nm->mkBoundVar(ss.str(), tn); } + std::stringstream ss; + ss << "i_" << old; + return sm->mkDummySkolem(ss.str(), tn, "created during sort inference"); } Node SortInference::simplifyNode( @@ -632,6 +637,8 @@ Node SortInference::simplifyNode( if( itv!=visited[n].end() ){ return itv->second; }else{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Trace("sort-inference-debug2") << "Simplify " << n << ", type context=" << tnn << std::endl; std::vector< Node > children; std::map< Node, std::map< TypeNode, Node > > new_visited; @@ -646,7 +653,7 @@ Node SortInference::simplifyNode( new_children.push_back( v ); var_bound[ n[0][i] ] = v; } - children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) ); + children.push_back(nm->mkNode(n[0].getKind(), new_children)); use_new_visited = true; } @@ -701,7 +708,7 @@ Node SortInference::simplifyNode( Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl; var_bound.erase( n[0][i] ); } - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + ret = nm->mkNode(n.getKind(), children); }else if( n.getKind()==kind::EQUAL ){ TypeNode tn1 = children[0].getType(); TypeNode tn2 = children[1].getType(); @@ -710,7 +717,7 @@ Node SortInference::simplifyNode( Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl; Assert(false); } - ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children ); + ret = nm->mkNode(kind::EQUAL, children); } else if (isHandledApplyUf(n.getKind())) { @@ -732,8 +739,9 @@ Node SortInference::simplifyNode( if( opChanged ){ std::stringstream ss; ss << "io_" << op; - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); - d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + TypeNode typ = nm->mkFunctionType(argTypes, retType); + d_symbol_map[op] = sm->mkDummySkolem( + ss.str(), typ, "op created during sort inference"); Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; model_replace_f[op] = d_symbol_map[op]; }else{ @@ -752,7 +760,7 @@ Node SortInference::simplifyNode( Assert(false); } } - ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + ret = nm->mkNode(kind::APPLY_UF, children); }else{ std::map< Node, Node >::iterator it = var_bound.find( n ); if( it!=var_bound.end() ){ @@ -767,7 +775,7 @@ Node SortInference::simplifyNode( //type is determined by context ret = getNewSymbol( n, tnn ); }else if( childChanged ){ - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + ret = nm->mkNode(n.getKind(), children); }else{ ret = n; } @@ -778,18 +786,24 @@ Node SortInference::simplifyNode( } Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::vector< TypeNode > tns; tns.push_back( tn1 ); - TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 ); - Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" ); + TypeNode typ = nm->mkFunctionType(tns, tn2); + Node f = + sm->mkDummySkolem("inj", typ, "injection for monotonicity constraint"); Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; - Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 ); - Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 ); - Node ret = NodeManager::currentNM()->mkNode( kind::FORALL, - NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), - NodeManager::currentNM()->mkNode( kind::OR, - NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(), - v1.eqNode( v2 ) ) ); + Node v1 = nm->mkBoundVar("?x", tn1); + Node v2 = nm->mkBoundVar("?y", tn1); + Node ret = + nm->mkNode(kind::FORALL, + nm->mkNode(kind::BOUND_VAR_LIST, v1, v2), + nm->mkNode(kind::OR, + nm->mkNode(kind::APPLY_UF, f, v1) + .eqNode(nm->mkNode(kind::APPLY_UF, f, v2)) + .negate(), + v1.eqNode(v2))); ret = theory::Rewriter::rewrite( ret ); return ret; } diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 1bb85ee81..eeb187984 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -274,6 +274,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode) int ret = 1; retNode = d_emptyRegexp; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); PairNodeStr dv = std::make_pair( r, c ); if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) { @@ -355,7 +356,8 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode) } } if(ret == 0) { - Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" ); + Node sk = + sm->mkDummySkolem("rsp", nm->stringType(), "Split RegExp"); retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk); if(!rest.isNull()) { retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest)); diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index ad36b8edd..ed9be34bb 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -154,7 +154,8 @@ Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c) Node SkolemCache::mkSkolem(const char* c) { // TODO: eliminate this - Node n = NodeManager::currentNM()->mkSkolem(c, d_strType, "string skolem"); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node n = sm->mkDummySkolem(c, d_strType, "string skolem"); d_allSkolems.insert(n); return n; } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8deba50ca..d18e10a16 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -17,6 +17,7 @@ #include "theory/strings/theory_strings_preprocess.h" #include "expr/kind.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/strings_options.h" #include "proof/proof_manager.h" @@ -58,6 +59,7 @@ Node StringsPreprocess::reduce(Node t, << "StringsPreprocess::reduce: " << t << std::endl; Node retNode = t; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node zero = nm->mkConst(Rational(0)); Node one = nm->mkConst(Rational(1)); Node negOne = nm->mkConst(Rational(-1)); @@ -266,7 +268,8 @@ Node StringsPreprocess::reduce(Node t, std::vector conc; std::vector< TypeNode > argTypes; argTypes.push_back(nm->integerType()); - Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); + Node u = + sm->mkDummySkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); Node lem = nm->mkNode(GEQ, leni, one); conc.push_back(lem); @@ -345,7 +348,7 @@ Node StringsPreprocess::reduce(Node t, Node emp = Word::mkEmptyWord(s.getType()); Node sEmpty = s.eqNode(emp); - Node k = nm->mkSkolem("k", nm->integerType()); + Node k = sm->mkDummySkolem("k", nm->integerType()); Node kc1 = nm->mkNode(GEQ, k, zero); Node kc2 = nm->mkNode(LT, k, lens); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); @@ -361,7 +364,8 @@ Node StringsPreprocess::reduce(Node t, std::vector conc2; std::vector< TypeNode > argTypes; argTypes.push_back(nm->integerType()); - Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); + Node u = + sm->mkDummySkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens)); conc2.push_back(lem); @@ -531,7 +535,7 @@ Node StringsPreprocess::reduce(Node t, std::vector argTypes; argTypes.push_back(nm->integerType()); Node us = - nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType())); + sm->mkDummySkolem("Us", nm->mkFunctionType(argTypes, nm->stringType())); TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType()); Node uf = sc->mkTypedSkolemCached( ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf"); @@ -670,7 +674,8 @@ Node StringsPreprocess::reduce(Node t, nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc"); std::vector argTypes; argTypes.push_back(nm->integerType()); - Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, t.getType())); + Node us = + sm->mkDummySkolem("Us", nm->mkFunctionType(argTypes, t.getType())); TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType()); Node uf = sc->mkTypedSkolemCached( ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf"); @@ -1013,7 +1018,8 @@ Node StringsPreprocess::mkForallInternal(Node bvl, Node body) } else { - qvar = nm->mkSkolem("qinternal", nm->booleanType()); + SkolemManager* sm = nm->getSkolemManager(); + qvar = sm->mkDummySkolem("qinternal", nm->booleanType()); // this dummy variable marks that the quantified formula is internal qvar.setAttribute(InternalQuantAttribute(), true); // remember the dummy variable diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 6b3b5ba0e..eb6145f9c 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -16,6 +16,7 @@ #include +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/uf_options.h" #include "smt/logic_exception.h" @@ -1126,6 +1127,8 @@ void SortModel::debugPrint( const char* c ){ bool SortModel::checkLastCall() { + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); TheoryModel* m = d_state.getModel(); if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; @@ -1163,7 +1166,7 @@ bool SortModel::checkLastCall() { std::stringstream ss; ss << "r_" << d_type << "_"; - Node nn = NodeManager::currentNM()->mkSkolem( + Node nn = sm->mkDummySkolem( ss.str(), d_type, "enumeration to meet negative card constraint"); d_fresh_aloc_reps.push_back( nn ); } @@ -1184,8 +1187,7 @@ bool SortModel::checkLastCall() } } Node cl = getCardinalityLiteral( d_maxNegCard ); - Node lem = NodeManager::currentNM()->mkNode( - OR, cl, NodeManager::currentNM()->mkAnd(force_cl)); + Node lem = nm->mkNode(OR, cl, nm->mkAnd(force_cl)); Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl; d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE); return false; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 75965e2c9..ebbc75e00 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -16,6 +16,7 @@ #include "theory/uf/ho_extension.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/uf_options.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_rewriter.h" @@ -66,10 +67,11 @@ Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached) std::vector argTypes = tn.getArgTypes(); std::vector skolems; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) { - Node k = - nm->mkSkolem("k", argTypes[i], "skolem created for extensionality."); + Node k = sm->mkDummySkolem( + "k", argTypes[i], "skolem created for extensionality."); skolems.push_back(k); } Node t[2]; @@ -120,6 +122,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) Node f = TheoryUfRewriter::decomposeHoApply(node, args, true); Node new_f = f; NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); if (!TheoryUfRewriter::canUseAsApplyUfOperator(f)) { NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f); @@ -147,7 +150,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end()); TypeNode nft = nm->mkFunctionType(newTypes, rangeType); - new_f = nm->mkSkolem("app_uf", nft); + new_f = sm->mkDummySkolem("app_uf", nft); for (const Node& v : vs) { new_f = nm->mkNode(HO_APPLY, new_f, v); @@ -161,7 +164,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) else { // introduce skolem to make a standard APPLY_UF - new_f = nm->mkSkolem("app_uf", f.getType()); + new_f = sm->mkDummySkolem("app_uf", f.getType()); lem = new_f.eqNode(f); } Trace("uf-ho-lemma") diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp index 880bb85e4..0ec1c5e56 100644 --- a/test/unit/node/attribute_black.cpp +++ b/test/unit/node/attribute_black.cpp @@ -55,7 +55,7 @@ class TestNodeBlackAttribute : public TestNode TEST_F(TestNodeBlackAttribute, ints) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); const uint64_t val = 63489; uint64_t data0 = 0; uint64_t data1 = 0; @@ -72,9 +72,9 @@ TEST_F(TestNodeBlackAttribute, ints) TEST_F(TestNodeBlackAttribute, tnodes) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); - Node val(d_nodeManager->mkSkolem("b", booleanType)); + Node val(d_skolemManager->mkDummySkolem("b", booleanType)); TNode data0; TNode data1; @@ -90,7 +90,7 @@ TEST_F(TestNodeBlackAttribute, tnodes) TEST_F(TestNodeBlackAttribute, strings) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); std::string val("63489"); std::string data0; @@ -108,7 +108,7 @@ TEST_F(TestNodeBlackAttribute, strings) TEST_F(TestNodeBlackAttribute, bools) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); bool val = true; bool data0 = false; diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index b9cac2169..1a739cf1b 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -39,7 +39,7 @@ class TestNodeBlackNodeAlgorithm : public TestNode TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1) { // The only symbol in ~x (x is a boolean varible) should be x - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, x); std::unordered_set syms; getSymbols(n, syms); @@ -53,8 +53,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2) // "var" is bound. // left conjunct - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->integerType()); Node left = d_nodeManager->mkNode(EQUAL, x, y); // right conjunct @@ -87,12 +87,13 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) std::map >(); // create test formula - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); Node plus = d_nodeManager->mkNode(PLUS, x, x); Node mul = d_nodeManager->mkNode(MULT, x, x); Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4)); + Node y = + d_skolemManager->mkDummySkolem("y", d_nodeManager->mkBitVectorType(4)); Node ext1 = theory::bv::utils::mkExtract(y, 1, 0); Node ext2 = theory::bv::utils::mkExtract(y, 3, 2); Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2); @@ -143,7 +144,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) Node two = d_nodeManager->mkConst(Rational(2)); Node x = d_nodeManager->mkBoundVar(integer); - Node a = d_nodeManager->mkSkolem("a", integer); + Node a = d_skolemManager->mkDummySkolem("a", integer); Node n1 = d_nodeManager->mkNode(MULT, two, x); std::unordered_map subs; diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 87121c1c2..cfe008ec0 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -26,6 +26,7 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node_value.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "test_node.h" #include "theory/rewriter.h" @@ -43,10 +44,11 @@ std::vector makeNSkolemNodes(NodeManager* nodeManager, TypeNode type) { std::vector skolems; + SkolemManager* sm = nodeManager->getSkolemManager(); for (uint32_t i = 0; i < n; i++) { - skolems.push_back(nodeManager->mkSkolem( - "skolem_", type, "Created by makeNSkolemNodes()")); + skolems.push_back( + sm->mkDummySkolem("skolem_", type, "Created by makeNSkolemNodes()")); } return skolems; } @@ -119,12 +121,12 @@ TEST_F(TestNodeBlackNode, operator_equals) { Node a, b, c; - b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType()); ASSERT_TRUE(a == a); ASSERT_TRUE(a == b); @@ -154,12 +156,12 @@ TEST_F(TestNodeBlackNode, operator_not_equals) { Node a, b, c; - b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType()); /*structed assuming operator == works */ ASSERT_TRUE(iff(a != a, !(a == a))); @@ -215,7 +217,7 @@ TEST_F(TestNodeBlackNode, operator_assign) { Node a, b; Node c = d_nodeManager->mkNode( - NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType())); + NOT, d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType())); b = c; ASSERT_EQ(b, c); @@ -232,8 +234,8 @@ TEST_F(TestNodeBlackNode, operator_less_than) // We don't have access to the ids so we can't test the implementation // in the black box tests. - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); ASSERT_TRUE(a < b || b < a); ASSERT_TRUE(!(a < b && b < a)); @@ -275,8 +277,8 @@ TEST_F(TestNodeBlackNode, operator_less_than) TEST_F(TestNodeBlackNode, eqNode) { TypeNode t = d_nodeManager->mkSort(); - Node left = d_nodeManager->mkSkolem("left", t); - Node right = d_nodeManager->mkSkolem("right", t); + Node left = d_skolemManager->mkDummySkolem("left", t); + Node right = d_skolemManager->mkDummySkolem("right", t); Node eq = left.eqNode(right); ASSERT_EQ(EQUAL, eq.getKind()); @@ -325,8 +327,8 @@ TEST_F(TestNodeBlackNode, orNode) TEST_F(TestNodeBlackNode, iteNode) { - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); Node cnd = d_nodeManager->mkNode(OR, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -382,8 +384,8 @@ TEST_F(TestNodeBlackNode, xorNode) TEST_F(TestNodeBlackNode, getKind) { - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, a); ASSERT_EQ(NOT, n.getKind()); @@ -391,8 +393,8 @@ TEST_F(TestNodeBlackNode, getKind) n = d_nodeManager->mkNode(EQUAL, a, b); ASSERT_EQ(EQUAL, n.getKind()); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType()); n = d_nodeManager->mkNode(PLUS, x, y); ASSERT_EQ(PLUS, n.getKind()); @@ -407,8 +409,8 @@ TEST_F(TestNodeBlackNode, getOperator) TypeNode booleanType = d_nodeManager->booleanType(); TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType); - Node f = d_nodeManager->mkSkolem("f", predType); - Node a = d_nodeManager->mkSkolem("a", sort); + Node f = d_skolemManager->mkDummySkolem("f", predType); + Node a = d_skolemManager->mkDummySkolem("a", sort); Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); ASSERT_TRUE(fa.hasOperator()); @@ -460,9 +462,9 @@ TEST_F(TestNodeBlackNode, getNumChildren) TEST_F(TestNodeBlackNode, iterator) { NodeBuilder b; - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); - Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType()); + Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType()); Node n = b << x << y << z << kind::AND; { // iterator @@ -487,9 +489,9 @@ TEST_F(TestNodeBlackNode, kinded_iterator) { TypeNode integerType = d_nodeManager->integerType(); - Node x = d_nodeManager->mkSkolem("x", integerType); - Node y = d_nodeManager->mkSkolem("y", integerType); - Node z = d_nodeManager->mkSkolem("z", integerType); + Node x = d_skolemManager->mkDummySkolem("x", integerType); + Node y = d_skolemManager->mkDummySkolem("y", integerType); + Node z = d_skolemManager->mkDummySkolem("z", integerType); Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y); @@ -510,13 +512,13 @@ TEST_F(TestNodeBlackNode, toString) { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem( + Node w = d_skolemManager->mkDummySkolem( "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node x = d_nodeManager->mkSkolem( + Node x = d_skolemManager->mkDummySkolem( "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem( + Node y = d_skolemManager->mkDummySkolem( "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node z = d_nodeManager->mkSkolem( + Node z = d_skolemManager->mkDummySkolem( "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder() << w << x << kind::OR; Node n = NodeBuilder() << m << y << z << kind::AND; @@ -528,13 +530,13 @@ TEST_F(TestNodeBlackNode, toStream) { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem( + Node w = d_skolemManager->mkDummySkolem( "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node x = d_nodeManager->mkSkolem( + Node x = d_skolemManager->mkDummySkolem( "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem( + Node y = d_skolemManager->mkDummySkolem( "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node z = d_nodeManager->mkSkolem( + Node z = d_skolemManager->mkDummySkolem( "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder() << x << y << kind::OR; Node n = NodeBuilder() << w << m << z << kind::AND; @@ -597,14 +599,14 @@ TEST_F(TestNodeBlackNode, dagifier) TypeNode intType = d_nodeManager->integerType(); TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType); - Node x = - d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = - d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME); - Node f = - d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); - Node g = - d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + Node x = d_skolemManager->mkDummySkolem( + "x", intType, "", NodeManager::SKOLEM_EXACT_NAME); + Node y = d_skolemManager->mkDummySkolem( + "y", intType, "", NodeManager::SKOLEM_EXACT_NAME); + Node f = d_skolemManager->mkDummySkolem( + "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + Node g = d_skolemManager->mkDummySkolem( + "g", fnType, "", NodeManager::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); @@ -702,7 +704,7 @@ TEST_F(TestNodeBlackNode, isConst) listType.getDType().getConstructors(); Node cons = lcons[0]->getConstructor(); Node nil = lcons[1]->getConstructor(); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); Node cons_x_nil = d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, @@ -764,8 +766,9 @@ TEST_F(TestNodeBlackNode, isConst) namespace { Node level0(NodeManager* nm) { + SkolemManager* sm = nm->getSkolemManager(); NodeBuilder nb(kind::AND); - Node x = nm->mkSkolem("x", nm->booleanType()); + Node x = sm->mkDummySkolem("x", nm->booleanType()); nb << x; nb << x; return Node(nb.constructNode()); diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 8c6145940..2b8ef7a04 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -92,7 +92,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) NodeBuilder noKind; ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); - Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode)); noKind << x << x; ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); @@ -112,7 +112,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) TEST_F(TestNodeBlackNodeBuilder, getNumChildren) { - Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode)); NodeBuilder nb; #ifdef CVC4_ASSERTIONS @@ -300,16 +300,16 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node) TEST_F(TestNodeBlackNodeBuilder, append) { - Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); - Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); - Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode); + Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode); + Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode); + Node z = d_skolemManager->mkDummySkolem("z", *d_boolTypeNode); Node m = d_nodeManager->mkNode(AND, y, z, x); Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z); Node o = d_nodeManager->mkNode(XOR, y, x); - Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode); - Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode); - Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode); + Node r = d_skolemManager->mkDummySkolem("r", *d_realTypeNode); + Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode); + Node t = d_skolemManager->mkDummySkolem("t", *d_realTypeNode); Node p = d_nodeManager->mkNode( EQUAL, @@ -389,13 +389,13 @@ TEST_F(TestNodeBlackNodeBuilder, leftist_building) { NodeBuilder nb; - Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode); + Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode); - Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode); - Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode); + Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode); + Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode); - Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode); - Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode); + Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode); + Node e = d_skolemManager->mkDummySkolem("e", *d_realTypeNode); nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE; diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index 5d21ff734..6ad6f583c 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -37,7 +37,7 @@ class TestNodeBlackNodeManager : public TestNode TEST_F(TestNodeBlackNodeManager, mkNode_not) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, x); ASSERT_EQ(n.getNumChildren(), 1u); ASSERT_EQ(n.getKind(), NOT); @@ -46,8 +46,8 @@ TEST_F(TestNodeBlackNodeManager, mkNode_not) TEST_F(TestNodeBlackNodeManager, mkNode_binary) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(IMPLIES, x, y); ASSERT_EQ(n.getNumChildren(), 2u); ASSERT_EQ(n.getKind(), IMPLIES); @@ -57,9 +57,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_binary) TEST_F(TestNodeBlackNodeManager, mkNode_three_children) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); - Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType()); + Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x, y, z); ASSERT_EQ(n.getNumChildren(), 3u); ASSERT_EQ(n.getKind(), AND); @@ -70,10 +70,10 @@ TEST_F(TestNodeBlackNodeManager, mkNode_three_children) TEST_F(TestNodeBlackNodeManager, mkNode_four_children) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); - Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); + Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4); ASSERT_EQ(n.getNumChildren(), 4u); ASSERT_EQ(n.getKind(), AND); @@ -85,11 +85,11 @@ TEST_F(TestNodeBlackNodeManager, mkNode_four_children) TEST_F(TestNodeBlackNodeManager, mkNode_five_children) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); - Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType()); - Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); + Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType()); + Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5); ASSERT_EQ(n.getNumChildren(), 5u); ASSERT_EQ(n.getKind(), AND); @@ -102,9 +102,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_five_children) TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); std::vector args; args.push_back(x1); args.push_back(x2); @@ -120,9 +120,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node) TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); std::vector args; args.push_back(x1); args.push_back(x2); @@ -138,7 +138,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode) TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name) { - Node x = d_nodeManager->mkSkolem( + Node x = d_skolemManager->mkDummySkolem( "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME); ASSERT_EQ(x.getKind(), SKOLEM); ASSERT_EQ(x.getNumChildren(), 0u); @@ -303,7 +303,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType) TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children) { #ifdef CVC4_ASSERTIONS - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); ASSERT_DEATH(d_nodeManager->mkNode(AND, x), "Nodes with kind AND must have at least 2 children"); #endif @@ -316,8 +316,8 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children) std::vector vars; const uint32_t max = metakind::getMaxArityForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); - Node skolem_i = d_nodeManager->mkSkolem("i", boolType); - Node skolem_j = d_nodeManager->mkSkolem("j", boolType); + Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType); + Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType); Node andNode = skolem_i.andNode(skolem_j); Node orNode = skolem_i.orNode(skolem_j); while (vars.size() <= max) diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index 66ac65cb5..a13e76d03 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -64,8 +64,8 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) TEST_F(TestNodeWhiteNodeManager, topological_sort) { TypeNode boolType = d_nodeManager->booleanType(); - Node i = d_nodeManager->mkSkolem("i", boolType); - Node j = d_nodeManager->mkSkolem("j", boolType); + Node i = d_skolemManager->mkDummySkolem("i", boolType); + Node j = d_skolemManager->mkDummySkolem("j", boolType); Node n1 = d_nodeManager->mkNode(kind::AND, j, j); Node n2 = d_nodeManager->mkNode(kind::AND, i, n1); diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp index 43eebcda9..fa4889540 100644 --- a/test/unit/node/node_self_iterator_black.cpp +++ b/test/unit/node/node_self_iterator_black.cpp @@ -32,8 +32,8 @@ class TestNodeBlackNodeSelfIterator : public TestNode TEST_F(TestNodeBlackNodeSelfIterator, iteration) { - Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); - Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode); + Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode); Node x_and_y = x.andNode(y); NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); ASSERT_NE(i, x_and_y.end()); diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 359cc0b6f..dacc1f543 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -16,6 +16,7 @@ #define CVC4__TEST__UNIT__TEST_NODE_H #include "expr/node_manager.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" @@ -29,6 +30,7 @@ class TestNode : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); @@ -38,6 +40,7 @@ class TestNode : public TestInternal std::unique_ptr d_scope; std::unique_ptr d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr d_boolTypeNode; std::unique_ptr d_bvTypeNode; std::unique_ptr d_intTypeNode; diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index f26bd0ff6..9be954059 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -19,6 +19,7 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "expr/proof_checker.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" @@ -43,6 +44,7 @@ class TestSmt : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); d_smtEngine->finishInit(); @@ -50,6 +52,7 @@ class TestSmt : public TestInternal std::unique_ptr d_nmScope; std::unique_ptr d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr d_smtEngine; }; @@ -59,12 +62,14 @@ class TestSmtNoFinishInit : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); } std::unique_ptr d_nmScope; std::unique_ptr d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr d_smtEngine; }; diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 586afd8b5..10a606d11 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -41,7 +41,8 @@ class TestTheoryWhiteBagsRewriter : public TestSmt std::vector elements(n); for (size_t i = 0; i < n; i++) { - elements[i] = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + elements[i] = + d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); } return elements; } @@ -63,8 +64,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) std::vector elements = getNStrings(2); Node x = elements[0]; Node y = elements[1]; - Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType()); - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->integerType()); + Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType()); Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d); Node emptyBag = d_nodeManager->mkConst( @@ -129,7 +130,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element) TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) { - Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node skolem = + d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(-1))); @@ -160,7 +162,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) TEST_F(TestTheoryWhiteBagsRewriter, bag_count) { int n = 3; - Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node skolem = + d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(skolem.getType()))); Node bag = d_nodeManager->mkBag( @@ -181,7 +184,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node bag = d_nodeManager->mkBag( d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5))); @@ -585,7 +588,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) TEST_F(TestTheoryWhiteBagsRewriter, choose) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node c = d_nodeManager->mkConst(Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); @@ -598,7 +601,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, choose) TEST_F(TestTheoryWhiteBagsRewriter, bag_card) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node zero = d_nodeManager->mkConst(Rational(0)); @@ -640,8 +643,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) { Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); - Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); + Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); // TODO(projects#223): complete this function @@ -662,7 +665,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) TEST_F(TestTheoryWhiteBagsRewriter, from_set) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) @@ -676,7 +679,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) TEST_F(TestTheoryWhiteBagsRewriter, to_set) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node bag = d_nodeManager->mkBag( d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5))); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 64ba39e7f..92e76d5f5 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -41,7 +41,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4)); d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4)); - d_sk = d_nodeManager->mkSkolem("sk", d_t.getType()); + d_sk = d_skolemManager->mkDummySkolem("sk", d_t.getType()); d_x = d_nodeManager->mkBoundVar(d_t.getType()); d_bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {d_x}); } @@ -139,7 +139,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit { s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4)); x = d_nodeManager->mkBoundVar(s2.getType()); - sk = d_nodeManager->mkSkolem("sk", s2.getType()); + sk = d_skolemManager->mkDummySkolem("sk", s2.getType()); t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8)); sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, x, s2); sc = getICBvConcat(pol, litk, 0, sk, sv_t, t); @@ -148,7 +148,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit { s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4)); x = d_nodeManager->mkBoundVar(s1.getType()); - sk = d_nodeManager->mkSkolem("sk", s1.getType()); + sk = d_skolemManager->mkDummySkolem("sk", s1.getType()); t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8)); sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x); sc = getICBvConcat(pol, litk, 1, sk, sv_t, t); @@ -159,7 +159,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4)); s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4)); x = d_nodeManager->mkBoundVar(s2.getType()); - sk = d_nodeManager->mkSkolem("sk", s1.getType()); + sk = d_skolemManager->mkDummySkolem("sk", s1.getType()); t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(12)); sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x, s2); sc = getICBvConcat(pol, litk, 1, sk, sv_t, t); @@ -195,7 +195,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit unsigned w = 8; Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(wx)); - Node sk = d_nodeManager->mkSkolem("sk", x.getType()); + Node sk = d_skolemManager->mkDummySkolem("sk", x.getType()); x = d_nodeManager->mkBoundVar(x.getType()); Node t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(w)); diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 33543cc42..920075674 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -33,11 +33,11 @@ class TestTheoryBlackStringsSkolemCache : public TestSmt TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) { Node zero = d_nodeManager->mkConst(Rational(0)); - Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType()); - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType()); - Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType()); - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType()); + Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType()); + Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->stringType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->stringType()); Node sa = d_nodeManager->mkNode( kind::STRING_SUBSTR, a, diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index 97bbb1bcf..2e266ce58 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -36,20 +36,20 @@ class TestUtilBlackBooleanSimplification : public TestNode { TestNode::SetUp(); - d_a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - d_b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - d_c = d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()); - d_d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); - d_e = d_nodeManager->mkSkolem("e", d_nodeManager->booleanType()); - d_f = d_nodeManager->mkSkolem( + d_a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + d_b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); + d_c = d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType()); + d_d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType()); + d_e = d_skolemManager->mkDummySkolem("e", d_nodeManager->booleanType()); + d_f = d_skolemManager->mkDummySkolem( "f", d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), d_nodeManager->booleanType())); - d_g = d_nodeManager->mkSkolem( + d_g = d_skolemManager->mkDummySkolem( "g", d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), d_nodeManager->booleanType())); - d_h = d_nodeManager->mkSkolem( + d_h = d_skolemManager->mkDummySkolem( "h", d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), d_nodeManager->booleanType())); -- 2.30.2