diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 3 | ||||
| -rw-r--r-- | src/theory/arith/operator_elim.cpp | 4 | ||||
| -rw-r--r-- | src/theory/fp/fp_expand_defs.cpp | 23 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 6 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 4 |
6 files changed, 15 insertions, 28 deletions
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 6b1749305..a3dd77fd1 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -38,8 +38,7 @@ CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - d_ranVariable = sm->mkDummySkolem( - "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME); + d_ranVariable = sm->mkDummySkolem("__z", nm->realType(), ""); #ifdef CVC5_POLY_IMP if (env.isTheoryProofProducing()) { diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 90f4a2cc7..afbb9b70f 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -462,8 +462,8 @@ Node OperatorElim::mkWitnessTerm(Node v, NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); // we mark that we should send a lemma - Node k = - sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this); + Node k = sm->mkSkolem( + v, pred, prefix, comment, SkolemManager::SKOLEM_DEFAULT, this); if (d_pnm != nullptr) { Node lem = SkolemLemma::getSkolemLemmaFor(k); diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index a499b9666..de86626af 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -50,11 +50,8 @@ Node FpExpandDefs::minUF(Node node) args[0] = t; args[1] = t; fun = sm->mkDummySkolem("floatingpoint_min_zero_case", - nm->mkFunctionType(args, - nm->mkBitVectorType(1U) - ), - "floatingpoint_min_zero_case", - NodeManager::SKOLEM_EXACT_NAME); + nm->mkFunctionType(args, nm->mkBitVectorType(1U)), + "floatingpoint_min_zero_case"); d_minMap.insert(t, fun); } else @@ -84,11 +81,8 @@ Node FpExpandDefs::maxUF(Node node) args[0] = t; args[1] = t; fun = sm->mkDummySkolem("floatingpoint_max_zero_case", - nm->mkFunctionType(args, - nm->mkBitVectorType(1U) - ), - "floatingpoint_max_zero_case", - NodeManager::SKOLEM_EXACT_NAME); + nm->mkFunctionType(args, nm->mkBitVectorType(1U)), + "floatingpoint_max_zero_case"); d_maxMap.insert(t, fun); } else @@ -121,8 +115,7 @@ Node FpExpandDefs::toUBVUF(Node node) args[1] = source; fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case", nm->mkFunctionType(args, target), - "floatingpoint_to_ubv_out_of_range_case", - NodeManager::SKOLEM_EXACT_NAME); + "floatingpoint_to_ubv_out_of_range_case"); d_toUBVMap.insert(p, fun); } else @@ -155,8 +148,7 @@ Node FpExpandDefs::toSBVUF(Node node) args[1] = source; fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case", nm->mkFunctionType(args, target), - "floatingpoint_to_sbv_out_of_range_case", - NodeManager::SKOLEM_EXACT_NAME); + "floatingpoint_to_sbv_out_of_range_case"); d_toSBVMap.insert(p, fun); } else @@ -183,8 +175,7 @@ Node FpExpandDefs::toRealUF(Node node) args[0] = t; fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case", nm->mkFunctionType(args, nm->realType()), - "floatingpoint_to_real_infinity_and_NaN_case", - NodeManager::SKOLEM_EXACT_NAME); + "floatingpoint_to_real_infinity_and_NaN_case"); d_toRealMap.insert(t, fun); } else diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 5af838354..b3033aedb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -188,10 +188,8 @@ Node SygusUnifRl::purifyLemma(Node n, // Build purified head with fresh skolem and recreate node std::stringstream ss; ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++; - Node new_f = sm->mkDummySkolem(ss.str(), - nb[0].getType(), - "head of unif evaluation point", - NodeManager::SKOLEM_EXACT_NAME); + Node new_f = sm->mkDummySkolem( + ss.str(), nb[0].getType(), "head of unif evaluation point"); // Adds new enumerator to map from candidate Trace("sygus-unif-rl-purify") << "...new enum " << new_f << " for candidate " << nb[0] << "\n"; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 324d6b7dc..a87466fab 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1407,8 +1407,7 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) stringstream stream; stream << "chooseUf" << setType.getId(); string name = stream.str(); - Node chooseSkolem = sm->mkDummySkolem( - name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME); + Node chooseSkolem = sm->mkDummySkolem(name, chooseUf, "choose function"); d_chooseFunctions[setType] = chooseSkolem; return chooseSkolem; } diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 60e6b6a01..fc68ddfc4 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -109,8 +109,8 @@ Node SkolemCache::mkTypedSkolemCached( { // for sequences of Booleans, we may purify Boolean terms, in which case // they must be Boolean term variables. - int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR - : NodeManager::SKOLEM_DEFAULT; + int flags = a.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR + : SkolemManager::SKOLEM_DEFAULT; sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags); } break; |