From 9d3eec992f14a8fa83a4b34de5eebe98604bdee6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 08:50:38 -0500 Subject: [PATCH] Make all dependencies in the fast enumerator optional (#6918) This allows one to use a fast enumerator without having access to sygus term database, statistics, etc. --- src/theory/datatypes/sygus_datatype_utils.cpp | 18 ++++++++ src/theory/datatypes/sygus_datatype_utils.h | 5 ++ src/theory/datatypes/sygus_extension.cpp | 6 +-- src/theory/datatypes/theory_datatypes_utils.h | 4 +- .../candidate_rewrite_database.cpp | 5 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 5 +- .../quantifiers/sygus/rcons_type_info.cpp | 2 +- .../quantifiers/sygus/sygus_enumerator.cpp | 46 ++++++++++++++----- .../quantifiers/sygus/sygus_enumerator.h | 30 +++++++++--- .../quantifiers/sygus/sygus_explain.cpp | 3 +- src/theory/quantifiers/sygus/sygus_pbe.cpp | 3 +- src/theory/quantifiers/sygus/sygus_unif.cpp | 3 +- .../quantifiers/sygus/sygus_unif_io.cpp | 6 ++- .../quantifiers/sygus/synth_conjecture.cpp | 5 +- .../quantifiers/sygus/term_database_sygus.cpp | 17 ------- .../quantifiers/sygus/term_database_sygus.h | 1 - 16 files changed, 107 insertions(+), 52 deletions(-) diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 7e5099d55..72ddd7b0e 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -718,6 +718,24 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, return sdtS; } +unsigned getSygusTermSize(Node n) +{ + if (n.getKind() != APPLY_CONSTRUCTOR) + { + return 0; + } + unsigned sum = 0; + for (const Node& nc : n) + { + sum += getSygusTermSize(nc); + } + const DType& dt = datatypeOf(n.getOperator()); + int cindex = indexOf(n.getOperator()); + Assert(cindex >= 0 && static_cast(cindex) < dt.getNumConstructors()); + unsigned weight = dt[cindex].getWeight(); + return weight + sum; +} + } // namespace utils } // namespace datatypes } // namespace theory diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 6f3791a4d..35672434c 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -227,6 +227,11 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, const std::vector& syms, const std::vector& vars); +/** + * Get SyGuS term size, which is based on the weight of constructor applications + * in n. + */ +unsigned getSygusTermSize(Node n); // ------------------------ end sygus utils } // namespace utils diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index ee96b95d8..63af57592 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1040,7 +1040,7 @@ Node SygusExtension::registerSearchValue(Node a, Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; - unsigned sz = d_tds->getSygusTermSize( nv ); + unsigned sz = utils::getSygusTermSize(nv); if( d_tds->involvesDivByZero( bvr ) ){ quantifiers::DivByZeroSygusInvarianceTest dbzet; Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " @@ -1143,7 +1143,7 @@ Node SygusExtension::registerSearchValue(Node a, } Trace("sygus-sb-exc") << std::endl; } - Assert(d_tds->getSygusTermSize(bad_val) == sz); + Assert(utils::getSygusTermSize(bad_val) == sz); // generalize the explanation for why the analog of bad_val // is equivalent to bvr @@ -1177,7 +1177,7 @@ void SygusExtension::registerSymBreakLemmaForValue( { TypeNode tn = val.getType(); Node x = getFreeVar(tn); - unsigned sz = d_tds->getSygusTermSize(val); + unsigned sz = utils::getSygusTermSize(val); std::vector exp; d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz); Node lem = diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 898ee3491..705e867b9 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H -#define CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H +#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_UTILS_H +#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_UTILS_H #include diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 789a723b9..c2ee563e3 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -20,6 +20,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -244,8 +245,8 @@ Node CandidateRewriteDatabase::addTerm(Node sol, // wish to enumerate any term that contains sol (resp. eq_sol) // as a subterm. Node exc_sol = sol; - unsigned sz = d_tds->getSygusTermSize(sol); - unsigned eqsz = d_tds->getSygusTermSize(eq_sol); + unsigned sz = datatypes::utils::getSygusTermSize(sol); + unsigned eqsz = datatypes::utils::getSygusTermSize(eq_sol); if (eqsz > sz) { sz = eqsz; diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 28788a5ea..544bdcc5c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -19,6 +19,7 @@ #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -205,8 +206,8 @@ bool CegisUnif::getEnumValues(const std::vector& enums, if (curr_val < prev_val) { // must have the same size - unsigned prev_size = d_tds->getSygusTermSize(prev_val); - unsigned curr_size = d_tds->getSygusTermSize(curr_val); + unsigned prev_size = datatypes::utils::getSygusTermSize(prev_val); + unsigned curr_size = datatypes::utils::getSygusTermSize(curr_val); Assert(prev_size <= curr_size); if (curr_size == prev_size) { diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index 1c62f030d..a1ae53ad1 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -31,7 +31,7 @@ void RConsTypeInfo::initialize(TermDbSygus* tds, NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true)); + d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true)); 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 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 0cf92b373..2dfd41fb4 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -20,6 +20,7 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "smt/logic_exception.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/type_node_id_trie.h" @@ -33,12 +34,14 @@ namespace quantifiers { SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p, - SygusStatistics& s, - bool enumShapes) + SygusStatistics* s, + bool enumShapes, + bool enumAnyConstHoles) : d_tds(tds), d_parent(p), d_stats(s), d_enumShapes(enumShapes), + d_enumAnyConstHoles(enumAnyConstHoles), d_tlEnum(nullptr), d_abortSize(-1) { @@ -54,6 +57,12 @@ void SygusEnumerator::initialize(Node e) d_tlEnum = getMasterEnumForType(d_etype); d_abortSize = options::sygusAbortSize(); + // if we don't have a term database, we don't register symmetry breaking + // lemmas + if (!d_tds) + { + return; + } // Get the statically registered symmetry breaking clauses for e, see if they // can be used for speeding up the enumeration. NodeManager* nm = NodeManager::currentNM(); @@ -141,7 +150,8 @@ Node SygusEnumerator::getCurrent() if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end()) { Trace("sygus-enum-exc") - << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl; + << "Exclude (external) : " << datatypes::utils::sygusToBuiltin(ret) + << std::endl; ret = Node::null(); } } @@ -330,9 +340,12 @@ bool SygusEnumerator::TermCache::addTerm(Node n) Assert(!n.isNull()); if (options::sygusSymBreakDynamic()) { - Node bn = d_tds->sygusToBuiltin(n); - Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); - ++(d_stats->d_enumTermsRewrite); + Node bn = datatypes::utils::sygusToBuiltin(n); + Node bnr = d_extr.extendedRewrite(bn); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTermsRewrite); + } if (options::sygusRewVerify()) { if (bn != bnr) @@ -358,7 +371,10 @@ bool SygusEnumerator::TermCache::addTerm(Node n) // if we are doing PBE symmetry breaking if (d_eec != nullptr) { - ++(d_stats->d_enumTermsExampleEval); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTermsExampleEval); + } // Is it equivalent under examples? Node bne = d_eec->addSearchVal(d_tn, bnr); if (!bne.isNull()) @@ -374,7 +390,10 @@ bool SygusEnumerator::TermCache::addTerm(Node n) } Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; } - ++(d_stats->d_enumTerms); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTerms); + } d_terms.push_back(n); return true; } @@ -474,8 +493,8 @@ Node SygusEnumerator::TermEnumSlave::getCurrent() Node curr = tc.getTerm(d_index); Trace("sygus-enum-debug2") << "slave(" << d_tn - << "): current : " << d_se->d_tds->sygusToBuiltin(curr) - << ", sizes = " << d_se->d_tds->getSygusTermSize(curr) << " " + << "): current : " << datatypes::utils::sygusToBuiltin(curr) + << ", sizes = " << datatypes::utils::getSygusTermSize(curr) << " " << getCurrentSize() << std::endl; Trace("sygus-enum-debug2") << "slave(" << d_tn << "): indices : " << d_hasIndexNextEnd << " " @@ -560,7 +579,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn) { eec = d_parent->getExampleEvalCache(d_enum); } - d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec); + d_tcache[tn].initialize(d_stats, d_enum, tn, d_tds, eec); } SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) @@ -578,7 +597,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) AlwaysAssert(ret); return &d_masterEnum[tn]; } - if (options::sygusRepairConst()) + if (d_enumAnyConstHoles) { std::map::iterator it = d_masterEnumFv.find(tn); if (it != d_masterEnumFv.end()) @@ -720,6 +739,7 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // If we are enumerating shapes, the first enumerated term is a free variable. if (d_enumShapes && !d_enumShapesInit) { + Assert(d_tds != nullptr); Node fv = d_tds->getFreeVar(d_tn, 0); d_enumShapesInit = true; d_currTermSet = true; @@ -1083,6 +1103,7 @@ void SygusEnumerator::TermEnumMaster::childrenToShape( Node SygusEnumerator::TermEnumMaster::convertShape( Node n, std::map& vcounter) { + Assert(d_tds != nullptr); NodeManager* nm = NodeManager::currentNM(); std::unordered_map visited; std::unordered_map::iterator it; @@ -1195,6 +1216,7 @@ bool SygusEnumerator::TermEnumMasterFv::initialize(SygusEnumerator* se, Node SygusEnumerator::TermEnumMasterFv::getCurrent() { + Assert(d_se->d_tds != nullptr); Node ret = d_se->d_tds->getFreeVar(d_tn, d_currSize); Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): mk " << ret << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 355108957..88133eb6e 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -56,10 +56,23 @@ class SygusPbe; class SygusEnumerator : public EnumValGenerator { public: - SygusEnumerator(TermDbSygus* tds, - SynthConjecture* p, - SygusStatistics& s, - bool enumShapes = false); + /** + * @param tds Pointer to the term database, required if enumShapes or + * enumAnyConstHoles is true, or if we want to include symmetry breaking from + * lemmas stored in the sygus term database, + * @param p Pointer to the conjecture, required if we wish to do + * conjecture-specific symmetry breaking + * @param s Pointer to the statistics + * @param enumShapes If true, this enumerator will generate terms having any + * number of free variables + * @param enumAnyConstHoles If true, this enumerator will generate terms where + * free variables are the arguments to any-constant constructors. + */ + SygusEnumerator(TermDbSygus* tds = nullptr, + SynthConjecture* p = nullptr, + SygusStatistics* s = nullptr, + bool enumShapes = false, + bool enumAnyConstHoles = false); ~SygusEnumerator() {} /** initialize this class with enumerator e */ void initialize(Node e) override; @@ -77,10 +90,13 @@ class SygusEnumerator : public EnumValGenerator TermDbSygus* d_tds; /** pointer to the synth conjecture that owns this enumerator */ SynthConjecture* d_parent; - /** reference to the statistics of parent */ - SygusStatistics& d_stats; + /** pointer to the statistics */ + SygusStatistics* d_stats; /** Whether we are enumerating shapes */ bool d_enumShapes; + /** Whether we are enumerating free variables as arguments to any-constant + * constructors */ + bool d_enumAnyConstHoles; /** Term cache * * This stores a list of terms for a given sygus type. The key features of @@ -171,6 +187,8 @@ class SygusEnumerator : public EnumValGenerator TypeNode d_tn; /** pointer to term database sygus */ TermDbSygus* d_tds; + /** extended rewriter */ + ExtendedRewriter d_extr; /** * Pointer to the example evaluation cache utility (used for symmetry * breaking). diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 395f16beb..23c315f42 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -18,6 +18,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "smt/logic_exception.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_invariance.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -220,7 +221,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, // we are tracking term size if positive if (sz >= 0) { - int s = d_tdb->getSygusTermSize(vn[i]); + int s = datatypes::utils::getSygusTermSize(vn[i]); sz = sz - s; } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 86d0bbc8e..892ee6dd4 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/synth_conjecture.h" @@ -180,7 +181,7 @@ bool SygusPbe::constructCandidates(const std::vector& enums, Trace("sygus-pbe-enum") << std::endl; if (!enum_values[i].isNull()) { - unsigned sz = d_tds->getSygusTermSize(enum_values[i]); + unsigned sz = datatypes::utils::getSygusTermSize(enum_values[i]); szs.push_back(sz); if (i == 0 || sz < min_term_size) { diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 16ca1f4e6..00370ffa2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_unif.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "util/random.h" @@ -52,7 +53,7 @@ Node SygusUnif::getMinimalTerm(const std::vector& terms) unsigned ssize = 0; if (it == d_termToSize.end()) { - ssize = d_tds->getSygusTermSize(n); + ssize = datatypes::utils::getSygusTermSize(n); d_termToSize[n] = ssize; } else diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 8c8f5ccd4..8207a07f2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/evaluator.h" #include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/synth_conjecture.h" @@ -835,7 +836,8 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) if (!vcc.isNull() && (d_solution.isNull() || (!d_solution.isNull() - && d_tds->getSygusTermSize(vcc) < d_sol_term_size))) + && datatypes::utils::getSygusTermSize(vcc) + < d_sol_term_size))) { if (Trace.isOn("sygus-pbe")) { @@ -846,7 +848,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) } d_solution = vcc; newSolution = vcc; - d_sol_term_size = d_tds->getSygusTermSize(vcc); + d_sol_term_size = datatypes::utils::getSygusTermSize(vcc); Trace("sygus-pbe-sol") << "PBE solution size: " << d_sol_term_size << std::endl; // We've determined its feasible, now, enable information gain and diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 1ddc2fa22..73bd6b8a4 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -827,7 +827,10 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) == options::SygusActiveGenMode::ENUM || options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO); - d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats)); + // if sygus repair const is enabled, we enumerate terms with free + // variables as arguments to any-constant constructors + d_evg[e].reset(new SygusEnumerator( + d_tds, this, &d_stats, false, options::sygusRepairConst())); } } Trace("sygus-active-gen") diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 826563401..3b0ea3312 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -359,23 +359,6 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) return ret; } -unsigned TermDbSygus::getSygusTermSize( Node n ){ - if (n.getKind() != APPLY_CONSTRUCTOR) - { - return 0; - } - unsigned sum = 0; - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - sum += getSygusTermSize(n[i]); - } - const DType& dt = datatypes::utils::datatypeOf(n.getOperator()); - int cindex = datatypes::utils::indexOf(n.getOperator()); - Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); - unsigned weight = dt[cindex].getWeight(); - return weight + sum; -} - bool TermDbSygus::registerSygusType(TypeNode tn) { std::map::iterator it = d_registerStatus.find(tn); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index e0a812069..80411b258 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -456,7 +456,6 @@ class TermDbSygus { Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); Node getNormalized(TypeNode t, Node prog); - unsigned getSygusTermSize( Node n ); /** involves div-by-zero */ bool involvesDivByZero( Node n ); /** get anchor */ -- 2.30.2