diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 13:36:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 18:36:15 +0000 |
commit | 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch) | |
tree | 03b1a5792f2f6ca5537353b86682f427090668da /src/preprocessing/passes | |
parent | 5059658ee0d6fc65e4cb1652c605895d016cd274 (diff) |
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.
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 14 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 15 | ||||
-rw-r--r-- | src/preprocessing/passes/fun_def_fmf.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/passes/ho_elim.cpp | 12 | ||||
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 10 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/nl_ext_purify.cpp | 12 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 15 | ||||
-rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 9 | ||||
-rw-r--r-- | src/preprocessing/passes/sep_skolem_emp.cpp | 18 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 4 |
11 files changed, 77 insertions, 42 deletions
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<TNode, TNodeHashFunction>& 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 <sstream> +#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<int, Node> 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 <sstream> #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<Node, Node>& newLambda) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); std::unordered_map<Node, Node, TNodeHashFunction>::iterator it; std::vector<Node> visit; TNode cur; @@ -90,7 +92,7 @@ Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& 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<Node, Node, NodeHashFunction>::iterator it; std::map<Node, Node> preReplace; std::map<Node, Node>::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<TypeNode> 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 <vector> #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<Node>& 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 <vector> +#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; i<n.getNumChildren(); i++ ){ std::stringstream ss; ss << "mda_" << op << ""; - Node v = NodeManager::currentNM()->mkSkolem( 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; a<m.getNumChildren(); a++ ){ std::stringstream ss; ss << "mda_" << op << ""; - Node v = NodeManager::currentNM()->mkSkolem( 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 <string> +#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<Node>& 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<Node>& 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 <vector> #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<Node, Node>::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 " |